Gödel, Escher, Bach, Isabelle SoSe 98

4. Aufgabenblatt

Ausgabe: 13.07.1998 Bearbeitungszeit: zwei Wochen

Sofie Czernik Christoph Lüth

Aufgabe 1: Waldarbeiten

1. Definiere einen Datentyp 'a bintree für binäre Bäume, die polymorph über 'a sind. Ein binäre Baum ist entweder ein Blatt (ohne Inhalt), oder ein Knoten, der ein 'a sowie linken und einen rechten Teilbaum enthält.

2. Definiere folgende (primitiv rekursive) Funktionen über binären Bäumen:

(a) n_leaves und n_nodes, die Anzahl Blätter bzw. Knoten eines Baumes;

(b) set_of_nodes, die Menge ('a set) der Knoten des Baumes

(c) preorder, inorder, postorder, die Knoten des Baumes als Liste ('a list) in preorder, inorder bzw. postorder Traversierung.

3. Beweise, daß jeder binäre Baum genau Blatt mehr als Knoten hat.

4. Verifiziere einen der Traversionsalgorithmen (nach Wahl).

Die Traversion soll jeden Knoten im Baum genau einmal besuchen. Die Verfikation geschieht in zwei Schritten:

(a) Zuerst zeigen wir, daß genauso viele Knoten besucht werden wie im Baum enthalten sind, indem wir zeigen, daß die Länge der Resultatsliste von genau der Anzahl der Knoten entspricht.

(b) Dann zeigen wir, daß genau die Knoten besucht werden, die auch in dem Baum enthalten sind (nicht mehr und nicht weniger), indem wir zeigen daß die Menge der Elemente der Resultatsliste gleich der Menge der Knoten des Baumes ist.

Hinweise: Die Länge einer Liste und die Menge der Elemente einer Liste werden durch die Funktionen

length :: 'a list => nat
set    :: 'a list => 'a set

gegeben. Alle Beweise sind durch einfache strukturelle Induktion zu erledigen — vgl. den Beweis der Idempotenz von rev aus der Vorlesung und die meisten anderen Beweise der Listentheorie in

/usr/local/pub-bkb/isabelle/Isabelle98/HOL/List.ML

Aufgabe 2: Kleinstes Gemeinsames Vielfaches

Zeige, daß die wohlfundiert rekursive Funktion euclid: [nat, nat]=> nat, die den Euklidschen Algorithmus implementiert, tatsächlich den größten gemeinsamen Teiler zweier Zahlen berechnet.

Hinweise: Das Theorem euclid_cd aus der Vorlesung ist die halbe Miete, jetzt wird noch ein Theorem euclid_maximal benötigt, welches folgendes besagt: wenn x m teilt, und x n teilt, dann teilt x euclid(m, n). Dieses Theorem wird durch Induktion und Fallunterscheidung gezeigt; die Simplifikation benötigt hierbei noch die zwei Theoreme dvd_mod und mod_less_divisor aus der Theorie Divides.

Der Hauptteil des Beweises ist dann eine einfache Simplifikation mit den

beiden Theoremen euclid_cd und euclid_maximal.

Aufgabe 3: Listensortierung

Die Theorie Sorting enthält die Spezifikation von sortierten Listen. Definiere eine Funktion, die eine Liste (durch einen Sortieralgorithmus nach Wahl) sortiert und zeige die Korrektheit. Als Beispiele können die Theorien InSort (implementiert Sortieren durch Einfügen) und Qsort (implementiert Quicksort) dienen.