Supplement to The Lambda Calculus
Appendix on Recursive Functions
To show that all recursive functions can be represented in the \(\lambda\)calculus, one reproduces the definition of recursive functions in the \(\lambda\)calculus. We recall the definition.
Definition The class of recursive functions is the (smallest) class of functions from natural numbers to natural numbers that contains:
Name  Definition  Condition 
\(Z\)  \(Z(n) = 0\)  
\(S\)  \(S(x) = x + 1\)  
\(U_{n,k}\)  \(U_{n,k}(x_1 ,\ldots x_n) = x_k\)  \(n \ge 1\) and \(1 \le k \le n\) 
and is closed under the operations of:
 substitution/composition: if \(G\) and \(H\) are recursive functions, and if the numeric function \(F\) satisfies the relation: there is a \(k\) such that for all \(x_1 ,\ldots ,x_n\): \(F(x_1 ,\ldots ,x_n) = H(x_1 ,\ldots x_{k1},G(x_1 ,\ldots x_n),x_{k+1},\ldots x_m)\), then \(F\) is a recursive function.
definition by primitive recursion: if \(G\) and \(H\) are recursive functions, and if the numeric function \(F\) satisfies the relations:
 for all \(x_1 ,\ldots ,x_n\): \(F(x_1 ,\ldots ,x_n,0) = G(x_1 ,\ldots ,x_n)\)
 for all k and all \(x_1 ,\ldots ,x_n\): \(F(x_1 ,\ldots ,x_n,k + 1) = H(x_1 ,\ldots ,x_n,k,F(x_1 ,\ldots ,x_n,k))\)
then \(F\) is a recursive function.

minimalization: if \(G\) is a recursive function, and if the numeric function \(F\) satisfies the relation
 \(F(x_1 ,\ldots ,x_n) = y\) iff \(G(x_1 ,\ldots ,x_n,y) = 1\) and for all \(x \lt y\) we have \(G(x_1 ,\ldots ,x_n,x) = 0\)
then \(F\) is a recursive function.
Say that a numbertheoretic function \(f\) of arity \(n\) is \(\lambda\)definable if there exists a \(\lambda\)term \(F\) with the property that for every natural number \(a\) and for every \(n\)tuple \((a_1 ,\ldots a_n)\) of natural numbers, we have
\[ f(a_1 ,\ldots a_n) = a \text{ iff } \lambda \vdash F\ulcorner a_1\urcorner \ldots \ulcorner a_n\urcorner = \ulcorner a\urcorner \]To show that the class of recursive functions can be represented in the \(\lambda\)calculus, one follows its definition; the stepbystep construction of an arbitrary recursive function from the initial functions can be mimicked in the \(\lambda\)calculus. One shows first that all initial functions can be represented; then one shows that the operations of substitution/composition, definition by primitive recursion, and minimalization can likewise be expressed. We require, first, a representation of natural numbers in the \(\lambda\)calculus. Representing the initial functions and substitution/composition will then be straightforward, but some work is required to show that definition by primitive recursion and minimalization can be adequately represented. The development that follows is standard (Barendregt, 1984).
We begin with a representation of natural numbers as \(\lambda\)terms. Define \(\ulcorner n\urcorner\) by recursion as:
\[\begin{align} \ulcorner 0\urcorner &= \bI \\ \ulcorner n + 1\urcorner &= \lambda x[x\bF\ulcorner n\urcorner] \end{align}\]Intuitively, to represent primitive recursion, one ought be able to proceed by cases because one has to test whether an argument is zero (‘base case’) or nonzero (‘recursion case’). One naturally searches for an analogue in the \(\lambda\)calculus for an ‘ifthenelse’ termbuilding operation. The \(\bB\) combinator accomplishes this. That is, \(\bB\) (given our representation of the constanttrue and constantfalse by the \(\lambda\)terms \(\bT\) and \(\bF\)) has the property that
\[ \bB\bT xy = x \text{ and } \bB\bF xy = y \]for all terms \(x\) and \(y\). We need, further, \(\lambda\)terms representing the numbertheoretic operations of successor and predecessor. In other words, we need \(\lambda\)terms \(\Succ\) (successor), \(\Pred\) (predecessor), and \(\Zero\) (test for zero) satisfying
\[\begin{align} &\Succ \ulcorner n\urcorner = \ulcorner n + 1\urcorner \\ &\Pred \ulcorner n + 1\urcorner = \ulcorner n\urcorner \\ &\Zero 0 = \bT \\ &\Zero \ulcorner n + 1\urcorner = \bF \end{align}\]for all natural numbers \(n\). With this representation of natural numbers, one can then show that the terms \(\Succ, \Pred\), and \(\Zero\) defined as
\[\begin{align} \Succ &:= \lambda x[\lambda y[y\bF x]] \\ \Pred &:= \lambda x[x\bF] \\ \Zero &:= \lambda x[x\bT] \end{align}\]have properties (1)–(4).
Function  Representation 
\(Z\)  \(\lambda\)x[\(\bI\)] 
\(S\)  \(\Succ\) 
\(U_{n,k}\)  \(\lambda x_1 \ldots \lambda\)x\(_n\)[x\(_k\)] 
Substitution/composition is represented straightforwardly: given that the \(\lambda\)terms \(G^*\) and \(H^*\) represent the numbertheoretic functions \(G\) and \(H\), the composition of \(G\) and \(H\) is given simply by
\[ \lambda x_1 \ldots x_n [H^* x_1 \ldots x_{k1}(G^* x_1 \ldots x_n)x_{k+1}\ldots x_n] \]The desired representation of definition by primitive recursion is a term \(Fxy\) satisfying
\[ Fxy = \ifthenelse \Zero x, Gy, H(\Pred xy,y)) \]The existence of such a term is settled by a fixedpoint theorem:
Theorem For every term \(F\), there exists a term \(X\) such that \(X = FX\).
(One can use Curry’s ‘paradoxical’ fixedpoint combinator \(\bY\) for this purpose.) The final task is to represent, in the \(\lambda\)calculus, the numbertheoretic minimalization operation \(\mu\) defined on properties of natural numbers:
\(\mu x[\phi(x)] =\) the smallest natural number \(n\) for which the numbertheoretic property \(\phi(n)\) holds
An adequate representation of \(\mu\) in the \(\lambda\)calculus is defined in stages. Define, for a \(\lambda\)term \(P\), the two terms \(H_P\) and \(\mu P\) as
\[\begin{align} H_P &:= \bTheta (\lambda h[\lambda z[\ifthenelse Pz, z, h \Succ z]] \\ \mu P &:= H_P\ulcorner 0\urcorner \end{align}\]The second clause of the definition can be intuitively understood as computing thus: Does 0 have property \(P\)? If so, then stop; \(\mu P\) is 0. If not, does 1 have property \(P\)? If so, then 1 is the answer. Proceeding in this fashion, one will eventually stop and the computed value will be \(\mu P\). The fixedpoint operator \(\Theta\) accomplishes the ‘looping’. One can then show that if \(X\) is a \(\lambda\)term with the property that
 for all natural numbers \(n\): either \(P\ulcorner n\urcorner = \bT\) or \(P\ulcorner n\urcorner = \bF\)
and if there exists a natural number \(n\) such that \(P\ulcorner n\urcorner = \bT\), then \(\mu P\) is the least natural number \(m\) such that \(P\ulcorner m\urcorner = \bT\). With these ingredients in place, one can then prove the following representation theorem (due to Church):
Theorem For every numbertheoretic function \(f\), we have that \(f\) is recursive iff \(f\) is \(\lambda\)definable.
One can extend the notion of \(\lambda\)definability to the wider concept of partial recursive (numbertheoretic) functions and prove for that class of functions a result analogous to the preceding theorem.