Rekursionssatz

Der Rekursionssatz oder Fixpunktsatz von Kleene ist ein Satz in der Theoretischen Informatik, genauer der Berechenbarkeitstheorie.

Er handelt von der algorithmischen Modifikation von Programm-Quelltexten. Im Satz kommt ein Programm f vor, das, wenn man ihm den Quelltext eines anderen Programms gibt, diesen nach einem festen Schema oder Algorithmus abändert.

Der Rekursionssatz besagt nun, dass man jedes Modifikationsprogramm austricksen kann: Zu einem gegebenen Modifikationsprogramm kann man immer einen Quelltext finden, dem die Modifikation nichts ausmacht. Das heißt, der Quelltext wird zwar modifiziert, dies hat aber für die Funktion des Programms, das durch diesen Quelltext dargestellt wird, keine Auswirkungen. Man kann sich zum Beispiel vorstellen, dass die Modifikation nur in einem Programmteil vorgenommen wird, der überhaupt nicht ausgeführt wird. Da sich also die Semantik des Programms nicht ändert, spricht man auch von einem Semantik-Fixpunkt der syntaktischen Programmtransformation.

Formale Fassung

Für alle totalen, berechenbaren Funktionen $f: \mathbb{N}\rightarrow\mathbb{N}$ gibt es ein $k\in\mathbb{N}$, so dass φ_k = φ_f(k), wobei φ_k das k-te Programm bezüglich einer beliebigen Gödel-Nummerierung ist. k ist also ein semantischer Fixpunkt der Modifikatorfunktion f.

Hier ist f das modifizierende Programm und k sozusagen der Quelltext des Programms, das modifiziert wird.

Alternative Formulierung und Beweis

Für berechenbare Funktionen f, die Beschreibungen von Turingmaschinen auf Beschreibungen von Turingmaschinen abbilden, gibt es eine Turingmaschine M, sodass $\forall x : f(M)(x) = M(x)$.

Beweis

Definiere nun eine berechenbare Funktion g die wieder Beschreibungen von Turingmaschinen auf Beschreibungen von Turingmaschinen abbildet, sodass $\forall x : g(M)(x) = M(M)(x)$, falls M(M) eine korrekte Beschreibung einer Turingmaschine ist. Ansonsten sei $g(M)(x) = \nearrow$. Nun existiert klarerweise auch die Turingmaschine $M_{f\circ g}$, welche die Hintereinanderausführung der beiden berechenbaren Funktionen f und g durchführt.

Der gesuchte Fixpunkt von f ist nun $g(M_{f\circ g})$, weil $\forall x : g(M_{f\circ g})(x) = M_{f\circ g}(M_{f\circ g})(x) = f(g(M_{f\circ g}))(x)$.

Sonstiges

Zu jeder Funktion gibt es nicht nur einen Fixpunkt, sondern es gibt immer unendlich viele Fixpunkte. Es gibt sogar eine Funktion, die diese Fixpunkte berechnet (effektive Variante des Fixpunktsatzes).

Anwendungen

Der Rekursionssatz wird gerne als Hilfssatz in Beweisen verwendet, wenn man die Existenz einer bestimmten berechenbaren Funktion zeigen will (zum Beispiel ein Quine, ein Programm, das seinen eigenen Quelltext ausgibt). Dazu definiert man sich die Modifikatorfunktion so, dass die gesuchte Funktion ein Fixpunkt ist. Im Fall der Quines wäre die Modifikatorfunktion z.B. die Funktion, die ein Programm zurückgibt, das den gerade eingegebenen Quelltext ausgibt (Pseudocode):

f(x): return "return " + x

Der Fixpunkt ist dann ein Quine.

Literatur

• 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