Past exam of the mathematics course of the University of Cambridge / 2022 / iii / Paper 120 / 3 / b / Solution

A combinator is a lambda term without free variables. It is a fixed-point combinator whenfor every lambda term $F$.

The fixed-point theorem for the untyped lambda calculus states that every untyped lambda term $F$ has a fixed point up to beta equivalence. PutOne beta reduction giveswhich proves the theorem. Equivalently,is a fixed-point combinator.

Apply the theorem to the lambda term $\mathrm{Succ}$. Its fixed point $Y\mathrm{Succ}$ is a nonnormalizing lambda term satisfying $Y\mathrm{Succ}{\equiv }_{\beta }\mathrm{Succ}(Y\mathrm{Succ})$; it is not a Church numeral. The definition of a lambda-definable function describes the representing term only on Church-numeral inputs, so it does not turn this syntactic fixed point into a natural number $n$ satisfying $n+1=n$.