Unentscheidbarkeit und das Halteproblem

Das Halteproblem fragt, ob ein gegebenes Programm bei einer gegebenen Eingabe irgendwann anhält, und Turings Beweis, dass kein Algorithmus dies für alle Fälle beantworten kann, ist das Gründungsbeispiel eines unentscheidbaren Problems.

Definition

Ein Entscheidungsproblem ist unentscheidbar, wenn kein Algorithmus es für jede Eingabe korrekt beantworten kann; das Halteproblem, das entscheidet, ob ein beliebiges Programm bei einer beliebigen Eingabe anhält, ist das kanonische unentscheidbare Problem, das durch ein selbstreferenzielles Diagonalargument bewiesen wurde.

Scope

Dieses Thema behandelt das Diagonalisierungsargument, das die Unentscheidbarkeit des Halteproblems begründet, die Unterscheidung zwischen entscheidbaren, erkennbaren und ko-erkennbaren Problemen, den Satz von Rice, der zeigt, dass alle nichttrivialen semantischen Eigenschaften von Programmen unentscheidbar sind, und den Katalog natürlicher unentscheidbarer Probleme in Logik, Mathematik und Informatik.

Core questions

• Warum kann kein einzelner Algorithmus entscheiden, ob jedes Programm anhält?
• Was ist der Unterschied zwischen einem entscheidbaren und einem lediglich erkennbaren Problem?
• Warum sind im Wesentlichen alle interessanten Eigenschaften des Programmverhaltens unentscheidbar?
• Wie breitet sich die Unentscheidbarkeit vom Halteproblem auf andere Probleme aus?

Key theories

Unentscheidbarkeit des Halteproblems

Die Annahme eines Algorithmus, der das Halten entscheidet, führt zu einem Widerspruch durch ein Programm, das genau dann anhält, wenn vorhergesagt wird, dass es nicht anhält; daher kann kein solcher Algorithmus existieren.

Satz von Rice

Jede nichttriviale Eigenschaft der von einem Programm berechneten Funktion – alles, was für einige Programme zutrifft und für andere aufgrund des Verhaltens nicht – ist unentscheidbar, was das Halteergebnis auf alle semantischen Eigenschaften verallgemeinert.

Clinical relevance

Da das Halten und, nach dem Satz von Rice, alle nichttrivialen Verhaltenseigenschaften von Programmen unentscheidbar sind, kann kein Werkzeug unendliche Schleifen perfekt erkennen, beliebige Korrektheit verifizieren oder jedes Programm vollständig analysieren; statische Analysatoren und Verifizierer müssen daher approximieren, Fehlalarme akzeptieren oder ihren Anwendungsbereich einschränken.

History

Turing bewies die Unentscheidbarkeit des Halteproblems und des Entscheidungsproblems für die Logik 1936 mit einem Diagonalargument, das von Cantor und Gödel inspiriert war. Rice bewies seine weitreichende Verallgemeinerung 1953, und in den folgenden Jahrzehnten wurden viele natürliche Probleme, einschließlich Hilberts zehntem Problem zu diophantischen Gleichungen, als unentscheidbar erwiesen.

Key figures

• Alan Turing
• Henry Gordon Rice
• Emil Post
• Alonzo Church

Seminal works

• turing1937
• sipser2013

Frequently asked questions

Warum können wir ein Programm nicht einfach ausführen, um zu sehen, ob es anhält?

Das Ausführen sagt Ihnen nur dann, dass es angehalten hat, wenn es tatsächlich anhält; wenn es ewig läuft, wird dies durch kein endliches Warten offenbart. Das Halteproblem erfordert eine Methode, die für jedes Programm und jede Eingabe immer die richtige Antwort in endlicher Zeit liefert, und Turing bewies, dass keine solche Methode existiert.

Macht Unentscheidbarkeit die Programmanalyse hoffnungslos?

Nein, aber es erklärt, warum eine perfekte Analyse unmöglich ist. Werkzeuge kommen damit zurecht, indem sie konservativ sind und alles kennzeichnen, was sie nicht als sicher beweisen können, indem sie eingeschränkte Klassen von Programmen exakt behandeln oder indem sie viele praktische Fälle lösen, während sie zugeben, dass sie bei adversen oder pathologischen Fällen versagen können.