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

Sintesi Tecnica: Una prova verificata da macchina della coerenza per i Sistemi di Tipi Puri Impredicativi

Problema e Contesto
Il saggio affronta le sfide della meccanizzazione della teoria dei tipi, concentrandosi in particolare sulle proprietà meta-teoretiche dei Sistemi di Tipi Puri (PTS). Una difficoltà centrale nella formalizzazione della sostituzione e della $\beta$-riduzione risiede nella gestione della rinomina delle variabili per prevenire la cattura dei nomi. Le definizioni tradizionali (ad esempio, Curry-Feys) richiedono l'induzione ben fondata sulla lunghezza del termine a causa dei passaggi di rinomina non primitivamente ricorsivi, rendendo difficile la meccanizzazione. Approcci alternativi come gli indici di de Bruijn (dBI), la sintassi localmente nominativa (locally nameless syntax) o l'Astrazione Sintattica di Ordine Superiore (HOAS) offrono soluzioni, ma introducono i propri svantaggi: il dBI è ingombrante per la leggibilità umana; la sintassi localmente nominativa richiede predicati di ben-formità che "inquinano" i risultati meta-teoretici; l'HOAS spesso impedisce la generazione di codice eseguibile o la formulazione di quesiti di decidibilità.

Gli autori mirano a valutare la fattibilità di un approccio che mantenga la sintassi classica (utilizzando variabili nominate) avvalendosi al contempo delle sostituzioni simultanee di Stoughton. Questo metodo esegue la rinomina delle variabili legate simultaneamente alla sostituzione tramite una singola ricorsione strutturale, evitando la necessità di induzione ben fondata sulla lunghezza del termine per la maggior parte delle prove.

Metodologia
Lo sviluppo è interamente verificato da macchina utilizzando Agda (v2.6.2.2) e la sua libreria standard. La metodologia si basa sui seguenti componenti principali:

1. Sostituzioni Simultanee di Stoughton: Le sostituzioni sono definite come funzioni da variabili a $\lambda$-termini ($Sub = V \to \Lambda$). L'operazione $M \bullet \sigma$ è definita per ricorsione strutturale. Per le astrazioni $\lambda$ e i tipi $\Pi$, la variabile legata viene rinominata in un nuovo nome $y$ scelto da una funzione $X$, e la sostituzione viene aggiornata per mappare la vecchia variabile legata a questo nuovo nome. Ciò garantisce che sia necessaria una sola chiamata ricorsiva per ogni astrazione, mantenendo la primitività ricorsiva.
2. Relazioni $\alpha$-commutative: Gli autori sviluppano una teoria di relazioni che commutano con la $\alpha$-conversione. Una relazione $S$ è $\alpha$-commutativa se $M \sim_\alpha N$ e $N S P$ implica l'esistenza di un $Q$ tale che $M S Q$ e $Q \sim_\alpha P$. Questo framework permette agli autori di trattare la confluenza fino alla $\alpha$-conversione in modo pulito, evitando la duplicazione di lemmi spesso presente in altre formalizzazioni.
3. Revisione di Takahashi della Prova di Confluenza: Inve sostituzione alla prova originale di Tait e Martin-Löf, il saggio impiega la revisione di Takahashi utilizzando la riduzione parallela ($\Rightarrow$). Gli autori definiscono la riduzione parallela senza esplicite regole di $\alpha$-conversione nei passaggi di riduzione, affidandosi invece alla proprietà del pentagono (una generalizzazione della proprietà del diamante fino alla $\alpha$-conversione) per dimostrare la confluenza.
4. Assunzione di Normalizzazione: La prova di coerenza assume che il particolare PTS in esame sia normalizzante (ogni termine ben tipizzato è debolmente normalizzante). Gli autori osservano che dimostrare la normalizzazione per sistemi impredicativi all'interno di Agda è probabilmente impossibile a causa della mancanza di impredicatività nel meta-linguaggio di Agda.

Contributi Chiave
Il saggio presenta prove formali per tre proprietà meta-teoretiche principali:

1. Confluenza della $\beta$-riduzione: Gli autori dimostrano il teorema di Church-Rosser per la sintassi sottostante del PTS. Utilizzando la teoria delle relazioni $\alpha$-commutative e la riduzione parallela di Takahashi, stabiliscono che la chiusura stella della riduzione parallela coincide con la $\beta$-riduzione a molti passi e soddisfa la proprietà del pentagono.
2. Riduzione del Soggetto (SR): Il saggio formalizza la preservazione della tipizzazione sotto riduzione. Seguendo le idee di McKinna e Pollack, gli autori estendono le riduzioni ai contesti e dimostrano un teorema simultaneo riguardante la validità dei contesti e la preservazione della tipizzazione per i soggetti. Ciò include la dimostrazione dell'injetività del prodotto, un lemma cruciale per l'inversione.
3. Coerenza per i PTS Impredicativi: Gli autori dimostrano che per una specifica sottoclasse di PTS impredicativi (quelli che soddisfano assiomi e regole specifiche, come $(\ast, \square) \in \mathcal{A}$ e $(\square, \ast, \ast) \in \mathcal{R}$), il tipo $\Pi[x : s]x$ (che rappresenta la falsità secondo il Curry-Howard) è privo di abitanti nel contesto vuoto. La prova estende la dimostrazione cartacea di Coquand per il Calculus of Constructions (CC). Essa si basa sulla correttezza e completezza delle forme normali e neutre definite induttivamente, sui lemmi di inversione e sull'assunta proprietà di normalizzazione.

Risultati e Valutazione

• Dimensione della Formalizzazione: L'intero sviluppo comprende circa 4.300 righe di codice (LoC), di cui 3.000 LoC sono attribuite al framework sottostante delle sostituzioni di Stoughton e della sintassi PTS derivanti da lavori precedenti.
• Confronto: Gli autori confrontano il proprio lavoro con le formalizzazioni che utilizzano indici di de Bruijn (Barras e Werner, ~2.900 LoC) e la sintassi localmente nominativa (Aydemir et al., ~4.800 LoC). Argomentano che il loro approccio ha una dimensione comparabile ma offre una trasparenza superiore riguardo alla sintassi utilizzata, poiché rispecchia da vicino le presentazioni matematiche informali (ad esempio, il lemma di indebolimento appare quasi identico alla notazione classica).
• Fattibilità: I risultati suggeriscono che l'approccio che utilizza la sintassi classica e le sostituzioni simultanee è fattibile per le teorie dei tipi dipendenti. Gli autori notano che solo un paio di lemmi hanno richiesto l'induzione ben fondata e che la dimensione del codice non è "esplosa".

Significato e Rivendicazioni
Il saggio sostiene che l'approccio utilizzando le sostituzioni di Stoughton offre una "presentazione e un trattamento più chiari" dei problemi meta-teoretici rispetto ad altri sviluppi simili, in particolare per quanto riguarda la gestione della $\alpha$-conversione. Gli autori affermano che la loro soluzione è più trasparente per i lettori umani rispetto agli approcci localmente nominativi o di de Bruijn, poiché evita il "disordine notazionale" dell'apertura dei termini e la gestione manuale dei parametri freschi.

Il significato del lavoro risiede nel dimostrare che una prova verificata da macchina della coerenza per i sistemi impredicativi è realizzabile senza abbandonare la sintassi classica, a condizione che la normalizzazione sia assunta. Gli autori riconoscono con modestia che una completa meccanizzazione della normalizzazione per le teorie impredicative è probabilmente impossibile in Agda a causa delle limitazioni della forza dimostrativa (implicazioni del teorema di incompletezza di Gödel), ma la prova di coerenza stessa rimane un passo sostanziale verso algoritmi di type-checking corretti per costruzione per tali sistemi. Il lavoro serve come validazione dell'utilità del framework per future formalizzazioni di teorie dei tipi dipendenti.