Abstiegsfunktion

Eine Abstiegsfunktion ist in der Mathematik und in der Informatik eine Funktion, mit der nachgewiesen werden kann, dass eine Rekursion terminiert.

Prinzip

Zu einer rekursiven Funktion $f\colon A\to B$ wird eine Abstiegsfunktion $g\colon A\to D$ definiert, deren Wert mit jedem Aufruf von $f$ abnimmt. Dafür wird der Einfachheit halber $D=\mathbb {N}$ gewählt. Eine solche Abstiegsfunktion kann beispielsweise so gewählt werden, dass sie die Anzahl der verbleibenden Rekursionsschritte angibt, bis die Rekursion terminiert. Anstelle der Relation < (ist kleiner als) in $\mathbb {N}$ kann jedoch auch jede beliebige andere wohlfundierte Relation in $D$ eingesetzt werden, also jede Relation in $D$, die in jeder Teilmenge von $D$ eine Ordnung herstellt, die mit einem bestimmten Element dieser Teilmenge beginnt.

Nun wird nachgewiesen, dass mit jedem Aufruf von $f$ der Wert von $g$ abnimmt, das heißt, wenn zur Berechnung von $f(x)$ der Wert von $f(x')$ notwendig ist, muss $g(x')<g(x)$ gelten.

Die Bedingung, dass die Relation < wohlfundiert sein muss, besagt hier, dass es ein Minimum geben muss. Es kann also irgendwann keinen Wert von $g(x)$ geben, zu dem noch ein kleinerer Wert gefunden werden kann. Daraus, dass der Wert von $g(x')$ laut Definition von $g$ bei jedem Rekursionsschritt aber abnehmen muss, lässt sich jetzt ableiten, dass ab irgendeinem Wert $x$ kein weiterer Rekursionsschritt stattfindet und damit, dass die Rekursion terminiert.

Beispiele

Mathematik

Sei

$f\colon \mathbb {Z} \to \mathbb {Z} ,x\mapsto f(x)={\begin{cases}f(x-1)+x,&{\mbox{wenn }}x>13\\0&{\mbox{sonst}}\end{cases}}$

Wir definieren die Abstiegsfunktion wie folgt:

$g\colon \mathbb {Z} \to \mathbb {N} ,x\mapsto g(x)=x-13$

Mit laut rekursiver Funktionsdefinition

$x'=x-1$

ist

${\begin{matrix}g(x')&<&g(x)\\g(x-1)&<&g(x)\end{matrix}}$

und damit

${\begin{matrix}(x-1)-13&<&x-13\\-14&<&-13\end{matrix}}$

wahr. Damit ist nachgewiesen, dass der Wert von $g(x)$ mit jedem Rekursionsschritt sinkt; da er in $\mathbb {N}$ aber nicht endlos sinken kann, terminiert die Rekursion.

Informatik

Ein Algorithmus ist angegeben durch den folgenden Java-Code:

 void triangle(String s) {
     System.out.println(s);
     if(s.length() <= 1) return;
     triangle(s.substring(1));
 }

Hier wird also die Funktion triangle mit einer Zeichenkette als Argument aufgerufen. Der übergebene Text wird ausgegeben, anschließend wird die Methode verlassen, falls die Länge des Strings nur ein Zeichen oder weniger beträgt. Falls sie jedoch größer ist, wird die Methode triangle rekursiv mit dem Rest der Zeichenkette nach Abschneiden des ersten Zeichens aufgerufen. Ein Aufruf mit der Zeichenkette "Hallo!" ergibt also die folgende Ausgabe:

Hallo!
allo!
llo!
lo!
o!
!

Um den Beweis zu führen, dass triangle nicht nur bei der Eingabe "Hallo!" terminiert, sondern auch bei allen anderen, ziehen wir als Abstiegsfunktion die Länge der Zeichenkette $s$ heran. Aus dem Abschneiden des ersten Zeichens bei der Rekursion ergibt sich damit

$g\colon \mathbb {N} \to \mathbb {N} ,length_{s}\mapsto g(length_{s})=length_{s}-1$

Und so auch über

${\begin{matrix}g(laenge_{s}')&<&g(laenge_{s})\\length_{s}-1&<&length_{s}\\1&>&0\end{matrix}}$

und die Definition der Fundiertheit, dass die Rekursion terminiert.

Siehe auch

• Fundierte Menge, Wohlordnung und Ordnungsrelation