Editing Kleene's recursion theorem (section)

== Rogers's fixed-point theorem ==
Given a function <math>F</math>, a '''fixed point''' of <math>F</math> is an index <math>e</math> such that <math>\varphi_e \simeq \varphi_{F(e)}</math>. 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.{{sfn|Rogers|1967|loc=§11.2}}
{{math theorem | name = Rogers's fixed-point theorem | math_statement = If <math>F</math> is a total computable function, it has a fixed point in the above sense.}}

This essentially means that if we apply an [[Effectiveness|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 theorem can therefore be interpreted in the following manner: “given any effective procedure to transform programs, there is always a program that, when modified by the procedure, does exactly what it did before”, or: “it’s impossible to write a program that changes the extensional behaviour of all programs”.

=== Proof of the fixed-point theorem ===

The proof uses a particular total computable function <math>h</math>, defined as follows. Given a natural number <math>x</math>, the function <math>h</math> outputs the index of the partial computable function that performs the following computation:
:Given an input <math>y</math>, first attempt to compute <math>\varphi_{x}(x)</math>. If that computation returns an output <math>e</math>, then compute <math>\varphi_e(y)</math> and return its value, if any. 
Thus, for all indices <math>x</math> of partial computable functions, if <math>\varphi_x(x)</math> is defined, then <math>\varphi_{h(x)} \simeq \varphi_{\varphi_x(x)}</math>. If <math>\varphi_x(x)</math> is not defined, then <math>\varphi_{h(x)}</math> is a function that is nowhere defined.   The function <math>h</math> can be constructed from the partial computable function <math>g(x,y)</math> described above and the [[s-m-n theorem]]: for each <math>x</math>, <math>h(x)</math> is the index of a program which computes the function <math>y \mapsto g(x,y)</math>.

To complete the proof, let <math>F</math> be any total computable function, and construct <math>h</math> as above. Let <math>e</math> be an index of the composition <math>F \circ h</math>, which is a total computable function.  Then <math>\varphi_{h(e)} \simeq \varphi_{\varphi_e(e)}</math> by the definition of <math>h</math>.
But, because <math>e</math> is an index of <math>F \circ h</math>, <math>\varphi_e(e) = (F \circ h)(e)</math>, and thus <math>\varphi_{\varphi_e(e)} \simeq \varphi_{F(h(e))}</math>. By the transitivity of <math>\simeq</math>, this means <math>\varphi_{h(e)} \simeq \varphi_{F(h(e))}</math>. Hence <math>\varphi_n \simeq \varphi_{F(n)}</math> for <math>n = h(e)</math>.

This proof is a construction of a [[partial recursive function]] which implements the [[Fixed-point combinator|Y combinator]].

=== Fixed-point-free functions ===
A function <math>F</math> such that <math> \varphi_e \not \simeq \varphi_{F(e)}</math> for all <math>e</math> is called '''fixed-point free'''.  The fixed-point theorem shows that no total computable function is fixed-point free, but there are many non-computable fixed-point-free functions. '''Arslanov's completeness criterion''' states that the only [[recursively enumerable]] [[Turing degree]] that computes a fixed-point-free function is '''0&prime;''', the degree of the [[halting problem]].{{r|Soare1987_88}}