Konfluenz: Automatisierung, Zertifizierung, Erweiterungen

Dieses Projekt beschäftigt sich mit Konfluenz von Termersetzungssystemen. Im Gegensatz zur Terminierung hat die Automatisierung von Konfluenzkriterien bisher nur wenig Aufmerksamkeit erfahren und Ansätze zur Zertifizierung sind uns gänzlich unbekannt. Dieses Projekt soll das ändern. Genauer gesagt, werden die folgenden Ziele verfolgt 1. Konfluenzkriterien zu automatisieren 2. Konfluenzbeweise zu certifizieren und 3. Forschung an Konfluenz zu erweitern. Das erste Ziel ist, hinreichende Bedingungen für Konfluenz zu automatisieren, die über die Techniken von ACP hinausgehen. ACP ist ein Konfluenzbeweiser welcher jüngst in Japan entwickelt wurde. Durch diesen Prozess wird die Erforschung neuer Konfluenzkriterien angespornt und als längerfristige Wirkung planen wir einen internationalen Wettkampf an Konfluenzbeweisern zu initiieren (ähnlich jenem von Terminierungsbeweisern). Verschiedenste Fehler in Terminierungsbeweisern haben die Notwendigkeit für unabhängige Zertifizierung ihrer Ausgabe aufgezeigt. Das zweite Ziel dieses Projekts ist deshalb Konfluenzbeweise zu zertifizieren. Dazu werden mächtige hinreichende Konfluenzkriterien formalisiert und ein Format zur Darstellung von Konfluenzbeweisen entworfen. Das dritte Ziel des Projekts ist es, Forschung an Konfluenz zu erweitern. Eine mögliche Richtung befasst sich mit einer Variante der Knuth-Bendix Vervollständigung, welche keine Terminierung verlangt. Eine zusätzliche Erweiterung ist das Generalisieren von Kriterien für höherstufige Ersetzungssysteme. Das dritte Thema bezüglich Erweiterungen beschäftigt sich mit dem Verallgemeinern von Kriterien für orthogonale Systeme auf eine allgemeinere Klasse von konfluenten Ersetzungssystemen.

Eine wichtige Eigenschaft von Computerprogrammen ist Terminierung: Wird ein Programm letztendlich ein Resultat liefern? Für Termersetzungssysteme wurde diese Eigenschaft genau untersucht und einige entwickelte Techniken werden für die Analyse von anwendungsnahen Programmen eingesetzt. Eine andere interessante Frage ist, ob Programme bei gleicher Eingabe immer die gleiche Ausgabe liefern. Dieses Problem ist von wachsender Bedeutung, da viele Programme ihre Berechnungen parallel ausführen und somit nicht-deterministisch arbeiten. Konfluenz ist eine Eigenschaft, die sicherstellt, dass Ergebnisse eindeutig sind, auch bei nicht-deterministischer Auswertung.Dieses Projekt leistet mehrere Beitrage zur Theorie der Konfluenz von Termersetzungssystemen und ihrer Automatisierung und Zertifizierung, ein Sprungbrett für die maschinelle Verifikation von Software. Wir haben unterschiedliche Techniken für das automatische Beweisen von Konfluenz entwickelt. Unser wichtigster Beitrag, neben dem Vorantreiben der Theorie der Konfluenz, ist ein automatisches Tool, CSI, das Konfluenz von vielen Termersetzungssystemen automatisch beweisen oder widerlegen kann.Wir betrachten Termersetzungssysteme, also Mengen von gerichteten Gleichungen, die verwendet werden können um Terme umzuformen, zum Beispiel um sie zu vereinfachen. Mit Termersetzungssystemen lassen sich im Prinzip beliebige Programme beschreiben. Aufgrund ihrer einfachen Struktur bilden Termersetzungssysteme eine attraktive Grundlage für die Entwicklung von Techniken zur Analyse von anwendungsnahen Programmen.In diesem Projekt haben wir ein Tool entwickelt (CSI), das Konfluenz von vielen Termersetzungssystemen automatisch beweisen oder widerlegen kann. Da CSI selbst nur ein Computerprogramm ist, dessen Code Fehler enthalten kann, ergibt sich ein weiteres Problem: Sind die Antworten des Tools tatsachlich korrekt? Weiterhin haben wir CeTA, einen Zertifizier für Terminierungsbeweise, für Konfluenzbeweise erweitert. Im Gegensatz zu CSI wird CeTA in einem interaktiven Theorembeweiser entwickelt und die Korrektheit seines Codes ist bewiesen. Daher erzeugt CSI zusammen mit CeTA in hohem Maße vertrauenswürdige Beweise für Konfluenz (oder Nichtkonfluenz) von Termersetzungssystemen.Im Zuge dieses Projekts wurden ein eigener Workshop zum Thema Konfluenz und einWettbewerb für automatische Konfluenzbeweiser initiiert. Beide finden seit 2012 jährlich statt und haben zu neuerlichem Interesse am Thema Konfluenz geführt.