Das Halteproblem

Kein Programm kann von einem beliebigen anderen entscheiden, ob es hält oder ewig weiterläuft. Das ist kein Mangel an Scharfsinn, sondern beweisbar unmöglich.

Als Nächstes empfohlen → Logik & Quantoren · MATH · T3

Der Beitrag

1928 legte David Hilbert — der einflussreichste Mathematiker seiner Generation — der Fachwelt eine Frage vor: Gibt es ein mechanisches Verfahren, das zu jeder mathematischen Aussage in endlicher Zeit entscheidet, ob sie beweisbar ist? Er nannte sie das Entscheidungsproblem — ein Wort, das die englischsprachige Literatur unübersetzt übernahm und allenfalls mit the decision problem erläutert —, und rechnete fest mit einem Ja. Acht Jahre später kam die Antwort von einem dreiundzwanzigjährigen Doktoranden in Cambridge, Alan Turing, und unabhängig davon vom amerikanischen Logiker Alonzo Church: nein. Ein solches Verfahren gibt es nicht. Turing musste dafür erst festlegen, was ein mechanisches Verfahren sein soll — heute heißt das eine Turingmaschine —, und dann eine Aufgabe vorführen, an der sie scheitert. Diese Aufgabe ist das Halteproblem.

Das Halteproblem lautet: Gegeben sind die Beschreibung eines Programms P und eine Eingabe I; zu entscheiden ist, ob P auf I hält (also fertig wird) oder ewig weiterläuft. Dass es dafür kein Entscheidungsverfahren geben kann, zeigte Turing mit einem Diagonalargument — demselben Kunstgriff, mit dem Cantor die Überabzählbarkeit der reellen Zahlen bewies, und einem nahen Verwandten von Gödels Konstruktion. Angenommen also, es gäbe ein Programm H, das (P, I) entgegennimmt und korrekt sagt, ob P auf I hält. Daraus baue man ein Programm D: D(P) befragt H(P, P); lautet die Auskunft „hält“, geht D in eine Endlosschleife, lautet sie „hält nicht“, hält D auf der Stelle. Und nun: Was tut D, wenn man ihm seine eigene Beschreibung vorlegt? Hält D(D), dann hatte H(D, D) das Gegenteil behauptet — Widerspruch; hält D(D) nicht, dann hatte H(D, D) gesagt, es halte — wieder Widerspruch. H kann es also nicht geben. Der Satz von Rice (1953) dehnt den Befund aus: Fast jede nichttriviale Eigenschaft des Programmverhaltens ist unentscheidbar — kein Programm entscheidet allgemein, ob ein anderes korrekt ist, terminiert, einer Spezifikation genügt oder frei von Fehlern läuft. An dieser theoretischen Grenze ist nicht zu rütteln. Rekursiv aufzählbar heißt eine Menge, deren Elemente ein Programm nacheinander ausgeben kann; entscheidbar heißt sie, wenn ihm das auch für die Nichtelemente gelingt. Das Halteproblem ist rekursiv aufzählbar und nicht entscheidbar. Nach der Church-Turing-These fallen alle vernünftigen Fassungen von „berechenbar“ zusammen, es gibt also nur einen einzigen, kanonischen Begriff rechnerischer Mächtigkeit. Und die Verwandtschaft mit Gödels Unvollständigkeit ist keine Ähnlichkeit, sondern dieselbe Beweisform: Beide zeigen, dass Systeme, die reich genug sind, um über sich selbst zu reden, blinde Flecken über sich selbst haben, und beide diagonalisieren dabei auf genau gleiche Weise.

Warum jetztOb ein Programm terminiert oder sich korrekt verhält, kann die statische Analyse im Allgemeinen nicht beweisen — unmittelbare Folge des Halteproblems. Typsysteme in Programmiersprachen halten sich deshalb an entscheidbare Ausschnitte des Programmverhaltens. Die formale Verifikation mit Coq, Isabelle oder Lean weicht der Schranke auf ihre Weise aus: Sie verlangt den Beweis vom Programmierer und prüft ihn dann maschinell nach — Nachprüfen ist entscheidbar, Finden nicht. Auch das KI-Alignment, die Frage, ob sich ein komplexes KI-System in jeder Lage gutartig verhält, läuft im technischen Kern in Unmöglichkeiten von der Bauart des Halteproblems. Das Halteproblem ist der Boden unter allem, was Berechnung je über sich selbst wissen kann, und es hat jeden ernsthaften Versuch geprägt, verlässliche Software zu bauen.