Editing Kleene's recursion theorem (section)

=== 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]].