Functional Logic Programming with Static Determinism Analysis : Design and Implementation

Die vorliegende Arbeit befasst sich mit der Entwicklung, Implementierung und Analyse funktional logischer Programmiersprachen mit besonderem Fokus auf die Kombination von fauler Auswertung und Nichtdeterminismus. Funktional logische Sprachen verbinden funktionale und logische Paradigmen und ermöglichen dadurch eine flexible und ausdrucksstarke Programmierumgebung.

Der erste Hauptbeitrag ist die Entwicklung eines monadischen Laufzeitsystems für die Programmiersprache Curry. Ein Schwerpunkt liegt auf einer effizienten Implementierung von Pull-Tabbing, einer Technik zur Handhabung von Nichtdeterminismus. Darüber hinaus betrachten wir verschiedene Erweiterungen funktional logischer Sprachen und zeigen, wie das Laufzeitsystem für deterministische Programmabschnitte optimiert werden kann. Das Ergebnis ist ein Compiler mit Laufzeitsystem, der gegenüber bestehenden Systemen messbare Verbesserungen bei der Ausführung funktional logischer Programme erzielt.

Der zweite Hauptbeitrag behandelt die Prototypisierung von Programmiersprachen mittels Compiler-Plugins, insbesondere im Kontext des GHC (Glasgow Haskell Compiler). Wir zeigen, wie sich mit Compiler-Plugins prototypische Sprachimplementierungen, zum Beispiel für einen Curry-Compiler, erstellen lassen, und diskutieren die Vorteile sowie die Herausforderungen dieses Ansatzes.

Der dritte Hauptbeitrag entwickelt Determinismus-Typen zur statischen Analyse funktional logischer Programme. Wir definieren ein Typsystem, das die Determinismuseigenschaften von Funktionen und Ausdrücken statisch analysierbar macht, und demonstrieren seine praktische Anwendbarkeit. Dazu führen wir eine formale Semantik ein und beweisen die Korrektheit des Ansatzes mithilfe des Beweisassistenzsystems Rocq. Auf Basis dieser Determinismusinformationen lässt sich die im ersten Beitrag entwickelte Optimierung gezielt auf geeignete Programmabschnitte anwenden, wodurch die Effizienz funktional logischer Programme weiter gesteigert wird. Zusätzlich liefert die statische Analyse Programmierenden präzisere Warnungen und hilfreiche Informationen. Ferner zeigen wir, wie die Inferenz von Determinismus-Typen realisiert werden kann, und präsentieren eine Implementierung des entsprechenden Algorithmus.