Stanford Encyclopedia of Philosophy

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.

Definition The class of recursive functions is the (smallest) class of functions from natural numbers to natural numbers that contains:

The initial functions
Name   Definition   Condition
Z Z(n) = 0
S S(x) = x + 1
Un,k Un,k(x1,…xn) = xk n ≥ 1 and 1 ≤ kn

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 x1,…,xn : F(x1,…,xn) = H(x1,…xk−1,G(x1,…xn),xk+1,…xm)

    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 x1,…,xn : F(x1,…,xn,0) = G(x1,…,xn)
    • for all k and all x1,…,xn : F(x1,…,xn,k + 1) = H(x1,…,xn,k,F(x1,…,xn,k))

    then F is a recursive function.

  • minimalization: if G is a recursive function, and if the numeric function F satisfies the relation

    F(x1,…,xn) = y iff G(x1,…,xn,y) = 1 and for all x < y we have G(x1,…,xn,y) = 0

    then F is 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 (a1,…an) of natural numbers, we have

f(a1,…an) = a iff λ ⊢ Fa1an = 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:

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 = x and BFxy = 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

  1. Succ n = n + 1
  2. Pred n + 1 = n
  3. Zero 0 = T
  4. 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

have properties (1)–(4).

Representation of the initial recursive functions in the λ-calculus
Function   Representation
Z λx[I]
S Succ
Un,k λx1 … λxn[xk]

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


The desired representation of definition by primitive recursion is a term Fxy satisfying

Fxy = if-then-else Zero x, Gy, H(Pred xy,y))

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

Theorem For every term F, there exists a term X such that X = 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 number n for 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 HP and μP as

HP := Θhz[if-then-else Pz, z, h Succ z]]

μP := HP0

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 numbers n: either Pn = T or Pn = F

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

Theorem For every number-theoretic function f, we have that f is recursive iff f is λ-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.