An Extensible Theorem Proving Frontend

Interaktive Theorembeweiser sind Softwarewerkzeuge zum computergestützten Beweisen, d.h. sie können entsprechend kodierte Beweise von logischen Aussagen sowohl verifizieren als auch beim Erstellen dieser unterstützen. In den letzten Jahren wurden weitreichende Formalisierungsprojekte über Mathematik sowie Programmverifikation mit solchen Theorembeweisern bewältigt. Der Theorembeweiser Lean insbesondere wurde nicht nur erfolgreich zum Verifizieren lange bekannter mathematischer Theoreme verwendet, sondern auch zur Unterstützung von aktueller mathematischer Forschung. Das Ziel des Lean-Projekts ist nichts weniger als die Arbeitsweise von Mathematikern grundlegend zu verändern, indem mit dem Computer formalisierte Beweise eine praktible Alternative zu solchen mit Stift und Papier werden sollen. ... mehrAufwändige manuelle Gutachten zur Korrektheit von Beweisen wären damit hinfällig und gleichzeitig wäre garantiert, dass alle nötigen Beweisschritte exakt erfasst sind, statt der Interpretation und dem Hintergrundwissen des Lesers überlassen zu sein. Um dieses Ziel zu erreichen, sind jedoch noch weitere Fortschritte hinsichtlich Effizienz und Nutzbarkeit von Theorembeweisern nötig.

Als Schritt in Richtung dieses Ziels beschreibt diese Dissertation eine neue, vollständig erweiterbare Theorembeweiser-Benutzerschnittstelle ("frontend") im Rahmen von Lean 4, der nächsten Version von Lean. Aufgabe dieser Benutzerschnittstelle ist die textuelle Beschreibung und Entgegennahme der Beweiseingabe in einer Syntax, die mehrere teils widersprüchliche Ziele optimieren sollte: Kompaktheit, Lesbarkeit für menschliche Benutzer und Eindeutigkeit in der Interpretation durch den Theorembeweiser. Da in der geschriebenen Mathematik eine umfangreiche Menge an verschiedenen Notationen existiert, die von Jahr zu Jahr weiter wächst und sich gleichzeitig zwischen verschiedenen Feldern, Autoren oder sogar einzelnen Arbeiten unterscheiden kann, muss solch eine Schnittstelle es Benutzern erlauben, sie jederzeit mit neuen, ausdrucksfähigen Notationen zu erweitern und ihnen mit flexiblen Regeln Bedeutung zuzuschreiben. Dieser Wunsch nach Flexibilität der Eingabesprache lässt sich weiterhin auch auf der Ebene der einzelnen Beweisschritte ("Taktiken") sowie höheren Ebenen der Beweis- und Programmorganisation wiederfinden.

Den Kernteil dieser gewünschten Erweiterbarkeit habe ich mit einem ausdrucksstarken Makrosystem für Lean realisiert, mit dem sich sowohl einfach Syntaxtransformationen ("syntaktischer Zucker") also auch komplexe, typgesteuerte Übersetzung in die Kernsprache des Beweisers ausdrücken lassen. Das Makrosystem basiert auf einem neuartigen Algorithmus für Makrohygiene, basierend auf dem der Lisp-Sprache Racket und von mir an die spezifischen Anforderungen von Theorembeweisern angepasst, dessen Aufgabe es ist zu gewährleisten, dass lexikalische Geltungsbereiche von Bezeichnern selbst für komplexe Makros wie intuitiv erwartet funktionieren. Besonders habe ich beim Entwurf des Makrosystems darauf geachtet, das System einfach zugänglich zu gestalten, indem mehrere Abstraktionsebenen bereitgestellt werden, die sich in ihrer Ausdrucksstärke unterscheiden, aber auf den gleichen fundamentalen Prinzipien wie der erwähnten Makrohygiene beruhen. Als ein Anwendungsbeispiel des Makrosystems beschreibe ich eine Erweiterung der aus Haskell bekannten "do"-Notation um weitere imperative Sprachfeatures. Die erweiterte Syntax ist in Lean 4 eingeflossen und hat grundsätzlich die Art und Weise verändert, wie sowohl Entwickler als auch Benutzer monadischen, aber auch puren Code schreiben.

Das Makrosystem stellt das "Herz" des erweiterbaren Frontends dar, ist gleichzeitig aber auch eng mit anderen Softwarekomponenten innerhalb der Benutzerschnittstelle verknüpft oder von ihnen abhängig. Ich stelle das gesamte Frontend und das umgebende Lean-System vor mit Fokus auf Teilen, an denen ich maßgeblich mitgewirkt habe. Schließlich beschreibe ich noch ein effizientes Referenzzählungsschema für funktionale Programmierung, welches eine Neuimplementierung von Lean in Lean selbst und damit das erweiterbare Frontend erst ermöglicht hat. Spezifische Optimierungen darin zur Wiederverwendung von Allokationen vereinen, ähnlich wie die erweiterte do-Notation, die Vorteile von imperativer und pur funktionaler Programmierung in einem neuen Paradigma, das ich "pure imperative Programmierung" nenne.

Interactive theorem provers (ITPs) are tools that can formally verify as well as help with writing computerized proofs, such as ones about mathematics or the correctness of programs. In recent years, extensive formalization projects have been completed using ITPs. The Lean theorem prover in particular has not only been used to formalize established theorems in mathematics but is now being utilized for formalizing novel mathematical topics as well. The goal of the Lean project is nothing less than to revolutionize how mathematicians work by making formalized proofs a realistic alternative to pen-and-paper proofs, removing the need for laborious step-wise refereeing and ensuring that all necessary proof steps are recorded accurately instead of requiring interpretation and implicit background knowledge from the reader. ... mehrMaking this goal a reality will require further breakthroughs in formalization efficiency and usability in order to close the convenience gap between pen and machine.

As one step towards this goal, this thesis discusses the design and implementation of a theorem prover frontend fully extensible by users as part of the latest version of Lean, Lean 4. The frontend is responsible for a particular aspect of formalization usability: accepting the user's input in a syntactical form that should optimize for multiple, partially contradictory goals: compactness, readability by humans, and unambiguous interpretability by the prover system. As the set of mathematical notations in use is extensive, growing every year, and often specific to a field, author, or even single paper, the frontend must allow users to extend it ad hoc with new, expressive notations with flexible interpretation rules. The same desire for flexible input syntax and interpretation rules can also be found at the level of individual proof steps ("tactics") and higher levels of organizing formalizations and programs.

The core part of this extensibility is an expressive macro system I have developed for Lean that covers both simple syntax transformations ("sugars") and complex, type-aware elaboration. The macro system is based on a novel hygiene algorithm inspired by that of the Lisp-family language Racket but custom-built for ITPs whose task is to ensure that lexical scoping works as intuitively expected even for complex macros. I have taken care in making the macro system approachable in general by providing multiple abstraction levels of increasing expressivity but based on the same fundamental principles. As one example use case of the macro system, I present an imperative extension of do notation known from Haskell and an implementation thereof as macros. The extended syntax has been integrated into Lean 4 and fundamentally changed the way both Lean developers as well as users write monadic and even pure Lean programs. I describe the notation's formal semantics and prove in Lean that this semantics coincides with the meaning of the program after macro expansion.

While the macro system is a central part of the extensible frontend, it is tightly connected to and dependent on other components. I give a description of the whole frontend and the greater Lean system, focusing on parts I have made significant contributions to. As motivation for this work, I review earlier attempts at extensibility of the frontend in Lean 3 and discuss lessons learned from them. Finally, I describe an efficient reference counting scheme for functional programming that has been instrumental in making the extensibility work in practice by allowing us to rewrite Lean in Lean itself. By transparently reusing allocations, the scheme, just like the extended do notation, combines benefits of imperative and pure functional programming into a new paradigm I call "pure imperative programming".