Rekursionssatz
aus Wikipedia, der freien Enzyklopädie
Der Rekursionssatz oder auch 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.
Inhaltsverzeichnis |
[Bearbeiten] Formale Fassung
Für alle totalen, berechenbaren Funktionen 
gibt es ein 
, so dass 
, wobei 
das k-te Programm bezüglich einer beliebigen Gödel-Nummerierung ist.
Hier ist f das modifizierende Programm und k sozusagen der Quelltext des Programms, das modifiziert wird.
[Bearbeiten] Weiterführendes
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).
[Bearbeiten] 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.
[Bearbeiten] Literatur
- Vorlesung Grundbegriffe der theoretischen Informatik von Prof. Dr. Joachim Biskup an der Universität Dortmund.
- Robert I. Soare: Recursively Enumerable Sets and Degrees, Springer-Verlag, 1987.
