Past exam of the mathematics course of the University of Cambridge / 2023 / iii / Paper 120 / 2 / f / Solution

Suppose a fixed-point combinator $F$ were typable in the simply typed lambda calculus. By the Weak normalization theorem for simply typed lambda calculus, it would have a beta-normal form. For a fresh variable $f$, the term $Ff$ would then also possess a beta-normal form, say $N$.

The fixed-point property givesReducing the occurrence of $Ff$ on the right to $N$ gives the normal form $fN$. The Church-Rosser theorem says that these beta-equivalent terms must have alpha-equivalent normal forms. This is impossible because $fN$ contains more symbols than $N$. Hence no typing context and simple type can type $F$.