Quelltext der Seite Terminiertheit

'''Terminiertheit''' ist ein Begriff aus der [[Berechenbarkeitstheorie]], einem Teilgebiet der [[theoretische Informatik|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 [[Computerprogramm]]s (dem [[Beweis (Mathematik)|Beweis]] der [[Korrektheit (Informatik)|Korrektheit]]) ist es, zu zeigen, dass das vorliegende Programm für gewisse Eingaben terminiert. Aus der Nicht-[[Entscheidbarkeit]] des [[Halteproblem]]s 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 [[Fleißiger Biber|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 ==
Fü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 [[Fundierte Ordnung|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<nowiki>]]</nowiki>
Die Funktion append steigt hier rekursiv über die Liste x ab, d.&nbsp;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 Funktion]]en 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 Award]]s 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.

== Weblinks ==
* [https://www.cs.utexas.edu/~moore/best-ideas/nqthm/index.html Boyer-Moore-Beweiser]

[[Kategorie:Berechenbarkeitstheorie]]