Offene Induktion, Kruskals Theorem und Einfache Terminierung

Terminierung nachzuweisen ist eine wichtige Komponente der Programmverifikation. Um wiederverwendbare und abstrakte Resultate zu ermöglichen, verwendet man für gewöhnlich, an Stelle einer bestimmten Programmiersprache, ein mathematisches Model der Berechenbarkeit. Für dieses Projekt handelt es sich dabei um die Termersetzung. Heutzutage gibt es viele Werkzeuge die Terminierung von Termersetzung automatisch beweisen können. Doch können diese Werkzeuge fehlerhaft sein. Daher benötigt man die Möglichkeit einer unabhängigen und verlässlichen Zertifizierung ihrer Resultate. Dies wiederum, wird von sogenannten Zertifizierern, Werkzeugen welche automatisch überprüfen können, ob ein von einem Terminierungswerkzeug erzeugter Beweis korrekt ist, gemacht. Die hohe Zuverlässigkeit solcher Zertifizierer kommt daher, dass diese meist auf Formalisierungen der zu Grunde liegenden Theorie mit Hilfe von Beweisassistenten, wie Isabelle/HOL, aufgebaut sind. Eine dieser Formalisierungen ist IsaFoR. Natürlich können Isabelle Formalisierungen nur Fakten verwenden, welche bereits zuvor in Isabelle formalisiert wurden. Aus diesem Grund ist eines der Projektziele, die mathematischen Grundlagen und Fakten, welche Isabelle Benutzern zur Verfügung stehen, zu erweitern. Als konkrete neue Beiträge denken wir hier an eine Formalisierung von (möglicherweise unendlichen) Bäumen und darauf aufbauend, einen Beweis des berühmten Baum Theorems von Kruskal, in Isabelle. Das Baum Theorem wiederum, wird es erlauben, die Verbindung von einfacher Terminierung zu Terminierung herzustellen: jedes einfach terminierende Termersetzungssystem ist auch terminierend. Dieses Resultat wird dann verwendet werden, um die Knuth-Bendix Ordnung (und möglicherweise andere Simplifizierungsordnungen) in IsaFoR einzubauen, wodurch die Anzahl der Terminierungsbeweise, welche automatisch zertifiziert werden können, steigt. Wie dem auch sei, das Baum Theorem ist nicht nur hinsichtlich einfacher Terminierung interessant, sondern auch in Hinblick auf seinen algorithmischen Inhalt. Diesbezüglich werden wir das Prinzip der Offenen Induktion in Isabelle formalisieren, um es anschließend für einen alternativen und konstruktiveren Beweis des Baum Theorems heranzuziehen. Außerdem werden wir nach anderen Theoremen suchen, für die das Prinzip der Offenen Induktion einen formalisierten Beweis ermöglichen könnte. Abschließend sei noch bemerkt, dass Offene Induktion auch verwendet werden kann um totale Funktionen zu definieren. Da Beweisassistenten die auf Logik höherer Ordnung aufbauen (so wie Isabelle) verlangen, dass alle definierten Funktionen total sind, werden wir die Offene Induktion verwenden, um Isabelles Funktionspaket um Funktionen zu erweitern, welche durch Offene Induktion definiert sind.

Die Haupterrungenschaft dieses Projekts ist ein computergestützter Beweis von Kruskals Theorem, welches ein (zumindest unter Mathematikern) berühmtes Resultat darstellt. Dieses Theorem beschäftigt sich mit dem Begriff eines Baums, einer mathematischen Struktur die zum Beispiel verwendet wird um beliebige mathematische Ausdrücke oder Syntax beliebiger Programmiersprachen zu modellieren. Nun zeigt Kruskals Theorem dass in jeder unendlichen Sequenz von Bäumen wie zum Beispiel durch eine Endlosschleife in einem Computerprogramm verursacht die einzelnen Elemente immer komplizierter werden. Diese Tatsache wiederum, kann verwendet werden um Endlosschleifen für eine bestimmte Klasse von Computerprogrammen vollständig auszuschließen und damit deren Terminierung zu beweisen. Kruskals Theorem wurde bereits 1960 zum ersten Mal bewiesen, doch konnte im Rahmen dieses Projektes der erste computergestützte Beweis erbracht werden. Wobei computergestützt in diesem Fall bedeutet, dass der Beweis mit Hilfe eines Beweisassistenten erbracht wurde, einem Computerprogramm welches es ermöglicht mathematische Beweise zu verfassen und dabei jeden Beweisschritt rigoros überprüft. Dies führt zu nahezu 100 %er Verlässlichkeit und ebnet den Weg um Kruskals Theorem auch als Teil von anderen computergestützten Verifikationswerkzeugen anzuwenden. Letztendlich wird dies zu einer äußerst zuverlässigen und mächtigen automatischen Sammlung von Werkzeugen um die Korrektheit von Computerprogrammen zu beweisen führen.Unser Zertifizierer CeTA stellt einen wichtigen Schritt auf dem Weg zu diesem Ziel dar. CeTA ist ein verifiziertes Computerprogramm, entwickelt mit Hilfe eines Beweisassistenten, welches die Ausgabe von einigen existierenden Termination Tools (automatische Werkzeuge die versuchen die Terminierung eines gegeben Programms zu beweisen) zertifizieren kann. Diese Termination Tools sind selbst in konventionellen Programmiersprachen verfasst und damit anfällig bezüglich derselben Art von Fehlern die wir ursprünglich vermeiden wollten; daher auch der Bedarf an einem Zertifizierer wie CeTA. Als Teil dieses Projektes wurde CeTAs Leistungsfähigkeit unter Verwendung des oben erwähnten Theorems von Kruskal gesteigert und ein generelles Rahmenwerk zur Entwicklung von Zertifizieren extrapoliert.