# Partial recursive functions in lambda calculus

Partial recursive functions are a functional model of universal computation developed by Kleene, Gödel and Herbrand. Partial recursive functions are built from a set of basic functions — projection, zero and successor (which apply to tuples of integers) — using the operations of composition, primitive recursion and minimisation.

## Integers, projection, zero and successor

The integers can be represented in lambda calculus by the standard Church numerals.

The projection functions return one integer from a tuple — projectionni(x1,x2,…,xn)=xi. This can be represented by the lambda expresssion λx1x2…xn.xi.

The zero functions return zero whatever their parameters — zeron(x1,x2,…,xn)=0. This can be represented by the lambda expression λx1x2…xn.zero, where ‘zero’ is the Church numeral zero.

The successor function returns the successor of an integer — this can be represented by the successor function for Church numerals.

## Composition

The composition of the function f with the functions g1, g2,… and gn, applied to the tuple (x1,x2,…,xm) is f(g1(x1,x2,…,xm),g2(x1,x2,…,xm),…,gn(x1,x2,…,xm)).

This can be represented by the lambda expression λfg1g2…gnx1x2…xm.f(g1x1x2…xm)(g2x1x2…xm)…(gnx1x2…xm).

## Primitive rescursion

ρn(f,g) is the function h such that:

• h(x1,x2,…,xn,0) = f(x1,x2,…,xn)
• h(x1,x2,…,xn,x+1) = g(x1,x2,…,xn,x,h(x1,x2,…,xn,x))

This can be represented by the following lambda expression, which uses the fixed-point function Y, the predecessor function, and the test for zero ‘iszero’:

λfgx1x2…xn.Y(λhx.iszerox(fx1x2…xn)(gx1x2…xn(predecessorx)(h(predecessorx))))

## Minimisation

μ(f)(x1,x2,…,xn) returns the smallest x such that f(x1,x2,…,xn,x)=0 (note that such an x may not exist).

This can be represented by the following lambda expression, which uses the fixed-point function Y, the successor function, and the test for zero ‘iszero’:

λfx1x2…xn.(Y(λhx.iszero(fx1x2…xnx)x(h(successorx)))zero)