The recursion theorems are three results of theoretical computer science , more precisely the computability theory , by Kleene , Rogers and Case. They describe self-referential properties of computable functions . This is achieved through algorithmic modification of natural numbers , which on the one hand serve as coding of program source texts and on the other hand as functional arguments. Despite the very different statements, all three sentences are formally equivalent; the other two can be derived from each of them. The recursion theorems all follow from the Smn theorem , which was also first proved by Kleene.
Kleene's recursion theorem
The Recursion Theorem of Kleene (ger .: Kleene's recursion theorem , KRT ) was already in 1938 by Stephen Cole Kleene proved and appeared in 1952 in his Introduction to Metamathematics . This version also justifies the designation as a recursion clause , as it originally referred to a recursively defined notation system for ordinals long before recursive became a synonym for calculable in the theory of calculability .
- Let an effective numbering of all partially calculable functions (e.g. the Gödel numbering of all deterministic Turing machines ) be.
- For every partially computable function there is then an index , so that .
- In fact, there is even a totally calculable function that increases strictly monotonically , so that applies .
For every possible calculation there is a program that performs this calculation on its own source code. A coding of this self-referential program can even be effectively determined from an index for the desired calculation. The non-constructive version follows from the constructive one through the setting .
Kleene's Fixed Point Theorem
The fixed point theorem Kleene (English frequently. Rogers' fixed-point theorem ) is a simpler version of the above Rekursionssatzes that in 1967 by Hartley Rogers jr. was specified. It quickly became apparent that the sentence is even equivalent to the original statement.
- For every totally computable function there is an index so that .
- With the additional setting , if , the statement can also be generalized to partial .
- In this case there is again a totally calculable function, increasing strictly monotonically, so that applies .
The fixed point principle means that for every (calculable) source code manipulation there is a program that does not mind the modification. This means that the source text is modified, but this has no effect on the function of the program that is represented by this source text. Since the semantics of the program do not change, one speaks of a semantic fixed point of the syntactic program transformation. Again, such a fixed point can be effectively determined from an index for the manipulation under consideration. In fact, there is an infinite number of semantic fixed points for every modification.
Operator recursion set
The operator Recursion Theorem (ger .: operator recursion theorem , ORT ) by John Case of 1974 dealt a seemingly more general version of the above Rekursionssätze. It describes a property of computable operators , that is, mappings between partial (not necessarily computable) functions that are implemented by a Turing machine.
- For every computable operator there is a totally computable function, increasing strictly monotonically, so that applies .
The main difference to Kleene's version is that ORT delivers not just a single self-referential index, but an infinite number of Gödel numbers , all of which - figuratively speaking - are aware of themselves and of all other indices. In addition, the operator recursion theorem works directly on the level of computable functions, while the versions above deal with source code manipulations. In fact, Case's version also follows from Kleene's original recursion theorem and is therefore equivalent to it.
The recursion clauses are a popular source of (counter) examples in computability theory and algorithmic learning theory . They are often used as auxiliary sentences in proofs when one wants to show the existence of a certain computable function.
For example, the existence of a quines - a program that outputs its own source code - very simply follows from the fixed point variant. To do this, define the modifier function so that the function you are looking for is a fixed point. In the case of quines, this would be the function that returns a program that outputs the source text that has just been entered (pseudocode):
f(x): return "return " + x
The fixed point is then a quine.
Conversely, the recursion sentences can also show the non- calculability of certain functions. For this purpose, one assumes that the mapping under consideration is calculable after all, then it explains a source code manipulation or a calculable operator. The resulting existence of self-referential indices or functions can then be used to construct a contradiction.
Kleene's recursion theorem provides an alternative proof of the undecidability of the halting problem : Assuming it is decidable , its complement can be enumerated recursively . That is, there is a partially computable function that holds (is defined) for input if and only if it does not hold. The existence of a program follows from Kleene's recursion theorem , so that . So all in all , a contradiction.
- Robert I. Soare: Recursively Enumerable Sets and Degrees. Springer, Berlin 1987. ISBN 0387152997
- Christos H. Papadimitriou: Computational Complexity. Addison-Wesley Publishing Company, 1994. ISBN 0-201-53082-1
- ↑ a b Stephen C. Kleene : On Notation for Ordinal Numbers . In: The Journal of Symbolic Logic . 3, 1938, pp. 150-155.
- ↑ a b Hartley Rogers, Jr .: Theory of Recursive Functions and Effective Computability . McGraw-Hill, Cambridge, Massachusetts 1967, ISBN 0-262-68052-1 , p. 179.
- ^ A b John W. Case: Periodicity in Generations of Automata . In: Springer-Verlag (Ed.): Mathematical Systems Theory . 8, No. 1, 1974, pp. 15-32. doi : 10.1007 / BF01761704 .
- ^ Stephen C. Kleene: Introduction to Metamathematics . North-Holland Publishing Company, New York City, New York 1952, pp. 352-353.
- ^ Neil D. Jones: Computability and Complexity from a Programming Perspective . MIT Press, Cambridge, Massachusetts 1997.