9
$\begingroup$

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?
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Guido Apr 23 '18 at 17:09
9
$\begingroup$
  1. Yes.
  2. I do not think so. You got the essence of the incompatibility.
  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.
$\endgroup$
  • $\begingroup$ Recursive types also allow you to type self-application, as well as $\Omega$. Pierce's TAPL contains a good explanation. $\endgroup$ – Guido Apr 23 '18 at 17:08

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.