Proof Theory and Dependent Type Theory: Distinct Foundations for Designing Proof Assistants

Stellen Sie sich vor, Sie versuchen, den ultimativen „Beweisassistenten“ zu bauen – einen superintelligenten Roboter, der Menschen dabei hilft, ihre Mathe- und Logikhausaufgaben zu überprüfen, um sicherzustellen, dass sie zu 100 % korrekt sind. Seit Jahrzehnten wurden die meisten dieser Roboter nach einem speziellen Bauplan namens Abhängige Typentheorie (Dependent Type Theory, DTT) gebaut. Es ist, als würde man einen Roboter aus einem sehr komplexen, hochtechnologischen Lego-Set bauen, bei dem jedes einzelne Teil mit einem spezifischen Etikett versehen ist und der Roboter prüft, ob die Etiketten perfekt übereinstimmen, bevor er das Zusammenstecken erlaubt.

Aber in diesem Paper schlägt der Autor Dale Miller vor, dass es einen anderen, vielleicht besseren Weg gibt, diese Roboter zu bauen. Er argumentt, dass wir uns in der Strukturellen Beweistheorie umsehen sollten, speziell in einem Rahmenwerk namens Sequenzenkalkül (Sequent Calculus). Betrachten Sie dies nicht als ein starres Lego-Set, sondern als ein dynamisches, bewegliches Puzzle, bei dem die Teile gleiten und ihre Form verändern können, solange die Logik Bestand hat.

Hier ist die Aufschlüsselung, warum Miller denkt, dass dieser „Puzzle“-Ansatz dem „Lego“-Ansatz überlegen sein könnte, unter Verwendung von sechs Kernideen:

1. Trennung von „Was“ und „Wie“

In der Lego-Welt (DTT) entscheidet der Roboter zwei Dinge gleichzeitig: was für eine Logik Sie verwenden und wie der Beweis aufgebaut wird. Es ist, als würde man sagen: „Wir dürfen nur Türme aus roten Steinen bauen, und die einzige Möglichkeit, sie zu stapeln, ist senkrecht nach oben.“
Miller schlägt vor, dies zu trennen. Wir können die Logik festlegen (die Regeln des Spiels) und dann jede beliebige Beweisstruktur wählen, um sie zu lösen. Es ist, als würde man entscheiden, dass man Fußball spielen möchte, und dann feststellen, dass man Tore auch durch Schießen, Köpfen oder sogar durch eine Torkanone erzielen kann, wenn die Regeln es erlauben. Der Sequenzenkalkül lässt Sie viele verschiedene „Züge“ (wie Natürliche Deduktion, Tableaux oder Resolution) nutzen, ohne Sie auf einen einzigen, starren Stil festzulegen.

2. Das Problem mit „Beweise als Code“

Der Lego-Ansatz behandelt einen Beweis wie ein Computerprogramm (einen λ-Term). Während Computer großartig darin sind, Programme auszuführen, können sie sehr wählerisch sein. Manchmal nimmt das Programm einen seltsamen Pfad, um zur Antwort zu gelangen, oder es bleibt stecken, weil es auf eine bestimmte Art von Eingabe wartet.
Miller weist darauf hin, dass der Lego-Ansatz mit unordentlichen Problemen wie „Universumsstufen“ (eine komplexe Art, Typen zu organisieren, damit sie nicht kollidieren) und „Beweis-Irrelevanz“ (Zeitverschwendung durch das Überprüfen von Teilen des Beweises, die eigentlich gar nicht wichtig sind) zu kämpfen hat. Der Sequenzenkalkül-Ansatz ist einfacher; er muss sich nicht mit diesen schweren Typregeln befassen, da er die Beweisstruktur direkter behandelt, eher wie einen Flussdiagramm als wie ein komplexes Skript aus Code.

3. Umgang mit „klassischer“ Logik (Das Entweder/Oder-Problem)

Einige Logiken sind „intuitionistisch“ (man muss beweisen, dass etwas existiert, indem man es konstruiert), und einige sind „klassisch“ (man kann beweisen, dass etwas existiert, indem man lediglich zeigt, dass es unmöglich ist, dass es nicht existiert).
Der Lego-Ansatz hat Schwierigkeiten, den „klassischen“ Stil reibungslos zu handhaben. Er muss oft zusätzliche, sperrige Regeln hinzufügen, um dies zu ermöglichen. Miller argumentt, dass der Sequenzenkalkül von Grund auf so konzipiert wurde, dass er beide Stile gleichermaßen gut handhabt – wie ein universeller Adapter, der in jede Steckdose passt, ohne dass man einen klobigen Konverter benötigt.

4. Das Akzeptieren von „Vielleicht“ (Nicht-Determinismus)

Dies ist ein entscheidender Punkt. Die Lego-Roboter sind darauf ausgelegt, „deterministisch“ zu sein, was bedeutet, dass sie einem einzigen, geraden Pfad folgen müssen, um einen Beweis zu prüfen. Wenn sie auf eine Sackgasse stoßen, halten sie an.
Miller schlägt vor, ein wenig „Nicht-Determinismus“ (Raten und Backtracking) zuzulassen, was eigentlich eine Superkraft ist. Stellen Sie sich ein Labyrinth vor. Ein deterministischer Roboter geht einen Pfad und bleibt stehen, wenn er auf eine Wand stößt. Ein nicht-deterministischer Roboter kann einen Pfad versuchen, gegen eine Wand prallen, „Ups“ sagen und sofort einen anderen Pfad ausprobieren.
Miller argumentt, dass wir durch das Zulassen von „Raten“ und „Backtracking“ beim Beweisprüfen die „Beweiszertifikate“ (die Hausaufgaben, die Sie abgeben) viel kleiner machen können. Der Roboter übernimmt die schwere Arbeit der Suche, sodass Sie nicht jeden einzelnen Schritt aufschreiben müssen. Es ist ein Kompromiss: ein kleineres Hausaufgabenblatt für einen Roben, der ein bisschen intensiver nachdenken muss.

5. Die Magie der „beweglichen Binder“

Dies ist der aufregendste Trick des Papers. In der Logik haben wir es oft mit Variablen zu tun, die „gebunden“ sind (wie das „x“ in „für alle x...“). In der Lego-Welt sind diese Variablen oft fest an einem Ort fixiert, und der Umgang mit ihnen ist ein Albtraum aus technischen Kopfschmerzen (wie die berühmte POPLMark-Herausforderung).
Miller schlägt eine Sichtweise vor, in der diese Variablen mobil sind. Er nennt dies λ-Baum-Syntax.
Stellen Sie sich vor, eine Variable ist ein Namensschild an einer Person. In der Lego-Welt kann das Namensschild verloren gehen oder verwirrt werden, wenn man die Person bewegt. In Millers Welt ist das Namensschild an die Person festgeklebt. Egal, wie man die Person im Raum (oder im Beweis) bewegt, das Namensschild bleibt bei ihr.
Er führt ein spezielles Werkzeug ein, das er den ∇-Quantor (gesprochen: „Nabla“) nennt. Denken Sie an dies als eine „lokale Scope“-Taste. Wenn Sie diese drücken, besagt sie: „Diese Variable gehört nur zu diesem spezifischen Teil des Beweises und kann niemals entkommen.“ Dies macht es unglaublich einfach, Sprachen zu analysieren, die komplexe Regeln haben, wie etwa Programmiersprachen oder das π-Kalkül (eine Methode, um zu modellieren, wie Computer miteinander kommunizieren).

6. Der Abella-Roboter

Miller spricht nicht nur darüber; er hat einen Roboter gebaut, um zu beweisen, dass es funktioniert. Er heißt Abella.
Abella ist ein Theorembeweiser, der vollständig auf diesen Prinzipien des Sequenzenkalküls basiert. Er nutzt die „beweglichen Binder“ und den ∇-Quantor, um komplexe Logik über Sprachen und Bindungen mit Leichtigkeit zu handhaben. Während die auf der Abhängigen Typentheorie basierenden Roboter (wie Coq oder Lean) sehr populär sind und riesige Bibliotheken mit vorgefertigten Beweisen besitzen, legt Abella nahe, dass für bestimmte schwierige Probleme – insbesondere solche, die mit der Benennung und Bewegung von Variablen zu tun haben – dieser neue Ansatz natürlicher und eleganter ist.

Das Faz-it

Miller sagt nicht, dass die Lego-Roboter (Abhängige Typentheorie) schlecht sind oder dass man sie wegwerfen sollte. Er erkennt an, dass sie ausgereift, weit verbreitet und für viele Dinge großartig sind.
Er schlägt jedoch vor, dass der Sequenzkalkül für die Grundlagen, wie wir diese Beweisassistenten entwerfen, ein flexibleres, einfacheres und leistungsfähigeres Werkzeugset bietet. Er trennt Logik von Struktur, akzeptiert kluges Raten und handhabt das knifflige Geschäft der „beweglichen Variablen“ mit einer Eleganz, der die aktuelle Norm kaum gewachsen ist. Es ist eine Einladung, das Problem aus einem anderen Blickwinkel zu betrachten, indem man ein Framework nutzt, das in vielen anderen Bereichen der Logik bereits erfolgreich war, aber bisher noch nicht im Rampenlicht der interaktiven Beweisassistenten stand.