SE1: Terminierungsbeweise

Terminierungsbeweise sind generell unmöglich. Im speziellen sind sie aber meist recht trivial und unter anderem müssen das alle SE1-Studenten mal machen. Das Schema hatte ich schon an die Tafel geschrieben und Jenny und Jonas haben es auch mal in digitaler Form verfügbar gemacht: http://sci-nexus.de/project_detail.php?c=1

Hier noch ein paar Hinweise:

  • Haltet euch an das Beweisschema: 3 Definitionen, 2 Beweise. Textuelle Begründungen reichen als Beweis nicht aus.
  • Der Parameterbereich, für den die Funktion terminiert, ist oft intuitiv ersichtlich. Manchmal (siehe Blatt 8, Aufgabe 2d) werden gewisse Einschränkungen jedoch erst klar, wenn man den restlichen Beweis geführt hat. Es lohnt sich also manchmal, den Parameterbereich nochmals anzusehen.
  • Haskell-Datentypen definieren solche Parameterbereiche. Das sind quasi schon Mengen. Mögliche Parameterbereiche sind also beispielsweise:
    • die Menge aller ganzen Zahlen bzw. Integer-Zahlen: P = \mathbb{Z} bzw. P = Integer
    • die Menge der Natürlichen Zahlen P = \mathbb{N}
    • die Menge aller Integer-Listen: P = [Integer]
    • die Menge aller endlichen Listen beliebigen Datentyps P = \{ l \in [a] | l \text{ endlich } \wedge \text{ a beliebiger Haskell-Typ}\}
    • die Menge aller Paare aus endlichen Integer-Listen P = \{ (a, b) | a, b \in \text{[Integer]} \wedge a, b \text{ endlich} \}
    • die Menge aller Binärbäume von Haskell-Typ Tree P = Tree
  • Eine Ordnung (M,\leq) heißt noethersch, wenn jede nicht-leere Teilmenge von M ein minimales Element besitzt. Diese Definition ist äquivalent zu: Eine Ordnung (M,\leq) heißt noethersch, wenn jede absteigende Kette irgendwann stationär wird. Letztere Definition finde ich etwas anschaulicher.
  • In den allermeisten Fällen ist (\mathbb{N}, \leq) die noethersche Ordnung, die in den Terminierungsbeweisen Verwendung findet.
  • In seltenen Fällen (beispielsweise bei der Ackermannfunktion) können auch andere Ordnungen sinnvoll sein. Bei der Ackermannfunktion wäre das beispielsweise (\mathbb{N}^2, \leq_{lex}) also 2D-Vektoren über \mathbb{N} mit lexikographischer Ordnung.
  • Die \delta-Funktion muss den selben Definitionsbereich haben, wie die zu untersuchende Funktion. Das sollte man insbesondere dann bedenken, wenn Tupel als Eingabe entgegen genommen werden. Auch, wenn nur eine der Komponenten abnimmt, muss die \delta-Funktion das ganze Tupel entgegen nehmen.
  • Eine passende \delta-Funktion findet man meist, wenn man sich die folgende Frage stellt: „Was wird kleiner?“. Das, was kleiner wird, muss die \delta-Funktion zurück liefern.
  • Die \delta-Funktion ist bei Listen meist, die Funktion, die die Länge der Liste liefert (also length), bei Bäumen meist die Höhe (alternativ, aber u.U. beim Beweis dass die Parameter kleiner werden etwas komplizierter, die Anzahl der Knoten) und bei Integer-Werten die Identitätsfunktion (also id). Bei Tupeln kann es auch die Funktion sein, die eine der Komponenten zurück liefert.
  • Eine \delta-Funktion kann man mathematisch definieren oder in Haskell-Notation. Letzteres ist meistens einfacher. Die Funktion, die die Höhe eines Baumes berechnet, kann beispielsweise so aussehen:
    1
    2
    3
    4
    data Tree = Leaf | Node Integer Tree Tree

    delta Leaf = 1
    delta (Node _ a b) = 1 + max (delta a) (delta b)

    max ist bereits in Prelude definiert und kann daher verwendet werden.

  • Nehmen mehrere Werte unabhängig voneinander ab (beispielsweise bei merge), so stellt man je eine \delta-Funktionen auf und addiert diese. Andere Kombinationen (statt der Addition) wie \max, \min oder die Multiplikation funktionieren in der Regel *nicht*.
  • Das Haskell-Typsystem stellt oft schon sicher, dass der Parameterbereich nicht verlassen wird. Wenn die Funktion nur Integer-Werte entgegen nimmt, wird daraus niemals ein String werden. Es müssen dann nur noch ggf. zusätzliche Bedingungen geprüft werden (z.B. \geq 0).
  • Oft ist bei solchen Fällen auch ein Verweis auf das Pattern-Matching angebracht. So kann z.B. für einen bestimmten rekursiven Aufruf gelten, dass ein Parameter \geq 1 ist, weil der Fall 0 schon im vorherigen Pattern abgefangen wurde.
  • Eine häufige zusätzliche Bedingung ist, dass Listen endlich sein müssen (Haskell kann ja auch mit unendlichen Listen arbeiten).
  • Man sollte nicht vergessen, dass man *jeden* rekursiven Aufruf prüfen muss.

Und hier noch die Beispiele zum Üben:

  1. 1
    2
    3
    add :: (Integer, Integer) -> Integer
    add (x, 0) = x
    add (x, y) = 1 + add (x, y-1)
  2. 1
    2
    3
    4
    ack :: (Integer, Integer) -> Integer
    ack (0, m) = m + 1
    ack (n, 0) = ack (n-1, 1)
    ack (n, m) = ack (n-1, ack (n, m-1))
  3. 1
    2
    3
    4
    sum :: [Integer] -> Integer
    sum [] = 0
    sum (0:xs) = sum xs
    sum (x:xs) = 1 + sum ((x-1):xs)

Ihr könnt aber auch quasi jede beliebige Haskell-Funktion nehmen, die ihr mal programmiert habt.

Und hier noch ein paar Lösungshinweise (BTW: Erst selbst versuchen, dann Lösung lesen, nicht umgekehrt!):

  1. Diese Funktion ist trivial und geht nach „Schema-F“.
  2. Hier sollte man als noethersche Ordnung (\mathbb{N}^2, \leq_{lex}) also 2D-Vektoren über \mathbb{N} mit lexikographischer Ordnung wählen. Der Rest geht wieder ganz einfach. Man darf sich nur nicht durch die geschachtelte Rekursion durcheinander bringen lassen. Es sind drei rekursive Aufrufe und der geschachtelte liefert einfach einen Wert (nachdem man gezeigt hat, dass dieser terminiert). BTW: Genau genommen müsste noch bewiesen werden, dass (\mathbb{N}^2, \leq_{lex}) noethersch ist. Das ist aber auch ganz einfach: Sei T \subseteq \mathbb{N}^2 ene beliebige Teilmenge von \mathbb{N}^2 und M = \{ n_1 \in \mathbb{N} | (n_1, n_2) \in T \text{ fuer ein } n_2 \}. Dann ist m = (m_1, m_2) mit m_1 = \min(M) und m_2 = \min(\{ n_2 \in \mathbb{N} | (n_1, n_2) \in T \wedge n_1 \in M \}) minimal bezüglich \leq_{lex}.
  3. Bei dieser Funktion (die angeblich mal ne Klausuraufgabe war) muss man bedenken, dass hier quasi zwei Rekursionen gibt, die unabhängig voneinander terminieren. Man könnte versuchen, dafür zwei getrennte Beweise auf zu stellen, aber das halte ich für unsauber. Die Schwierigkeit bei dieser Aufgabe besteht darin, eine passende \delta-Funktion zu finden. Hier fragt man sich wieder: „Was wird kleiner?“. Die Länge der Liste wird kleiner. Aber nicht immer. Und das erste Element wird irgendwie kleiner. Aber nicht immer. Das erste Element kann sogar größer werden – nämlich im zweiten Fall (0:xs). Die Summe der Elemente der Liste wird meistens kleiner. Allerdings nicht, wenn die Liste nur aus Nullen besteht. ==> Des Rätsels Lösung ist die Kombination aus Länge und Summe: \delta(l) = \mathrm{length}(l) + \mathrm{sum}(l) sum kann hier über eine Funktion berechnet werden, die offensichtlicher terminiert, sodass wir hier also nicht in infiniten Regress geraten. Hat man diese \delta-Funktion, geht der Rest ganz einfach.

Update (26.01.11) Hinweise ergänzt und verdeutlicht.
Update2 (28.01.11) Sebastian hat auch noch ein paar Hinweise und Beispiele (auch zu den anderen Beweisverfahren) zusammen gestellt und Jenny hat ein paar Aufgaben gemacht.


Hinweis für die SE1-Leute

Das, was ich hier schreibe ist inoffizielles Zusatzmaterial. Es kann euch vielleicht für die Klausur (und/oder darüber hinaus) helfen, aber ihr werdet euch vermutlich nicht darauf berufen können. Im Zweifel gilt nicht das, was hier steht, sondern das Skript bzw. die Vorlesung.

Anmerkungen jeglicher Art sind gerne gesehen. Persönlich, per Mail oder auch als Blog-Kommentar. Wie immer gilt: Bei Fragen: fragen.

Schreibe einen Kommentar

Deine E-Mail-Adresse wird nicht veröffentlicht. Erforderliche Felder sind mit * markiert.