Concept

Kleene's recursion theorem

Summary
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 and appear in his 1952 book Introduction to Metamathematics. A related theorem, which constructs fixed points of a computable function, is known as Rogers's theorem and is due to Hartley Rogers, Jr. 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 of the partial recursive functions, such that the function corresponding to index is . If and are partial functions on the natural numbers, the notation indicates that, for each n, either and are both defined and are equal, or else and are both undefined. Given a function , a fixed point of is an index such that . Note that the comparison of in- and outputs here is not in terms of numerical values, but in terms of their associated functions. Rogers describes the following result as "a simpler version" of Kleene's (second) recursion theorem. The proof uses a particular total computable function , defined as follows. Given a natural number , the function outputs the index of the partial computable function that performs the following computation: Given an input , first attempt to compute . If that computation returns an output , then compute and return its value, if any. Thus, for all indices of partial computable functions, if is defined, then . If is not defined, then is a function that is nowhere defined. The function can be constructed from the partial computable function described above and the s-m-n theorem: for each , is the index of a program which computes the function . To complete the proof, let be any total computable function, and construct as above. Let be an index of the composition , which is a total computable function. Then by the definition of .
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.