General recursive function

The recursive functions are a class of functions which provide a formal model of computability under the conditions set forth by computability theory. Any operation which can be described by a recursive function is called computable; in this respect, recursive functions are similar to Turing machines, Lambda calculus, and other models of computability. Recursive functions are related to primitive recursive functions, and their inductive definition (below) builds upon that of the primitive recursive functions.

Definition

Take as axioms the axioms of the primitive recursive functions, but extend the definitions so as to allow for partial functions. Add one further operator, the least search or unbounded search operator, defined by the following axiom:

If f(x,z₀,z₁,...) is a partial function on the natural numbers, then the function μx f(x,z₀,z₁,...), which returns the least x such that f(0,z₀,z₁,...), f(1,z₀,z₁,...), f(x,z₀,z₁,...), ... are all defined and f(x,z₀,z₁,...) = 0, if such an x exists, is a recursive function. (If such an x does not exist, the operation is undefined on the input z₀,z₁,....)

In the equivalence of models of computability the parallel is drawn between Turing machines which do not terminate for certain inputs and an undefined result for that input in the corresponding recursive function. The unbounded search operator is not definable by the rules of primitive recursion as they do not provide a mechanism for these "infinite loops" (undefined values).

The set of partial recursive functions is the smallest set of partial functions of any arity from natural numbers to natural numbers which contains the zero, successor, and projection functions, and which is closed under composition, primitive recursion, and unbounded search.

The set of recursive functions is the subset of partial recursive functions which are total.

It is interesting to note that if the application of the unbounded search operator in the definition above is limited strictly to regular functions (functions which are guaranteed to be total when the unbounded search operator is applied to them), the resulting set is the same -- in other words, the requirement for partial functions can be partially obviated. The set provided by this definition has historically been labelled the set of general recursive functions, though it is one and the same as the set of recursive functions.