Von Konfluenz zu eindeutigen Normalformen: Zertifizierung und Komplexität

Dieses Projekt befasst sich mit Konfluenz und der verwandten Eigenschaft eindeutiger Normalformen in Termersetzungssystemen. In den letzten Jahren wurden viele mächtige Methoden für Konfluenz entwickelt und in Konfluenzbeweisern implementiert, welche an dem kürzlich etablierten Konfluenzwettbewerb teilnehmen. Es wurden auch erste Schritte in Richtung automatischer Zertifizierung unternommen, aber dort bleibt viel zu tun. Das Ziel dieses Nachfolgeprojektes ist es, zwei wichtige Lücken bei der Zertifizierung zu füllen, Methoden für Eindeutigkeit von Normalformen zu untersuchen, und Komplexitätsaspekte von Konfluenz und Eindeutigkeit von Normalformen zu betrachten. Weiterhin werden wir das Konfluenzbeweiser CSI sowie den Zertifizierer CeTA für Konfluenz weiterentwickeln. Im Einzelnen sind die Ziele 1. das layer-framework zu formalisieren, welches wichtige Resultate für die Zerlegung von Konfluenzproblemen in Teilprobleme wie z.B. Modularität und Persistenz erfasst, 2. eine Formalisierung des Beweises für Konfluenz von development-closed links-linearen Ersetzungssystemen auf der Basis von Beweistermen und Residuentheorie zu entwickeln, 3. Techniken im Zusammenhang mit conditional linearization wie den Satz von Chew zu erforschen, um automatisierbare Kriterien für die Eindeutigkeit von Normalformen zu finden, 4. (praktisch) entscheidbare Klassen für Konfluenz und eindeutige Normalformen sowie die Komplexität von Suchproblemen im Zusammenhang konkreter Konfluenzmethoden zu untersuchen, 5. und die so gewonnen Erkenntnisse zu nutzen um die Stärke und Effizienz des Konfluenzbeweisers CSI sowie des automatischen Zertifizierers CeTA für Konfluenz zu verbessern.

Eine wichtige Frage für Programme ist, ob sie für dieselbe Eingabe immer dasselbe Ergebnis liefern. Bei Programmen, die in verteilten und parallelen Umgebungen ausgeführt werden, ist dies nicht offensichtlich. Eindeutigkeit von Normalformen ist eine Eigenschaft die garantiert, dass Ergebnisse unabhängig vom eingeschlagenen Berechnungspfad sind. Konfluenz ist eine bekannte Eigenschaft, die eindeutige Normalformen garantiert. Sollte Konfluenz nicht gelten, so ist Eindeutigkeit von Normalformen eine wünschenswerte Eigenschaft. In diesem Projekt haben wir zur Theorie der Konfluenz und eindeutigen Normalformen von Termersetzungssystemen beigetragen, insbesondere in Bezug auf Automatisierung und formale Verifikation. Termersetzungssysteme sind ein abstraktes Berechnungsmodell, das auf Ersetzungsregeln beruht, also orientierten Gleichungen, die man verwendet, um Ausdrücke auszuwerten oder zu vereinfachen. Es gibt zahlreiche Anwendungen für Termersetzungssysteme, angefangen bei der Analyse und Optimierung von Programmen bis hin zu Entscheidungsverfahren für Aussagen in logischen und algebraischen Strukturen. Es gibt etliche Varianten von Termersetzungssystemen, die sich in der Art der Terme unterscheiden (Terme erster oder höherer Stufe, getypt und ungetypt, ...) oder auch in der Art und Weise wie die Regeln angewandt werden dürfen (keine Einschränkungen; Regeln mit Vorbedingungen, ...). Wir haben verschiedene Techniken entwickelt, um Konfluenz und Eindeutigkeit von Normalformen von Ersetzungssystemen automatisch zu beweisen oder zu widerlegen, sowohl für Systeme erster Stufe als auch für Systeme höherer Ordnung. Neben Fortschritten in der Theorie sind die wichtigsten Beiträge des Projekts automatische Beweiser für Ersetzungssysteme erster (CSI) und höherer Ordnung (CSI^ho). Beträchtlicher Aufwand war nötig um Techniken die von CSI verwendet werden durch einen unabhängigen höchst vertrauenswürdigen Beweiser formal zu verifizieren. Dies beinhaltet wichtige divide-and-conquer Techniken um Konfluenz nachzuweisen, wie Toyamas gefeiertes Modularitätstheorem, welches besagt, dass die Vereinigung zweier konfluenter Systeme, die keine Funktionssymbole gemeinsam haben, gleichfalls konfluent ist, sowie das Resultat, dass Konfluenz eines Ersetzungssystems erster Stufe aus der Konfluenz des gleichen Systems auf wohlgetypten Termen bezüglich einer mit dem System kompatiblen Typisierung folgt. Die Formalisierungen wurden in Isabelle/HOL, einem interaktiven Theorembeweiser, durchgeführt. Als Basis diente dabei die IsaFoR-Bibliothek. Weitere Resultate des Projektes betreffen Termersetzungssysteme ohne Variablen, eine Klasse von Ersetzungssysteme, für die Eindeutigkeit von Normalformen und Konfluenz entscheidbar sind. Für diese Entscheidungsprobleme wurden verbesserte Komplexitätsschranken gefunden. Um den Informationsaustausch im Forschungsbereich Konfluenz voranzutreiben, haben wir aktiv den Internationalen Konfluenzwettbewerb (Confluence Competition, CoCo) samt zugehöriger Softwareinfrastruktur weiterentwickelt, was zu einer erhöhten Forschungsaktivitität im Bereich von Softwaretools für Konfluenz und verwandter Eigenschaften für diverse Ersetzungssystemformate geführt hat. Im diesjährigen Wettbewerb (Mai 2019) haben 15 verschiedene Tools von Forschern aus 5 Ländern in 12 Kategorien teilgenommen. Im Vergleich zum Vorjahr sind 5 neue Tools und 3 neue Kategorien dazugekommen.