#### Supplement to The Lambda Calculus

## Appendix on Recursive Functions

To show that all recursive functions can be represented in the λ-calculus, one reproduces the definition of recursive functions in the λ-calculus. We recall the definition.

DefinitionThe class ofis the (smallest) class of functions from natural numbers to natural numbers that contains:recursive functions

The initial functions Name Definition Condition ZZ(n) = 0SS(x) =x+ 1U_{n,k}U_{n,k}(x_{1},…x_{n}) =x_{k}n≥ 1 and 1 ≤k≤nand is closed under the operations of:

: ifsubstitution/compositionGandHare recursive functions, and if the numeric functionFsatisfies the relationthere is aksuch that for allx_{1},…,x_{n}:F(x_{1},…,x_{n}) =H(x_{1},…x_{k−1},G(x_{1},…x_{n}),x_{k+1},…x_{m})then

Fis a recursive function.

: ifdefinition by primitive recursionGandHare recursive functions, and if the numeric functionFsatisfies the relations:

- for all
x_{1},…,x_{n}:F(x_{1},…,x_{n},0) =G(x_{1},…,x_{n})- for all k and all
x_{1},…,x_{n}:F(x_{1},…,x_{n},k+ 1) =H(x_{1},…,x_{n},k,F(x_{1},…,x_{n},k))then

Fis a recursive function.

: ifminimalizationGis a recursive function, and if the numeric functionFsatisfies the relationF(x_{1},…,x_{n}) =yiffG(x_{1},…,x_{n},y) = 1 and for allx<ywe haveG(x_{1},…,x_{n},y) = 0then

Fis a recursive function.

Say that a number-theoretic function *f* of arity *n*
is **λ-definable** if there exists a
λ-term *F* with the property that for every natural
number *a* and for every *n*-tuple
(*a*_{1},…*a*_{n}) of natural
numbers, we have

f(a_{1},…a_{n}) =aiff λ ⊢F^{┌}a_{1}^{┐}…^{┌}a_{n}^{┐}=^{┌}a^{┐}

To show that the class of recursive functions can be represented in the λ-calculus, one follows its definition; the step-by-step construction of an arbitrary recursive function from the initial functions can be mimicked in the λ-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 λ-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
λ-terms. Define ^{┌}*n*^{┐} by
recursion as:

^{┌}0^{┐}=**I**^{┌}*n*+ 1^{┐}= λ*x*[*x***F**^{┌}*n*^{┐}]

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 non-zero (‘recursion case’).
One naturally searches for an analogue in the λ-calculus for an
‘if-then-else’ term-building operation.
The **B** combinator accomplishes this. That
is, **B** (given our representation of the constant-true
and constant-false by the λ-terms **T**
and **F**) has the property that

BTxy=xandBFxy=y

for all terms *x* and *y*. We need, further,
λ-terms representing the number-theoretic operations of
successor and predecessor. In other words, we need
λ-terms **Succ**
(successor), **Pred** (predecessor),
and **Zero** (test for zero) satisfying

**Succ**^{┌}*n*^{┐}=^{┌}*n*+ 1^{┐}**Pred**^{┌}*n*+ 1^{┐}=^{┌}*n*^{┐}**Zero**0 =**T****Zero**^{┌}*n*+ 1^{┐}=**F**

for all natural numbers *n*. With this representation of
natural numbers, one can then show that the
terms **Succ**, **Pred**,
and **Zero** defined as

**Succ**:= λ*x*[λ*y*[*y***F***x*]]**Pred**:= λ*x*[*x***F**]**Zero**:= λ*x*[*x***T**]

have properties (1)–(4).

Representation of the initial recursive functions in the λ-calculus

Function Representation Zλx[ I]SSuccU_{n,k}λ x_{1}… λx_{n}[x_{k}]

Substitution/composition is represented straightforwardly: given
that the λ-terms *G*^{*} and *H*^{*}
represent the number-theoretic functions *G* and *H*, the
composition of *G* and *H* is given simply by

λx_{1}…x_{n}[H^{*}x_{1}…x_{k−1}(G^{*}x_{1}…x_{n})x_{k+1}…x_{n}]

The desired representation of definition by primitive recursion is
a term *F**x**y* satisfying

Fxy=if-then-elseZerox,Gy,H(Predxy,y))

The existence of such a term is settled by a *fixed-point
theorem*:

TheoremFor every termF, there exists a termXsuch thatX=FX.

(One can use Curry's ‘paradoxical’ fixed-point
combinator **Y** for this purpose.) The final task is to
represent, in the λ-calculus, the number-theoretic
minimalization operation μ defined on properties of natural
numbers:

μx[φ(x)] = the smallest natural numbernfor which the number-theoretic property φ(n) holds

An adequate representation of μ in the λ-calculus is
defined in stages. Define, for a λ-term *P*, the two
terms *H*_{P} and μ*P* as

H_{P}:=Θ(λh[λz[if-then-elsePz,z,hSuccz]]μ

P:=H_{P}^{┌}0^{┐}

The second clause of the definition can be intuitively understood
as computing thus: Does 0 have property *P*? If so, then stop;
μ*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 μ*P*. The fixed-point
operator **Θ** accomplishes the
‘looping’. One can then show that if *X* is a
λ-term with the property that

for all natural numbersn: eitherP^{┌}n^{┐}=TorP^{┌}n^{┐}=F

and if there exists a natural number *n* such
that *P*^{┌}*n*^{┐}
= **T**, then μ*P* is the least natural
number *m* such
that *P*^{┌}*m*^{┐}
= **T**. With these ingredients in place, one can then
prove the following representation theorem (due to Church):

TheoremFor every number-theoretic functionf, we have thatfis recursive ifffis λ-definable.

One can extend the notion of λ-definability to the wider concept of partial recursive (number-theoretic) functions and prove for that class of functions a result analogous to the preceding theorem.