Patricia-Bäume sind eine effiziente Baum-Datenstruktur für Maps mit ganzzahligen Schlüsseln und Mengen von ganzen Zahlen. Die Haskell-Standardbibliothek implementiert Patricia-Bäume in Data.IntMap.
Patricia-Bäume haben gegenüber gewöhnlichen Suchbämen wie AVL- oder Rot-Schwarz-Bäumen den Vorteil, dass sie auch die Vereinigung von Bäumen effizient unterstützen.
Aufgabe:
Ziel der Arbeit ist es, Big Endian Patricia-Bäume und die Standard-Operationen lookup, Einfügen und Vereinigung in Isabelle/HOL zu formalisieren und als korrekt nachzuweisen. Ggf. kann man weitere Operationen wie Löschen oder Traversion auch noch hinzufügen. Die formalisierten Operationen sollen mittels Isabelles Code Generator ausführbar sein. Für die implementierten Operationen soll die Laufzeit des generierten Codes mit anderen Datenstrukturen in Isabelle (z.B. Rot-Schwarz-Bäume) verglichen werden.
Das Herausfordernde an der Arbeit wird sein, die nötigen Invarianten für die Bäume zu finden.
Voraussetzungen
- Kenntnisse in funktionaler Programmierung
- Analytisches Denkvermögen
- Freude an formal korrektem Arbeiten
Literatur
- Einführung in Isabelle/HOL:
Tutorial
und
Praktikum
- D. R. Morrison: PATRICIA - practical algorithm to retrieve information coded in alphanumeric. J. ACM 15,4 (1968), pp. 514-534.
- Chris Okasaki and Andrew Gill: Fast Mergeable Integer Maps. In: Workshop on ML, 1998, pp. 77-86.
Veröffentlichungen
Betreuer
Studenten
