Theoretisches Konzept

Grundlegendes Konzept ist die Anwendung sogenannter äquivalenzerhaltender Formel-Transformationen auf die ursprüngliche Spezifikation. Die zulässigen Transformationen werden aus einem Katalog von Basisregeln ausgewält und durch eventuelle Angabe von Parametern gesteuert. Diese Steuerung wird übernommen von der zentralen LOPS-strategie unterstützt durch Heuristiken, welche abhängig von den semantischen Informationen versuchen, die günstigsten Parameter auszuwählen. Essentiell ist daher das Vorhandensein von Domänenwissen (Prädikate, Funktionen, aber auch - soweit bekannt - Grundschemata der Programmierung), auf das diese Heuristiken zurückgreifen können.

Schwerpunkt der Arbeit an LOPS innerhalb des ALPES während der letzten Jahre war die Implementierung eines ersten Prototyps. Die meisten der dafür verwandten Konzepte (Transformationen und zentrale Strategien) stützen sich auf Ideen des frühere LOPS-System. Die wesentlichen Strategischen sind das sogennante GUESSing, die Einführung von Rekursion und die Anwendung von äquivalenzlemmata. Heuristiken übernehmen Entdeckung und (Auslösung der) Substitution von Gleichheiten oder Widersprüchen, Suche nach Lemmata, welche Umformungen in "einfachere" Formeln vornehmen, Tests auf Auswertbarkeit usw.

Aus theoretischer Sicht benötigen die zu verwendenden Transformationen und Strategien allerdings noch eine exakte Fundierung, um die Korrektheit und Erfolgssaussichten der Synthese sicherzustellen. Insbesondere der Begriff "äquivalenzerhaltend" wäre entsprechend der Aufgabenstellung festzulegen. Dazu kommt die Notwendigkeit eines strukturierten Aufbaus von Domänenwissen und es ist noch unklar, ob es sinnvoll wäre, die gesamte theoretische Grundlage auf eine Modifikation der Intuitionistischen Typentheorie abzustützen.

Systemkonzipierung und Implementierung

Die Realisierung von LOPS soll in steigenden Abstraktionsleveln geschehen. Auf dem Grundlevel steht ein bereits entwickeltes Formelmanipulatiossystem XPRTS, welches auch die Metaprogrammiersprache für die Entwicklung der höheren Stufen bereitstellt. Level 1 erhält die "Transformationsregeln" des Systems, deren Korrektheit garantiert werden soll. Diese Regeln werden die einzige Möglichkeit darstellen, die zu synthetisierende Formel zu verändern, wodurch die Korrektheit des gesamten LOPS-Systems auf jedem Level sichergestellt ist. Auf Level 2 wird eine voll interaktive Anwendung dieser Regeln bereitgestellt, d.h. eine Möglichkeit, Regeln und Parameter anzugeben und deren Ausführungsergebnisse zu beobachten.

Level 0-2 bilden zusammen ein allgemeines interaktives System zur äquivalenzerhaltenden Transformation von logischen Formeln, welches einem Benutzer ermöglicht, jede Synthese von Hand durchzuführen. (Diese Idee, sowie einige andere, sind dem NuPRL-System nachempfunden.) Eine Strategie wird auf dieser Ebene noch nicht vorgegeben. Dies ist insbesondere bei der Entwicklung der höheren Level von Nutzen, in denen Strategien und Heuristiken zur Realisierung eines bestimmten Synthesizers auf Regeln der niedrigeren Level abgestützt werden (Tactic-Konzept). Auf diese Art wird die zunächst interaktive Synthese schrittweise automatisiert, wobei im Falle des Misserfolgs einer Strategie / Heuristik immer noch auf Hilfe durch den Benutzer (Level 2) zurückgegriffen werden kann.

In diesem Sinne wird das LOPS-System als eine komplexe Strategie eines hohen Levels realisiert, welche sich aus mehreren Einzelstrategien zusammensetzt.