3.5 Strukturelle Induktion

Gegeben sei eine Menge von Funktionssymbolen F. Strukturelle Induktion erlaubt, Eigenschaften aller Terme in T_{F} zu beweisen, indem folgende Schlußregel verwendet wird.

Theorem 1 (Prinzip der strukturellen Induktion) Sei P (x) eine Eigenschaft über Termen x in T_{F}. Wenn man für alle Funktionssymbole f in F die Implikation

∀t_{1}, …, t_{n} : T_{F} . P (t_{1}) ∧ … ∧ P (t_{n}) ⊃ P (f(t_{1}, …, t_{n}))

zeigen kann, so gilt P (t) für alle t in T_{F}.

Wir geben ein Beispiel für seine Anwendung, welches die zentrale Bedeutung dieses Prinzips zur Verifikation funktionaler Programme zeigt. Betrachte folgende Funktion, die Binärbäume rekursiv spiegelt.

- fun swap empty = empty
=   | swap leaf = leaf
=   | swap(node(t1,t2))  = node(swap(t2),swap(t1));
val swap = fn : btree -> btree
- countleaves(swap(node(node(leaf,leaf),leaf)));
val it = 3 : int

Wir beweisen, daß für alle Konstruktorterme t vom Typ btree

            value(countleaves(swap(t))) = value(countleaves(t)).

In diesem Fall besteht also unser f aus den Funktionen empty, leaf und node. Wir haben also drei Fälle zu untersuchen:

(i) f = empty : Hier ist das n aus dem Induktionsprinzip 0 und es bleibt zu zeigen, daß

        value(countleaves(swap(empty))) = value(countleaves(empty)).

welches sich direkt durch Reduktion von swap(empty) zu empty mit der ersten Regel von swap ergibt.

(ii) f = leaf: Hier ist n ebenfalls 0 und es gilt

         value(countleaves(swap(leaf))) = value(countleaves(leaf)).

durch Reduktion von swap(leaf) zu leaf mit der zweiten Regel von swap.

(iii) f = node : btree * btree -> btree: Hier ist n = 2. Wir nehmen an, um die Implikation zu zeigen, daß

            value(countleaves(swap(t_{i}))) = value(countleaves(t_{i})).

für beliebige t_{i}, i = 1, 2. (Diese Annahme nennt man die Induktionsannahme.) Nun berechnen wir (wobei wir value zu v abkürzen)

 v(countleaves(swap(node(t_{1}, t_{2}))))

= v(countleaves(node(swap(t_{2}), swap(t_{2}))))  (Regel 3 von swap)

 = v(countleaves(swap(t_{2})) + countleaves(swap(t_{1})))  (Regel 3 countleaves)

= v(v(countleaves(swap(t_{2}))) + v(countleaves(swap(t_{1}))))  (Striktheit von +)
= v(v(countleaves(t_{2})) + v(countleaves(swap(t_{1}))))  (Ind.-Annahme für t_{2})
= v(v(countleaves(t_{2})) + v(countleaves(t_{1})))  (Ind.-Annahme für t_{1})
= v(v(countleaves(t_{1})) + v(countleaves(t_{2})))  (+ ist kommutativ)
= v(countleaves(t_{1}) + countleaves(t_{2}))  (+ ist strikt)

 = v(countleaves(node(t_{1}, t_{2})))  (Regel 3 countleaves)

und erhalten die Gleichung, die zu zeigen war. Bzgl. der Striktheit von Funktionen vgl. Gleichung (??). Die Anwendungen der Regeln aus den Funktionsdefinitionen nach Gleichung (??) sind allesamt zulässig. Die t_{i} sind Konstruktorterme, so daß die jeweiligen Positionen mit den genannten Regeln reduzierbar sind.

Das oben angegebene Schema ist nicht praktikabel, wenn die Menge der Konstruktoren unendlich ist und dann es normalerweise auch mehr als einen Termtyp gibt. Nehmen wir daher an, daß T y eine Menge von Termtypen ist und daß wir eine Eigenschaft P für die Terme dieser Typen per Induktion zeigen wollen. Wegen der Typisierung ist es sinnvoll anzunehmen, daß es für jeden Typ τ in T y eine Spezialisierung P_{τ} (x_{τ}) von P gibt, die für Terme x_{τ} vom Typ τ zuständig ist.

Theorem 2 (Prinzip der strukturellen Induktion: typisierte Variante) Wenn man für jedes Funktionssymbol

f : τ_{1} ∗ … ∗ τ_{n} ∗ σ_{1} ∗ … ∗ σ_{m} → τ

in F mit Typen τ_{i} in T y und Typen σ_{j} nicht in T y die Implikation

∀t_{1} : τ_{1}, …, t_{n} : τ_{n}, x_{1} : σ_{1}, …, x_{m} : σ_{m} .
P_{τ_{1}}(t_{1}) ∧ … ∧ P_{τ_{n}}(t_{n}) ⊃ P_{τ_{0}}(f(t_{1}, …, t_{n}, x_{1}, …, x_{m}))

zeigen kann, so gilt für jedes τ in T y die Eigenschaft P_{τ} (t) für alle Terme t vom Typ τ.

Diese Variante wendet man an, wenn datatype=Deklarationen mehr als einen Typ einführen, und wenn Konstuktorterme Blätter enthalten, die aus unendlichen Typen (Zahlen, Zeichenreihen, Funktionstypen) stammen. Als Beispiel sei folgende (etwas synthetische) Typdefinition betrachtet:

   datatype S = f1 of S * int * T
        and T = f2 of S * T | g of (S -> T) *S;

Um Eigenschaften P solcher Terme zu beweisen, nimmt man zweckmäßigerweise T y = {S, T }, spaltet P in P_{S} und P_{T} gemäß der 2 möglichen Termtypen auf, und somit belaufen sich die Beweisverpflichtungen gemäß Theorem 2 auf

\begin{aligned}∀s : S, n : int, t : T & . & P_{S}(s) ∧ P_{T} (t) & ⊃ & P_{S}(f1(s, n)) \\ ∀s : S, t : T & . & P_{S}(s) ∧ P_{T} (t) & ⊃ & P_{T} (f2(s, t)) \\ ∀h : (S → T), s : S & . & P_{S}(s) & ⊃ & P_{T} (g(h, s)) . \end{aligned}