= Solution
A <combinator> is a lambda term without free variables. It is a <fixed-point combinator> when
$$
YF\equiv_\beta F(YF)
$$
for 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>. Put
$$
X=(\lambda x.F(xx))(\lambda x.F(xx)).
$$
One beta reduction gives
$$
X\longrightarrow_\beta F((\lambda x.F(xx))(\lambda x.F(xx)))=F(X),
$$
which proves the theorem. Equivalently,
$$
Y=\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))
$$
is a fixed-point combinator.
Apply the theorem to the lambda term $\operatorname{Succ}$. Its fixed point $Y\operatorname{Succ}$ is a nonnormalizing lambda term satisfying $Y\operatorname{Succ}\equiv_\beta\operatorname{Succ}(Y\operatorname{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$.
Back to article page
