A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism

1. Il Problema

Il lavoro affronta la necessità di fornire caratterizzazioni astratte e unificate delle teorie dei tipi, in particolare quelle con polimorfismo esplicito degli universi.

• Limiti degli approcci tradizionali: Le presentazioni standard delle teorie dei tipi si basano su grammatiche e regole di inferenza. Questo approccio richiede scelte sintattiche specifiche e include numerose regole di "bookkeeping" (gestione della sintassi), rendendo difficile dimostrare l'equivalenza tra diverse formulazioni o provare proprietà metateoriche generali (come la congettura dell'inizialità).
• La Congettura di Inizialità di Voevodsky: Voevodsky ha proposto che ogni sistema di deduzione formale possa essere specificato come una teoria quasi-equazionale, la cui categoria dei modelli possiede un oggetto iniziale (il modello dei termini). L'obiettivo è definire una classe generale di teorie dei tipi dipendenti e sviluppare una metateoria generica per essa.
• Sfida specifica: Gestire il polimorfismo degli universi in modo esplicito, dove i livelli degli universi non formano un tipo interno ma sono gestiti tramite giudizi esterni o variabili di livello, richiede una struttura matematica che possa catturare sia la gerarchia degli universi che la loro interazione con i costruttori di tipi (come prodotti dipendenti).

2. Metodologia

Gli autori adottano un approccio basato sulla Logica Categorica, utilizzando due strumenti principali:

1. Teorie Algebriche Generalizzate (GATs - Generalized Algebraic Theories): Introdotte da Cartmell, le GATs generalizzano le teorie algebriche multisorte permettendo a simboli di tipo e operatori di avere tipi dipendenti. Le GATs catturano la struttura logica essenziale senza i dettagli sintattici ridondanti.
2. Categorie con Famiglie (CwF - Categories with Families): Un modello categorico per le teorie dei tipi dipendenti che include contesti, morfismi di contesto (sostituzioni), tipi e termini.

Strategia di costruzione:

• Gli autori definiscono due GATs specifiche che corrispondono a due varianti della teoria dei tipi di Martin-Löf:
  • $\Sigma_{tower}$: Per la teoria con una torre esterna di universi (indici naturali esterni).
  • $\Sigma_{up}$: Per la teoria con polimorfismo esplicito degli universi (universi indicizzati internamente per livelli).
• Invece di lavorare direttamente con la sintassi, definiscono le teorie come insiemi di simboli di sorta, operatori ed equazioni.
• Sfruttano il risultato precedente (in [6]) secondo cui per ogni GAT finita esiste un modello iniziale costruita genericamente, che corrisponde alla teoria dei termini della teoria logica.

3. Contributi Chiave

A. La GAT per la Torre Esterna di Universi ($\Sigma_{tower}$)

• Struttura: Estende la GAT delle CwF con strutture per i formatori di tipi standard ($\Pi, \Sigma, N_0, N_1, N_2, N, W, Id$) e una torre di universi $U_l$ indicizzata da numeri naturali esterni $l \in \mathbb{N}$.
• Operazioni: Include operatori per la decodifica ($T_l$), la formazione di codici per i prodotti dipendenti ($\Pi_{l,l'}$) e, opzionalmente, operatori di cumulatività ($T^m_l$) per sollevare termini da un universo a uno più grande.
• Natura Infinitaria: Poiché la torre è infinita, $\Sigma_{tower}$ è una GAT infinitaria. Gli autori mostrano come costruire il modello iniziale come un'unione di modelli finiti troncati.

B. La GAT per il Polimorfismo Esplicito ($\Sigma_{up}$)

Questa è la parte più innovativa del lavoro, che gestisce i livelli degli universi come parte della teoria stessa.

• Cwf Indicizzato per Livelli: Invece di una singola CwF, il modello è una presheaf $P: C^{op} \to CwF$, dove la base $C$ è una ucwf (unityped cwf) dei livelli.
  • La ucwf dei livelli gestisce i giudizi $l \text{ level}$ e $l = l'$.
  • Include operatori per il "next level" ($l^+$) e il join ($l \vee l'$), formando un semilattice superiore.
• Sorte di Uguaglianza dei Livelli ($leq$): Poiché le GATs non permettono assunzioni di uguaglianza come precondizioni, gli autori introducono una nuova sorta $leq_n(l, l')$ per rappresentare l'uguaglianza proposizionale tra livelli. Questo permette di esprimere vincoli come $l < m$ (definito come $l^+ \vee m = m$) all'interno della teoria.
• Prodotti Indicizzati per Livelli: Introducono operatori per la quantificazione universale sui livelli $[\alpha]A$, con astrazione $\langle \alpha \rangle a$ e applicazione $a_l$, permettendo di trattare famiglie di tipi dipendenti da un livello.
• Finitezza: A differenza di $\Sigma_{tower}$, $\Sigma_{up}$ è una GAT finitaria, il che semplifica la costruzione del modello iniziale.

C. Costruzione dei Modelli Iniziali

• Sostituzione Esplicita vs Implicita: Gli autori confrontano la costruzione del modello iniziale basata su una sintassi con sostituzione esplicita (costruita direttamente dalla GAT) con la costruzione basata su una sintassi con sostituzione implicita (la teoria dei tipi standard con regole di inferenza).
• Dimostrazione di Inizialità: Mostrano che il modello dei termini della teoria dei tipi (con sostituzione implicita) è isomorfo all'esternalizzazione del modello iniziale della GAT. Questo conferma che la GAT cattura correttamente la struttura astratta della teoria dei tipi.

4. Risultati

1. Caratterizzazione Astratta: Le teorie $TT_{tower}$ (torre esterna) e $TT_{up}$ (polimorfismo esplicito) sono caratterizzate come modelli iniziali delle rispettive GATs ($\Sigma_{tower}$ e $\Sigma_{up}$).
2. Unificazione: Viene dimostrato che è possibile astrarre dai dettagli grammaticali e dalle regole di inferenza specifiche, focalizzandosi sulla struttura categoriale di alto livello.
3. Gestione dei Livelli: Viene fornita una formalizzazione rigorosa del polimorfismo esplicito degli universi all'interno del quadro delle GATs, risolvendo il problema di come gestire vincoli di ordine tra livelli ($l < m$) senza ricorrere a giudizi esterni.
4. Connessione con la Congettura di Voevodsky: Il lavoro fornisce un passo concreto verso la realizzazione della congettura di inizialità, mostrando come teorie complesse possano essere definite come modelli iniziali di strutture algebriche ben definite.

5. Significato e Impatto

• Avanzamento della Logica Categorica: Il lavoro funge da studio di caso per un approccio uniforme alla logica categorica basato su GATs e CwF, estendendo la portata oltre le semplici teorie dei tipi dipendenti.
• Fondamenti per la Matematica Univalente: Supporta il progetto di Voevodsky sulle Fondazioni Univalenti, fornendo strumenti per definire classi generali di teorie dei tipi e sviluppare metateorie generiche, riducendo la dipendenza da implementazioni sintattiche specifiche.
• Flessibilità e Generalità: L'approccio permette di trattare sistemi logici diversi (logica predicativa non tipata, logica predicativa tipata, ecc.) come variazioni di CwF indicizzate, tutte formalizzabili come GATs.
• Relazione con Altri Formalismi: Il paper colloca le GATs in relazione con i Framework Logici (come LF o Dedukti) e con i tipi induttivi-quotient (QIITs), suggerendo che le GATs offrono una via intermedia che bilancia espressività e struttura algebrica.

In sintesi, il paper dimostra che le teorie dei tipi con polimorfismo esplicito degli universi possono essere comprese e studiate non come insiemi di regole sintattiche, ma come oggetti algebrici iniziali in categorie di modelli, offrendo una base solida per la verifica formale e lo sviluppo di nuovi sistemi logici.