Ein Algorithmus heißt terminiert, wenn er für jede Eingabe nach endlich vielen Schritten anhält.
Für ausgewählte Algorithmen ist es mit den Methoden der formalen Semantik möglich, zu bestimmen, für welche Eingaben sie halten und für welche nicht. Eine Möglichkeit besteht darin, mit Hilfe einer Abstiegsfunktion die Terminiertheit induktiv zu beweisen.