Halteproblem

Das Halteproblem ist ein Problem aus der Theoretischen Informatik. Es besteht darin, zu entscheiden, ob die Ausführung einer bestimmten Berechnungsvorschrift (eines Algorithmus oder Programms) zu einem Ende gelangt. Alan Turing bewies, dass dieses Problem in dem von ihm eingeführten Kalkül der Turingmaschine nicht algorithmisch entscheidbar ist. Auch wenn für viele Algorithmen die Frage, ob sie irgendwann terminieren, leicht beantwortet werden kann, gibt es also keinen Algorithmus, der diese Frage für alle möglichen Algorithmen und beliebigen Eingaben beantwortet. Turings Resultat spielt eine grundlegende Rolle in der Theorie der Berechenbarkeit.

Problemstellung

Das Halteproblem stellt die Frage, ob es eine Turingmaschine H gibt, die für jede Turingmaschine T mit jeder Eingabe w entscheidet, ob T irgendwann anhält oder endlos weiterläuft. Die Eingabe für H besteht dabei jeweils aus einer codierten Beschreibung b(T) der Maschine T und deren Eingabe w.

Alan Turing bewies 1936, dass eine solche Maschine H nicht existiert.

Beweisskizze

Der Nachweis, dass das Halteproblem nicht entscheidbar ist, geschieht durch einen Widerspruchsbeweis. Man nimmt an, dass die oben beschriebene Maschine H existiert, und zeigt, dass dies zu einem logischen Widerspruch führt. Dies gelingt mit der folgenden Konstruktion von Marvin Minsky:^[1]

Angenommen, H existiert. Man darf ohne Beschränkung der Allgemeinheit annehmen, dass die Eingabe für H die Form b(T) * w hat. Dabei ist * eine Zeichenkette, die weder in der Beschreibung b(T) der Turingmaschine T noch in deren Eingabe w vorkommt.

Es ist möglich, um H herum eine Maschine G zu konstruieren, die sich bis auf einen Unterschied so verhält wie H:

• Wenn H, angesetzt auf die Beschreibung b(T) einer Maschine T mit der Eingabe w, das Ergebnis liefert, dass T auf w nicht hält, dann liefert auch G dieses Ergebnis.
• Wenn hingegen H unter derselben Eingabe das Ergebnis liefert, dass T hält, dann lässt man G in eine Endlosschleife laufen.

Dann gilt in tabellarischer Darstellung:

Maschine T  Eingabe w	Maschine H Eingabe b(T) * w	Maschine G Eingabe b(T) * w
hält nicht	hält  Ergebnisanzeige 0	hält  Ergebnisanzeige 0
hält	hält  Ergebnisanzeige 1	hält nicht

Um G herum kann eine Turingmaschine F mit der folgenden einfachen Erweiterung konstruiert werden: F ersetzt eine beliebige Eingabe x durch x * x. Anschließend ruft F das Programm von G auf.

Wenn man F mit ihrer eigenen Beschreibung b(F) als Eingabe in Betrieb setzt, dann passiert Folgendes:

1. F ersetzt die Eingabe b(F) durch b(F) * b(F).
2. F ruft G mit der Eingabe b(F) * b(F) auf.
3. G ruft H mit der Eingabe b(F) * b(F) auf.

Angenommen, H hält mit dem Ergebnis 1, d.h. F mit der Eingabe b(F) hält. Dann geht es folgendermaßen weiter:

4. G setzt ihr Programm fort, geht in eine Endlosschleife, und hält nicht.
5. Die G umfassende Maschine F hält nicht.

Angenommen H hält mit dem Ergebnis 0, d.h. F mit der Eingabe b(F), hält nicht. Dann geht es folgendermaßen weiter:

4. G hält mit dem Ergebnis 0.
5. F hält.

F mit der Eingabe b(F) hält genau dann, wenn F nicht hält. Die Annahme, dass H existiert, hat zu diesem Widerspruch geführt – also ist diese Annahme falsch. H existiert nicht, das Halteproblem ist nicht entscheidbar.

Grafische Darstellung der Beweiskonstruktion

Konsequenzen

Bereits durch den gödelschen Unvollständigkeitssatz wurde gezeigt, dass es unmöglich war, die Mathematik durch eine strikte Axiomatisierung vollständig und widerspruchsfrei zu formulieren. Er erbrachte den Beweis, dass Hilberts Programm zum Scheitern verurteilt war. Auch nach den Erkenntnissen von Turing ist so etwas grundsätzlich nicht möglich: in jedem System, das einer Turingmaschine gleichmächtig ist, lassen sich Aussagen formulieren, die weder bewiesen noch widerlegt werden können.^[2] Des Weiteren folgt aus der Unlösbarkeit des Halteproblems, dass es Funktionen gibt, die zwar wohldefiniert sind, deren Werte sich jedoch nicht für jeden Parameter berechnen lassen. Ein bekanntes Beispiel für eine solche Funktion ist die Radó-Funktion.

Setzt man nun die churchsche These als wahr voraus, so kann das Halteproblem grundsätzlich nicht gelöst werden. Das führt zu der philosophisch weitreichenden Aussage, dass nicht jedes Problem lösbar ist, selbst dann nicht, wenn man eigentlich alle relevanten Informationen kennt und sich streng an einen mächtigen Formalismus hält.

Für die Softwareentwicklung folgt aus der Nichtentscheidbarkeit des Halteproblems, dass im Allgemeinen eine automatisierte Verifikation einer Programmlogik nicht möglich ist. Insbesondere ist es im generellen Fall nicht möglich, automatisiert festzustellen, welche Programme jemals zu einem Ende finden. Die gängigen Programmiersprachen sind nämlich Turing-vollständig, das heißt, einer Turingmaschine gleichmächtig. Mit ihnen lassen sich alle Funktionen berechnen, die auch eine Turingmaschine berechnen kann, und umgekehrt.

Viele in der Praxis vorkommende Programme und Verfahren sind jedoch so strukturiert, dass dennoch ein automatisierter Terminierungsbeweis geführt werden kann.

Literatur

• Alan Turing: On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, 2, 42 (1936), S. 230–265. Online-Fassung

Einzelnachweise

1. ↑ Vorlesungsskript der Old Dominion University, abgerufen am 13. Juli 2011
2. ↑ Eine gut verständliche Darstellung der Zusammenhänge und Konsequenzen aus Gödels und Turings Arbeiten bietet beispielsweise Douglas R. Hofstadter: Besprechung von Alan Turing: The Enigma, in Metamagicum, Klett-Cotta, Stuttgart 1988, ISBN 3-608-93089-2, S. 519–528.