Kleene's recursion theorem: Difference between revisions

Revision as of 01:38, 20 August 2022

Revision as of 09:28, 25 December 2022

Line 12:

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

:'''Rogers's fixed-point theorem'''. If <math>F</math> is a total computable function, it has a fixed point.

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