Rekursionssatz


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.

Inhaltsverzeichnis

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

Wikimedia Foundation.

Schlagen Sie auch in anderen Wörterbüchern nach:

  • 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,… …   Deutsch Wikipedia

  • Rekursionsanfang — Dieser Artikel erläutert die Technik der rekursiven Definition; zum Begriff rekursive Menge siehe entscheidbar. Als Rekursion (lat. recurrere „zurücklaufen“) bezeichnet man die Technik in Mathematik, Logik und Informatik, eine Funktion durch sich …   Deutsch Wikipedia

  • Rekursionsformel — Dieser Artikel erläutert die Technik der rekursiven Definition; zum Begriff rekursive Menge siehe entscheidbar. Als Rekursion (lat. recurrere „zurücklaufen“) bezeichnet man die Technik in Mathematik, Logik und Informatik, eine Funktion durch sich …   Deutsch Wikipedia

  • Rekursionsschritt — Dieser Artikel erläutert die Technik der rekursiven Definition; zum Begriff rekursive Menge siehe entscheidbar. Als Rekursion (lat. recurrere „zurücklaufen“) bezeichnet man die Technik in Mathematik, Logik und Informatik, eine Funktion durch sich …   Deutsch Wikipedia

  • Rekursionstiefe — Dieser Artikel erläutert die Technik der rekursiven Definition; zum Begriff rekursive Menge siehe entscheidbar. Als Rekursion (lat. recurrere „zurücklaufen“) bezeichnet man die Technik in Mathematik, Logik und Informatik, eine Funktion durch sich …   Deutsch Wikipedia

  • Rekursiv — Dieser Artikel erläutert die Technik der rekursiven Definition; zum Begriff rekursive Menge siehe entscheidbar. Als Rekursion (lat. recurrere „zurücklaufen“) bezeichnet man die Technik in Mathematik, Logik und Informatik, eine Funktion durch sich …   Deutsch Wikipedia

  • Rekursive Endlosschleife — Dieser Artikel erläutert die Technik der rekursiven Definition; zum Begriff rekursive Menge siehe entscheidbar. Als Rekursion (lat. recurrere „zurücklaufen“) bezeichnet man die Technik in Mathematik, Logik und Informatik, eine Funktion durch sich …   Deutsch Wikipedia

  • Rekursive Funktion — Dieser Artikel erläutert die Technik der rekursiven Definition; zum Begriff rekursive Menge siehe entscheidbar. Als Rekursion (lat. recurrere „zurücklaufen“) bezeichnet man die Technik in Mathematik, Logik und Informatik, eine Funktion durch sich …   Deutsch Wikipedia

  • Rekursivität — Dieser Artikel erläutert die Technik der rekursiven Definition; zum Begriff rekursive Menge siehe entscheidbar. Als Rekursion (lat. recurrere „zurücklaufen“) bezeichnet man die Technik in Mathematik, Logik und Informatik, eine Funktion durch sich …   Deutsch Wikipedia

  • Kleene — Stephen Cole Kleene (* 5. Januar 1909 in Hartford, Connecticut, USA; † 25. Januar 1994 in Madison, Wisconsin) war ein US amerikanischer Mathematiker und Logiker. Er gilt als einer der Begründer der theoretischen Informatik, besonders der formalen …   Deutsch Wikipedia