= 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 gives
$$
Ff\equiv_\beta f(Ff).
$$
Reducing the occurrence of $Ff$ on the right to $N$ gives the normal form $fN$. The <Church-Rosser theorem> says that these <beta equivalence>[beta-equivalent] terms must have <alpha equivalence>[alpha-equivalent] normal forms. This is impossible because $fN$ contains more symbols than $N$. Hence no typing context and simple type can type $F$.
Back to article page
