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 — projection^{n}_{i}(x_{1},x_{2},…,x_{n})=x_{i}. This can be represented by the lambda expresssion λx_{1}x_{2}…x_{n}.x_{i}.
The zero functions return zero whatever their parameters — zero^{n}(x_{1},x_{2},…,x_{n})=0. This can be represented by the lambda expression λx_{1}x_{2}…x_{n}.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 g_{1}, g_{2},… and g_{n}, applied to the tuple (x_{1},x_{2},…,x_{m}) is f(g_{1}(x_{1},x_{2},…,x_{m}),g_{2}(x_{1},x_{2},…,x_{m}),…,g_{n}(x_{1},x_{2},…,x_{m})).
This can be represented by the lambda expression λfg_{1}g_{2}…g_{n}x_{1}x_{2}…x_{m}.f(g_{1}x_{1}x_{2}…x_{m})(g_{2}x_{1}x_{2}…x_{m})…(g_{n}x_{1}x_{2}…x_{m}).
Primitive rescursion
ρ^{n}(f,g) is the function h such that:
- h(x_{1},x_{2},…,x_{n},0) = f(x_{1},x_{2},…,x_{n})
- h(x_{1},x_{2},…,x_{n},x+1) = g(x_{1},x_{2},…,x_{n},x,h(x_{1},x_{2},…,x_{n},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’:
λfgx_{1}x_{2}…x_{n}.Y(λhx.iszerox(fx_{1}x2…x_{n})(gx_{1}x_{2}…x_{n}(predecessorx)(h(predecessorx))))
Minimisation
μ(f)(x_{1},x_{2},…,x_{n}) returns the smallest x such that f(x_{1},x_{2},…,x_{n},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’:
λfx_{1}x_{2}…x_{n}.(Y(λhx.iszero(fx_{1}x_{2}…x_{n}x)x(h(successorx)))zero)