d

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 λx1x2xn.xi.

The zero functions return zero whatever their parameters — zeron(x1,x2,…,xn)=0. This can be represented by the lambda expression λx1x2xn.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 λfg1g2gnx1x2xm.f(g1x1x2xm)(g2x1x2xm)…(gnx1x2xm).

Primitive rescursion

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

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’:

λfgx1x2xn.Y(λhx.iszerox(fx1x2xn)(gx1x2xn(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’:

λfx1x2xn.(Y(λhx.iszero(fx1x2xnx)x(h(successorx)))zero)