= Solution
A partial function $f:\mathbb N^k\rightharpoonup\mathbb N$ is lambda-definable when a <lambda term> $F$ sends the corresponding <Church numerals> to the numeral for $f(\mathbf n)$ whenever the value is defined and produces no numeral otherwise; in other words, it is a <lambda-definable partial function>. The initial functions are represented by
$$
\mathbf 0=\lambda f.\lambda x.x,
\qquad
\operatorname{Succ}=\lambda n.\lambda f.\lambda x.f(nfx),
$$
and the appropriate variable in $\lambda x_1\ldots x_k.x_i$. If $G,H_1,\ldots,H_m$ represent $g,h_1,\ldots,h_m$, then
$$
\lambda\mathbf x.\,G(H_1\mathbf x)\cdots(H_m\mathbf x)
$$
represents their composition.
Church Booleans supply a lazy conditional, and
$$
\operatorname{IsZero}=\lambda n.\,n(\lambda x.\mathbf{False})\mathbf{True}
$$
tests whether a Church numeral is zero. A standard predecessor term is
$$
\operatorname{Pred}
=\lambda n.\lambda f.\lambda x.\,
n(\lambda g.\lambda h.\,h(gf))(\lambda u.x)(\lambda u.u).
$$
Let $G$ and $H$ represent the base and step functions of a primitive recursion. With a <fixed-point combinator> $Y$, define
$$
R=Y\bigl(\lambda r.\lambda\mathbf x.\lambda n.\,
\operatorname{If}(\operatorname{IsZero}n)
(G\mathbf x)
(H\mathbf x(\operatorname{Pred}n)(r\mathbf x(\operatorname{Pred}n)))\bigr).
$$
Normal-order <beta reduction> evaluates only the selected branch. Induction on the input numeral gives the two recursion equations, so this is the <lambda definition of primitive recursion>.
For <unbounded minimization>, let $G$ represent $g(\mathbf x,n)$ and define
$$
M=Y\bigl(\lambda r.\lambda\mathbf x.\lambda n.\,
\operatorname{If}(\operatorname{IsZero}(G\mathbf x n))
n
(r\mathbf x(\operatorname{Succ}n))\bigr).
$$
Then $M\mathbf x\mathbf0$ tests $0,1,2,\ldots$ in order and returns the least zero of $g$. If no zero is reached, or a required earlier computation is undefined, reduction never produces a Church numeral. This is the <lambda definition of unbounded minimization>. Since the partial recursive functions are generated from the initial functions by composition, primitive recursion, and minimization, every <partial computable function> is represented by a lambda term on Church numerals.
Back to article page
