A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

Technisches Resümee: Ein maschinell überprüfter Beweis der Konsistenz für impredikative reine Typensysteme

Problem und Kontext
Die Arbeit befasst sich mit den Herausforderungen der Mechanisierung der Typentheorie, wobei der Schwerpunkt auf den metatheoretischen Eigenschaften von reinen Typensystemen (Pure Type Systems, PTS) liegt. Eine zentrale Schwierigkeit bei der Formalisierung von Substitution und $\beta$-Reduktion liegt im Umgang mit der Umbenennung von Variablen, um Namenskollisionen (Name Capture) zu vermeiden. Traditionelle Definitionen (z. B. Curry-Feys) erfordern eine wohldefinierte Induktion über die Termlänge aufgrund der nicht-primitiv-rekursiven Umbenennungsschritte, was die Mechanisierung erschwert. Alternative Ansätze wie de Bruijn-Indizes (dBI), lokal namenlose Syntax oder Higher-Order Abstract Syntax (HOAS) bieten Lösungen an, bringen jedoch ihre eigenen Nachteile mit sich: dBI ist für die menschliche Lesbarkeit umständlich; lokal namenlose Syntax erfordert Prädikate der Wohltypheit, die metatheoretische Resultate „verunreinigen“; und HOAS verhindert oft die Generierung von ausführbarem Code oder die Formulierung von Entscheidbarkeitsfragen.

Die Autoren untersuchen die Machbarkeit eines Ansatzes, der die klassische Syntax (unter Verwendung benannter Variablen) beibehält und gleichzeitig Stoughtons simultane Substitutionen nutzt. Diese Methode führt die Umbenennung gebundener Variablen simultan zur Substitution über eine einzige strukturelle Rekursion durch, wodurch die Notwendigkeit einer wohldefinierten Induktion über die Termlänge für die meisten Beweise vermieden wird.

Methodik
Die Entwicklung wurde vollständig unter Verwendung von Agda (v2.6.2.2) und der Standardbibliothek maschinell überprüft. Die Methodik stützt sich auf die folgenden Kernkomponenten:

1. Stoughtons simultane Substitutionen: Substitutionen werden als Funktionen von Variablen zu $\lambda$-Termen definiert ($Sub = V \to \Lambda$). Die Operation $M \bullet \sigma$ wird durch strukturelle Rekursion definiert. Für $\lambda$-Abstraktionen und $\Pi$-Typen wird die gebundene Variable in einen frischen Namen $y$ umbenannt, der durch eine Funktion $X$ gewählt wird, und die Substitution wird aktualisiert, um die alte gebundene Variable auf diesen neuen Namen abzubilden. Dies stellt sicher, dass pro Abstraktion nur ein einziger rekursiver Aufruf benötigt wird, wodurch die Primitiv-Rekursivität gewahrt bleibt.
2. $\alpha$-kommutative Relationen: Die Autoren entwickeln eine Theorie von Relationen, die mit der $\alpha$-Konversion kommutieren. Eine Relation $S$ ist $\alpha$-kommutativ, wenn $M \sim_\alpha N$ und $N S P$ impliziert, dass es ein $Q$ gibt, sodass $M S Q$ und $Q \sim_\alpha P$ gilt. Dieser Rahmen ermöglicht es den Autoren, Konfluenz bis auf $\alpha$-Konversion sauber zu behandeln und so die Duplikation von Lemmata zu vermeiden, wie sie oft in anderen Formalisierungen vorkommt.
3. Takahashis Revision des Konfluenzbeweises: Anstatt des ursprünglichen Beweises von Tait und Martin-Löf verwendet das Paper die Revision von Takahashi mittels paralleler Reduktion ($\Rightarrow$). Die Autoren definieren die parallele Reduktion ohne explizite $\alpha$-Konversionsregeln in den Reduktionsschritten und verlassen sich stat stattdessen auf die Pentagon-Eigenschaft (eine Verallgemeinerung der Diamant-Eigenschaft bis auf $\alpha$-Konversion), um Konfluenz zu beweisen.
4. Normalisierungsannahme: Der Beweis der Konsistenz setzt voraus, dass das spezifische PTS unter Betrachtung normalisierend ist (jeder wohltypierte Term ist schwach normalisierend). Die Autoren merken an, dass der Beweis der Normalisierung für impredikative Systeme innerhalb von Agda aufgrund der fehlenden Impredikativität der Metasprache wahrscheinlich unmöglich ist.

Wesentliche Beiträge
Das Paper präsentiert formale Beweise für drei metatheoretische Eigenschaften:

1. Konfluenz der $\beta$-Reduktion: Die Autoren beweisen das Church-Rosser-Theorem für die zugrunde liegende Syntax von PTS. Durch die Nutzung der Theorie der $\alpha$-kommutativen Relationen und der parallelen Reduktion nach Takahashi etablieren sie, dass der Stern-Abschluss der parallelen Reduktion mit der mehrstufigen $\beta$-Reduktion übereinstimmt und die Pentagon-Eigenschaft erfüllt.
2. Subject Reduction (SR): Das Paper formalisiert die Erhaltung der Typisierung unter Reduktion. In Anlehnung an Ideen von McKinna und Pollack erweitern die Autoren die Reduktionen auf Kontexte und beweisen ein simultanes Theorem bezüglich der Gültigkeit von Kontexten und der Erhaltung der Typisierung für Subjekte. Dies beinhaltet den Beweis der Produkt-Injektivität, ein entscheidendes Lemma für die Inversion.
3. Konsistenz für impredikative PTS: Die Autoren beweisen, dass für eine spezifische Unterklasse von impredikativen PTS (die bestimmte Axiome und Regeln erfüllen, wie $(\ast, \square) \in \mathcal{A}$ und $(\square, \ast, \ast) \in \mathcal{R}$) der Typ $\Pi[x : s]x$ (der unter Curry-Howard die Falschheit repräsentiert) im leeren Kontext unbewohnbar ist. Der Beweis erweitert Coquands handschriftlichen Beweis für den Kalkül der Konstruktionen (CC). Er stützt sich auf die Korrektheit und Vollständigkeit induktiv definierter normaler und neutraler Formen, Inversionslemmata und die angenommene Normalisierungseigenschaft.

Ergebnisse und Evaluierung

• Größe der Formalisierung: Die gesamte Entwicklung umfasst etwa 4.300 Zeilen Code (LoC), wovon 3.000 LoC auf das zugrunde liegende Framework der Stoughton-Substitutionen und der PTS-Syntax aus vorangegangenen Arbeiten entfallen.
• Vergleich: Die Autoren vergleichen ihre Arbeit mit Formalisierungen unter Verwendung von de Bruijn-Indizes (Barras und Werner, ~2.900 LoC) und lokal namenloser Syntax (Aydemir et al., ~4.800 LoC). Sie argumentieren, dass ihr Ansatz in der Größe vergleichbar ist, aber eine überlegene Transparenz hinsichtlich der verwendeten Syntax bietet, da er der informellen mathematischen Darstellung (z. B. sieht das Schwächungslemma fast identisch aus) sehr nahe kommt.
• Machbarkeit: Die Ergebnisse legen nahe, dass der Ansatz unter Verwendung klassischer Syntax und simultaner Substitutionen für abhängige Typentheorien machbar ist. Die Autoren stellen fest, dass nur wenige Lemmata eine wohdefinierte Induktion erforderten und die Codegröße nicht „explodierte“.

Bedeutung und Ansprüche
Das Paper behauptet, dass der Ansatz der Stoughton-Substitutionen eine „klarere Präsentation und Behandlung“ metatheoretischer Probleme im Vergleich zu ähnlichen Entwicklungen bietet, insbesondere hinsichtlich des Umgangs mit der $\alpha$-Konversion. Die Autoren behaupten, dass ihre Lösung für menschliche Leser transparenter ist als de Bruijn- oder lokal namenlose Ansätze, da sie den „notationalen Ballast“ des Öffnen von Termen und das manuelle Verwalten frischer Parameter vermeidet.

Die Bedeutung der Arbeit liegt darin, zu zeigen, dass ein maschinell überprüfter Beweis der Konsistenz für impredikative Systeme möglich ist, ohne die klassische Syntax aufzugeben, sofern die Normalisierung angenommen wird. Die Autoren räumen bescheiden ein, dass eine vollständige Mechanisierung der Normalisierung für impredikative Theorien in Agda aufgrund der beschränkten Beweiskraft (Implikationen des Gödelschen Unvollständigkeitssatzes) wahrscheinlich unmöglich ist, der Konsistenzbeweis selbst jedoch ein bedeutender Schritt hin zu korrekten-durch-Konstruktion Typisierungsalgorithmen für solche Systeme bleibt. Die Arbeit dient als Validierung der Nützlichkeit des Frameworks für zukünftige Formalisierungen abhängiger Typentheorien.