Rekursionssatz

Überblick

Die Rekursionssätze sind drei formal äquivalente Resultate der Berechenbarkeitstheorie von Kleene, Rogers und Case. Sie beschreiben Selbstbezüglichkeit berechenbarer Funktionen: Natürliche Zahlen können zugleich Codierungen von Programm-Quelltexten und Eingaben von Funktionen sein. Dadurch lassen sich Programme konstruieren, die ihre eigene Codierung in Berechnungen verwenden.

Alle drei Sätze folgen aus dem Smn-Theorem von Kleene. Sie sind wichtig, weil sie die Existenz bestimmter berechenbarer Funktionen oder Programme beweisen und auch Widersprüche zur Annahme einer Berechenbarkeit herleiten können.

Kleenes Rekursionssatz

Sei \{\varphi_p\}_{p\in\mathbb N} eine effektive Nummerierung aller partiell berechenbaren Funktionen, etwa durch Gödel-Nummern deterministischer Turing-Maschinen.

In der nicht-konstruktiven Fassung gilt: Für jede partiell berechenbare Funktion f\in\mathcal P gibt es einen Index e\in\mathbb N mit \forall x\in\mathbb N:\ \varphi_e(x)=f(e;x). Das Programm mit Index e führt also eine Berechnung aus, die seinen eigenen Index verwendet.

Die konstruktive Fassung ist stärker: Es gibt eine total berechenbare, streng monoton wachsende Funktion e\in\mathcal R, sodass \forall p,x\in\mathbb N:\ \varphi_{e(p)}(x)=\varphi_p(e(p);x). Aus einem Index p für die gewünschte Berechnung kann die Codierung e(p) eines passenden selbstreferenziellen Programms effektiv bestimmt werden. Die nicht-konstruktive Fassung folgt durch f=\varphi_p.

Semantische Fixpunkte

Der Fixpunktsatz von Kleene, häufig auch Rogers' fixed-point theorem genannt, besagt für jede total berechenbare Funktion f\in\mathcal R: Es gibt einen Index e\in\mathbb N, für den \forall x\in\mathbb N:\ \varphi_e(x)=\varphi_{f(e)}(x).

f beschreibt dabei eine Quelltext-Manipulation. Obwohl sie den Index beziehungsweise Quelltext verändert, berechnet das ursprüngliche Programm e dieselbe Funktion wie das manipulierte Programm f(e). Daher heißt e ein semantischer Fixpunkt einer syntaktischen Programmtransformation. Für jede Modifikation gibt es sogar unendlich viele solcher Fixpunkte.

Auch für partielles f\in\mathcal P gibt es eine konstruktive Verallgemeinerung, wenn \varphi_{f(e)}=\bot gesetzt wird, falls f(e)=\bot. Dann existiert eine total berechenbare, streng monoton wachsende Funktion e\in\mathcal R mit \forall p,x\in\mathbb N:\ \varphi_{e(p)}(x)=\varphi_{\varphi_p(e(p))}(x).

Operator-Rekursion

Der Operator-Rekursionssatz von John Case (1974) behandelt berechenbare Operatoren. Ein Operator ist eine durch eine Turing-Maschine realisierte Abbildung \Theta:(\mathbb N\rightsquigarrow\mathbb N)\to(\mathbb N\rightsquigarrow\mathbb N) zwischen partiellen, nicht unbedingt berechenbaren Funktionen.

Für jeden berechenbaren Operator \Theta existiert eine total berechenbare, streng monoton wachsende Funktion e\in\mathcal R, sodass \forall p,x\in\mathbb N:\ \varphi_{e(p)}(x)=\Theta(e)(p;x). Im Unterschied zu Kleenes Fassung entstehen nicht nur ein selbstreferenzieller Index, sondern unendlich viele Gödel-Nummern e(p), die sich bildlich gesprochen selbst und die anderen Indizes berücksichtigen. Der Satz arbeitet direkt auf der Ebene berechenbarer Funktionen, ist aber ebenfalls äquivalent zum Rekursionssatz von Kleene.

Anwendungen und Beispiele

Rekursionssätze dienen in der Berechenbarkeitstheorie und algorithmischen Lerntheorie als Hilfssätze, besonders für Existenzbeweise und Gegenbeispiele.

Ein Beispiel ist ein Quine, also ein Programm, das seinen eigenen Quelltext ausgibt. Dazu kann man die Modifikatorfunktion definieren als:

f(x):\ \text{return "return " + x}

Ein Fixpunkt dieser Funktion ist ein Quine.

Die Sätze können auch Nicht-Berechenbarkeit zeigen. Für das Halteproblem H=\{(p;x)\mid\varphi_p(x)\downarrow\} nimmt man an, es sei entscheidbar. Dann wäre sein Komplement rekursiv aufzählbar: Es gäbe eine partiell berechenbare Funktion f, die für (p;x) genau dann hält, wenn \varphi_p(x)\uparrow nicht hält. Der Rekursionssatz liefert ein e mit \varphi_e(x)=f(e;x). Damit folgt \varphi_e(x)\uparrow\Leftrightarrow f(e;x)\downarrow\Leftrightarrow\varphi_e(x)\downarrow, ein Widerspruch. Somit ist das Halteproblem unentscheidbar.