Fixpunktsatz von Kleene

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 $\varphi_{k} = \varphi_{f(k)}$, wobei $\varphi_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.

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. Jedoch hilft dieser Satz nicht dabei, Quines zu finden. Er stellt nur sicher, dass es in jeder (Turing-vollständigen) Programmiersprache Quines gibt.

Quelle

• Grundbegriffe der theoretischen Informatik. Vorlesung von Prof. Dr. Joachim Biskup an der Technischen Universität Dortmund.

Literatur

• Robert I. Soare: Recursively Enumerable Sets and Degrees. Springer, Berlin 1987. ISBN 0387152997