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?