Automatisierung der Ersetzungstheorie erster Ordnung

Termersetzung ist ein abstraktes Berechnungsmodell, in welchem man formal über Computer- programme argumentieren kann, die in einer deklarativen Programmiersprache geschrieben wurden. So kann man zum Beispiel folgern, dass ein Programm immer ein Ergebnis berechnet (Terminierung), oder dass unterschiedliche Durchläufe von einem Programm zum selben Ergebnis führen. Zu diesem Zweck wird das jeweilige Programm in ein Termersetzungssystem übersetzt, welches im Wesentlichen aus Regeln besteht, mit denen man Ausdrücke durch äquivalente, häufig jedoch einfachere Ausdrücke ersetzten kann. In diesem Projekt betrachten wir eine syntaktisch eingeschränkte Klasse von Ersetzungssystemen, in der jede Eigenschaft entscheidbar ist, die in der Ersetzungstheorie erster Ordnung (Prädikaten- logik erster Ordnung, wobei Ersetzungsrelationen die Rolle von Prädikaten übernehmen) ausgedrückt werden kann. Das schließt Eigenschaften wie Terminierung und Konfluenz ein. Das Entscheidungsverfahren wurde in den späten 1980ern entwickelt und verwendet Baumautomaten die auf Termen arbeiten. Eine erste Implementierung des Entscheidungsverfahrens wurde vor kurzem von Franziska Rapp während ihrer Masterarbeit entwickelt. Das resultierende Tool FORT (First-Order Rewriting Tool) ist mit einem nützlichen Synthese-Modus ausgestattet, womit Ersetzungssysteme generiert werden können, die eine gegebene Eigenschaft erfüllen. Wie jede komplexe Software könnte FORT Fehler enthalten. Seine Korrektheit formal zu beweisen ist keine Option, da ein solcher Beweis, falls überhaupt möglich, von eingeschränktem Nutzen ist, da sich FORT weiterentwickeln wird. Um das Vertrauen in FORT zu verbessern, ist stattdessen die Zertifizierung des Outputs ein Ziel dieses Projekts. Dies erfordert Korrektheitsbeweise der im Entscheidungsverfahren verwendeten Baumautomaten-Konstruktionen in einem interaktiven Beweisassistenten und führt zu einer formalisierten Bibliothek für Baumautomaten. Außerdem müssen geeignete Zertifikate entwickelt werden, die von FORT erzeugt und von einem aus der Bibliothek mittels Code Generierung erhaltenen Zertifizierer überprüft werden können. Ein zweites Ziel des Projekts ist es die Performance von FORT zu verbessern, indem modernste Verfahren für Baumautomaten angewandt und weiterentwickelt werden. Parallele Programmier- techniken werden die Effizienz weiter steigern. Darüber hinaus gibt es viele verschiedene Arten eine gegebene Formel in Baumautomaten-Operationen umzuwandeln, sodass alle zum gleichen Resultat führen, aber große Variation in Berechnungszeit und Speicherplatz besteht. Verfahren zur Findung einer effizienten Transformation werden auch untersucht. Ein letztes Ziel des Projekts besteht in der Verbesserung der Ausdrucksstärke von FORT durch Hinzufügen von neuen Features wie der Unterstützung von Eigenschaften die sich auf zwei oder mehr Ersetzungssysteme beziehen, oder der Generierung von bezeugenden Beispielen. Ein besseres Verständnis der Einschränkungen von FORT soll auch erlangt werden. Das erwartete Ergebnis des Projekts ist ein hocheffizientes und vertrauenswürdiges Tool für die Ersetzungstheorie erster Ordnung, welches bestens für Bildungszwecke geeignet ist. Außerdem wird eine umfassende, formalisierte Bibliothek für Baumautomaten für weitere Entwicklungen zur Verfügung stehen.

FORTissimo: Automatisierung der Ersetzungstheorie erster Ordnung Termersetzung ist ein abstraktes Berechnungsmodell, in welchem man formal über Computerprogramme argumentieren kann, die in einer deklarativen Programmiersprache geschrieben wurden. So kann man zum Beispiel folgern, dass ein Programm immer ein Ergebnis liefert (Terminierung), oder dass unterschiedliche Durchläufe von einem Programm zum selben Ergebnis führen (Konfluenz). Zu diesem Zweck wird das jeweilige Programm in ein Termersetzungssystem übersetzt, welches im Wesentlichen aus Regeln besteht, mit denen man Ausdrücke durch äquivalente, häufig jedoch einfachere Ausdrücke ersetzen kann. In diesem Projekt haben wir eine syntaktisch eingeschränkte Klasse von Ersetzungssystemen betrachtet, in der jede Eigenschaft entscheidbar ist, die in der Ersetzungstheorie erster Ordnung (Prädikatenlogik erster Ordnung, wobei die Prädikate jeweils Ersetzungsrelationen repräsentieren) ausgedrückt werden kann. Das schließt Eigenschaften wie Terminierung und Konfluenz ein. Das Entscheidungsverfahren wurde in den späten 1980ern entwickelt und verwendet Baumautomaten, die auf Termen arbeiten. Startpunkt des Projekts war die Implementierung des Entscheidungsverfahrens im Programm FORT. Drei weitere Programme (FORT-h, FORT- s, FORTify) wurden im Laufe des Projektes entwickelt. Diese können von der Projektwebseite herunter geladen oder direkt im dort zur Verfügung gestellten Webinterface verwendet werden. Wie in jedem komplexen Softwareprojekt kann FORT Programmfehler beinhalten. Um das Vertrauen in die Korrektheit von FORT zu verbessern haben wir eine neue Variante des zugrunde liegenden Entscheidungsverfahrens im Beweisassistenten Isabelle formalisiert. Verglichen mit dem ursprünglichen Entscheidungsverfahren unterstützt die neue Variante eine ausdrucksstärkere Sprache (z.B. können Eigenschaften dargestellt werden, die mehrere Ersetzungssysteme involvieren) und sie kann mit einer größeren Klasse an Ersetzungssystemen umgehen. Wir haben eine formelle Sprache entwickelt, die die grundlegenden Schritte des Entscheidungsverfahrens ausdrücken kann. Das Programm FORT-h, der in Haskell geschriebene Nachfolger von FORT, kann Zertifikate in dieser Sprache produzieren. Die Korrektheit der Zertifikate wird von FORTify, einem aus der Isabelle Formalisierung gewonnenen und daher vertrauenswürdigen Programm, überprüft. FORT-h und FORTify nehmen am jährlichen Konfluenz-Wettbewerb teil. Für die Klasse der Probleme, die in den Anwendungsbereich des Entscheidungsverfahrens fallen, können die Programme in kürzerer Zeit mehr Lösungen finden als deren Mitbewerber. Um den Anwendern und Anwenderinnen ein besseres Verständnis zu vermitteln, weshalb eine Eigenschaft gilt oder nicht gilt, kann FORT-h Beispiele sowie Gegenbeispiele generieren. Das neue Programm FORT-s kann Ersetzungssysteme synthetisieren, die eine gegebene Eigenschaft erfüllen. Dies ist nützlich, um Gegenbeispiele zu finden, oder um nicht-triviale Ersetzungssysteme für Klausuraufgaben oder Wettbewerbe zu generieren. Techniken zur parallelen Berechnung wurden verwendet, um die Performanz von FORT-s zu verbessern. Die Formalisierung beinhaltet viele Resultate zu Baumautomaten, welche als Startpunkt für weitere, auf Baumautomaten basierende, Eigenschaften und Algorithmen verwendete werden können. Beispiele hierfür können in der Programmanalyse und Programmsicherheit gefunden werden.