Kleene's recursion theorem

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. (1967). 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. (1967). 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 φ {displaystyle varphi } of the partial recursive functions, such that the function corresponding to index e {displaystyle e} is φ e {displaystyle varphi _{e}} . In programming terms, e {displaystyle e} represents a program and φ e {displaystyle varphi _{e}} represents the function computed by this program. If F {displaystyle F} and G {displaystyle G} are partial functions on the natural numbers, the notation F ≃ G {displaystyle Fsimeq G} indicates that, for each n, either F ( n ) {displaystyle F(n)} and G ( n ) {displaystyle G(n)} are both defined and are equal, or else F ( n ) {displaystyle F(n)} and G ( n ) {displaystyle G(n)} are both undefined. Given a function F {displaystyle F} , a fixed point of F {displaystyle F} is an index e {displaystyle e} such that φ e ≃ φ F ( e ) {displaystyle varphi _{e}simeq varphi _{F(e)}} . Rogers (Rogers 1967: §11.2) describes the following result as 'a simpler version' of Kleene's (second) recursion theorem. The proof uses a particular total computable function h {displaystyle h} , defined as follows. Given a natural number x {displaystyle x} , the function h {displaystyle h} outputs the index of the partial computable function that performs the following computation: Thus, for all indices x {displaystyle x} of partial computable functions, if φ x ( x ) {displaystyle varphi _{x}(x)} is defined, then φ h ( x ) ≃ φ φ x ( x ) {displaystyle varphi _{h(x)}simeq varphi _{varphi _{x}(x)}} . If φ x ( x ) {displaystyle varphi _{x}(x)} is not defined, then φ h ( x ) {displaystyle varphi _{h(x)}} is a function that is nowhere defined. The function h {displaystyle h} can be constructed from the partial computable function g ( x , y ) {displaystyle g(x,y)} described above and the s-m-n theorem: for each x {displaystyle x} , h ( x ) {displaystyle h(x)} is the index of a program which computes the function y ↦ g ( x , y ) {displaystyle ymapsto g(x,y)} . To complete the proof, let F {displaystyle F} be any total computable function, and construct h {displaystyle h} as above. Let e {displaystyle e} be an index of the composition F ∘ h {displaystyle Fcirc h} , which is a total computable function. Then φ h ( e ) ≃ φ φ e ( e ) {displaystyle varphi _{h(e)}simeq varphi _{varphi _{e}(e)}} by the definition of h {displaystyle h} .But, because e {displaystyle e} is an index of F ∘ h {displaystyle Fcirc h} , φ e ( e ) = ( F ∘ h ) ( e ) {displaystyle varphi _{e}(e)=(Fcirc h)(e)} , and thus φ φ e ( e ) ≃ φ F ( h ( e ) ) {displaystyle varphi _{varphi _{e}(e)}simeq varphi _{F(h(e))}} . By the transitivity of ≃ {displaystyle simeq } , this means φ h ( e ) ≃ φ F ( h ( e ) ) {displaystyle varphi _{h(e)}simeq varphi _{F(h(e))}} . Hence φ n ≃ φ F ( n ) {displaystyle varphi _{n}simeq varphi _{F(n)}} for n = h ( e ) {displaystyle n=h(e)} . This proof is a construction of a partial recursive function which implements the Y combinator.