# 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:

1. Is my proof correct?
2. Is there a better proof?
3. Does there exist some extension of lambda calculus where $\Omega$ can be typed?
• I would also add that $T$ and $T \rightarrow U$ are different only since we consider finite types. One could think of an infinite type $U = T \rightarrow (T \rightarrow (T \rightarrow \ldots)))$ that satisfies that equation. – Guido Apr 23 '18 at 17:09

3. 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.
• Recursive types also allow you to type self-application, as well as $\Omega$. Pierce's TAPL contains a good explanation. – Guido Apr 23 '18 at 17:08