Past exam of the mathematics course of the University of Cambridge / 2015 / iii / Paper 25 / 4 / Solution

We use untyped lambda calculus and normal-order beta reduction. The Church numeral for $n$ is $\overline{n}=\lambda s.\lambda z.s^{n}z$. A lambda term represents a partial function if on numeral inputs it has the correct numeral normal form exactly when the function is defined. We use a lambda simulation of a Turing machine; this also ensures that undefined computations do not accidentally produce an output through an ignored argument.

First all total primitive recursive functions are lambda-definable. The initial functions of recursion theory are represented byComposition is obtained by substitution of representing terms. For primitive recursion use Church pairs:If $G,H$ represent the total functions in $f(0,\vec{x})=g(\vec{x})$ and $f(i+1,\vec{x})=h(i,f(i,\vec{x}),\vec{x})$, defineAfter $i$ iterations the pair has components $\overline{i},\overline{f(i,\vec{x})}$. Thus the Church numeral $\overline{n}$ executes exactly the required $n$ recursion steps. Since these functions are total on numeral inputs, substitution for composition causes no undefined-argument issue.

Now fix a deterministic Turing machine computing the given partial computable function. Encode a configuration by its finite control state and two natural numbers for the tape portions on the two sides of the head, allowing blank bits beyond the finite nonblank tape. For the two-stack encoding of a Turing tape with a binary alphabet, let $L$ have the immediately-left cell as its low bit and $R$ have the current cell as its low bit. Reading and removing a bit use remainder and quotient by two. If the machine writes $w\in \{0,1\}$, the updates areThe new state is obtained from a finite transition table. These operations, the initial configuration, the halting test, and output decoding are total primitive recursive functions on configuration codes. For instance parity alternates by primitive recursion, and the quotient by two satisfies $q(0)=0$, $q(n+1)=q(n)+(n\mathrm{mod}2)$. A fixed finite alphabet can be handled by the same stack construction in a larger base. Choose a standard delimited input and output convention, for example unary words in a finite tape alphabet with a distinct blank symbol. Initialization is primitive recursive. On a halting configuration the output is a finite word; decoding can be implemented by a bounded scan of the encoded tape, with a default output for malformed words. This is total primitive recursive and introduces no additional unbounded search. Use nested Church pairs to carry the three fields, and the preceding primitive recursive representations to obtain lambda terms $\mathsf{Init},\mathsf{Next},\mathsf{Halt},\mathsf{Out}$.

Represent Church Booleans by $\mathsf{True}=\lambda ab.a$ and $\mathsf{False}=\lambda ab.b$. A Church numeral zero test is $\mathsf{IsZero}=\lambda n.n(\lambda z.\mathsf{False})\mathsf{True}$. Use a numerical test equal to zero on halting configurations and one otherwise; applying this zero test gives the required Boolean halting test. With the fixed-point combinatorputNormal-order reduction evaluates the halting test on the current configuration. If it is true, it selects the output branch without evaluating the recursive branch. Otherwise it advances the configuration and repeats. Induction on the number of machine steps shows that a computation halting with output $y$ makes $F\overline{x_1}\cdots \overline{x_k}$ reduce to $\overline{y}$.

If the machine never halts, the normal-order beta reduction repeatedly takes the recursive branch. Each individual configuration transition and test terminates, but there is always another required transition; hence the reduction never reaches a normal form. The normal-order normalization theorem says that a lambda term with a beta-normal form is normalized by normal-order beta reduction. Therefore in the nonhalting case there is no numeral normal form at all. We have provedConfluence of beta reduction ensures uniqueness of the resulting numeral. This handles genuinely partial computations. Simply composing terms for partial subcomputations would need extra care, because lambda reduction can discard an unevaluated argument.