Induktive Strukturen

Induktive Strukturen "im Alltag"

Induktive Strukturen finden sich überall in der Welt. Beispiel: Ein Lego-Schloss besteht aus mehreren einzelnen Steinen, es ist also zusammengesetzt. Wahrscheinlich wundert man sich jetzt, wo die typische Rekursion ist. Antwort: Nicht vorhanden. Wichtig ist das Wort zusammengesetzt: Induktiv meint genau das hier. Ein Lego-Schloss ist eine zusammengesetzte Struktur, zusammengesetzt aus mehreren Steinen. Das, was man wahrscheinlich typischerweise unter Rekursion versteht, kommt dadurch zustande, dass man mehrere Lego-Schlösser zu einem größeren Lego-Schloss zusammensetzt (wie auch immer das genau funktionieren soll). Solche Strukturen kann man auch in Coq darstellen. Machen wir das doch einfach mal an unserem Lego-Schloss (zunächst in der einfachen Variante):

Was passiert hier?

• Inductive ist das Schlüsselwort für zusammengesetzte Strukturen.
• castle ist der Typ unserer Lego-Schlösser.
• sets_of_stones ist eine Menge an Mengen an Steinen. Nicht weiter drüber nachdenken, das dient hier gerade nur der Darstellung.
• castle_of_stones sagt uns, wie man ein castle bauen kann: Man braucht dafür lediglich eine Menge an Steinen some_set.

Schauen wir uns noch kurz an, wie man Schlösser zusammensetzen kann:

Der neue sogenannte Konstruktor castle_of_castles gibt also eine zweite Möglichkeit an, ein castle zu bauen: Man nimmt zwei bereits bekannte castles und baut daraus ein neues castle.

Natürliche Zahlen

Solche Beschreibungen lassen sich natürlich auch verbalisieren:

• zero ist eine natürliche Zahl NAT.
• Falls n bereits eine natürliche Zahl NAT ist, dann ist auch succ(n) eine natürliche Zahl NAT.

Man könnte das auch noch lascher formulieren:

• zero ist ein NAT.
• Falls n bereits ein NAT ist, dann ist auch succ(n) ein NAT.

Diese Formulierung unterstützt nochmal mehr, dass wir eine Menge an Dingen gebaut haben, die wir NAT nennen, oder eben die Menge der natürlichen Zahlen. Etwas machen können wir damit bisher nicht. Dazu später mehr.

Syntax von Aussagenlogik

Wir brauchen strings, um Atome repräsentieren zu können.

top ist eine formula.

bottom ist eine formula.

Jedes Atom (repräsentiert durch einen string) ist eine formula.

Falls f1 eine formula ist, dann ist auch negation(f1) eine formula.

Falls f1 und f2 formulas sind, dann ist auch conjunction(f1,f2) eine formula.

Falls f1 und f2 formulas sind, dann ist auch disjunction(f1,f2) eine formula.

Falls f1 und f2 formulas sind, dann ist auch implication(f1,f2) eine formula.

Falls f1 und f2 formulas sind, dann ist auch biimplication(f1,f2) eine formula.

Hier mal ein Beispiel:

Rekursion

Mittels Rekursion kann man nun Funktionen auf solchen induktiven Strukturen definieren. Rekursion meint hier lediglich, dass man für jeden Konstruktor sagen muss, wie sich die Funktion verhalten soll. Dabei kann sich die Funktion selbst aufrufen, wenn der Konstruktor Argumente desselben induktiven Typs hat.

Addition auf NAT

Hier ein Beispiel auf unseren natürlichen Zahlen NAT:

Was passiert hier?

• Fixpoint ist das Schlüsselwort für rekursive Funktionen.
• add ist der Name unserer Funktion.
• n1 und n2 sind die beiden Argumente der Funktion, beide vom Typ NAT.
• Die Funktion gibt eine natürliche Zahl NAT zurück.
• Durch match wird eine Fallunterscheidung auf n1 gemacht.
• Falls n1 = zero, gibt die Funktion n2 zurück, weil 0 + n2 = n2.
• Falls n1 = succ (n1'), gibt die Funktion succ (add (n1') n2) zurück, weil (n1 +1) + n2 = 1 + (n1 + n2).
• end beendet die Fallunterscheidung.

Check auf zero

Solche Funktionen müssen aber keine wirkliche Rekursion verwenden, wie das folgende Beispiel zeigt:

Die Konsole sagt genau das: Not a truly recursive fixpoint. In solchen Fällen kann man dann auch das Schlüsselwort Definition verwenden:

Atome in einer formula

Machen wir noch ein Beispiel auf formula:

Da formula mehr Konstruktoren hat, müssen wir die rekursive Funktion atom_occurs auch für mehr Fälle definieren. Aber das Prinzip ist das gleiche geblieben.

Semantik von Aussagenlogik

Schauen wir uns doch einmal mit Blick auf sinnvolle Theoreme an, wie sich die typische Semantik auf Aussagenlogik definieren lässt. Dazu brauchen wir zunächst den Begriff einer Wahrheitsbelegung:

Eine Wahrheitsbelegung ist also eine Funktion, die jedem Atom einen Wahrheitswert true oder false zuordnet. Damit lässt sich die Semantik nun wie folgt (rekursiv) definieren:

Eine Bemerkung zur Reduktion von Verwirrung: Wir verwenden hier Prop (und nicht bool), da wir uns in diesem Kontext Prop als das Universum unserer "Alltagslogik" vorstellen können, während z.B. bool irgendetwas ist, was "wir" uns selbst aufgebaut haben. Achtung: In GLoIn wird Prop meist verwendet, um die Struktur von Fitch-Beweisen nachzubilden.

Einschränkung der möglichen Formeln

... auf bottom, atom und disjunction

Mittels des folgenden Prädikats ist es z.B. möglich, unsere Menge an Formeln einzuschänken:

(Strukturelle) Induktion

Induktion ist nun das korrespondierende Beweisprinzip für rekursive Funktionen. Mit Rekursion definiert man eine Funktion, indem man für jeden Konstruktor eine Definitionsvorschrift angibt. Mit Induktion gibt man einen Beweis für jeden Konstruktor an, um eine Aussage für alle Elemente der induktiven Struktur zu beweisen. Schauen wir uns das direkt praktisch an:

Assoziativität von add

Wir haben jetzt das Theorem niedergeschrieben, das wir beweisen wollen. Wir wollen also zeigen, dass die Addition add, die wir oben definiert haben, assoziativ ist, also dass n1 + (n2 + n3) = (n1 + n2) + n3 für alle n1,n2 und n3 gilt. Mittels Proof leiten wir nun den Beweis ein.

Mit intros n1 leiten wir den Beweis mit den typischen Worten "Sei n1 eine natürliche Zahl NAT." ein.

Kommen wir nun zum spannenden Teil: Induktion über (die natürliche Zahl) n1. Durch das Pattern [|n1' IH] benennen wir die "kleineren" Argumente:

• Im ersten Fall nehmen wir n1 = zero an, weshalb wir hier keine neuen Variablen haben.
• Im zweiten Fall nehmen wir n1 = succ (n1') an, weshalb wir n1' benannt haben. Außerdem geben wir der Induktionshypothese den Namen IH.

Fall 1, oft auch Induktionsanfang genannt. (Auch wenn ich persönlich diese Benennung für nicht notwendig halte.) Weil wir hier den Fall betrachten, dass n1 = zero, müssen wir noch zeigen, dass für alle n2 und n3 gilt, dass 0 + (n2 + n3) = (0 + n2) + n3. Dazu führen wir nun zunächst die beiden NAT's n2 und n3 mittels intros n2 n3 ein.

Die Taktik simpl vereinfacht das Beweisziel. Dies ist hier möglich, weil die Funktion add ausgewerted werden kann, weil die Struktur des ersten Arguments (zero) bekannt ist.

Da nun links und rechts das gleiche steht, gilt diese Gleichung. Dies zeigen wir mittels reflexivity.

Nun zu Fall 2, oft auch Induktionsschritt genannt. (Auch diese Benennung halte ich persönlich für nicht notwendig.) Weil wir hier den Fall betrachten, dass n1 = succ(n1'), müssen wir (unter Annahme der IH) zeigen, dass (n1' + 1) + (n2 + n3) = ((n1' + 1) + n2) + n3 für alle n2 und n3 gilt. Wir verfahren wie im ersten Fall:

Durch specialize spezialisieren wir nun die IH auf unser aktuelles Beweisziel. Mit rewrite IH können wir diese Gleichung zum Umschreiben des Beweisziels verwenden. Kurze Frage zum Nachdenken: Warum ist die IH allquantifiziert über n2 und n3? Wäre das auch bei Pen&Paper-Beweisen der Fall?

Beispiel: Kommutativität von add

Probieren wir uns an der Kommutativität von add. Auch hier ist Induktion der natürliche Weg.

Klappt nicht. Hier brauchen wir ein Hilfslemma add_zero_r. Schauen wir uns noch den schnell den anderen Fall an.

Noch ein Hilfslemma...

Frage zum Nachdenken: Wieso ergibt es "Sinn", dass die nachfolgenden Lemmatas nötig sind?

Typischerweise beginnt man Beweise per Induktion nicht mit "Sei ...", sondern direkt mit "Beweis per Induktion über ...". Entsprechend brauchen wir auch hier nicht intros n, um induction anwenden zu können.

Die beiden Teilbeweise sind zur Übung offen gelassen.

Wie sieht es hier aus?

Mit Hilfe der beiden Lemmata add_zero_r und add_succ_r können wir nun einfach zeigen, dass add kommutativ ist.

Man kann rewrite mit jeder Form von Gleichung verwenden, also auch in Kombination mit anderen Lemmata.

Disjunktive Korrektheit

Nun ein Beispiel mit Aussagenlogik. Wichtig ist es hier, dass wir wieder ein Theorem haben, das über einer induktiven Struktur allquantifiziert: "Für alle f : formula gilt...". Entsprechend bietet sich auch hier ein Beweis per Induktion an.

"Sei"

"Wenn"

"Dann"

Beweis per Induktion...

Hier folgt jetzt das entsprechende Benennungsschema für die einzelnen Fälle. Zum Beispiel besteht eine Disjunktion aus zwei Teilformeln, für die jeweils eine Induktionshypothese benötigt wird.

top

bottom

atom

negation

conjunction

disjunction

implication

biimplication

Fall 1: f = top

top wird natürlich immer erfüllt (per Definition).

Schauen wir uns aber noch einen anderen möglichen Beweis für diesen Fall an.

Wir können mit H3 einen Widerspruch herleiten, da top weder bottom noch ein atom noch eine disjunction ist.

Und noch eine Möglichkeit:

Da das Atom a nicht in top vorkommt, führt auch H2 zu einem Widerspruch.

Fall 2: f = bottom

Hier führt nur ein Weg zum Ziel. Welcher?

Fall 3: f = atom (a')

Wir wissen per H2, dass das Atom a in atom (a') vorkommt. Vereinfachen wir doch zunächst H2. Also muss a' = a gelten.

Die Taktik subst a' ersetzt a' im gesamten Kontext durch a, der rechten Seite der Gleichung H4.

Fall 4: f = negation (f1)

Widerspruch in H3, da einen Negation weder bottom, atom oder disjunction ist.

Fall 5: f = conjunction (f1) (f2)

Widerspruch in H3, da einen Konjunktion weder bottom, atom oder disjunction ist.

Fall 6: f = disjunction (f1) (f2)

Um zu zeigen, dass disjunction f1 f2 von k erfüllt wird, müssen wir zeigen, dass f1 oder f2 von k erfüllt werden. So ist zumindest satisfaction definiert.

Leider wissen wir an der Stelle noch nicht, ob f1 oder f2 von k erfüllt wird. Wir müssen also woanders weitermachen. Wir können zunächst H3 auseinanderbauen. Da disjunction (f1) (f2) eine Disjunktion ist ist, wissen wir auch, dass f1 als auch f2 nur bottom, ein atom oder eine disjunction sein können.

Da das Atom a in disjunction (f1) (f2) vorkommt, muss es mindestens in f1 oder f2 vorkommen. Dieses Oder können wir wegen der Definition von atom_occurs sichtbar machen.

Mit destruct bekommen wir jetzt eine entsprechende Fallunterscheidung.

Fall: Das Atom a kommt in f1 vor. Nun kann man bereits erkennen, dass f1 von k erfüllt wird.

Hierfür brauchen wir die Induktionshypothese IH1 für f1.

Was fehlt hier noch?

Was fehlt hier noch?

Wie funktioniert der zweite Fall?

Fall 7: f = implication (f1) (f2)

Wie geht es jetzt weiter?

Fall 8: f = biimplication (f1) (f2) Endspurt!

Fazit: Induktionsbeweise über größeren Strukturen wie z.B. formula sind deutlich ausführlicher und erfordern eventuell komplexere Zwischenschritte in den einzelnen Teilbeweisen. Das Grundprinzip ist aber das gleiche geblieben! Wir haben einen Teilbeweis pro Konstruktur, und pro Teilbeweis so viele Induktionshypothesen zur Verfügung, wie der Konstruktor stellig ist!