Problem

Das Halteproblem ist ein Problem aus der Theoretischen Informatik. Es besteht darin, in einem bestimmten Berechnungskalkül zu entscheiden, ob die Ausführung einer bestimmten Berechnungsvorschrift zu einem Ende gelangt.

Alan Turing bewies als erster, dass das Halteproblem in dem von ihm eingeführten Kalkül der Turingmaschine nicht entscheidbar ist.

Genau genommen hat er gezeigt, dass nicht immer beweisbar ist, dass eine nicht-terminierende Turingmaschine nicht hält. Umgekehrt kann jedoch immer gezeigt werden, dass eine terminierende Turingmaschine anhält. Hier gibt es auch einen wichtigen Zusammenhang zur Unvollständigkeit sehr komplexer formaler Systeme. Ein Problem mit der Eigenschaft, dass positive Beantwortung prinzipiell bzw. manchmal möglich ist, negative jedoch nicht, heißt semi-entscheidbares Problem.

Inhaltsverzeichnis [Verbergen]
1 Das Selbstanwendbarkeitsproblem von Turingmaschinen ist nicht entscheidbar
2 Halteproblem und Mächtigkeit von Potenzmengen
3 Konsequenzen
4 Zum mechanischen Beweisen von Terminierung
5 Siehe auch
6 Weblinks


Das Selbstanwendbarkeitsproblem von Turingmaschinen ist nicht entscheidbar [Bearbeiten]
Die wichtigste Fragestellung bezüglich des Halteproblems ist hier, ob es entscheidbar ist, also ob eine Turingmaschine existiert, die für jedes Paar aus kodierter Turingmaschine und Eingabe berechnen kann, ob die kodierte Maschine auf dieser Eingabe anhält. In der praktischen Informatik lautet die Frage: Kann man ein Programm entwickeln, das als Eingabe den Quelltext eines zweiten Programms sowie dessen Eingabewerte erhält, welches entscheiden kann, ob das zweite Programm terminiert, d. h. nicht endlos weiterläuft?

Alan Turing bewies 1936, dass es keine Turingmaschine gibt, die das Halteproblem für alle Eingaben löst.

Halteproblem und Mächtigkeit von Potenzmengen [Bearbeiten]
Ungefähr gleichzeitig mit der Entwicklung speicherprogrammierbarer, universeller Rechenanlagen wurde mathematisch der Begriff der Berechenbarkeit präzisiert. Insbesondere stellt ein brauchbarer Berechenbarkeitsbegriff immer eine Aufzählung der berechenbaren Funktionen in Form einer universellen Funktion zur Verfügung, die das Programm (die Gödelnummer) auf die Funktion des Programms abbildet.

Da es sich jeweils zeigen ließ, dass sich alle gefassten „universellen“ Berechnungsbegriffe durch Übersetzung der Programme ineinander überführen ließen, und sich ein allgemeinerer Berechenbarkeitsbegriff nicht fassen ließ, liegt es nahe, anzunehmen, dass dieser auch „universell“ in dem Sinne ist, dass er alle Funktionen enthält, also vollständig ist.

Das Halteproblem zeigt nun, dass dies nicht annähernd der Fall ist. Die tiefere Ursache dafür liegt darin, dass jede Potenzmenge echt größer ist als ihre Grundmenge. Der Zusammenhang zwischen Potenzmengen und dem Halteproblem liegt darin, dass Terminierungsaussagen über Programme von Turingmaschinen Prädikate sind.

Da es so viele Gödelnummern (Programme) gibt, wie natürliche Zahlen, muss es auch so viele Prädikate geben, wie die Potenzmenge der natürlichen Zahlen Elemente hat, wobei jedes Prädikat irgendeine Eigenschaft der mit ihnen getesteten Programme in eine Aussage fasst. Die Zahl der Prädikate über einer Menge ist aber gerade so groß wie die Zahl der Teilmengen dieser Menge.

Da die Menge der natürlichen Zahlen unendlich ist, mag man nun vermuten, es gäbe eine Möglichkeit, die Potenzmenge der natürlichen Zahlen irgendwie in die natürlichen Zahlen selbst einzubetten, die Prädikate also alle irgendwie durch Gödelnummern darzustellen. Während in der Tat beispielsweise alle endlichen Tupel natürlicher Zahlen (etwa die rationalen Zahlen) problemlos in die natürlichen Zahlen eingebettet werden können, ist dies jedoch für Potenzmengen nicht mehr der Fall.

Der allgemeine Beweis dafür geht auf Georg Cantor zurück.

Satz (Mächtigkeit von Potenzmengen)

Sei X eine Menge. Es gibt keine surjektive Abbildung von X auf die Potenzmenge .
Beweis (durch Widerspruch):

Angenommen, es gäbe eine surjektive Abbildung f von X nach .
Wir definieren die folgende Teilmenge :
.
Da wir annehmen, f sei surjektiv, gibt es ein mit f(x0) = Y.
Versuchen wir nun, x0 zu lokalisieren:
. Widerspruch.
. Widerspruch.
x0 liegt also weder in Y noch in , was nicht möglich ist. Folglich war die Annahme, dass es eine surjektive Abbildung von X auf gibt, falsch.
Man nennt diese Beweistechnik auch Cantor-Diagonalisierung, da mit x0 die Diagonale zwischen der Menge X und ihren Teilmengen (dargestellt durch f(x)) zur Konstruktion eines widersprechenden Elements verwendet wird. Obiger Beweis des Halteproblems folgt genau diesem Beweisschema und ist eine Variation des voranstehenden Beweises.

Die Prädikate über eine Menge können also nicht mehr durch die Menge selber vollständig dargestellt werden. Konsequenterweise gibt es also Prädikate über die Menge von Programmen, die selbst nicht mehr durch Programme dargestellt werden können.

Nun hätte es durchaus sein können, dass sich unter den nicht beschreibbaren (d. h. nicht berechenbaren) Prädikaten nur uninteressante befinden. Das Halteproblem ist aber gerade das Prädikat „dieses Programm terminiert“, was zweifellos zu den „interessanten“ Prädikaten gehört. Der Satz von Rice verschärft dies auf alle, den „Inhalt“, d. h. die Funktion von Programmen betreffenden Aussagen. Der Umstand, dass mit der Menge der „intuitiv“ berechenbaren Funktionen die Menge der Funktionen nicht vollständig dargestellt wird, macht sich also auch praktisch bemerkbar.

Das Halteproblem ist „überraschend“ und „irritierend“ darum, weil die über den Berechenbarkeitsbegriff fassbaren Funktionen „intuitiv“ als „alle“ Funktionen aufgefasst werden, man also nicht erwartet, irgend etwas „intuitiv“ Berechenbares nicht auf diese Weise berechnen zu können. Insbesondere hatte man gehofft, dass vor allem auch die „inhaltlichen“ Prädikate berechenbar sein würden.

Konsequenzen [Bearbeiten]
Die Entdeckung der Nichtentscheidbarkeit des Halteproblems (und des Gödelschen Unvollständigkeitssatzes) hatte eine erschütternde Wirkung auf das damals herrschende mathematische Weltbild. Damals versuchte man gerade, die Mathematik durch eine strikte Formalisierung zu vereinheitlichen und den Regeln der Logik zu unterwerfen (siehe Hilberts Programm). Man ging davon aus, dass sich jedes mathematische Problem durch eine geeignete Formalisierung lösen lässt; dass es also immer möglich sei, eine Aussage so zu formulieren, dass man durch die Regeln der Logik und Mathematik erkennen kann, ob sie wahr oder falsch ist – gesucht war also ein vollständiges und widerspruchfreies System. Nach den Erkenntnissen von Turing und Gödel ist so etwas jedoch grundsätzlich nicht möglich: in jedem System, das turingmächtig ist (bzw. die Mächtigkeit der Arithmetik besitzt) lassen sich Aussagen formulieren, die weder bewiesen noch widerlegt werden können: solche Systeme sind grundsätzlich unvollständig. Oder anders ausgedrückt: es gibt Funktionen, die zwar wohldefiniert sind, deren Werte sich dennoch im Allgemeinen nicht berechnen lassen.

Setzt man nun die Churchsche These als wahr voraus, so können Maschinen und letztlich Menschen das Halteproblem (und viele andere Probleme) grundsätzlich nicht lösen. 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 bedeutet die Nichtentscheidbarkeit des Halteproblems, dass im Allgemeinen eine automatisierte Überprüfung einer Programmlogik nicht möglich ist (siehe auch Verifikation). Insbesondere bedeutet das, dass es nicht möglich ist, automatisiert festzustellen, welche Programme jemals zu einem Ende finden werden, d. h. anhalten werden.

Zu den philosophischen Randbemerkungen siehe auch Kausalität, Determinismus, Indeterminismus

Die Konsequenzen des Halteproblems werden jedoch gelegentlich überschätzt. Das Halteproblem und seine Konsequenz, der Satz von Rice, wird z. B. fälschlich auch dahingehend interpretiert, dass ein automatisches Beweisen von Programmeigenschaften in keinem Fall möglich sei. Mit Verweis auf das Halteproblem wird bisweilen auch behauptet, man könne nie sicher sein, ob ein (gerade ausgeliefertes) Programm einen Fehler enthält oder nicht.

Das Halteproblem bedeutet aber nur, dass es Aufgabenstellungen gibt, die nicht mechanisch (d. h. mit den Mitteln der Turing-Maschine) gelöst werden können. Eine Beschränkung der Mittel setzt aber keineswegs die Logik außer Kraft. Natürlich terminiert eine Turing-Maschine, angesetzt auf ein konkretes Wort oder eben nicht, aber kein Drittes. Lediglich kann dies mit Mitteln, die selbst auf die einer Turing-Maschine beschränkt sind, evtl. nicht entschieden, d. h. vorhergesehen werden.

Ebenso wenig setzt auch die Unvollständigkeit der Logik nicht die Logik selbst, etwa den Satz vom ausgeschlossenen Dritten außer Kraft, sondern beschreibt nur Eigenschaften formaler Logikkalküle (Spiel mit Symbolen) und bezieht sich auf den syntaktischen Wahrheitsbegriff. Genauere Konsequenz für die Logik erhellt sich erst unter Hinzuziehung des semantischen Wahrheitsbegriffs, in dem der syntaktische (Axiome und Regeln) fußt. Die Beziehung zwischen beiden wird in der Modelltheorie beschrieben.

Auch bei Beschränkung auf bestimmte Mittel gilt Nichtentscheidbarkeit nicht für alle Aufgabenstellungen und nicht unbedingt für alle ihre Fälle. Dass das Halteproblem in bisweilen überraschend einfachen Zusammenhängen, wie etwa in der Arithmetik, im Postschen Korrespondenzproblem oder in der Wang-Parkettierung auftritt, bedeutet keineswegs, dass nicht auch komplexe Zusammenhänge in vielen Fällen erfolgreich mechanisch bearbeitet werden können.

Entsprechend differenziert sind die Konsequenzen des Halteproblems zu bewerten.

Zum mechanischen Beweisen von Terminierung [Bearbeiten]
Ganz im Gegenteil zur Lage im Allgemeinen ist ein Terminierungsbeweis gängiger Programme und Algorithmen meist trivial und kann auch entsprechend leicht automatisiert werden. Der Grund dafür ist, dass die Verläufe eines terminierenden Programms ein Absteigen auf einer fundierten Ordnung darstellen. Typischerweise wird z. B. eine Datenstruktur rekursiv zerlegt. Das Programm terminiert, weil es die Blattknoten irgendwann erreichen muss, wenn die Datenstruktur selbst endlich ist.

Beispiel (Verkettung zweier Listen):

append[x,y] = if empty[x] then y else cons[first[x],append[rest[x],y]]
Die Funktion append steigt hier rekursiv über die Liste x ab, d. h. beim rekursiven Aufruf wird die Liste verkürzt. Die Funktion terminiert, weil die Liste x nicht unendlich lang ist. Die fundierte Ordnung im rekursiven Aufruf ist x > rest[x], definiert etwa über die Länge oder das Gewicht der Liste.

Nur in seltenen Fällen terminieren Programme aus nennenswert komplizierteren Gründen, etwa bei Berechnung von Hüllen oder Fixpunkten, deren Existenz weniger offensichtlich ist. Trotzdem lässt sich auch in solchen Fällen eine fundierte Ordnung angeben, wenn das Programm terminiert, da der Begriff der Terminierung mit dem der fundierten Ordnung eng verwandt ist. Fundierte Ordnungen werden auch als terminierend oder noethersch (im Englischen irritierenderweise als well-founded) bezeichnet.

Da die schlichte Natur obigen Beispiels eine Beschränkung des skizzierten Verfahrens etwa auf primitiv-rekursive Funktionen vermuten lässt, sei hier als weiteres Beispiel auf die Ackermannfunktion verwiesen, die in der Rekursion genau so einfach über die lexikalische Ordnung ihrer Parameter absteigt.

Die fundierte Ordnung stellt zugleich auch eine Induktion zur Verfügung, die für den Nachweis von Eigenschaften terminierender Programme eine geeignete Schlussregel ist.

Ein Beispiel für einen automatischen Beweiser auf dieser Grundlage ist der Boyer-Moore-Beweiser, der durchaus stark genug ist, um etwa den Beweis des Halteproblems und andere nicht offensichtliche Beweise zu finden oder nachzuvollziehen. Selbst das Auftreten der universellen Funktion als Gegenstand des Beweises schließt ein automatisiertes Führen desselben noch nicht aus.

Für die sehr erfolgreichen Arbeiten im Bereich des Beweiserbaus wurden verschiedene Turing Awards vergeben.

Umgekehrt führte die verhältnismäßige Einfachheit vieler Beweiskonstruktionen ursprünglich zur Annahme, dass im Allgemeinen Beweise mechanisch geführt werden können, was aber nicht der Fall ist und u. a. seinen Ausdruck im Halteproblem findet. Insbesondere lässt sich ein automatischer Programmbeweiser nicht so vervollständigen, dass er seine eigene Korrektheit beweisen könnte.

Siehe auch [Bearbeiten]
Berechenbarkeit
Entscheidungsproblem
Gödelscher Unvollständigkeitssatz
Erfüllbarkeit
Abzählbarkeit
Satz von Rice
Weblinks [Bearbeiten]
Boyer-Moore-Beweiser
Von „http://de.wikipedia.org/wiki/Halteproblem“
Kategorie: Berechenbarkeitstheorie