Kleene's recursion theorem: Difference between revisions

Revision as of 10:55, 18 December 2023

Latest revision as of 15:38, 17 March 2025

(3 intermediate revisions by 3 users not shown)

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

Line 91 ⟶ 85:

== The first recursion theorem ==

While the second recursion theorem is about fixed points of computable functions, the first recursion theorem is related to fixed points determined by enumeration operators, which are a computable analogue of inductive definitions. An '''enumeration operator''' is a set of pairs (''A'',''n'') where ''A'' is a ([[Gödel number|code]] for a) finite set of numbers and ''n'' is a single [[natural number]]. Often, ''n'' will be viewed as a code for an ordered pair of natural numbers, particularly when functions are defined via enumeration operators. Enumeration operators are of central importance in the study of [[enumeration reducibility]].

Each enumeration operator Φ determines a function from sets of naturals to sets of naturals given by

Line 102 ⟶ 96:

:# For any computable enumeration operator Φ there is a recursively enumerable set ''F'' such that Φ(''F'') = ''F'' and ''F'' is the smallest set with this property.

:# For any recursive operator Ψ there is a partial computable function φ such that Ψ(φ) = φ and φ is the smallest partial computable function with this property.

The first recursion theorem is also called Fixed point theorem (of recursion theory).<ref>{{Cite book |last=Cutland |first=Nigel |title=Computability: an introduction to recursive function theory}}</ref>. There is also a definition which can be applied to [[Primitive recursive functional|recursive functionals]] as follows:

Let <math>\Phi: \mathbb{F}(\mathbb{N}^k) \rightarrow (\mathbb{N}^k)</math> be a recursive functional. Then <math>\Phi</math> has a least fixed point <math>f_{\Phi}: \mathbb{N}^k \rightarrow \mathbb{N}</math> which is computable i.e.

Line 125 ⟶ 119:

The first recursion theorem (in particular, part 1) states that there is a set ''F'' such that {{nowrap|1=Φ(''F'') = F}}. The set ''F'' will consist entirely of ordered pairs of natural numbers, and will be the graph of the factorial function ''f'', as desired.

The restriction to recursion equations that can be recast as recursive operators ensures that the recursion equations actually define a [[least fixed point]]. For example, consider the set of recursion equations:<math display="block">\begin{align}

&g(0) = 1\\

&g(n + 1) = 1\\

Line 132 ⟶ 126:

=== Proof sketch for the first recursion theorem ===

The proof of part 1 of the first recursion theorem is obtained by iterating the enumeration operator Φ beginning with the [[empty set]]. First, a sequence ''F''_''k'' is constructed, for <math>k = 0, 1, \ldots</math>. Let ''F''₀ be the empty set. Proceeding inductively, for each ''k'', let ''F''_{''k'' + 1} be <math>F_k \cup \Phi(F_k)</math>. Finally, ''F'' is taken to be <math display="inline">\bigcup F_k</math>. The remainder of the proof consists of a verification that ''F'' is recursively enumerable and is the least fixed point of Φ. The sequence ''F''_''k'' used in this proof corresponds to the Kleene chain in the proof of the [[Kleene fixed-point theorem]].

The second part of the first recursion theorem follows from the first part. The assumption that Φ is a recursive operator is used to show that the fixed point of Φ is the graph of a partial function. The key point is that if the fixed point ''F'' is not the graph of a function, then there is some ''k'' such that ''F''_''k'' is not the graph of a function.