Kleene's recursion theorem: Difference between revisions

Revision as of 09:35, 21 June 2024

Revision as of 09:50, 18 July 2024

Line 16:

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 such that, when modified by the procedure, it does exactly what it did beforebefore”, or: it's“it’s impossible to write a program that changes the extensional behaviour of all other programs”.

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

Line 37 ⟶ 39:

The theorem can be proved from Rogers's theorem by letting <math>F(p)</math> be a function such that <math>\varphi_{F(p)}(y) = Q(p,y)</math> (a construction described by the [[Smn theorem|S-m-n theorem]]). One can then verify that a fixed-point of this <math>F</math> is an index <math>p</math> as required. The theorem is constructive in the sense that a fixed computable function maps an index for <math>Q</math> into the index <math>p</math>.

This can be further extended to [[Computable function|computable functions]] with this statement:

Let <math>f: \mathbb{N} \rightarrow \mathbb{N}</math> be a total computable function. Then, there exists a program <math>e_0 \in \mathbb{N} </math> such that <math>\phi_{e_0} = \phi_{(f_{(e_0)})}</math>.

This essentially means that if we take a program, we apply an [[Effectiveness|effective]] transformation in an extensional way (say, replace instructions such as successor, jump, remove lines), there will always be a program which is not changed by the transformation of the function, even before or after it.

This theorem can therefore be interpreted in the following manner “given any effective procedure to transform programs, there is always a program such that, when modified by the procedure, it does exactly what it did before, or it's impossible to write a program that changes the extensional behaviour of all other programs”.

=== Comparison to Rogers's theorem ===