Does the Y combinator contradict the Curry-Howard correspondence?

Question

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?

Answer 1

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

Answer 2

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.

Answer 3

Look at the construction for $Y = λf·(λx·f (x x))(λx·f (x x))$. Carefully apply the type rules to it $$\begin{align} f:& C → A,\\ x:& B → C,\\ x:& B,\\ x x:& C,\\ f (x x):& A,\\ λx·f (x x):& B → A,\\ λx·f (x x) (λx·f (x x)):& A,\\ λf·(λx·f (x x) (λx·f (x x))):& A → A, \end{align}$$ where, in order to make the applications $x x$ and $(λx·f (x x))(λx·f (x x))$ consistently work, we need the following equations $$B = B → C,\quad A = B.$$

As with all other cases of type-matching, this puts restrictions on the set of types involved in the typing. This typing is assumed to hold for all $(A,B,C)$ that satisfy these equations. In logic, if you have a statement $B$ that satisfies the equivalence $B ⇔ B → C$ with respect to another statement $C$, then by Modus Ponens: $C$ follows from $B$. Since $(⋯) → (⋯)$ is monotonically increasing with respect to the second argument, then that means $B$ follows from $B → B$, which - in logic - is the tautology value $⊤$, therefore $B = ⊤$. Since $C$ follows from $B = ⊤$, then we also have $C = ⊤$.

Under Curry-Howard, $⊤$ would correspond to a type that solves $⊤ = ⊤ → ⊤$ and contains all other types. Its key equivalences, motivated by logic, would be $A → ⊤ ⇔ ⊤$ and $⊤ → A ⇔ A$. For the construction given above, the types are all restricted to $A = B = C = B → C = ⊤$.

There is no finite construction that yields a generic type $Y: (A → A) → A$, except with $A = ⊤$. On the other hand, a rational infinite construction $f(f(f(⋯)))$ yields the type $f(f(f(⋯))): A$, for any $f: A → A$, so that you could write $$Y = λf·f(f(f(⋯))): (A → A) → A.$$ The corresponding proof is infinite (though rational). It has an end - consisting of an infinite number of Modus Ponens all identical in form, followed by a discharge of hypothesis - but no beginning.

If you apply this to the combinator $I = λx·x: A → A$, you get what one might call the "Curry Paradox Term" $(λf·f(f(f(⋯)))) I$, whose corresponding proof is similarly infinite, but is capped off with that final Modus Ponens with the tautology $A → A$ to get the conclusion $A$, for arbitrary $A$.

If you abstract $λf·f(f(f(⋯)))$ using the rule $λx·x y = U (λx·y)$, where $U = λxλy·y(xy)$, then you can proceed to write $Y = U(U(U(⋯)))$. The combinator $U$ has, as its most general type, $$U: ((A → B) → A) → (A → B) → B.$$ So, it applies to this construction of $Y$, provided you impose the constraint $A = A → B$, which lands everything right back at the previous construction of $Y$. The corresponding proof is an infinitely-layered natural deduction proof (though rational infinite), with an infinite number of hypotheses discharged.

So, I'm not sure you can get $Y$, with the typing $Y: (A → A) → A$ for arbitrary $A$, even with rational infinite combinator expressions.

On the other hand, $(λf·f(f(f(⋯)))) U: (A → B) → B$, with the constraint $A = B$ imposed by the construction, works just fine as an equivalent form for $Y$.

A brief search uncovers two articles that touch on the issue Infinite λ-Calculus And Types and All the λ-Terms are Meaningful for the Infinitary Relational Model.