In computability theory, Kleene's recursion theorems are a pair of fundamental results about the application of computable functions to their own descriptions.
The theorems were first proved by Stephen Kleene in 1938[1] and appear in his 1952 book Introduction to Metamathematics.
[2] A related theorem, which constructs fixed points of a computable function, is known as Rogers's theorem and is due to Hartley Rogers, Jr.[3] The recursion theorems can be applied to construct fixed points of certain operations on computable functions, to generate quines, and to construct functions defined via recursive definitions.
The statement of the theorems refers to an admissible numbering
are partial functions on the natural numbers, the notation
Rogers describes the following result as "a simpler version" of Kleene's (second) recursion theorem.
is a total computable function, it has a fixed point in the above sense.
This essentially means that if we apply an effective transformation to programs (say, replace instructions such as successor, jump, remove lines), there will always be a program whose behaviour is not altered by the transformation.
This proof is a construction of a partial recursive function which implements the Y combinator.
Arslanov's completeness criterion states that the only recursively enumerable Turing degree that computes a fixed-point-free function is 0′, the degree of the halting problem.
One informal interpretation of the second recursion theorem is that it is possible to construct self-referential programs; see "Application to quines" below.
The theorem is constructive in the sense that a fixed computable function maps an index for
in this case yields a computable function that outputs its own index when applied to any value.
[8] When expressed as computer programs, such indices are known as quines.
: The second recursion theorem can be used to show that such equations define a computable function, where the notion of computability does not have to allow, prima facie, for recursive definitions (for example, it may be defined by μ-recursion, or by Turing machines).
This recursive definition can be converted into a computable function
Jones presents a view of the second recursion theorem based on a reflexive language.
While the second recursion theorem is about fixed points of computable functions, the first recursion theorem is related to fixed points determined by enumeration operators, which are a computable analogue of inductive definitions.
Often, n will be viewed as a code for an ordered pair of natural numbers, particularly when functions are defined via enumeration operators.
Each enumeration operator Φ determines a function from sets of naturals to sets of naturals given by A recursive operator is an enumeration operator that, when given the graph of a partial recursive function, always returns the graph of a partial recursive function.
[10] There is also a definition which can be applied to recursive functionals as follows: Let
However, the recursive operator will actually define the graph of f. First, Φ will contain the pair
This indicates that, if f(n) is m, then f(n + 1) is (n + 1)m, so that the pair (n + 1, (n + 1)m) is in the graph of f. Unlike the base case f(0) = 1, the recursive operator requires some information about f(n) before it defines a value of f(n + 1).
The first recursion theorem (in particular, part 1) states that there is a set F such that Φ(F) = F. The set F will consist entirely of ordered pairs of natural numbers, and will be the graph of the factorial function f, as desired.
Thus there is no fixed point g satisfying these recursion equations.
The proof of part 1 of the first recursion theorem is obtained by iterating the enumeration operator Φ beginning with the empty set.
The remainder of the proof consists of a verification that F is recursively enumerable and is the least fixed point of Φ.
[3] One difference between the first and second recursion theorems is that the fixed points obtained by the first recursion theorem are guaranteed to be least fixed points, while those obtained from the second recursion theorem may not be least fixed points.
[11] A Gödel numbering is a precomplete numbering on the set of computable functions so the generalized theorem yields the Kleene recursion theorem as a special case.
with two parameters there exists a total computable function