💻 computer science

Are Dependent Types in Set Theory Feasible?

Questo articolo presenta un'implementazione meccanizzata nel proof assistant Lisa di tipi dipendenti e gerarchie di universi all'interno della teoria degli insiemi di Tarski-Grothendieck, dimostrando come un approccio basato sulla corrispondenza tipi-insiemi consenta un ragionamento automatizzato e completamente verificato per il controllo dei tipi.

Autori originali: Yunsong Yang, Simon Guilloud, Viktor Kunčak

Pubblicato 2026-03-16

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Yunsong Yang, Simon Guilloud, Viktor Kunčak

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di avere due modi completamente diversi per costruire una casa.

Il primo metodo, quello che usano da oltre un secolo i matematici classici, è come costruire con mattoni rossi e malta. È il sistema della Teoria degli Insiemi (Set Theory). È solido, semplice da capire: un insieme è solo una scatola che contiene oggetti. Se vuoi dire che "Mario è un uomo", dici semplicemente che "Mario" è dentro la scatola "Uomini". È la base su cui è costruita quasi tutta la matematica moderna.

Il secondo metodo, quello usato dai moderni assistenti di prova come Lean o Rocq, è come costruire con Lego colorati e intelligenti. Questo è il Calcolo dei Tipi Dipendenti (Dependent Type Theory). Qui, ogni pezzo Lego non è solo un pezzo, ma ha un'etichetta che dice esattamente dove può essere attaccato. Se provi a mettere un pezzo rosso in un buco blu, il sistema ti dice subito: "Ehi, non va bene!". Questo rende la costruzione incredibilmente sicura e automatica, ma è anche molto complicata da costruire e controllare dall'interno.

Il problema:
Negli ultimi anni, molti matematici hanno iniziato a preferire i "Lego intelligenti" (i tipi dipendenti) perché sono più facili da usare per scrivere prove complesse. Tuttavia, c'è un problema: i "Lego" sono un sistema chiuso e complicato. Se vuoi tradurre una prova fatta con i Lego in un sistema di mattoni (o viceversa), è come cercare di tradurre un linguaggio fatto di suoni in un linguaggio fatto di immagini: è difficile e spesso si perdono dettagli.

La soluzione di questo paper:
Gli autori di questo articolo (Yunsong Yang, Simon Guilloud e Viktor Kunčak) hanno avuto un'idea geniale: "Perché non costruiamo i Lego intelligenti dentro la casa dei mattoni?"

Hanno creato un sistema che permette di usare le regole potenti e flessibili dei "tipi dipendenti" (i Lego) ma facendole funzionare all'interno della solida e semplice teoria degli insiemi (i mattoni).

Ecco come funziona, spiegato con metafore semplici:

1. I "Tipi" sono solo "Scatole"

Nel loro sistema, quando dici "Questo numero è un intero", non stai usando una magia complessa. Stai semplicemente dicendo: "Questo numero è dentro la scatola chiamata 'Interi'".
Hanno preso le regole complesse dei tipi dipendenti e le hanno tradotte in regole semplici di "scatole dentro scatole".

L'analogia: Immagina che ogni tipo di dato (un numero, una lista, una funzione) sia una scatola. Una "funzione" è una scatola che prende un oggetto da una scatola e ne produce un altro. Tutto è gestito con la logica semplice di "cosa c'è dentro cosa".

2. Le "Universi" (Le Scatole Giganti)

C'era un problema: nella teoria degli insiemi classica, non puoi avere una scatola che contiene tutte le scatole (diventerebbe troppo grande e creerebbe paradossi). Ma nei tipi dipendenti, hai bisogno di livelli infiniti: una scatola che contiene altre scatole, che ne contengono altre ancora.

La soluzione: Hanno usato un trucco matematico chiamato "Axioma di Tarski-Grothendieck". Immagina di avere una serie infinita di magazzini giganti. Ogni magazzino contiene tutte le scatole necessarie per un certo livello di complessità. Se hai bisogno di una scatola più grande, vai nel magazzino successivo. Questo permette di avere livelli infiniti senza rompere le regole della logica.

3. Il "Traduttore Automatico" (Il Tattico)

Il pezzo più bello è che hanno costruito un robot traduttore (chiamato Typecheck.prove).

Come funziona: Tu scrivi una prova complessa usando la sintassi elegante dei tipi dipendenti (come se stessi usando i Lego).
Cosa fa il robot: Il robot prende la tua prova, la smonta pezzo per pezzo, la traduce in una serie di affermazioni semplici sui mattoni (teoria degli insiemi) e poi costruisce una prova formale che il sistema di base può verificare.
Il risultato: Alla fine, ottieni una prova che è garantita al 100% perché è basata sulle regole solide dei mattoni, ma tu hai lavorato con la facilità dei Lego.

Perché è importante?

Immagina che il mondo della matematica sia diviso in due città: la Città dei Mattoni (vecchia scuola, solida) e la Città dei Lego (moderna, potente).
Fino a oggi, se vivevi nella Città dei Lego, non potevi facilmente portare le tue prove nella Città dei Mattoni.
Questo lavoro è come costruire un ponte sicuro e automatico tra le due città.

Permette di usare le nuove tecnologie potenti (tipi dipendenti) senza dover fidarsi di un sistema "scatola nera" complesso.
Garantisce che ogni prova sia verificata dalle regole più antiche e sicure della matematica.
Apre la strada per tradurre automaticamente le prove scritte in Lean (il linguaggio dei Lego più popolare oggi) in sistemi basati sulla teoria degli insiemi.

In sintesi:
Hanno dimostrato che puoi avere il meglio di due mondi: la potenza e la sicurezza dei tipi dipendenti, ma con la semplicità e la trasparenza della teoria degli insiemi. È come se avessero insegnato ai Lego a parlare la lingua dei mattoni, permettendo loro di costruire cose incredibili su fondamenta che tutti conoscono e capiscono.

Titolo: I Tipi Dipendenti nella Teoria degli Insiemi sono Fattibili?

Autori: Yunsong Yang, Simon Guilloud, Viktor Kunčak (EPFL e KTH)
Contesto: Integrazione dei tipi dipendenti in un assistente alla prova basato sulla logica del primo ordine e la teoria degli insiemi (Lisa).

1. Il Problema

Per oltre un secolo, la teoria degli insiemi di Zermelo-Fraenkel con l'assioma della scelta (ZFC) è rimasta il fondamento standard della matematica. Tuttavia, il panorama della dimostrazione interattiva di teoremi è dominato da sistemi basati sulla Teoria dei Tipi Dipendenti (DTT), come Rocq (ex Coq) e Lean 4.
Sebbene la DTT offra proprietà pratiche utili (come il controllo dei tipi prevedibile e la valutazione integrata), i suoi kernel logici sono complessi da implementare e validare, portando a bug di implementazione e difficoltà nella verifica formale della correttezza del sistema stesso.
Esiste un interesse crescente a trasferire prove e concetti da sistemi basati su DTT (specialmente Lean 4) verso assistenti basati sulla teoria degli insiemi per garantire interoperabilità e maggiore fiducia nei fondamenti. La sfida principale è: è possibile implementare i tipi dipendenti (inclusi i prodotti dipendenti e le gerarchie di universi) all'interno di un sistema basato sulla teoria degli insiemi, mantenendo la semplicità e la verificabilità della logica del primo ordine?

2. Metodologia

Gli autori hanno sviluppato un'implementazione meccanizzata all'interno di Lisa, un assistente alla prova con un kernel logico piccolo basato sulla logica del primo ordine con uguaglianza e assiomi della teoria degli insiemi di Tarski-Grothendieck.

A. Embedding dei Tipi Dipendenti in λFOL

Per rappresentare l'astrazione ( $\lambda$ ) e l'applicazione tipiche della DTT all'interno della logica del primo ordine, gli autori utilizzano $\lambda$ FOL (Logica del Primo Ordine con termini $\lambda$ ), un'estensione di Lisa che include termini $\lambda$ e l'operatore $\epsilon$ di Hilbert.

Mappatura: I termini della teoria dei tipi vengono mappati in termini $\lambda$ $λ$ FOL.
- L'astrazione $\lambda x : T. u$ diventa un insieme di coppie $\{ \langle x, L(x) \rangle \mid x \in T \}$ .
- L'applicazione $t\ u$ è definita tramite l'operatore $\epsilon$ : $\epsilon y. (u, y) \in t$ .
- Il prodotto dipendente $\Pi x : T_1. T_2$ è definito come l'insieme delle funzioni $f$ il cui dominio è $T_1$ e il cui valore per ogni $x$ appartiene a $T_2(x)$ .
Riduzione $\beta$ : Viene dimostrato che questa definizione recupera il comportamento di riduzione $\beta$ ($app(abs(T)(L))(t) = L(t)$), giustificando l'uso di termini di ordine superiore all'interno di un sistema fondamentalmente del primo ordine.

B. Gestione degli Universi (Tarski-Grothendieck)

La ZFC standard non possiede un concetto interno di "universo" chiuso sotto tutte le costruzioni (incluso l'operatore $\Pi$ ), rendendo impossibile modellare gerarchie di tipi cumulativi ( $Type_i : Type_{i+1}$ ).

Soluzione: Gli autori adottano l'Assioma di Tarski, che garantisce l'esistenza di infiniti Universi di Grothendieck.
Definizione: Un universo è un insieme chiuso sotto coppie, unioni, insiemi delle parti e sostituzioni funzionali.
Gerarchia: Viene definita una gerarchia di universi iterando un operatore universeOf(x), permettendo di gestire i livelli di universo necessari per la polimorfia e la formazione dei tipi dipendenti.

C. Generazione di Prove e Controllo dei Tipi

È stato implementato un tattica di controllo dei tipi bidirezionale (Typecheck.prove) che genera prove meccanizzate direttamente nel kernel di Lisa.

Modalità: Il sistema opera in modalità "Check" (verifica contro un tipo atteso) e "Infer" (inferisce il tipo di un termine).
Sottotipaggio: Viene supportato una forma di sottotipaggio, in particolare la covarianza nel codominio dei tipi funzione, con dominio invariante. Il sottotipaggio contravariante è evitato perché non si traduce direttamente in un'interpretazione insiemistica predicativa (porterebbe a insiemi troppo grandi).
Output: Invece di restituire un semplice booleano, la tattica sintetizza un oggetto di prova formale (sequenza di deduzioni logiche) che può essere verificato dal kernel di Lisa.

3. Contributi Chiave

Embedding Set-Teorico dei Tipi Dipendenti: La prima realizzazione meccanizzata completa dei prodotti dipendenti e delle gerarchie di universi all'interno di un assistente basato su logica del primo ordine e teoria degli insiemi (Lisa).
Interfaccia di Sintassi e Ragionamento: Un'interfaccia che offre la sintassi e le proprietà chiave della DTT, ma dove il controllo dei tipi è formalmente giustificato dagli assiomi della teoria degli insiemi.
Tattica di Generazione di Prove: Un algoritmo di controllo dei tipi bidirezionale che produce prove verificabili, supportando anche il sottotipaggio (covarianza).
Interoperabilità Potenziale: Un passo fondamentale verso il trasferimento di prove da Lean 4 e Rocq verso sistemi basati sulla teoria degli insiemi, facilitando l'interoperabilità tra paradigmi diversi.

4. Risultati ed Esempi

Verifica Formale: Gli autori hanno dimostrato teoremi fondamentali come la regola di introduzione ( $T_{abs}$ ), l'eliminazione ( $T_{app}$ ) e la riduzione $\beta$ , tutti derivati direttamente dagli assiomi della teoria degli insiemi.
Caso d'Uso: È stato implementato un esempio di composizione polimorfica (simile a quanto avviene in Lean), combinando una funzione generica con una funzione identità polimorfica. La tattica Typecheck.prove ha automaticamente derivato la prova che l'espressione risultante è ben tipata, generando un oggetto di prova verificabile dal kernel.
Efficienza: L'approccio evita la complessità di codifiche profonde (deep encoding) tipiche dei precedenti tentativi di modellare la DTT in ZFC, utilizzando invece una traduzione sintattica superficiale (shallow translation) resa possibile da $\lambda$ FOL.

5. Significato e Implicazioni

Questo lavoro dimostra che i tipi dipendenti sono fattibili all'interno della teoria degli insiemi senza sacrificare la semplicità del kernel logico.

Fiducia nei Fondamenti: Permette di utilizzare le potenti funzionalità della DTT (come il controllo dei tipi avanzato) mantenendo la fiducia che deriva da un kernel basato su ZFC, che è più semplice da verificare e meno soggetto a bug rispetto ai kernel complessi della DTT.
Interoperabilità: Fornisce un ponte teorico e pratico per tradurre prove da sistemi moderni (Lean, Rocq) in sistemi basati sulla teoria degli insiemi, un obiettivo cruciale per la comunità matematica che utilizza diversi assistenti.
Estensibilità: L'approccio "soft type system" su una base insiemistica permette di estendere le funzionalità dei tipi (es. sottotipaggio, nuovi costruttori) garantendo la correttezza attraverso gli assiomi di base.

In sintesi, il paper stabilisce che è possibile costruire un sistema di tipi dipendenti robusto e verificabile su fondamenta insiemistiche, offrendo una via alternativa e complementare alla pura teoria dei tipi per la dimostrazione automatizzata di teoremi.