Fixpunktsatz von Kleene

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.

Inhaltsverzeichnis

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

Wikimedia Foundation.

Игры ⚽ Нужна курсовая?

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

  • Fixpunktsatz — Ein Fixpunktsatz ist in der Mathematik ein Satz, der einem unter gewissen Voraussetzungen die Existenz von Fixpunkten einer Abbildung garantiert. Das heißt der Satz garantiert die Existenz eines Punktes mit . Inhaltsverzeichnis 1 Überblick …   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

  • Stephen 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

  • Stephen Cole Kleene — (* 5. Januar 1909 in Hartford, Connecticut; † 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 Sprachen und der… …   Deutsch Wikipedia

  • Liste von Sätzen der Informatik — Inhaltsverzeichnis A B C D E F G H I J K L M N O P Q R S T U V W X Y Z C Satz von Cook: Es existiert eine Teilmenge von …   Deutsch Wikipedia

  • Liste mathematischer Sätze — Inhaltsverzeichnis A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A Satz von Abel Ruffini: eine allgemeine Polynomgleichung vom …   Deutsch Wikipedia

  • Quine (Computerprogramm) — Ein Quine ist ein Computerprogramm, das eine Kopie seiner selbst (üblicherweise seines Quelltextes) als Ausgabe schreibt. Es handelt sich somit um eine Form der Selbstbezüglichkeit. Hacker und Geeks sehen es als sportliche Herausforderung, die… …   Deutsch Wikipedia

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

  • L.E.J. Brouwer — Luitzen E. J. Brouwer (* 27. Februar 1881 in Overschie; † 2. Dezember 1966 in Blaricum) war ein niederländischer Mathematiker. Er schuf grundlegende topologische Methoden und Begriffe und bewies bedeutende topologische Sätze. Nach ihm ist der… …   Deutsch Wikipedia

  • L. E. J. Brouwer — Luitzen E. J. Brouwer (* 27. Februar 1881 in Overschie; † 2. Dezember 1966 in Blaricum) war ein niederländischer Mathematiker. Er schuf grundlegende topologische Methoden und Begriffe und bewies bedeutende topologische Sätze. Nach ihm ist der… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”