The <Church numeral> corresponding to the <natural number> $n$ is
$$
c_n=\lambda f.\lambda x.f^n x.
$$
A function $g:\mathbb N^k\to\mathbb N$ is a <lambda-definable function> if some closed lambda term $G$ satisfies
$$
G c_{n_1}\cdots c_{n_k}\equiv_\beta c_{g(n_1,\ldots,n_k)}
$$
for all natural numbers $n_1,\ldots,n_k$.

Define
$$
\operatorname{Succ}=\lambda n.\lambda f.\lambda x.f(nfx).
$$
Then <beta reduction> gives
$$
\operatorname{Succ}\,c_n
\equiv_\beta\lambda f.\lambda x.f(f^n x)
=c_{n+1}.
$$
Therefore the <successor function> is lambda-definable; this is the <lambda definition of the successor function>.

Solution

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

 Solution

ID: past-exam-of-the-mathematics-course-of-the-university-of-cambridge/2022/iii/paper-120/3/a/solution