Algorithmus zur Lösung von Turings "Halting Problem"

23

"Alan Turing hat 1936 bewiesen, dass ein allgemeiner Algorithmus zur Lösung des Halteproblems für alle möglichen Programm-Eingabe-Paare nicht existieren kann."

Kann ich einen allgemeinen Algorithmus finden, um das Halteproblem für einige mögliche Programmeingabepaare zu lösen ?

Kann ich eine Programmiersprache (oder Sprachen) finden, in der ich für jede Art von Programm in dieser Sprache entscheiden kann, ob das Programm beendet wird oder für immer ausgeführt wird?

Kaveh
quelle
3
CACM hatte im Mai einen sehr interessanten Artikel: Proving Program Termination
Christoph Walesch
3
"Ein allgemeiner Algorithmus [...] für einige mögliche Programmeingabepaare" - das ist fast widersprüchlich. Ich nehme an, Sie möchten sich auf eine unendliche Unterklasse aller Programme beschränken?
Raphael

Antworten:

25

Kann ich einen allgemeinen Algorithmus finden, um das Halteproblem für einige mögliche Programmeingabepaare zu lösen?

Ja sicher. Sie könnten beispielsweise einen Algorithmus schreiben, der für jedes Programm, das weder Schleifen noch Rekursionen enthält, "Ja, es wird beendet" und für jedes Programm, das eine while(true)Schleife enthält , die definitiv erreicht wird und keine enthält, "Nein, es wird nicht beendet" eine break-Anweisung und "Dunno" für alles andere.

Kann ich eine Programmiersprache (oder Sprachen) finden, in der ich für jede Art von Programm in dieser Sprache entscheiden kann, ob das Programm beendet wird oder für immer ausgeführt wird?

Nicht wenn diese Sprache Turing-vollständig ist, nein.

Es gibt jedoch vollständige Nicht-Turing-Sprachen wie zum Beispiel Coq , Agda oder Microsoft Dafny, für die das Problem des Anhaltens entschieden werden kann (und in der Tat von den jeweiligen Typsystemen bestimmt wird, wodurch sie zu Gesamtsprachen werden (dh ein Programm, das möglicherweise nicht beendet wird, wird dies nicht tun) kompilieren)).

sepp2k
quelle
1
Die Klasse der primitiv-rekursiven Funktionen ist eine bekannte "Programmiersprache", für die das Halteproblem trivial entscheidbar ist.
Raphael
Es gibt mehrere " Total Functional Programming " -Sprachen, in denen nachweislich alle Programme enden.
Anderson Green
3

Ich denke, alle Antworten hier sind vollständig und verfehlen den Punkt. Die Antwort auf die Frage lautet: Unter der Annahme, dass das Programm anhalten soll, sollten Sie in der Lage sein, anzuzeigen, dass es anhält. Wenn Sie nicht zeigen können, dass es leicht stoppt, sollte das Programm als sehr schlecht geschrieben und von der Qualitätskontrolle als solches abgelehnt angesehen werden.

Ob Sie tatsächlich einen geeigneten Maschinenalgorithmus schreiben können, hängt von der eingegebenen Programmiersprache ab und davon, wie ehrgeizig Sie sind. Es ist ein vernünftiges Entwurfsziel für eine Programmiersprache, die Beendigung leicht nachweisen zu können.

Wenn die Sprache C ++ ist, können Sie das Tool wahrscheinlich nicht schreiben, in der Tat ist es unwahrscheinlich, dass Sie jemals den Parser zum Laufen bringen, geschweige denn die Kündigung beweisen. Für eine besser strukturierte Sprache sollten Sie in der Lage sein, einen Beweis zu erstellen, oder zumindest mit bestimmten Annahmen: Im letzteren Fall sollte das Tool diese Annahmen ausgeben. Ein ähnlicher Ansatz wäre, Abschlusszusagen in die Sprache aufzunehmen und in komplexen Situationen zu verwenden, in denen das Tool den Zusagen vertraut.

Die Quintessenz ist, dass niemand zu verstehen scheint, dass der Beweis, dass ein Programm anhält, in der Tat möglich ist, weil (gute) Programmierer, die beabsichtigen, solche anhaltenden Programme zu schreiben, dies immer absichtlich und mit einem mentalen Bild davon tun, warum sie abbrechen und richtig handeln: Ein solcher Code ist absichtlich geschrieben, so ist es klar, dass sie anhalten und korrekt sind und wenn ein vernünftiger Algorithmus dies nicht beweisen kann, möglicherweise mit einigen Hinweisen, dann sollte das Programm abgelehnt werden.

Der Punkt: Programmierer schreiben keine willkürlichen Programme, so dass die These des Haltesatzes nicht erfüllt ist und die Schlussfolgerung nicht zutrifft.

Yttrill
quelle
4
Ich denke, Sie haben den Punkt völlig und gänzlich verpasst. Der erste Absatz Ihrer Antwort gilt nicht für die Frage, weil sie nach Algorithmen fragt - nicht danach, was ein Mensch beweisen kann oder nicht. Der Rest der Antwort beantwortet den ersten Absatz der Frage, dh ob ein Algorithmus die Beendigung für einige Programme nachweisen könnte. Alle vorherigen Antworten haben bereits zu dieser Frage mit "Ja" geantwortet.
SEPP2K
3
Ihre Behauptung, dass es möglich ist, einen Algorithmus zu schreiben, der die Beendigung jedes gut geschriebenen Programms in einer ausreichend einfachen Turing-vollständigen Sprache beweist, ist einfach völlig falsch. Für jeden möglichen Algorithmus, der versucht, die Beendigung zu prüfen, gibt es Probleme, bei denen nicht nachgewiesen werden kann, dass jedes Programm, das dieses Problem löst, durch diesen Algorithmus angehalten wird. Wenn Sie also nicht sagen, dass jedes Programm, das dieses Problem löst, per Definition schlecht geschrieben ist (was lächerlich wäre), widerlegt dies Ihren Standpunkt.
20.
1
@Sam Wenn mich jemand fragt, ob ein Code anhält, schaue ich mir den Code an und versuche, es herauszufinden. Aber ich bin kein Algorithmus. Und ja, es ist möglich, einen Algorithmus zu schreiben, der überprüft, ob ein Programm für viele Programme anhält. Aber das hat Yttrill nicht gesagt. Yttrill sagte, dass es für alle gut geschriebenen Programme möglich ist. Und wie ich in meinem vorherigen Kommentar sagte, ist das einfach falsch, es sei denn, Sie behaupten, dass bestimmte Probleme nur durch schlecht geschriebene Programme gelöst werden können (was wiederum lächerlich wäre).
3.
1
@Sam "Es erscheint mir unkompliziert, dass Programme, die absichtlich zum Anhalten geschrieben wurden, leicht auf Anhaltebedingungen analysiert werden können" - wenn dies der Fall wäre, warum haben wir dann keine solchen Tools? Es ist nicht so, als würden die Leute es nicht versuchen. (Ein Täter ist das Überschreiben von Methoden:
Raphael
1
@Sam "Gibt es eine Endlosschleife?" Ist eine schwierige Sache, auch für reale Schleifen. Natürlich wurde mir beigebracht, wie man Schleifeninvarianten findet, aber das bedeutet nicht, dass ich in vielen Fällen eine (leicht) finden kann. Nach meinem Kenntnisstand ist erraten & beweisen heutzutage der Goldstandard. Noch einmal, wenn es waren ziemlich allgemeine Algorithmen, würde ich erwarten , dass sie in großen compiliert oder IDEs aufgenommen werden (was tun einige trivial, syntaktische Überprüfungen durchführen). Können Sie auf einen einigermaßen starken Algorithmus verweisen?
Raphael
3

ausgezeichnete und (wahrscheinlich ungewollt tiefe) Frage. Es gibt in der Tat Programme zur Erkennung von Unterbrechungen, die bei einer begrenzten Anzahl von Eingaben erfolgreich sein können. Es ist ein aktives Forschungsgebiet. es ist sehr eng mit (automatisierten) Theoremprüfbereichen verbunden.

Die Informatik scheint jedoch keinen genauen Begriff für "Programme" zu haben, die "manchmal" erfolgreich sind. Das Wort "Algorithmus" ist normalerweise für Programme reserviert, die immer anhalten.

Das Konzept scheint sich deutlich von probabilistischen Algorithmen zu unterscheiden, bei denen CS-Theoretiker darauf bestehen, dass eine bekannte oder berechenbare Wahrscheinlichkeit für ihren Erfolg besteht.

Es gibt einen Begriff Semialgorithmen , der manchmal verwendet wird, aber anscheinend ein Synonym für rekursiv aufzählbar oder nicht berechenbar ist.

Nennen Sie sie hier also Quasialgorithmen . Das Konzept ist anders als entscheidbar oder unentscheidbar.

AXBYXYXYBA

in CS scheint diese "Quasi-Algorithmus-Hierarchie" bislang meist nur informell untersucht worden zu sein.

es zeigt sich in der fleißigen Biberforschung [1] und dem PCP-Problem [2]. Tatsächlich kann ein DNA-basierter Angriff auf PCP als quasialer Algorithmus angesehen werden. [3] und es ist in anderen Bereichen zu sehen, die bereits erwähnt wurden, wie der Beweis des Theorems [4].

[1] New Millenium Attack auf das Problem der beschäftigten Biber

[2] Korrespondenzprobleme bei der Bekämpfung von Posts von Zhao (v2?)

[3] Verwenden von DNA zur Lösung des Bounded-Post-Correspondence-Problems von Kari et al

[4] Beweisen der Programmbeendigung durch Cook et al., Comm. der ACM

(Das ist also eigentlich eine sehr tiefe Frage, die es definitiv verdient, auf TCS.SE zu sein, imho ... vielleicht kann jemand sie dort so nachfragen, dass sie passt und bleibt)

vzn
quelle
ps als eindrucksvolles Beispiel für die Leistungsfähigkeit der Quasialgorithmen weist das ACM darauf hin, dass ackermanns Funktion durch einen Quasialgorithmus zum Stillstand gebracht werden kann, aber größer ist als (nicht berechenbar durch) alle primitiven rekursiven Funktionen.
VZN
1
"Das Wort" Algorithmus "ist normalerweise für Programme reserviert, die immer anhalten." - Ich bin mir nicht sicher, ob das stimmt. Es gibt viele teilweise terminierende Algorithmen (va in Verifikation) und ich habe noch nie jemanden gehört, der nicht "Algorithmus" sagt.
Raphael
Es gibt informelle Verwendungen von "Algorithmus". "teilweise terminieren" ist ok aber prob nonstd. Wie bereits erwähnt, scheint es noch keinen einheitlichen Begriff zu geben. wikipedia definiert einen Algorithmus als effektive Methode, dh entscheidbar mit folgenden Merkmalen (1) Geben Sie immer eine Antwort, anstatt jemals eine Antwort zu geben. (2) immer die richtige Antwort geben und niemals eine falsche Antwort geben; (3) immer in einer endlichen Anzahl von Schritten und nicht in einer unendlichen Anzahl abgeschlossen sein; (4) Arbeit für alle Fälle von Problemen der Klasse.
VZN
und später in demselben Artikel heißt es dann: "Eine weitere Erläuterung des Begriffs" effektive Methode "kann die Anforderung enthalten, dass die Methode bei einem Problem von außerhalb der Klasse, für die die Methode wirksam ist, für immer anhalten oder eine Schleife bilden kann, ohne anzuhalten , darf aber kein Ergebnis zurückgeben, als wäre es die Antwort auf das Problem. " dh es widerspricht sich fast!?! Es ist bemerkenswert, dass in der Schlüsselfrage einige echte Verwirrung herrscht und die vorhandene Terminologie nicht streng ist. Beachten Sie, dass das Wort "Algorithmus" fast ein Jahrtausend alt ist und sich erheblich verschoben hat ....
vzn
Es ist wahr: Die traditionelle Bedeutung ist wahrscheinlich "effektive Methode" in der Art, wie Wikipedia sagt (es gibt keinen Widerspruch in dem Satz, den Sie zitieren; es ist jedoch ein bisschen unklar) - die Leute haben keine Funktionen / Algorithmen erfunden, die nicht beendet wurden (z einige Eingänge). Ich denke, das hat sich seit den 1950er Jahren geändert. wie gesagt, heute wird eine teilweise terminierende Methode eindeutig als "Algorithmus" bezeichnet.
Raphael
2

Solange die betreffende Programmiersprache ausreichend komplex ist (dh wenn sie vollständig ist), gibt es immer Programme in der Sprache, die kein Programm als beendet erweisen kann.

Da alle bis auf die primitivsten Sprachen Turing vollständig sind (es sind nur Variablen und Bedingungen erforderlich), können Sie wirklich nur sehr kleine Spielzeugsprachen erstellen, für die Sie das Halteproblem lösen können.

Bearbeiten: Lassen Sie mich in Anbetracht der Kommentare etwas präziser sein: Jede Sprache, für die Sie das Halteproblem lösen könnten, müsste zwangsläufig unvollständig sein. Dies schließt jede Sprache aus, die einen geeigneten Satz grundlegender Bestandteile enthält (z. B. "Variablen, Bedingungen und Sprünge" oder, wie @ sepp2k sagt, eine generische "while" -Schleife).

Anscheinend gibt es mehrere praktische "einfache" Sprachen wie diese (zB Theoremlöser wie Coq und Agda). Wenn diese Ihrer Vorstellung einer "Programmiersprache" entsprechen, können Sie untersuchen, ob sie eine Art von Vollständigkeit erfüllen oder ob das Halteproblem für sie lösbar ist.


quelle
3
"Da bis auf die primitivsten Sprachen alle Turing-Sprachen vollständig sind (es werden nur Variablen und Bedingungen benötigt)" Das stimmt nicht. Zunächst müssten Sie zumindest eine Rekursion oder eine Art Schleifenkonstrukt durchführen (das sollte so leistungsfähig sein wie eine while-Schleife - eine einfache Zählschleife reicht nicht aus). Zweitens glaube ich nicht, dass es viele Leute gibt, die Sprachen wie Coq oder Agda (die total und daher nicht vollständig sind) als primitive oder Spielzeugsprachen bezeichnen.
8.
@ sepp2k: Na ja. Peano-Arithmetik ist auch sehr nützlich und nicht vollständig. Eine vereinfachte Aussage, nehme ich an. Wenn das OP mit dem Problem hinreichend vertraut ist, kann es hoffentlich die technischen Details ergänzen.
3
Es gibt eine große Lücke zwischen "ausreichend komplex" und "vollständig". Coq ist in der Tat komplex und eignet sich für eine Vielzahl von praktischen Aufgaben.
1
@Kerrek SB Nun, es ist möglich, dass die Sprache Turing-complete in einer Weise verwendet wird, die bis zur Beendigung nachweisbar bleibt. Wenn Sie nachweisen können, dass sich eine rekursive Formel immer ihrer Endbedingung nähert (wie die Fakultätsfunktion), können Sie nachweisen, dass sie endet, obwohl Sie nicht in der Lage wären, jede Art von Rekursion zu behandeln.
@ArtB: Sicher, es gibt immer einige Programme, deren Beendigung nachgewiesen werden kann. Die erste Frage des OP könnte darauf hindeuten, obwohl ich nicht sicher bin, ob ich sie vollständig befolge. Sie könnten beispielsweise keinen "generischen Algorithmus" haben, der feststellt, ob eine bestimmte Programmfamilie endet, während Sie möglicherweise eine eingeschränkte Funktionsfamilie erstellen könnten , bei der angenommen wird, dass eine Funktion zu dieser Familie gehört, und Sie könnten algorithmisch feststellen, ob sie endet beendet. (Ich bin mir nicht sicher, ob diese Familie nicht trivial sein kann. Ich denke, es kann, aber ich kann kein Beispiel geben.)
2

TT

Das ist ziemlich trivial. Wenn wir die Vereinigung einer Teilmenge von angehaltenen TMs und einer Teilmenge von nicht angehaltenen TMs nehmen, wird das Ergebnis aus TMs gebildet, für die das Anhalten-Problem entschieden werden kann (führen Sie beide Maschinen parallel aus, wenn die erste die TM akzeptiert) stoppt, wenn der zweite akzeptiert, stoppt die Maschine nicht). Dies wird jedoch nicht zu interessanten Sprachen führen.

ALogTimecM

Kaveh
quelle
1

Ja, das kannst du, aber ich bezweifle, dass es nützlich sein wird. Sie müssten wahrscheinlich eine Fallanalyse durchführen und könnten dann nur nach den offensichtlichsten Fällen suchen. Beispielsweise könnten Sie eine Datei für den Code abrufen while(true){}. Wenn die Datei diesen Code hat, wird ^ nie beendet. Allgemeiner könnte man sagen, dass ein Programm ohne Schleife oder Rekursion immer beendet wird, und es gibt mehrere Fälle, in denen Sie garantieren könnten, dass ein Programm beendet wird oder nicht, aber selbst für ein mittelgroßes Programm wäre dies sehr schwierig und in vielen Fällen wäre es nicht möglich, Ihnen eine Antwort zu geben.

tl; dr: Ja, aber Sie werden nicht in der Lage sein, es für die meisten nützlichen Programme nützlich zu machen.


^ Ja, technisch gesehen, wenn dieser Code nicht im Codepfad ist oder es andere Threads gibt, könnte er immer noch enden, aber ich mache hier einen allgemeinen Punkt.


quelle
4
Warum sind Coq und Agda Ihrer Meinung nach nicht nützlich? Sie überschätzen den Wert der Turing-Vollständigkeit.
Ich habe Coq verwendet, aber meine Behauptung bleibt bestehen, da die meisten kommerziellen Programme in Java / C ++ / Ruby / C # geschrieben sind, für die meine Behauptungen zutreffen. Die Art von Programmen, die 90% der Menschen für das Schreiben interessieren, würde nicht profitieren. Wenn Sie Coq / Agda usw. nicht kennen, sind Sie im Grunde nicht der Zielmarkt dafür.
5
Ich würde sagen, 99% der Programme der realen Welt würden davon profitieren, wenn sie in einer nicht Turing-vollständigen Teilmenge einer Sprache implementiert würden. Sie werden beispielsweise die Ackermann-Funktion nicht jeden Tag implementieren. 100% von CRUD benötigen keine "echte" Sprache. Die Datenverarbeitung ist fast immer trivial. Sehen Sie sich das Terminator-Projekt an - es stellt sogar eine anständige Untermenge möglicher C ++ - Programme bereit, was für die Dinge der realen Welt mehr als ausreichend ist (einschließlich Treiber und anderen Low-Level-Code).
Die meisten realen Projekte möchten Bibliotheken, die in Turing-vollständigen Sprachen geschrieben wurden, wiederverwenden und ihre IDEs sowie Debugger und Tutorials verwenden. Ja, Sie könnten Dinge in Nicht-Turing-Sprachen erledigen, aber ich kann mir nicht vorstellen, dass einige sagen "Ich möchte X machen" und meine Antwort lautet "Use Coq". ps- danke, dass du mich bei The Terminator Project vorgestellt hast .
4
Ein unvorstellbar großer Teil der Geschäftslogik ist bereits in einem nicht Turing-vollständigen SQL implementiert. Und DSLs und eDSLs sind auf dem Vormarsch. So werden die meisten Business-Apps-Programmierer bald alle "Allzweck" -Sprachen vergessen.