rntz

23 ms·

181.
by rntz 10y ago
I don't like that you're being downvoted. You're making a fair point. I do like the second half of the article, for the record. I think that attribution matters; albeit probably more the attribution to Church and Turing than
182.
by rntz 10y ago
This article has many misstatements in its first half. > John McCarthy wrote 6 easy things in machine code, then combined them to make a programming language. John McCarthy didn't implement Lisp in machine code. Steve Russell did. I
183.
by rntz 10y ago
The "hole-driven" development style originated in dependently typed languages such as Agda and Idris, which I imagine Matthew's video was inspired by. So if you want to experience it right now, go learn Agda and use agda-mode
184.
by rntz 10y ago
www.nearlyfreespeech.net is cheap (really cheap, hence the name) and reliable - they've been around since 2002, and I've used them since 2008.
185.
by rntz 10y ago
> Property based testing frameworks tend to show you the simplest concrete example of your error. Type checkers tend to show you the most abstract example of your error. Maybe if type checkers started to to incorporate more concrete exam
186.
by rntz 10y ago
I think you are confusing the object-level and the meta-level (and incidentally confusing everyone who doesn't know advanced set theory). In any case, if you want to talk about the computable reals, then call them computable reals. Don
187.
by rntz 10y ago
You don't need to understand anything about infinitesimals to understand 0.999... = 1. Perhaps you meant limits? The "standard" approach would be to point out that Σ_{i=1}^∞ 9/(10^i) = 1 (that is, the sum from i = 1 to i
188.
by rntz 10y ago
For equality, yes, Theta works! But I care not just about equality but about comparison. In particular, it would be nice if the "natural" ordering on A(f) had the property that A(f) <= A(g) iff f is O(g) Theta(g) is a
189.
by rntz 10y ago
Your claims about what little-o and big-O mean don't match the explanation at https://cathyatseneca.gitbooks.io/data-structures-and-algori... That page says o(f) == O(f) and not Theta(f). When you say "small-o is
190.
by rntz 10y ago
This is indeed the standard solution. There is also a more difficult version: Every prisoner is required to have the same strategy (so you cannot pick a unique person F). (Every thread runs the same program, and threads do not have access t
191.
by rntz 10y ago
Ah, of course! That guarantees there are no "tails"; every name (& box) is part of exactly one cycle. And this is then a property of cycles of permutations generally. Thanks!
192.
by rntz 10y ago
Couldn't I start in a "tail" leading to a cycle that doesn't include my name? Suppose my name is "A", and I proceed: check box A - read name B; check box B - read name C; check box C - read name B and now I&#x2
193.
by rntz 10y ago
(Static) types may be seen as propositions, but this is just one interpretation of them. We can also interpret types as sets (although this doesn't work out very well except in very simple languages), as domains (most commonly), as cpo
194.
by rntz 10y ago
Acceleration and gravity are entirely interchangeable. The feeling you get due to gravity is also because of something "pushing against you" - namely, the ground. If you didn't have the ground to push against, nor air to drag
195.
by rntz 10y ago
Many folks would say that's not a proof, because it's not efficiently checkable. To tell whether it actually proves the thing, I have to go off and check every number, which takes an enormous amount of time compared to the length
196.
by rntz 10y ago
That isn't a proof, it's a procedure for finding a proof. The procedure might fail , and whether it will fail or not cannot be checked without running it - which is not guaranteed to halt! Of course, to guarantee that it halts, y
197.
by rntz 10y ago
I think that means only that programs written in a language described by a CFG could exhibit "criticality", not that they will. "Exhibiting criticality" is a property of a distribution (e.g. a corpus of human-written p
198.
by rntz 10y ago
To get a constant horizontal speed, a small-radius wheel must turn faster than a large-radius wheel. For a constant turn rate & rim mass, a small-radius wheel will have less energy than a large-radius one. I suspect (given the article&#
199.
by rntz 10y ago
Arguably the first 1000-processor chip was the CM-1, made in the 1980's: https://en.wikipedia.org/wiki/Connection_Machine They also bury the lede somewhat. Apparently the KiloCore is a 1.78 Terahertz chip: >
200.
by rntz 10y ago
Godel's completeness theorem applies to first-order predicate logic, which is not powerful enough on its own even to express , let alone prove , 1+1=2. First order logic is best thought of as a framework on which other, useful logics
201.
by rntz 10y ago
If a permanent change in your psychology did not correspond with some permanent change in your physical person, then what would there be that was causing the change in your psychology? Some non-physical "soul" or "mind&qu
202.
by rntz 10y ago
Although this is true, learning that there is a specific physical sign in the brains of those who have suffered blasts at close range, and that this sign is not present in those who have suffered other forms of stress, is a significant br
203.
by rntz 10y ago
What it means in practice is that any Java typechecker is either (a) incomplete - it will disallow some programs that should typecheck; (b) unsound - it will allow some programs that shouldn't typecheck; or (c) non-total - it will fail
204.
by rntz 10y ago
Natural joins only require equality testing. General unification is stronger. Prolog can unify [X,3|T] with [2,Y,4,5] to find X = 2, Y = 3, T = [4,5], for example.
205.
by rntz 10y ago
Prolog allows unification, which doesn't have a parallel in relational algebra. I'm not sure how much more power this gives you without recursion, though. If you're interested in connections between relational algebra (and SQ
206.
by rntz 10y ago
It's basically a certain kind of documentation of design patterns in programming languages. PLT emphasizes the use of formal logic and mathematics. It focuses on systems that can be rigorously defined, and theorems that can be proven
207.
by rntz 10y ago
Ah, good point! I was thinking of unsigned overflow, but signed overflow is a different matter, as pointed out elsewhere in this thread. I retract my statement about trapping overflow.
208.
by rntz 10y ago
> And over integers too, in the presence of overflows (in junk languages without bignums) I don't think this is true. Modular addition is commutative and associative. As long as the behavior of overflow is modular (as it is in 2&#x2
209.
by rntz 10y ago
Goddamit, I downvoted you when I meant to upvote. Sorry.
210.
by rntz 10y ago
Chez is known for being very fast, and for using state-of-the-art compiler technology.

More ›