Proving that $\Omega = (\lambda x.xx)(\lambda x.xx)$ is not typable in the simply typed lambda calculus
I am trying to prove that $\Omega = (\lambda x.xx)(\lambda x.xx)$ is not typable in the simply typed lambda calculus. Surprisingly, different textbooks and lecture notes do not contain that proof, please correct me if I am wrong.
The proof is important, because $\Omega$ does not have a normal form and if it cannot be typed then normalisation theorems do not apply.
From the book Proofs and Types by Girard, Taylor, and Lafont, I read:
If $t$ and $u$ are terms respectively $U \rightarrow V$ and $U$, then $t \; u$ is a term of type $V$.
I am going to prove that any lambda term of type $x \; x$ cannot be typed.
Suppose that the type of the latter $x$ is $T$, then the type of the former $x$ should be $T \rightarrow U$.
That is impossible, because $x$ cannot have two different types.
This implies that $\Omega$ is not typable in the simply typed lambda calculus, because it contains an expression of the form $x\; x$.
My questions are:
- Is my proof correct?
- Is there a better proof?
- Does there exist some extension of lambda calculus where $\Omega$ can be typed?
Solution 1:
- Yes.
- I do not think so. You got the essence of the incompatibility.
- Yes. The most notable example employs intersection-types which allow, following the example of your choice, assignments like $$x\ \ :\ \ T\ \wedge\ T\!\rightarrow\!U$$ and, consequently $$x x\ \ :\ \ U$$ and $$\lambda x.xx\ \ :\ \ T\!\rightarrow\!U \wedge T\!\rightarrow\!U$$ More details expressed in an introductive form can be found, among the many others, in the 1998 article titled Intersection Types, $\lambda$-models, and Bohm Trees, by M. Dezani-Ciancaglini, E. Giovannetti, and U. De'Liguoro.