Entwurf und Implementierung eines übersetzenden Systems für das intuitionistische logische Programmieren basierend auf der Warren Abstract Machine
Das Hornklauselfragment der Prädikatenlogik, das bisher hauptsächlich als Grundlage für das logische Programmieren dient, insbesondere für die Programmiersprache PROLOG, ist in seiner Ausdrucksmächtigkeit sehr eingeschränkt. In den letzten Jahren sind viele Erweiterungen der Hornklausellogik untersucht worden. Eine Erweiterung, die durch zusätzliche Typen von Formeln und entsprechende Ableitungsregeln diese Einschränkungen teilweise aufhebt, ist das intuitionistische logische Programmieren.
Die theoretischen Grundlagen dieser Erweiterung sind in der Literatur schon umfangreich untersucht worden. Im Gegensatz dazu ist der praktische Aspekt dieser Erweiterung noch weitgehend unberücksichtigt geblieben. Diese Arbeit beschäftigt sich mit der Entwicklung, Implementierung und Untersuchung eines kompletten und praktikablen Systems für das intuitionistische logische Programmieren.
Einleitend werden die Konzepte, die diese Erweiterung ausmachen, vorgestellt, und die Sprache, ein erweiterter Unifikationsalgorithmus und die zugehörige prozedurale Semantik definiert.
Dieses liefert den Ausgangspunkt für die praktische Umsetzung. Es wird eine Erweiterung der "Warren Abstract Machine" (WAM) entworfen, deren Instruktionssatz als Zielsprache für die übersetzung intuitionistischer logischer Programme dient. Bei dem Entwurf wird insbesondere auf die Möglichkeit zur Integration anderer Erweiterungen des logischen Programmierens, die in ihrer Realisierung auch auf die WAM aufsetzen, geachtet.
Basierend auf dem KA--PROLOG System, wird ein komplettes System für das intuitionistische logische Programmieren realisiert. Dieses System umfaßt die vorher entworfene Maschine, den zugehörigen Übersetzer und weitere Komponenten, wie zum Beispiel einen Debugger und ein Modulkonzept.
Die Untersuchung der Praktikabilität hinsichtlich der effizienten Unterstützung der Paradigmen des intuitionistischen logischen Programmierens durch Laufzeitmessungen und Untersuchung der gemessenen Werte bildet die Grundlage für die Beurteilung und Diskussion des realisierten Systems. Die Diskussion berücksichtigt neben dem Vergleich des erhaltenen mit einem bereits existierenden System auch Schwächen und Erweiterungsmöglichkeiten der entworfenen und realisierten Systemkomponenten. Ein Ausblick auf weitere Möglichkeiten schließt die Arbeit ab.
Diploma Thesis, Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe (TH), 1992.