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

Technische Samenvatting: Een door de machine gecontroleerd bewijs van consistentie voor impredicatieve Pure Type Systems

Probleem en Context
Het artikel behandelt de uitdagingen bij het mechaniseren van type-theorie, met een specifieke focus op de meta-theoretische eigenschappen van Pure Type Systems (PTS). Een centrale moeilijkheid bij het formaliseren van substitutie en $\beta$-reductie ligt in het afhandelen van variabele hernoeming om naam-capturing te voorkomen. Traditionele definities (bijv. Curry-Feys) vereisen wel-gegronde inductie op de lengte van termen vanwege niet-primitief recursieve hernoemingsstappen, wat mechanisering bemoeilijkt. Alternatieve benaderingen zoals de Bruijn-indices (dBI), locally nameless syntax, of Higher-Order Abstract Syntax (HOAS) bieden oplossingen, maar introduceren hun eigen nadelen: dBI is omslachtig voor de menselijke leesbaarheid; locally nameless syntax vereist welgevormdheidspredicaten die meta-theoretische resultaten "vervuilen"; en HOAS verhindert vaak het genereren van uitvoerbare code of het formuleren van beslisbaarheidsvragen.

De auteurs beoogden de haalbaarheid te toetsen van een aanpak die klassieke syntaxis (met gebruik van benoemde variabelen) behoudt terwijl zij gebruikmaken van Stoughton's simultane substituties. Deze methode voert de hernoeming van gebonden variabelen simultaan uit met de substitutie via een enkele structurele recursie, waardoor de noodzaak voor wel-gegronde inductie op termlengte voor de meeste bewijzen wordt vermeden.

Methodologie
De ontwikkeling is volledig machinaal gecontroleerd met behulp van Agda (v2.6.2.2) en de standaardbibliotheek. De methodologie rust op de volgende kerncomponenten:

1. Stoughton's Simultane Substituties: Substituties worden gedefinieerd als functies van variabelen naar $\lambda$-termen ($Sub = V \to \Lambda$). De operatie $M \bullet \sigma$ wordt gedefinieerd door structurele recursie. Voor $\lambda$-abstracties en $\Pi$-types wordt de gebonden variabele hernoemd naar een verse naam $y$, gekozen door een functie $X$, en wordt de substitutie bijgewerkt om de oude gebonden variabele naar deze nieuwe naam te mappen. Dit zorgt ervoor dat er slechts één recursieve aanroep nodig is per abstractie, wat de primitieve recursiviteit handhaaft.
2. $\alpha$-Commutatieve Relaties: De auteurs ontwikkelen een theorie van relaties die commuteert met $\alpha$-conversie. Een relatie $S$ is $\alpha$-commutatief als $M \sim_\alpha N$ en $N S P$ impliceert dat er een $Q$ bestaat waarvoor $M S Q$ en $Q \sim_\alpha P$ gelden. Dit kader stelt de auteurs in staat om confluentie tot $\alpha$-conversie helder te behandelen, waardoor duplicatie van lemma's die vaak bij andere formalisaties voorkomt, wordt vermeden.
3. Takahashi's Revisie van het Confluentiebewijs: In plaats van het oorspronkelijke bewijs van Tait en Martin-Löf, gebruikt het artikel de revisie van Takahashi met behulp van parallelle reductie ($\Rightarrow$). De auteurs definiëren parallelle reductie zonder expliciete $\alpha$-conversieregels in de reductiestappen, waarbij zij vertrouwen op de pentagon-eigenschap (een generalisatie van de diamant-eigenschap tot $\alpha$-conversie) om confluentie te bewijzen.
4. Normalisatie-aanname: Het bewijs van consistentie gaat ervan uit dat het specifieke PTS in kwestie normaliserend is (elke goed-getypeerde term is zwak normaliserend). De auteurs merken op dat het bewijzen van normalisatie voor impredicatieve systemen binnen Agda waarschijnlijk onmogelijk is vanwege het gebrek aan impredicativiteit in de meta-taal van Agda.

Kernbijdragen
Het artikel presenteert formele bewijzen voor drie belangrijke meta-theoretische eigenschappen:

1. Confluentie van $\beta$-reductie: De auteurs bewijzen de Church-Rosser-stelling voor de onderliggende syntaxis van PTS. Door gebruik te maken van de theorie van $\alpha$-commutatieve relaties en Takahashi's parallelle reductie, stellen zij vast dat de ster-sluiting van parallelle reductie samenvalt met veel-staps $\beta$-reductie en de pentagon-eigenschap bevredigt.
2. Subject Reduction (SR): Het artikel formaliseert het behoud van typering onder reductie. Volgens ideeën van McKinna en Pollack breiden de auteurs reducties uit naar contexten en bewijzen zij een simultane stelling betreffende de geldigheid van contexten en het behoud van typering voor subjects. Dit omvat het bewijzen van product-injectiviteit, een cruciaal lemma voor inversie.
3. Consistentie voor Impredicatieve PTS: De auteurs bewijzen dat voor een specifieke subklasse van impredicatieve PTS (die voldoet aan specifieke axioma's en regels, zoals $(\ast, \square) \in \mathcal{A}$ en $(\square, \ast, \ast) \in \mathcal{R}$) de type $\Pi[x : s]x$ (die de onwaarheid representeert onder Curry-Howard) onbewoonbaar is in de lege context. Het bewijs breidt het pen-en-papier bewijs van Coquand voor de Calculus of Constructions (CC) uit. Het steunt op de soundheid en volledigheid van inductief gedefinieerde normale en neutrale vormen, inversie-lemma's en de aangenomen normalisatie-eigenschap.

Resultaten en Evaluatie

• Omvang van de Formalisering: De gehele ontwikkeling bestaat uit ongeveer 4.300 regels code (LoC), waarvan 3.000 LoC toe te schrijven zijn aan het onderliggende framework van Stoughton's substituties en de PTS-syntaxis uit eerder werk.
• Vergelijking: De auteurs vergelijken hun werk met formalisaties met de Bruijn-indices (Barras en Werner, ~2.900 LoC) en locally nameless syntax (Aydemir et al., ~4.800 LoC). Zij beargumenteren dat hun aanpak qua omvang vergelijkbaar is, maar een superieure transparantie biedt met betrekking tot de gebruikte syntaxis, aangezien het de klassieke notatie nauwgezet volgt (bijv. het zwakheidslemma ziet er bijna identiek uit als de klassieke notatie).
• Haalbaarheid: De resultaten suggereren dat de aanpak met klassieke syntaxis en simultane substituties haalbaar is voor afhankelijke type-theorieën. De auteurs merken op dat slechts een handvol lemma's wel-gegronde inductie vereisten en dat de code-omvang niet is "geëxplodeerd".

Betekenis en Claims
Het artikel claimt dat de aanpak met Stoughton's substituties een "helderdere presentatie en behandeling" biedt van meta-theoretische problemen vergeleken met soortgelijke ontwikkelingen, met name wat betreft de afhandeling van $\alpha$-conversie. De auteurs stellen dat hun oplossing transparanter is voor menselijke lezers dan de de Bruijn- of locally nameless-benaderingen, omdat het de "notatieruis" vermijdt van het openen van termen en het handmatig beheren van verse parameters.

De betekenis van het werk ligt in het aantonen dat een machinaal gecontroleerd bewijs van consistentie voor impredicatieve systemen haalbaar is zonder de klassieke syntaxis op te geven, mits normalisatie wordt aangenomen. De auteurs erkennen bescheiden dat een volledige mechanisering van normalisatie voor impredicatieve theorieën waarschijnlijk onmogelijk is in Agda vanwege de beperkingen in de bewijstheoretische kracht (implicaties van de onvolledigheidsstelling van Gödel), maar het consistentiebewijs zelf blijft een substantiële stap richting correct-door-constructie type-checking algoritmen voor dergelijke systemen. Het werk dient als een validatie van de bruikbaarheid van het framework voor toekomstige formalisaties van afhankelijke type-theorieën.