= Solution
Represent a nonnegative <integer> $n$ by the <Church numeral>
$$
\underline n=\lambda f.\lambda x.f^n x.
$$
A closed <lambda term> $F$ represents a <partial computable function> $f$ if, on inputs in its domain, $F\underline{n_1}\cdots\underline{n_k}$ reduces to the <Church numeral> of the value, and on other inputs it produces no <Church numeral>. We use <untyped lambda calculus> and <normal-order beta reduction>.
First every <primitive recursive function> has such a representation on all inputs. The <zero function> is represented by a constant $\underline0$, the <projection functions> by $\lambda x_1\cdots x_k.x_i$, and the <successor function> by
$$
\mathsf{Succ}=\lambda n f x.f(nfx).
$$
For <function composition in recursion theory>, substitute the represented inner functions into the represented outer function:
$$
\lambda\mathbf x.\,G(H_1\mathbf x)\cdots(H_m\mathbf x).
$$
These constituent functions are total, so there is no undefined argument to be discarded.
For <primitive recursion>, use <Church Booleans> and <Church pairs>:
$$
\mathsf T=\lambda a b.a,\quad \mathsf F=\lambda a b.b,\quad
\mathsf{Pair}=\lambda a b p.pab,\quad
\mathsf{Fst}=\lambda p.p\mathsf T,\quad
\mathsf{Snd}=\lambda p.p\mathsf F.
$$
If $G,H$ represent the total functions defining a recursion, put
$$
\mathsf{Step}_{\mathbf x}=\lambda p.\,
\mathsf{Pair}\bigl(\mathsf{Succ}(\mathsf{Fst}\,p)\bigr)
\bigl(H\mathbf x(\mathsf{Fst}\,p)(\mathsf{Snd}\,p)\bigr),
$$
and
$$
R=\lambda\mathbf x n.\,
\mathsf{Snd}\bigl(n\mathsf{Step}_{\mathbf x}
(\mathsf{Pair}\,\underline0\,(G\mathbf x))\bigr).
$$
After $j$ iterations the <Church pair> contains the counter $\underline j$ and the recursively computed value at $j$, by <mathematical induction>. Thus this <lambda definition of primitive recursion by pair iteration> represents the recursion. A <structural induction for primitive recursive functions> now represents every <primitive recursive function>.
To pass to arbitrary <partial computable functions>, use the <Kleene normal form theorem> in the following form: for every $f:\mathbb N^k\rightharpoonup\mathbb N$, there are total <primitive recursive functions> $C,U$ such that
$$
f(\mathbf x)=U\bigl(\mu t\,[C(\mathbf x,t)=0]\bigr),
$$
with $f$ undefined precisely when no such $t$ exists. The predicate checks codes of valid finite halting histories for the chosen program; $U$ extracts their common output. This expresses <unbounded minimization> of a total predicate, so no earlier undefined test can interfere with the search.
Let $\widehat C,\widehat U$ be the represented total functions. The <Church numeral zero test> and a <fixed-point combinator> are
$$
\mathsf{Zero}=\lambda n.n(\lambda z.\mathsf F)\mathsf T,
\qquad
Y=\lambda h.(\lambda z.h(zz))(\lambda z.h(zz)).
$$
Define the search <lambda term>
$$
Q=Y\bigl(\lambda q\,\mathbf x\,t.\,
(\mathsf{Zero}(\widehat C\mathbf x t))
(\widehat U t)
(q\mathbf x(\mathsf{Succ}\,t))\bigr),
\qquad F=\lambda\mathbf x.Q\mathbf x\underline0.
$$
All displayed abbreviations expand to finite closed <lambda terms>; $\mathbf x$ stands for the fixed finite tuple of input variables. Because $YH\equiv_\beta H(YH)$, <normal-order beta reduction> tests $t=0,1,2,\ldots$. At the first successful test the <Church Boolean> selects $\widehat U t$, which reduces to the correct <Church numeral>. The unused recursive branch is discarded.
If no test succeeds, every finite search step returns to another head search, never exposing a numeral. The term has no <head normal form> and hence cannot be <beta equivalent> to a <Church numeral>. This last point is why the output operation occurs inside the successful branch: simply applying a possibly argument-discarding outer function to a divergent search would not justify undefinedness. Therefore \b[every computable function is representable], including <partial computable functions> with their correct undefined inputs:
$$
\boxed{\begin{aligned}f(\mathbf n)\downarrow\ &\Longrightarrow\
F\underline{\mathbf n}\to_\beta^*\underline{f(\mathbf n)};
\\ f(\mathbf n)\uparrow\ &\Longrightarrow\text{no numeral result}.\end{aligned}}
$$
Back to article page
