Terminiertheit
Terminiertheit ist ein Begriff aus der Berechenbarkeitstheorie, einem Teilgebiet der theoretischen Informatik. Man sagt, ein Algorithmus terminiert für die Eingabe a, wenn er für die Eingabe a nach endlich vielen Arbeitsschritten zu einem Ende kommt, so dass die Berechnung in endlicher Zeit abgeschlossen wird. Man sagt, der Algorithmus terminiert überall oder ist terminierend, wenn er für jede Eingabe terminiert. Dabei wird keine für alle Eingaben gemeinsam gültige Obergrenze für die Anzahl der ausgeführten Arbeitsschritte gefordert.
Eine wichtige Aufgabe der Verifikation eines Computerprogramms (dem Beweis der Korrektheit) ist es, zu zeigen, dass das vorliegende Programm für gewisse Eingaben terminiert. Aus der Nicht-Entscheidbarkeit des Halteproblems folgt, dass es keinen, für jedes Paar gültigen, Algorithmus gibt, der zu einem Paar (Programm, Eingabe) immer entscheiden kann, ob das Programm terminiert. Auch die Frage, ob ein Programm überall terminiert, ist unentscheidbar. Dies folgt aus einer Abwandlung des Halteproblems, dem uniformen Halteproblem.
Für viele praktische Algorithmen ist deren Terminierung aber einfach zu beweisen. Ein bekanntes Beispiel für eine Funktion, zu der bewiesen wurde, dass es für sie kein terminierendes Berechnungsverfahren gibt, ist die Radó-Funktion. Das Collatz-Problem ist ein Beispiel für eine Funktion, für die weder ein terminierendes Berechnungsverfahren gefunden wurde, noch bewiesen wurde, dass es ein solches Verfahren nicht gibt.
Mechanische Terminierungsbeweise
BearbeitenFür viele gängige Programme und Algorithmen kann der Terminierungsbeweis leicht automatisiert werden. Der Grund dafür ist, dass die Verläufe eines terminierenden Programms ein Absteigen auf einer fundierten Ordnung darstellen. Typischerweise wird 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.
Das skizzierte Verfahren ist nicht auf primitiv-rekursive Funktionen beschränkt. Auch die nicht primitiv-rekursive Ackermannfunktion steigt einfach über die lexikalische Ordnung ihrer Parameter ab.
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 stark genug ist, um etwa den Beweis des Halteproblems und andere nicht offensichtliche Beweise zu finden oder nachzuvollziehen. Für die erfolgreichen Arbeiten im Bereich des Beweiserbaus wurden verschiedene Turing Awards vergeben.
Aus dem Halteproblem folgt jedoch, dass sich ein automatischer Programmbeweiser nicht so vervollständigen lässt, dass er seine eigene Korrektheit beweisen könnte.