Der Rekursionssatz von Kleene - Kleene's recursion theorem

In der Berechenbarkeitstheorie sind Kleenes Rekursionssätze ein Paar grundlegender Ergebnisse über die Anwendung berechenbarer Funktionen auf ihre eigenen Beschreibungen. Die Sätze wurden erstmals 1938 von Stephen Kleene bewiesen und erscheinen 1952 in seinem Buch Introduction to Metamathematics . Ein verwandter Satz, der Fixpunkte einer berechenbaren Funktion konstruiert, ist als Satz von Rogers bekannt und geht auf Hartley Rogers, Jr. zurück .

Die Rekursionssätze können angewendet werden, um Fixpunkte bestimmter Operationen an berechenbaren Funktionen zu konstruieren , um Quine zu erzeugen und um durch rekursive Definitionen definierte Funktionen zu konstruieren .

Notation

Die Aussage der Theoreme bezieht sich auf eine zulässige Nummerierung der partiellen rekursiven Funktionen , so dass die dem Index entsprechende Funktion ist . ${\displaystyle\varphi}$${\displaystyle e}$${\displaystyle \varphi_{e}}$

Wenn und sind Teilfunktionen an den natürlichen Zahlen, die Schreibweise zeigt an, daß für jeden n entweder und sowohl definiert und gleich ist, oder aber auch , und sind beide nicht definiert. ${\displaystyle F}$${\displaystyle G}$${\displaystyle F\simeq G}$${\displaystyle F(n)}$${\displaystyle G(n)}$${\displaystyle F(n)}$${\displaystyle G(n)}$

Der Fixpunktsatz von Rogers

Bei einer gegebenen Funktion ist ein Fixpunkt von ein Index, so dass . Rogers beschreibt das folgende Ergebnis als "einfachere Version" von Kleenes (zweitem) Rekursionssatz. ${\displaystyle F}$${\displaystyle F}$${\displaystyle e}$${\displaystyle \varphi_{e}\simeq\varphi_{F(e)}}$

Der Fixpunktsatz von Rogers . Wenn eine total berechenbare Funktion ist, hat sie einen Fixpunkt.${\displaystyle F}$

Beweis des Fixpunktsatzes

Der Beweis verwendet eine bestimmte berechenbare Gesamtfunktion , die wie folgt definiert ist. Bei einer gegebenen natürlichen Zahl gibt die Funktion den Index der partiellen berechenbaren Funktion aus, die die folgende Berechnung durchführt: ${\displaystyle h}$${\displaystyle x}$${\displaystyle h}$

Wenn eine Eingabe gegeben ist , versuchen Sie zuerst zu berechnen . Wenn diese Berechnung eine Ausgabe zurückgibt , berechnen Sie den Wert und geben Sie ihn zurück, falls vorhanden.${\displaystyle y}$${\displaystyle \varphi_{x}(x)}$${\displaystyle e}$${\displaystyle \varphi_{e}(y)}$

Somit gilt für alle Indizes von partiellen berechenbaren Funktionen, wenn definiert ist, dann . Wenn nicht definiert ist, dann ist eine Funktion, die nirgendwo definiert ist. Die Funktion kann von der Teil berechenbare Funktion konstruiert werden oben beschrieben und das SMN - Theorem : für jeden , der Index eines Programms , das die Funktion berechnet . ${\displaystyle x}$${\displaystyle \varphi_{x}(x)}$${\displaystyle \varphi_{h(x)}\simeq\varphi_{\varphi_{x}(x)}}$${\displaystyle \varphi_{x}(x)}$${\displaystyle \varphi_{h(x)}}$${\displaystyle h}$${\displaystyle g(x,y)}$${\displaystyle x}$${\displaystyle h(x)}$${\displaystyle y\mapsto g(x,y)}$

Um den Beweis zu vervollständigen, sei eine beliebige total berechenbare Funktion und konstruiere wie oben. Sei ein Index der Zusammensetzung , die eine insgesamt berechenbare Funktion ist. Dann nach der Definition von . Aber weil ist ein Index von , , und somit . Durch die Transitivität von bedeutet dies . Daher für . ${\displaystyle F}$${\displaystyle h}$${\displaystyle e}$${\displaystyle F\circ h}$${\displaystyle \varphi_{h(e)}\simeq\varphi_{\varphi_{e}(e)}}$${\displaystyle h}$${\displaystyle e}$${\displaystyle F\circ h}$${\displaystyle \varphi_{e}(e)=(F\circ h)(e)}$${\displaystyle \varphi_{\varphi_{e}(e)}\simeq\varphi_{F(h(e))}}$${\displaystyle\simeq}$${\displaystyle \varphi_{h(e)}\simeq\varphi_{F(h(e))}}$${\displaystyle \varphi_{n}\simeq\varphi_{F(n)}}$${\displaystyle n=h(e)}$

Dieser Beweis ist eine Konstruktion einer partiellen rekursiven Funktion, die den Y-Kombinator implementiert .

Festpunktfreie Funktionen

Eine Funktion , so dass für alle heißt Festpunkt - frei . Der Fixpunktsatz zeigt, dass keine total berechenbare Funktion fixpunktfrei ist, aber es gibt viele nicht berechenbare fixpunktfreie Funktionen. Das Vollständigkeitskriterium von Arslanov besagt, dass der einzige rekursiv aufzählbare Turing-Grad , der eine festpunktfreie Funktion berechnet, 0′ ist , der Grad des Halteproblems . ${\displaystyle F}$${\displaystyle \varphi_{e}\not\simeq\varphi_{F(e)}}$${\displaystyle e}$

Kleenes zweiter Rekursionssatz

Der zweite Rekursionssatz ist eine Verallgemeinerung des Satzes von Rogers mit einer zweiten Eingabe in die Funktion. Eine informelle Interpretation des zweiten Rekursionssatzes ist, dass es möglich ist, selbstreferenzielle Programme zu konstruieren; siehe "Anwendung auf Quinen" unten.

Der zweite Rekursionssatz . Für jede partielle rekursive Funktion gibt es einen Index, so dass .${\displaystyle Q(x,y)}$${\displaystyle p}$${\displaystyle \varphi_{p}\simeq \lambda yQ(p,y)}$

Der Satz kann aus dem Satz von Rogers bewiesen werden, indem man eine Funktion so sein lässt, dass (eine durch den Satz von Smn beschriebene Konstruktion ). Man kann dann nach Bedarf überprüfen, ob ein Fixpunkt davon ein Index ist . Der Satz ist insofern konstruktiv, als eine feste berechenbare Funktion einen Index für Q in den Index p abbildet . ${\displaystyle F(p)}$${\displaystyle \varphi_{F(p)}(y)=Q(p,y)}$${\displaystyle F}$${\displaystyle p}$

Vergleich mit dem Satz von Rogers

Der zweite Rekursionssatz von Kleene und der Satz von Rogers können beide ziemlich einfach voneinander bewiesen werden. Ein direkter Beweis des Satzes von Kleene verwendet jedoch kein universelles Programm, was bedeutet, dass der Satz für bestimmte subrekursive Programmiersysteme gilt, die kein universelles Programm haben.

Anwendung auf Quinen

Ein klassisches Beispiel für den zweiten Rekursionssatz ist die Funktion . Der entsprechende Index ergibt in diesem Fall eine berechenbare Funktion, die bei Anwendung auf einen beliebigen Wert einen eigenen Index ausgibt. Als Computerprogramme ausgedrückt, werden solche Indizes als Quines bezeichnet . ${\displaystyle Q(x,y)=x}$${\displaystyle p}$

Das folgende Beispiel in Lisp veranschaulicht, wie das im Korollar effektiv aus der Funktion erzeugt werden kann . Die Funktion im Code ist die Funktion dieses Namens, die vom Smn-Theorem erzeugt wird . ${\displaystyle p}$${\displaystyle Q}$s11

Q kann in eine beliebige Zwei-Argument-Funktion geändert werden.

(setq Q '(lambda (x y) x))
(setq s11 '(lambda (f x) (list 'lambda '(y) (list f x 'y))))
(setq n (list 'lambda '(x y) (list Q (list s11 'x 'x) 'y)))
(setq p (eval (list s11 n n)))

Die Ergebnisse der folgenden Ausdrücke sollten gleich sein. ${\displaystyle\varphi}$ p(nil)

(eval (list p nil))

Q(p, nil)

(eval (list Q p nil))

Antrag auf Rekursionsbeseitigung

Angenommen, und sind insgesamt berechenbare Funktionen, die in einer rekursiven Definition für eine Funktion verwendet werden : ${\displaystyle g}$${\displaystyle h}$${\displaystyle f}$

${\displaystyle f(0,y)\simeq g(y),}$

${\displaystyle f(x+1,y)\simeq h(f(x,y),x,y),}$

Der zweite Rekursionssatz kann verwendet werden, um zu zeigen, dass solche Gleichungen eine berechenbare Funktion definieren, wobei der Begriff der Berechenbarkeit prima facie keine rekursiven Definitionen zulassen muss (z. B. kann er definiert werden durch μ-Rekursion oder durch Turing Maschinen ). Diese rekursive Definition kann in eine berechenbare Funktion umgewandelt werden , die davon ausgeht, dass sie ein Index für sich selbst ist, um eine Rekursion zu simulieren: ${\displaystyle \varphi_{F}(e,x,y)}$${\displaystyle e}$

${\displaystyle \varphi_{F}(e,0,y)\simeq g(y),}$

${\displaystyle \varphi_{F}(e,x+1,y)\simeq h(\varphi_{e}(x,y),x,y).}$

Der Rekursionssatz stellt die Existenz einer berechenbaren Funktion fest, so dass . Damit ist die gegebene rekursive Definition erfüllt. ${\displaystyle\varphi_{f}}$${\displaystyle\varphi_{f}(x,y)\simeq\varphi_{F}(f,x,y)}$${\displaystyle f}$

Reflexive Programmierung

Reflexive oder reflexive Programmierung bezieht sich auf die Verwendung von Selbstreferenz in Programmen. Jones präsentiert eine Ansicht des zweiten Rekursionssatzes basierend auf einer reflexiven Sprache. Es wird gezeigt, dass die definierte reflexive Sprache nicht stärker ist als eine Sprache ohne Reflexion (weil ein Dolmetscher für die reflexive Sprache ohne Reflexion implementiert werden kann); dann wird gezeigt, dass der Rekursionssatz in der reflexiven Sprache fast trivial ist.

Der erste Rekursionssatz

Während es beim zweiten Rekursionssatz um Fixpunkte berechenbarer Funktionen geht, bezieht sich der erste Rekursionssatz auf Fixpunkte, die durch Aufzählungsoperatoren bestimmt werden, die ein berechenbares Analogon induktiver Definitionen sind. Ein Aufzählungsoperator ist eine Menge von Paaren ( A , n ), wobei A eine ( Code für a) endliche Menge von Zahlen und n eine einzelne natürliche Zahl ist. Oft n wird als ein Code für ein geordnetes Paar von natürlichen Zahlen betrachtet werden, insbesondere , wenn Funktionen über Auszählung Operatoren definiert sind. Aufzählungsoperatoren sind von zentraler Bedeutung bei der Untersuchung der Aufzählungsreduzierbarkeit .

Jeder Aufzählungsoperator Φ bestimmt eine Funktion von Mengen von natürlichen Zahlen zu Mengen von natürlichen Zahlen gegeben durch

${\displaystyle \Phi(X)=\{n\mid \exists A\subseteq X[(A,n)\in\Phi]\}.}$

Ein rekursiver Operator ist ein Aufzählungsoperator, der bei gegebenem Graph einer partiell rekursiven Funktion immer den Graph einer partiell rekursiven Funktion zurückgibt.

Ein Fixpunkt eines Aufzählungsoperators Φ ist eine Menge F mit Φ( F ) = F . Der erste Aufzählungssatz zeigt, dass Fixpunkte effektiv erhalten werden können, wenn der Aufzählungsoperator selbst berechenbar ist.

Erster Rekursionssatz . Die folgenden Aussagen gelten.

1. Für jeden berechenbaren Aufzählungsoperator Φ gibt es eine rekursiv aufzählbare Menge F mit Φ( F ) = F und F ist die kleinste Menge mit dieser Eigenschaft.
2. Für jeden rekursiven Operator Ψ gibt es eine partielle berechenbare Funktion φ mit Ψ(φ) = φ und φ ist die kleinste partielle berechenbare Funktion mit dieser Eigenschaft.

Beispiel

Wie der zweite Rekursionssatz kann der erste Rekursionssatz verwendet werden, um Funktionen zu erhalten, die Systeme von Rekursionsgleichungen erfüllen. Um den ersten Rekursionssatz anzuwenden, müssen die Rekursionsgleichungen zunächst als rekursiver Operator umgeformt werden.

Betrachten wir die Rekursion Gleichungen für die faktorielle Funktion f :

${\displaystyle f(0)=1}$

${\displaystyle f(n+1)=(n+1)\cdot f(n)}$

Der entsprechende rekursive Operator Φ enthält Informationen, die angeben, wie man vom vorherigen Wert zum nächsten Wert von f gelangt . Der rekursive Operator wird jedoch tatsächlich den Graphen von f definieren . Zuerst enthält Φ das Paar . Dies zeigt an, dass f (0) eindeutig 1 ist und somit das Paar (0,1) im Graphen von f vorhanden ist . ${\displaystyle (\varnothing ,(0,1))}$

Als nächstes enthält für jedes n und m das Paar . Dies zeigt an, dass, wenn f ( n ) m ist , dann f ( n  +1) ( n  +1) m ist , so dass das Paar ( n  +1, ( n  +1) m ) im Graphen von f ist . Im Gegensatz zum Basisfall f (0) = 1 benötigt der rekursive Operator einige Informationen über f ( n ), bevor er einen Wert von f ( n  + 1) definiert. ${\displaystyle (\{(n,m)\},(n+1,(n+1)\cdot m))}$

Der erste Rekursionssatz (insbesondere Teil 1) besagt, dass es eine Menge F mit Φ( F ) = F gibt. Die Menge F besteht ausschließlich aus geordneten Paaren natürlicher Zahlen und ist der Graph der Fakultätsfunktion f , wie gewünscht.

Die Beschränkung auf Rekursionsgleichungen, die als rekursive Operatoren umformbar sind, stellt sicher, dass die Rekursionsgleichungen tatsächlich einen kleinsten Fixpunkt definieren. Betrachten Sie zum Beispiel den Satz von Rekursionsgleichungen:

${\displaystyle g(0)=1}$

${\displaystyle g(n+1)=1}$

${\displaystyle g(2n)=0}$

Es gibt keine Funktion g, die diese Gleichungen erfüllt, weil sie g (2) = 1 und auch g (2) = 0 implizieren . Somit gibt es keinen Fixpunkt g , der diese Rekursionsgleichungen erfüllt. Es ist möglich, einen Aufzählungsoperator entsprechend diesen Gleichungen zu erstellen, aber es wird kein rekursiver Operator sein.

Beweisskizze für den ersten Rekursionssatz

Den Beweis von Teil 1 des ersten Rekursionssatzes erhält man, indem man den Aufzählungsoperator Φ beginnend mit der leeren Menge iteriert. Zunächst wird eine Folge F _k konstruiert, z . Sei F ₀ die leere Menge. Ausgehend induktiv, für jedes k , lassen F _{k + 1} sein . Schließlich wird F angenommen als . Der Rest des Beweises besteht aus einem Nachweis, dass F rekursiv aufzählbar ist und der kleinste Fixpunkt von Φ ist. Die in diesem Beweis verwendete Folge F _k entspricht der Kleene-Kette im Beweis des Kleene-Fixpunktsatzes . ${\displaystyle k=0,1,\ldots}$${\displaystyle F_{k}\cup \Phi(F_{k})}$${\displaystyle \bigcup F_{k}}$

Der zweite Teil des ersten Rekursionssatzes folgt aus dem ersten Teil. Die Annahme, dass Φ ein rekursiver Operator ist, wird verwendet, um zu zeigen, dass der Fixpunkt von Φ der Graph einer Teilfunktion ist. Der entscheidende Punkt ist, dass, wenn der Fixpunkt F nicht der Graph einer Funktion ist, es einige k gibt, so dass F _k nicht der Graph einer Funktion ist.

Vergleich mit dem zweiten Rekursionssatz

Im Vergleich zum zweiten Rekursionssatz liefert der erste Rekursionssatz eine stärkere Schlussfolgerung, jedoch nur, wenn engere Hypothesen erfüllt sind. Rogers verwendet den Begriff des schwachen Rekursionssatzes für den ersten Rekursionssatz und den starken Rekursionssatz für den zweiten Rekursionssatz.

Ein Unterschied zwischen dem ersten und dem zweiten Rekursionstheorem besteht darin, dass die durch das erste Rekursionstheorem erhaltenen Fixpunkte garantiert die kleinsten Fixpunkte sind, während die aus dem zweiten Rekursionstheorem erhaltenen nicht kleinste Fixpunkte sein können.

Ein zweiter Unterschied besteht darin, dass der erste Rekursionssatz nur für Gleichungssysteme gilt, die als rekursive Operatoren umgeformt werden können. Diese Einschränkung ähnelt der Einschränkung auf stetige Operatoren im Kleene-Fixpunktsatz der Ordnungstheorie . Der zweite Rekursionssatz kann auf jede totalrekursive Funktion angewendet werden.

Verallgemeinerter Satz

Im Kontext seiner Numerierungstheorie zeigte Ershov , dass der Rekursionssatz von Kleene für jede prävollständige Numerierung gilt . Eine Gödel-Nummerierung ist eine vorvollständige Nummerierung der Menge berechenbarer Funktionen, so dass der verallgemeinerte Satz den Kleene-Rekursionssatz als Spezialfall liefert.

Bei einer vorvollständigen Nummerierung existiert dann für jede partielle berechenbare Funktion mit zwei Parametern eine total berechenbare Funktion mit einem Parameter, so dass ${\displaystyle \nu}$${\displaystyle f}$${\displaystyle t}$

${\displaystyle \forall n\in\mathbb{N} :\nu\circ f(n,t(n))=\nu\circ t(n).}$

Siehe auch

• Denotationssemantik , wobei ein anderer Satz der kleinsten Fixpunkte für den gleichen Zweck wie der erste Rekursionssatz verwendet wird.
• Festkomma-Kombinatoren , die in der Lambda-Kalküle für den gleichen Zweck wie der erste Rekursionssatz verwendet werden.

Verweise

• Ershov, Yuri L. (1999). „Teil 4: Mathematik und Berechenbarkeitstheorie. 14. Theorie der Numerierung“. In Griffor, Edward R. (Hrsg.). Handbuch der Berechenbarkeitstheorie . Studium der Logik und der Grundlagen der Mathematik. 140 . Amsterdam: Sonst . S. 473–503. ISBN 9780444898821. OCLC  162130533 . Abgerufen am 6. Mai 2020 .
• Jones, Neil D. (1997). Berechenbarkeit und Komplexität: Aus Programmierperspektive . Cambridge, Massachusetts : MIT-Presse . ISBN 9780262100649. OCLC  981293265 .
• Kleene, Stephen C. (1952). Einführung in die Metamathematik . Bibliotheca Mathematica. Nordholland Publishing . ISBN 9780720421033. OCLC-  459805591 . Abgerufen am 6. Mai 2020 .
• Rogers, Hartley (1967). Theorie rekursiver Funktionen und effektive Berechenbarkeit . Cambridge, Massachusetts : MIT-Presse . ISBN 9780262680523. OCLC  933975989 . Abgerufen am 6. Mai 2020 .

Fußnoten

Weiterlesen

• Jockusch, CG ; Lermann, M.; Soare, RI ; Solovay, RM (1989). "Rekursiv aufzählbare Mengen modulo iterierte Sprünge und Erweiterungen von Arslanovs Vollständigkeitskriterium". Die Zeitschrift für symbolische Logik . 54 (4): 1288–1323. doi : 10.1017/S0022481200041104 . ISSN  0022-4812 . JSTOR  2274816 .

Externe Links

• "Recursive Functions" -Eintrag von Piergiorgio Odifreddi in der Stanford Encyclopedia of Philosophy , 2012.