In der Berechenbarkeitstheorie stellt der Lehrsatz von Rice fest, dass, für jedes nichttriviale Eigentum von teilweisen Funktionen, es keine allgemeine und wirksame Methode gibt zu entscheiden, ob ein Algorithmus eine teilweise Funktion mit diesem Eigentum schätzt. Hier wird ein Eigentum von teilweisen Funktionen trivial genannt, wenn es für alle teilweisen berechenbaren Funktionen oder für niemanden hält, und eine wirksame Entscheidungsmethode allgemein genannt wird, wenn es richtig für jeden Algorithmus entscheidet.

Der Lehrsatz wird nach Henry Gordon Rice genannt, und ist auch bekannt als der Lehrsatz von Rice-Myhill-Shapiro nach Rice, John Myhill und Norman Shapiro.

Einführung

Eine andere Weise, den Lehrsatz von Rice festzusetzen, der in der Berechenbarkeitstheorie nützlicher ist, folgt.

Lassen Sie S eine Reihe von Sprachen sein, der nichttrivial ist, bedeutend

1. dort besteht eine Maschine von Turing, die eine Sprache in S anerkennt
2. dort besteht eine Maschine von Turing, die eine Sprache nicht in S anerkennt

Dann ist es unentscheidbar, um zu bestimmen, ob die durch eine willkürliche Maschine von Turing entschiedene Sprache in S. liegt

In der Praxis bedeutet das, dass es keine Maschine gibt, die immer entscheiden kann, ob die Sprache einer gegebenen Maschine von Turing ein besonderes nichttriviales Eigentum hat. Spezielle Fälle schließen die Unentscheidbarkeit dessen ein, ob eine Maschine von Turing eine besondere Schnur akzeptiert, ob eine Maschine von Turing eine besondere erkennbare Sprache anerkennt, und ob die durch eine Maschine von Turing anerkannte Sprache durch eine nichttriviale einfachere Maschine wie ein begrenzter Automat anerkannt werden konnte.

Es ist wichtig zu bemerken, dass der Lehrsatz von Rice nichts über jene Eigenschaften von Maschinen oder Programmen sagt, die nicht auch Eigenschaften von Funktionen und Sprachen sind. Zum Beispiel, ob Maschinenläufe für mehr als 100 Schritte auf einem Eingang ein entscheidbares Eigentum sind, wenn auch es nichttrivial ist. Als sie genau dieselbe Sprache durchgeführt haben, könnten zwei verschiedene Maschinen eine verschiedene Zahl von Schritten verlangen, denselben Eingang anzuerkennen. Ähnlich, ob eine Maschine mehr als 5 Staaten hat, ist ein entscheidbares Eigentum. Wo ein Eigentum der Art ist, die entweder der zwei Maschinen kann oder es nicht haben kann, durch das stille Einführen genau derselben Sprache, das Eigentum der Maschinen und nicht der Sprache ist, und der Lehrsatz von Rice nicht gilt.

Mit der Charakterisierung von Rogers von annehmbaren Programmiersystemen kann der Lehrsatz von Reis im Wesentlichen von Maschinen von Turing bis die meisten Computerprogrammiersprachen verallgemeinert werden: Dort besteht keine automatische Methode, die mit der Allgemeinheit nichttriviale Fragen auf dem Verhalten des schwarzen Kastens von Computerprogrammen entscheidet.

Als ein Beispiel, denken Sie die folgende Variante des stockenden Problems. Lassen Sie P das folgende Eigentum von teilweisen Funktionen F eines Arguments sein: P bedeutet (F), dass F für das Argument '1' definiert wird. Es ist offensichtlich nichttrivial, da es teilweise Funktionen gibt, die an 1 definiert werden und andere, die an 1 unbestimmt sind. Das 1-Halt-Problem ist das Problem des Entscheidens jedes Algorithmus, ob es eine Funktion mit diesem Eigentum, definiert

d. h. ob der Algorithmus auf dem Eingang 1 hinkt. Durch den Lehrsatz von Reis ist das 1-Halt-Problem unentscheidbar. Ähnlich ist die Frage dessen, ob eine Maschine von Turing T auf einem am Anfang leeren Band endet (aber nicht mit einem anfänglichen Wort w gegeben als das zweite Argument zusätzlich zu einer Beschreibung von T, als im vollen stockenden Problem) noch unentscheidbar.

Formelle Behauptung

Lassen Sie, der berechenbaren Funktionen numerierender Gödel zu sein; eine Karte von den natürlichen Zahlen bis die Klasse von unären (teilweisen) berechenbaren Funktionen.

Zeigen Sie durch den th (teilweise) berechenbare Funktion an.

Wir identifizieren jedes Eigentum, das eine berechenbare Funktion mit der Teilmenge haben kann, aus den Funktionen mit diesem Eigentum zu bestehen.

So in Anbetracht eines Satzes hat eine berechenbare Funktion Eigentum F wenn und nur wenn. Für jedes Eigentum gibt es ein verbundenes Entscheidungsproblem der Bestimmung, gegeben e, ob.

Der Lehrsatz von Reis stellt fest, dass das Entscheidungsproblem entscheidbar ist (auch hat rekursiv oder berechenbar genannt), wenn und nur wenn oder.

Beispiele

Gemäß dem Lehrsatz von Reis, wenn es mindestens eine berechenbare Funktion in einer besonderen Klasse C von berechenbaren Funktionen und einer anderen berechenbaren Funktion nicht in C dann das Problem des Entscheidens gibt, ob ein besonderes Programm eine Funktion in C schätzt, ist unentscheidbar. Zum Beispiel zeigt der Lehrsatz von Reis, dass jeder der folgenden Sätze von berechenbaren Funktionen unentscheidbar ist:

• Die Klasse von berechenbaren Funktionen, die 0 für jeden Eingang und seine Ergänzung zurückkehren.
• Die Klasse von berechenbaren Funktionen, die 0 für mindestens einen Eingang und seine Ergänzung zurückkehren.
• Die Klasse von berechenbaren Funktionen, die, und seine Ergänzung unveränderlich sind.

Beweis durch den recursion Lehrsatz von Kleene

Eine Folgeerscheinung zum recursion Lehrsatz von Kleene stellt fest, dass für jeden Gödel, der der berechenbaren Funktionen und jeder berechenbaren Funktion numeriert, es einen solchen Index dass Umsatz gibt. (Im folgenden werden wir sagen, dass "Umsatz", wenn entweder, oder beide und unbestimmt sind.) Intuitiv, ist ein quine, eine Funktion, die seinen eigenen Quellcode (Zahl von Gödel) zurückgibt, außer dass man es anstatt direkt zurückgibt, passiert seine Zahl von Gödel dazu und gibt das Ergebnis zurück.

Lassen Sie, eine Reihe berechenbarer solcher Funktionen dass zu sein. Dann gibt es berechenbare Funktionen und. Nehmen Sie an, dass der Satz von solchen Indizes, der entscheidbar ist; dann, dort besteht eine Funktion, die wenn, und sonst zurückkehrt. Durch die Folgeerscheinung zum recursion Lehrsatz gibt es einen solchen Index dass Umsatz. Aber dann, wenn, dann dieselbe Funktion wie, und deshalb ist; und wenn, dann, und deshalb ist. In beiden Fällen haben wir einen Widerspruch.

Beweis durch die Verminderung vom stockenden Problem

Probeskizze

Nehmen Sie für die Greifbarkeit an, dass wir einen Algorithmus haben, für ein Programm p zu untersuchen und unfehlbar zu bestimmen, ob p eine Durchführung der Quadrieren-Funktion ist, die eine ganze Zahl d nimmt und d zurückgibt. Der Beweis arbeitet genauso gut, wenn wir einen Algorithmus haben, um ein anderes nichttriviales Eigentum von Programmen zu entscheiden, und im Allgemeinen unten gegeben werden.

Der Anspruch besteht darin, dass wir unseren Algorithmus umwandeln können, um Quadrieren-Programme in dasjenige zu identifizieren, das Funktionen dieser Halt identifiziert. Wir werden einen Algorithmus beschreiben, der Eingänge a und ich nimmt und ob Programm Halte, wenn gegeben, eingegeben i bestimmt.

Der Algorithmus, um das zu entscheiden, ist begrifflich einfach: Es baut (die Beschreibung) ein neues Programm t, das ein Argument n nimmt, der (1) erst Programm a auf dem Eingang i (sowohl a als auch ich durchführt, in die Definition von t hart codiert werden), und (2) dann Umsatz das Quadrat von n. Wenn (i) Läufe für immer, dann wird t zum Schritt (2) unabhängig von n nie kommen. Dann klar ist t eine Funktion für Rechenquadrate, wenn, und nur wenn Schritt (1) endet. Seitdem wir angenommen haben, dass wir Programme für Rechenquadrate unfehlbar identifizieren können, können wir bestimmen, ob t, der von a und mir abhängt, solch ein Programm und das für jeden a und mich ist; so haben wir ein Programm erhalten, das ob Programm Halte auf dem Eingang i entscheidet. Bemerken Sie, dass unser Algorithmus der stockenden Entscheidung nie t durchführt, aber nur seine Beschreibung zum Programm der Quadrieren-Identifizierung passiert, das durch die Annahme immer endet; da der Aufbau der Beschreibung von t auch in einem Weg getan werden kann, der immer endet, kann die stockende Entscheidung nicht scheitern, auch zu hinken.

Halte (a, i) {

definieren Sie t (n) {\

(ich)

kehren Sie n×n zurück

}\

geben Sie is_a_squaring_function (t) zurück

}\

Diese Methode hängt spezifisch vom im Stande Sein nicht ab, Funktionen anzuerkennen, die Quadrate schätzen; nicht weniger als kann ein Programm tun, was wir versuchen anzuerkennen, können wir einen Anruf hinzufügen, um unseren t zu erhalten. Wir könnten eine Methode gehabt haben, um Programme anzuerkennen, um Quadratwurzeln oder Programme zu schätzen, für die Monatslohnliste oder Programme zu schätzen, die, wenn gegeben, den Eingang oder Programme halten, die Reihe-Grenze-Fehler begehen; in jedem Fall würden wir im Stande sein, das stockende Problem ähnlich zu beheben.

Formeller Beweis

Für den formellen Beweis, wie man wagt, definieren Algorithmen teilweise Funktionen über Schnuren und werden selbst durch Schnuren vertreten. Die teilweise Funktion, die durch den Algorithmus geschätzt ist, der durch eine Schnur vertreten ist von angezeigtem F zu sein. Dieser Beweis geht durch die reductio Anzeige absurdum weiter: Wir nehmen an, dass es ein nichttriviales Eigentum gibt, das durch einen Algorithmus entschieden wird, und dann zeigen Sie dass, hieraus folgt dass wir das stockende Problem entscheiden können, das, und deshalb ein Widerspruch nicht möglich ist.

Lassen Sie uns jetzt annehmen, dass P (a) ein Algorithmus ist, der ein nichttriviales Eigentum von F entscheidet. Ohne Verlust von

Allgemeinheit wir können annehmen, dass P (ohne Halte) = "nein", mit dem ohne Halte, der die Darstellung eines Algorithmus ist, der nie hinkt. Wenn das nicht wahr ist, dann wird das für die Ablehnung des Eigentums halten. Da P ein nichttriviales Eigentum entscheidet, hieraus folgt dass es eine Schnur b gibt, der einen Algorithmus und P (b) = "ja" vertritt. Wir können dann einen Algorithmus H (a, i) wie folgt definieren:

:1. bauen Sie eine Schnur t, der einen Algorithmus T (j) solch dass vertritt

:* T täuscht zuerst die Berechnung von F (ich) vor

:* dann täuscht T die Berechnung von F (j) vor und gibt sein Ergebnis zurück.

:2. geben Sie P (t) zurück.

Wir können jetzt zeigen, dass H das stockende Problem entscheidet:

• Nehmen Sie dass der Algorithmus an, der durch Halte auf dem Eingang i vertreten ist. In diesem Fall F = F und, weil P (b) = "ja" und die Produktion von P (x) nur von F, hieraus folgt dass P (t) = "ja" und, deshalb H (a, i) = "ja" abhängt.
• Nehmen Sie an, dass der Algorithmus, der durch einen nicht vertreten ist, auf dem Eingang i hinkt. In diesem Fall F = F, d. h., die teilweise Funktion, die nie definiert wird. Seitdem P (ohne Halte) = hängen "nein" und die Produktion von P (x) nur von F, hieraus folgt dass P (t) = "nein" und, deshalb H (a, i) = "nein" ab.

Da, wie man bekannt, das stockende Problem unentscheidbar ist, ist das ein Widerspruch und die Annahme, dass es einen Algorithmus P (a) gibt, der ein nichttriviales Eigentum für die durch ein Müssen vertretene Funktion entscheidet, falsch zu sein.

Der Lehrsatz von Reis und Index-Sätze

Der Lehrsatz von Reis kann in Bezug auf Index-Sätze kurz und bündig festgesetzt werden:

:

wo der Satz von natürlichen Zahlen einschließlich der Null ist.

Eine Entsprechung des Lehrsatzes von Rice für rekursive Sätze

Man kann den Lehrsatz von Rice als das Erklären betrachten, dass die Unmöglichkeit des wirksamen Entscheidens für irgendwelchen rekursiv enumerable gesetzt

hat

ob es ein bestimmtes nichttriviales Eigentum hat.

In dieser Abteilung geben wir eine Entsprechung des Lehrsatzes von Rice für rekursive Sätze, statt rekursiv enumerable Sätze.

Grob sprechend, sagt die Entsprechung dass, wenn man für einen rekursiven Satz effektiv bestimmen kann, ob es ein bestimmtes Eigentum, hat

dann begrenzt bestimmen viele ganze Zahlen, ob ein rekursiver Satz das Eigentum hat.

Dieses Ergebnis ist dem Lehrsatz des ursprünglichen Rices analog, weil beide behaupten, dass ein Eigentum "entscheidbarer" ist

nur wenn man bestimmen kann, ob ein Satz dieses Eigentum durch das Überprüfen für höchstens begrenzt viele hat

(für nein, für den ursprünglichen Lehrsatz), wenn dem Satz gehört.

Lassen Sie, eine Klasse zu sein (hat ein einfaches Spiel genannt und hat als ein Eigentum gedacht) rekursiver Sätze.

Wenn ein rekursiver Satz, dann für einige, berechenbare Funktion ist

ist die charakteristische Funktion dessen. Wir nennen einen charakteristischen Index danach.

(Es gibt ungeheuer viele solcher.)

Wollen wir sagen, dass die Klasse berechenbar ist, wenn es einen Algorithmus gibt (berechenbare Funktion), der entscheidet

für jede natürliche Zahl (nicht notwendigerweise ein charakteristischer Index),

• wenn ein charakteristischer Index für einen rekursiven Satz ist, der dem gehört, dann gibt der Algorithmus "ja";
• wenn ein charakteristischer Index für einen rekursiven Satz ist, der nicht dem gehört, dann gibt der Algorithmus "nein".

Ein Satz erweitert eine Reihe von 0's und 1's

wenn für irgendwelchen

das th Element dessen ist 1 wenn; ist 0 sonst.

Zum Beispiel, erweitert Schnur.

Eine Schnur gewinnt Bestimmung, wenn ein rekursives Satz-Verlängern dem gehört.

Eine Schnur verliert Bestimmung, wenn kein rekursives Satz-Verlängern dem gehört.

Wir können jetzt die folgende Entsprechung des Lehrsatzes von Rice festsetzen

(Kreisel, Lacombe und Shoeneld, 1959,

Kumabe und Mihara, 2008):

Eine Klasse von rekursiven Sätzen ist berechenbarer

wenn, und nur wenn es rekursiv enumerable Satz gibt, Bestimmung von Schnuren zu verlieren

und rekursiv enumerable Satz, Bestimmung von solchen Schnuren dass zu gewinnen

jeder rekursive Satz erweitert eine Schnur darin.

Dieses Ergebnis ist auf foundational Probleme in der rechenbetonten sozialen Wahl (weit gehender, algorithmische Spieltheorie) angewandt worden.

Zum Beispiel, Kumabe und Mihara (2008, 2008)

wenden Sie dieses Ergebnis auf eine Untersuchung der Zahlen von Nakamura für einfache Spiele in der kooperativen Spieltheorie und sozialen auserlesenen Theorie an.

Siehe auch

• Die Unvollständigkeitslehrsätze von Gödel
• Stockendes Problem
• Lehrsatz von Rice-Shapiro
• Theorie von Recursion

Referenzen

.

• Reis, H. G. "Klassen von Rekursiv Enumerable Sätzen und Ihren Entscheidungsproblemen." Trans. Amer. Mathematik. Soc. 74, 358-366, 1953.

.

Links