Zertifizierung Redux

Termersetzung ist ein einfaches aber dennoch ausdrucksstarkes Berechenbarkeitsmodel, welches zu großen Teilen der deklarativen Pogrammierung sowie dem computerunterstützen Beweisen zu Grunde liegt. Außerdem gibt es Methoden welche die Verifikation von Computerprogrammen auf das Nachweisen bestimmter Eigenschaften von entsprechenden Termersetzungssystemen reduzieren. Die beiden wohl wichtigsten Eigenschaften in der Termersetzung sind Konfluenz und Terminierung. Während Terminierung sicherstellt dass es keine Endlosschleifen gibt, garantiert Konfluenz das Berechnungen deterministisch in dem Sinne sind, dass beliebige zwei Berechnungspfade stets wieder vereint werden können. Zusammen implizieren diese beiden Eigenschaften, dass man unabhängig von der gewählten Auswertungsstrategie stets das selbe Resultat für die selbe Eingabe erhält. Terminierende und konfluente Systeme von Ersetzungsregeln sind von besonderem Interesse, da sie Entscheidungsverfahren für ihre jeweilige Gleichungstheorie liefern (wenn man wissen will ob zwei Terme äquivalent sind, muss man diese nur vollständig mit Hilfe der Ersetzungsregeln reduzieren und anschließend auf syntaktische Gleichheit überprüfen). Die sogenannte Vervollständigung, stellt eine Möglichkeit dar um eine gegebene Menge von Gleichungen in eine äquivalente Menge von terminierenden und konfluenten Ersetzungsregeln umzuwandeln. Seit Kurzem ist die Zertifizierung von automatischen Terminierungs- und Konfluenzbeweisen äußerst erfolgreich. Wobei wir mit Zertifizierung die automatische und zuverlässige Verifikation von Beweisen meinen, welche von einem beliebigen externen Programm generiert wurden (z.B. einem automatischen Terminierungs-, Konfluenz-, oder Vervollständigungsprogramm). Der vorherrschende Ansatz in der Zertifizierung kann in zwei Phasen eingeteilt werden: Zuerst formalisiert man die zu Grunde liegende Theorie und die Techniken welche von dem externen Programm verwendet werden mit Hilfe eines Beweisassistenten (z.B. Isabelle/HOL). Danach stellt man für einen gegeben Beweis, der von solch einem Programm erstellt wurde, sicher, dass alle verwendeten Techniken korrekt angewandt wurden. In der ersten Phase überprüft man also, dass die mathematischen Grundlagen der genutzten Techniken im Allgemeinen korrekt sind und dass keine impliziten Annahmen übersehen wurden. In der zweiten Phase stellt man die korrekte Anwendung dieser Techniken auf ein konkretes Problem sicher. Einer der verfügbaren Zertifizierer ist unser Programm CeTA, das automatisch aus unserer Isabelle Formalisierung der Ersetzungstheorie (IsaFoR) generiert wird. Unsere Hauptprojektziele umfassen die folgenden Erweiterungen von IsaFoR und CeTA: (1) Eine Formalisierung der kürzlich vorgestellten Weighted Path Order (WPO). Weiters soll diese auf den Fall von Ersetzung modulo Assoziativität und Kommutativität erweitert werden. (2) CeTA-Unterstützung für Konfluenzbweise von konditionalen Ersetzungssystemen. (3) Eine Formalisierung von Ersetzung und Unifikation modulo Assoziativität und Kommutativität, sowie die Unterstützung sogenannter normalisierter Vervollständigungsbweise durch CeTA. Das Erreichen dieser Ziele wird CeTA auf den neuesten Stand bezüglich der jüngsten Entwicklung von Terminierungs-, Konfluenz-, und Vervollständigungsprogrammen bringen.

Eines der verbreitetsten Hilfsmittel in der Verifikation von Computerprogrammen ist das Anwenden von Gleichungen (zum Beispiel um Teile eines Programms durch andere zu ersetzen die die selben Ergebnisse liefern aber effizienter in der Laufzeit sind). Das Problem mit Gleichung ist, dass man diese immer in zwei Richtungen einsetzen kann, von links nach rechts oder verkehrt herum. Daher kann man beim Anwenden von Gleichungen nie so genau sagen ob man sich seinem Ziel überhaupt nähert und wann man aufhören kann. Dieses Problem wird mit Hilfe der Termersetzung behandelt, in der man Gleichungen durch Regeln ersetzt die nur von links nach rechts anwendbar sind. Zwei der wichtigsten Eigenschaften der resultierenden Termersetzungssysteme sind Terminierung und Konfluenz. Terminierung bedeutet dass es keine Endlosschleifen in der Regelanwendung gibt: man kommt immer irgendwann zu einem Ergebnis auf das keine Regel mehr passt. Und Konfluenz besagt dass egal in welcher Reihenfolge wir Regeln anwenden, wir nichts "kaputt" machen, sondern immer alle Ergebnisse erreichen können. Ein Termersetzungssystem welches beide Eigenschaften erfüllt ist besonders nützlich, da wir dessen Regeln einfach automatisch von einem Computer ausführen lassen können und stets zu einem eindeutigen Ergebnis kommen. Daher sind wir auch an der sogenannten Vervollständigung interessiert, einem Prozess bei dem wir mit Gleichungen anfangen die zum Beispiel ein Computerprogramm mathematisch charakterisieren und deren Erfolg uns ein terminierendes und konfluentes Termersetzungssystem liefert welches alle ursprünglichen Gleichungen erfüllt. Im Projekt "Certification Redux" ging es um die Weiterentwicklung des sogenannten Zertifizierungsansatzes. Dabei handelt es ich um eine generelle Herangehensweise, die dazu dienen soll Eigenschaften von Termersetzungssystemen automatisch zu verifizieren. Hierbei entwickeln wir zwei Arten von Werkzeugen: Zum einen automatische Beweiser, also Programme welche zum Beispiel Terminierung oder Konfluenz eines Termersetzungssystems automatisch überprüfen können und im Falle eines Erfolgs einen entsprechenden Beweise, ein sogenanntes Zertifikat, generieren. Und zum anderen einen Zertifizierer, dessen Aufgabe es ist, die generierten Zertifikate der automatischen Beweiser zu validieren. Nun wäre es jedoch unzureichend, als Zertifizierer einfach ein Computerprogramm zu schreiben das Zertifikate auf Korrektheit überprüfen soll: Warum sollten wir diesem Programm mehr vertrauen als den automatischen Beweisern? Um eine höchstmögliche Verlässlichkeit zu gewährleisten, beweisen wir daher die Korrektheit des Zertifizierers mit Hilfe eines sogenannten Beweisassistenten. Als Resultat unseres Projektes können wir nun Konfluenz von Termersetzungssystemen deren Regeln mit Bedingungen versehen sind automatisch beweisen und zertifizieren. Zusätzlich haben wir die Theorie der Vervollständigung mit Hilfe eines Beweisassistenten erfasst und können nun eine besonders erfolgreiche aber auch komplexe Variante der Vervollständigung, die sogenannte geordnete Vervollständigung zertifizieren. Beide Ergebnisse stellen nützliche Werkzeuge für die Programmverifikation dar.