Constructing (Co)inductive Types via Large Sizes

1. Enunciato del Problema

Gli assistenti alla dimostrazione (ad esempio Agda, Lean, Rocq) si basano sulla teoria dei tipi dipendenti per garantire coerenza e decidibilità. Un requisito critico è che tutte le funzioni ricorsive debbano essere totali (terminanti) e tutte le funzioni corecursive debbano essere produttive.

• Limitazioni Attuali: La maggior parte dei sistemi impone la totalità tramite controlli sintattici (ad esempio, ricorsione strutturale o terminazione basata sul cambiamento di dimensione). Questi controlli sono spesso restrittivi, non modulari e sensibili al refactoring del codice.
• Tipi Dimensionati: Un'alternativa basata sui tipi utilizza le "dimensioni" (ordini) per annotare i tipi, permettendo di dimostrare la terminazione tramite induzione ben fondata sulla dimensione.
• L'Incoerenza di Agda: Agda implementa i tipi dimensionati ma introduce una dimensione massima ($\infty$) per definire il tipo induttivo/coinduttivo completo come sua approssimazione a $\infty$. Ciò porta a un'incoerenza logica: il sistema dimostra $\infty < \infty$, violando l'irriflessività dei buoni ordini stretti.
• Lavori Teorici Precedenti: I tentativi precedenti di risolvere questo problema utilizzando quantificatori parametrici (esistenziale $\exists$ per i tipi induttivi, universale $\forall$ per i tipi coinduttivi) erano limitati. Nello specifico, potevano costruire solo tipi induttivi a ramificazione finita perché il tipo dimensione era interpretato come l'insieme dei numeri naturali ($\mathbb{N}$), che manca degli ordinali limite necessari per le strutture a ramificazione infinita.

Obiettivo: Costruire una teoria dei tipi coerente che supporti tutti i tipi (co)induttivi (inclusi quelli a ramificazione infinita) utilizzando tipi dimensionati e quantificatori parametrici, senza fare affidamento su una dimensione massima incoerente.

2. Metodologia

Gli autori estendono la Teoria dei Tipi di Martin-Löf (MLTT) con caratteristiche specifiche per realizzare questa costruzione e ne dimostrano la coerenza tramite un modello di realizzabilità.

A. La Teoria dei Tipi Estesa

La teoria include le funzionalità standard della MLTT (universi, $\Sigma$, $\Pi$, tipi di identità) più:

1. Un Tipo di Dimensioni (Size):
   • Equipaggiato con uno zero ($0$) e un successore ($\uparrow i$).
   • Ordinato da un preordine ($\leq$) codificato come una mera proposizione.
   • Crucialmente: Size è un tipo grande (non nell'universo $U$), ma la quantificazione su di esso può produrre tipi piccoli.
2. Quantificatori Parametrici:
   • $\exists i. A(i)$ (Esistenziale): Rappresenta l'unione delle approssimazioni. I termini sono coppie $\langle s, a \rangle$, ma la dimensione $s$ è astratta (non può essere sottoposta a pattern matching). L'eliminazione è limitata ai tipi piccoli.
   • $\forall i. A(i)$ (Universale): Rappresenta l'intersezione delle approssimazioni. Le funzioni agiscono uniformemente su qualsiasi dimensione.
   • Assiomi di Parametricità: La teoria include assiomi che affermano che questi quantificatori commutano con i costruttori di tipi (ad esempio, $\Pi x:A. \exists i. B(x,i) \simeq \exists i. \Pi x:A. \exists j < i. B(x,j)$). Questo interiorizza l'idea che le dimensioni siano trattate uniformemente.
3. Induzione Ben Fondata (fix):
   • Un operatore di punto fisso che permette la definizione per induzione sulle dimensioni: $fix\ f : \forall i. A(i)$ dato $f : \forall i. ((\forall j < i. A(j)) \to A(i))$.
   • La regola $\beta$ è proposizionale (non definizionale) per preservare la decidibilità del controllo dei tipi.

B. Costruzione dei Tipi (Co)induttivi

Gli autori codificano i tipi (co)induttivi come algebre iniziali e coalgebre finali per endofunctor polinomiali ($F$).

1. Approssimazioni Ordinali: Definiscono funtori indicizzati per dimensione $F[\exists -]$ e $F[\forall -]$. Utilizzando l'operatore fix, costruiscono algebre iniziali ($\mu_3 F$) e coalgebre finali ($\nu_2 F$) per questi funtori indicizzati per dimensione. Questi rappresentano il tipo troncato a una dimensione specifica.
2. Tipi Completi tramite Quantificazione:
   • Tipi Induttivi: Definiti come $\mu F := \exists i. (\mu_3 F) i$. Il quantificatore esistenziale raccoglie tutti i termini limitati da alcuna dimensione.
   • Tipi Coinduttivi: Definiti come $\nu F := \forall i. (\nu_2 F) i$. Il quantificatore universale garantisce che i termini siano osservabili a qualsiasi profondità.
3. Gestione dei Tipi a Ramificazione Infinita: L'innovazione chiave consiste nel dimostrare che i funtori polinomiali commutano debolmente con il quantificatore esistenziale. Ciò richiede l'esistenza di ordinali limite (supremi di sequenze di dimensioni), il che è impossibile se le dimensioni sono semplicemente $\mathbb{N}$.

C. Dimostrazione di Coerenza: Modello di Realizzabilità

Per dimostrare che la teoria è coerente, gli autori costruiscono un modello di realizzabilità basato sul Topos Effettivo di Hyland.

• Interpretazione dei Tipi:
  • Tipi Piccoli: Interpretati come Relazioni di Equivalenza Parziali (PER) sui numeri naturali (dati computabili).
  • Tipi Grandi: Interpretati come Assemblaggi (insiemi con relazioni di computabilità).
• Interpretazione di Size:
  • Il tipo Size è interpretato come $\nabla \omega_1$, dove $\omega_1$ è il primo ordinale non numerabile (l'insieme di tutti gli ordinali numerabili).
  • Gli viene data la relazione di realizzabilità "piena", il che significa che i morfismi devono trattare tutte le dimensioni uniformemente (parametricità).
• Validazione:
  • Poiché $\omega_1$ contiene ordinali limite, il modello valida gli assiomi di parametricità richiesti per i tipi induttivi a ramificazione infinita.
  • Il modello valida l'Impredicatività (quantificare su tipi grandi produce tipi piccoli) e l'Unicità delle Dimostrazioni di Identità (UIP), anche se la sintassi non le assume. Ciò dimostra che la sintassi è compatibile con teorie più forti (come la Teoria dei Tipi Omotopica) senza esserne limitata.

3. Contributi Chiave

1. Costruzione Generale di Tipi (Co)induttivi: A differenza degli approcci parametrici precedenti limitati ai tipi a ramificazione finita, questo lavoro costruisce tutti i tipi (co)induttivi, inclusi quelli a ramificazione infinita (ad esempio, ordinali di Brouwer, modelli della teoria degli insiemi costruttiva).
2. Risoluzione dell'Incoerenza di Agda: Sostituendo la dimensione massima incoerente ($\infty$) con quantificatori parametrici su un tipo grande di dimensioni, gli autori forniscono un'alternativa coerente all'attuale implementazione di Agda.
3. Quantificatori Parametrici come Meccanismo: Dimostrano che interiorizzare la parametricità tramite $\exists$ e $\forall$ sulle dimensioni impone efficacemente l'astrazione necessaria per prevenire comportamenti non terminanti e incoerenze logiche.
4. Modello di Realizzabilità Robusto: La costruzione di un modello in cui Size è interpretato come $\omega_1$ fornisce una giustificazione semantica rigorosa per la teoria, dimostrando che gli assiomi di parametricità sono coerenti.

4. Risultati

• Correttezza Teorica: Il lavoro dimostra che l'algebra iniziale e la coalgebra finale per qualsiasi endofunctor polinomiale esistono all'interno della teoria estesa.
• Coerenza: Il modello di realizzabilità conferma che la teoria è coerente. Mostra che gli assiomi per i quantificatori parametrici valgono quando le dimensioni sono interpretate come un ordinale non numerabile.
• Compatibilità: Le costruzioni non fanno affidamento su UIP o impredicatività nella sintassi, rendendo i risultati compatibili con la Teoria dei Tipi Omotopica (HoTT), nonostante il modello soddisfi queste proprietà.

5. Significato e Lavori Futuri

• Impatto sugli Assistenti alla Dimostrazione: Questo lavoro offre una via per implementare tipi dimensionati negli assistenti alla dimostrazione (come Agda) senza l'incoerenza attuale causata dalla dimensione $\infty$. Permette un controllo di terminazione più modulare e composizionale.
• Comportamento Computazionale: Gli autori riconoscono che, sebbene la teoria sia coerente, la sintassi attuale manca di comportamento computazionale per gli assiomi di parametricità (essi sono assiomi, non regole di riduzione). I lavori futuri devono collegare questo alla parametricità interna (ad esempio, tramite tipi ponte o teoria dei tipi cubica) per garantire decidibilità e canonicità nella pratica.
• Decidibilità della Disuguaglianza: Il modello implica che la disuguaglianza sulle dimensioni non è generalmente decidibile (a causa dei supremi). Gli autori suggeriscono un approccio ibrido (disuguaglianza definizionale vs proposizionale) per l'implementazione pratica.
• Generalizzazione: Il modello potrebbe potenzialmente essere generalizzato ad altre algebre combinatorie parziali o integrato con effetti e univocità.

In sintesi, il lavoro colma con successo il divario tra la necessità teorica di tipi dimensionati parametrici e il requisito pratico di coerenza, permettendo la costruzione di complessi tipi (co)induttivi in un quadro teorico dei tipi solido.