On Thu, Apr 24, 2014 at 10:52 AM, Joerg Arndt <arndt@jjj.de> wrote:
* Mike Stay <metaweta@gmail.com> [Apr 24. 2014 18:44]:
The Y combinator handles the duplication for you so you only have to write the code once. Of course, any modern language allows names for functions, so it's pretty much useless unless you're trying to explain some of the finer points of the Curry-Howard isomorphism.
The *what*? (don't try, I will not understand).
Don't worry: it's a fancy name for an easy concept (though one with deep implications): logic has an interpretation in terms of types and programs. Let F denote the empty set, T denote the 1-element set, X -> Y denote the set of functions from the set X to the set Y, and ~= denote isomorphism. Then F -> F ~= T F -> T ~= T T -> F ~= F T -> T ~= T Boolean implication is a special case of the arrow type. It's why they both use the same symbol. Now think of a sets X and Y as being the set of values satisfying some propositions P and Q, respectively. A total program from X to Y is a constructive intuitionistic proof that P implies Q. The law of the excluded middle says P OR NOT(P) is TRUE. In intuitionistic logic, that translates to "either you have a proof of P or you have a proof of NOT(P)". That's clearly false: we have neither a proof nor disproof of Riemann's hypothesis, and Gödel showed there's no algorithm, in general, for supplying such a proof or disproof. So in intuitionistic logic, the law of the excluded middle doesn't hold. -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com