15
$\begingroup$

The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Curry-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true theorem. However $a \rightarrow a$ is always true, so it appears as if the Y combinator's type corresponds to the theorem $a$, which is not always true. How can this be?

$\endgroup$

migrated from cstheory.stackexchange.com Oct 30 '14 at 21:41

This question came from our site for theoretical computer scientists and researchers in related fields.

9
$\begingroup$

The Curry-Howard relates type systems to logical deduction systems. Among other things, it maps:

  • programs to proofs
  • program evaluation to transformations on proofs
  • inhabited types to true propositions
  • type systems to logical deduction systems

If the type system admits a Y combinator, then that means that the corresponding logical deduction system is inconsistent — every theorem is true. On the program side, the Y combinator allows any function of type $a \to b$ to be defined, for any $a$ and $b$: $Y (\lambda x. x) \to Y (\lambda x.M)$. The corresponding deduction rule allows any proposition to be derived from any other proposition. Thus the logical system is inconsistent.

The Curry-Howard correspondence is just that: a correspondence. In itself, it doesn't say that certain theorems are true. It says that typability/provability carries from one side to the other.

The Curry-Howard correspondence is useful as a proof tool with many type systems: simply typed lambda calculus, system F, calculus of constructions, etc. All these type systems have the property that the corresponding logic is consistent (if the usual mathematics are consistent). They also have the property of not allowing arbitrary recursion. The Curry-Howard correspondence shows that these two properties are related.

The Curry-Howard still applies to non-terminating typed calculi and inconsistent deduction systems. It's just not particularly useful there.

$\endgroup$
20
$\begingroup$

The original Curry-Howard correspondence is an isomorphism between intuitionistic propositional logic and the simply-typed lambda calculus.

There are, of course, other Curry-Howard-like isomorphisms; Phil Wadler famously pointed out that the double-barrelled name "Curry-Howard" predicts other double-barrelled names like "Hindley-Milner" and "Girard-Reynolds". It would be funny if "Martin-Löf" was one of them, but it isn't. But I digress.

The Y combinator does not contradict this, for one key reason: it is not expressible in the simply-typed lambda calculus.

In fact, that was the whole point. Haskell Curry discovered the fixpoint combinator in the untyped lambda calculus, and used it to prove that the untyped lambda calculus is not a sound deduction system.

Interestingly, the type of Y corresponds to a logical paradox which isn't as well-known as it should be, called Curry's paradox. Consider this sentence:

If this sentence is true, then Santa Claus exists.

Suppose the sentence were true. Then, clearly, Santa Claus would exist. But this is precisely what the sentence says, so the sentence is true. Therefore, Santa Claus exists. QED

$\endgroup$
  • 6
    $\begingroup$ Santa Claus doesn't exist?! $\endgroup$ – Andrej Bauer Oct 31 '14 at 10:49
  • 10
    $\begingroup$ He does, and I just proved it. $\endgroup$ – Pseudonym Nov 1 '14 at 5:24
  • 6
    $\begingroup$ Phew, I was worried for a moment. $\endgroup$ – Andrej Bauer Nov 2 '14 at 17:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.