= Solution
The machine characterization is computation by a <Turing machine>: the machine halts with $f(\mathbf n)$ exactly on inputs in the <domain of a partial function> and does not halt elsewhere. The syntactic characterization is the least class containing the <initial functions of recursion theory> and closed under <composition of partial functions>, <primitive recursion> and <unbounded minimization>. Such functions are the <partial recursive functions>, equivalently the <partial computable functions>.
For clarity, composition here is strict: $g(h_1(\mathbf n),\ldots,h_r(\mathbf n))$ is defined only when every inner value is defined and $g$ is defined on the resulting tuple. Likewise primitive recursion requires all preceding recursive values. The partial minimization $\mu y\,[g(\mathbf n,y)=0]$ is defined when such a $y$ exists and all earlier values are defined and nonzero; an undefined earlier value blocks the search.
A <lambda-definable partial function> is represented by a closed <untyped lambda calculus> term $F$ satisfying
$$
f(\mathbf n)=m\iff F\,c_{n_1}\cdots c_{n_k}\equiv_\beta c_m,
\qquad c_n=\lambda a.\lambda b.a^n b.
$$
On an input outside its domain there must be no <Church numeral> beta-equivalent to the result. A stronger representation can be arranged: undefined inputs have no <head normal form>.
Here are the components for proving that every partial recursive function is lambda-definable. Zero and projections are immediate; <lambda definition of the successor function> uses $\mathrm{Succ}=\lambda n.\lambda a.\lambda b.a(nab)$. <Church Booleans> encode a conditional by $bUV$, with $\mathrm{True}=\lambda u.\lambda v.u$ and $\mathrm{False}=\lambda u.\lambda v.v$. Put
$$
\begin{aligned}
\mathrm{Pair}&=\lambda a.\lambda b.\lambda k.kab,\\
\mathrm{First}&=\lambda p.p\,\mathrm{True},\qquad \mathrm{Second}=\lambda p.p\,\mathrm{False},\\
\mathrm{Step}&=\lambda p.\mathrm{Pair}\,(\mathrm{Second}\,p)\,(\mathrm{Succ}(\mathrm{Second}\,p)),\\
\mathrm{Pred}&=\lambda n.\mathrm{First}\bigl(n\,\mathrm{Step}\,(\mathrm{Pair}\,c_0\,c_0)\bigr),\\
\mathrm{IsZero}&=\lambda n.n(\lambda z.\mathrm{False})\,\mathrm{True}.
\end{aligned}
$$
Iteration takes $(0,0)$ to $(n-1,n)$ for $n>0$, proving that $\mathrm{Pred}\,c_n$ encodes the <predecessor function> and that $\mathrm{IsZero}$ correctly tests zero.
Use a <fixed-point combinator> $Y$ and the strict sequencing operation
$$
\mathrm{Force}=\lambda n.\lambda k.n\,(\lambda z.z)\,k.
$$
For any numeral $c_m$, $\mathrm{Force}\,c_m\,K$ reduces to $K$. If the first argument has no <head normal form>, neither does the whole expression. Thus composition is implemented by nesting $\mathrm{Force}$ on every inner result before applying the outer representing term. This guard is important: an unguarded projection could discard an undefined inner computation.
For <lambda definition of primitive recursion>, with $g,h$ already represented by $G,H$, take
$$
\begin{aligned}
R=Y\bigl(\lambda r.\lambda\mathbf x.\lambda n.\;
\mathrm{IsZero}\,n\;(G\mathbf x)\;
\bigl(\mathrm{Force}\,(r\mathbf x(\mathrm{Pred}\,n))\,
(H\mathbf x(\mathrm{Pred}\,n)(r\mathbf x(\mathrm{Pred}\,n)))\bigr)\bigr).
\end{aligned}
$$
The tuple notation abbreviates successive abstractions and applications. On numeral inputs, induction on $n$ proves the required recursion equations, including strict propagation of undefined preceding values. The <beta reduction> follows the selected conditional branch only.
For <lambda definition of unbounded minimization>, use
$$
Q=Y\bigl(\lambda q.\lambda\mathbf x.\lambda j.\;
\mathrm{IsZero}(G\mathbf xj)\;j\;(q\mathbf x(\mathrm{Succ}\,j))\bigr),
\qquad F\mathbf x=Q\mathbf x c_0.
$$
This searches in increasing order. An undefined value blocks the zero test; an infinite sequence of nonzero values continues forever; the first zero returns its numeral. Under <normal-order beta reduction>, both failure cases have no <head normal form>. Structural induction on partial-recursive declarations now supplies the stronger representation claimed above.
Conversely, <beta reduction> is an effective operation on finitely encoded <lambda terms>. Enumerate all finite reduction sequences from $F\mathbf c_n$, stopping when a result is a <Church numeral> in <beta-normal form>. If $F\mathbf c_n\equiv_\beta c_m$, the <Church-Rosser theorem> gives a reduction to that numeral. It also makes the output unique. The enumeration therefore computes exactly the represented partial function; by the equivalence of the first two characterizations it is partial recursive. Hence
$$
\boxed{\text{partial computable}=\text{partial recursive}=\text{lambda-definable partial}.}
$$
Back to article page
