💻 computer science

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory

Questo articolo costruisce modelli di insiemi materiali non ben fondati nella Teoria dei Tipi Omotopici che soddisfano gli Assiomi di Anti-Fondazione di Scott e di Aczel tramite M-tipi e coalgebra terminali, estende tali assiomi ai livelli di tipo superiore all'interno della Teoria degli Insiemi Materiali Univalenti e fornisce una caratterizzazione dei tipi di identità di M-tipo, con tutti i risultati formalizzati in Agda.

Autori originali: Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri

Pubblicato 2026-07-01

📖 6 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri

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

Il Quadro Generale: Costruire un Universo di Insiemi "Rotanti"

Immaginate di stare costruendo un universo di oggetti (insiemi). Nel modo tradizionale di fare matematica (chiamata teoria degli insiemi "ben fondata"), ogni oggetto è costruito partendo da oggetti più piccoli, che a loro volta sono costruiti da oggetti ancora più piccoli, fino ad arrivare al nulla. È come una piramide: non puoi avere un blocco sospeso nel vuoto; deve poggiare su qualcosa che sta sotto di lui.

Ma cosa succederebbe se voleste costruire un universo in cui le cose possono poggiare su se stesse? Cosa succederebbe se aveste una scatola che contiene se stessa? O una catena di scatole dove la Scatola A è dentro la Scatola B, che è dentro la Scatola C, che è dentro la Scatola A? Nella matematica tradizionale, questo è proibito perché crea un loop infinito. In questo articolo, gli autori esplorano come costruire un universo matematico che permetta questi loop, utilizzando un framework moderno chiamato Teoria dei Tipi Omotopici (HoTT).

Il documento fa due cose:

Costruisce un modello di insiemi che permette i loop, seguendo le regole stabilite da un matematico di nome Scott.
Costruisce un modello diverso di insiemi che permette i loop, seguendo le regole stabilite da un matematico di nome Aczel.

Gli Strumenti: Alberi, Coalgebre e "Svolgimento"

Per comprendere i loro modelli, immaginate un albero.

Alberi ben fondati (il vecchio modo) sono come alberi genealogici. Hanno una radice, dei rami e alla fine terminano in foglie. Smettono di crescere.
Alberi non ben fondati (il nuovo modo) possono essere come un frattale o una galleria di specchi. Un ramo potrebbe tornare indietro e diventare la radice stessa. Oppure un ramo potrebbe dividersi in due rami identici che sembrano esattamente l'intero albero.

Gli autori utilizzano un concetto chiamato Coalgebra per descrivere questi alberi. Pensate a una coalgebra come a una "macchina" che vi dice come guardare un nodo e vedere cosa viene dopo.

Se la macchina dice "fermati", avete una foglia.
Se la macchina dice "vai a questi figli", avete dei rami.
Se la macchina dice "vai a un figlio che è in realtà te stesso", avete un loop.

L'articolo si chiede: Qual è la macchina "ultima" capace di descrivere tutti i possibili loop?

I Due Modelli: Scott vs. Aczel

Gli autori costruiscono due diverse "macchine ultime" (modelli matematici) per gestire questi loop. Esse corrispondono a due diverse filosofie su come trattare l'uguaglianza in questi mondi circolari.

1. Il Modello dello "Specchio" (L'Assioma di Anti-Fondazione di Scott)

L'Analogia: Immaginate una galleria di specchi. Se vi posizionate davanti a uno specchio, vedete un riflesso. Se quel riflesso è dentro un altro specchio, vedete un riflesso di un riflesso.
La Regola: In questo modello, due oggetti sono considerati "uguali" se i loro schemi di svolgimento (unfolding patterns) appaiono uguali. Se continuate ad aprire gli strati di un insieme (come sbucciare una cipolla o sviluppare un albero), e il pattern dei rami è identico a quello di un altro insieme, allora sono lo stesso oggetto.
Il Risultato: Gli autori hanno costruito un tipo specifico di struttura ad albero (chiamata $V^0_\infty$ ) che funge da questo modello. È un "punto fisso", il che significa che se applicate le regole dell'universo a esso, ottenete lo stesso universo.
Risultato Chiave: Questo modello non è la macchina "finale" o "terminale" nel senso più stretto. È una "terza opzione": non è il punto di partenza (iniziale) e non è l'assoluto punto di arrivo (terminale). Si trova nel mezzo. Soddisfa le regole di Scott, che sono più rigide su come i loop vengono identificati.

2. Il Modello "Universale" (L'Assioma di Anti-Fondazione di Aczel)

L'Analogia: Immaginate un catalogo maestro di ogni possibile storia che potreste raccontare, incluse le storie che raccontano se stesse.
La Regola: In questo modello, qualsiasi grafo (un disegno di punti e linee) può essere trasformato in un insieme. Se avete il disegno di un loop, esiste un insieme unico che corrisponde perfettamente a quel disegno.
Il Risultato: Gli autori hanno costruito una "Coalgebra Terminale" (la macchina ultima) per questo scopo. Tuttavia, per costruire questa macchina specifica, hanno dovuto utilizzare uno strumento matematico speciale e alquanto controverso chiamato Ridimensionamento Proposizionale (Propositional Resizing).
- Cos'è il Ridimensionamento Proposizionale? Immaginate di avere una gigantesca biblioteca di libri (proposizioni). Questo strumento vi permette di rimpicciolire l'intera biblioteca in modo che stia su un singolo scaffale, senza perdere nessuna delle storie. È una scorciatoata potente che rende possibile la costruzione.
Risultato Chiave: Questo modello soddisfa le regole di Aczel. È l'oggetto "terminale", il che significa che è la versione più completa possibile di un universo di insiemi con loop.

L'Enigma dell'Identità: Cosa Rende Due Cose Uguali?

Una parte importante dell'articolo consiste nel risolvere un enigma complicato: Come facciamo a sapere quando due alberi circolari sono in realtà lo stesso oggetto?

Nella matematica standard, se due cose appaiono uguali, sono uguali. Ma in un mondo con i loop, le cose si fanno strane.

Gli autori hanno scoperto che l' "uguaglianza" tra due punti nei loro alberi circolari può essere descritta come un altro tipo di albero (un "M-tipo indicizzato").
La Metafora: Immaginate di confrontare due frattali infiniti. Per dimostrare che sono uguali, non vi basta guardare l'immagine intera; dovete confrontare ogni singolo ramo, ogni sottobranco e ogni sotto-sotto-branco. L'articolo fornisce una ricetta precisa (una "caratterizzazione") su come effettuare questo confronto. Hanno dimostrato che l' "uguaglianza" di questi complessi loop è essa stessa un oggetto strutturato e infinito.

Sintesi dei Risultati

Il Modello di Scott: Hanno costruito un universo di insiemi che permette i loop, dove l'uguaglianza è determinata dalla forma dell'albero di "svolgimento". Questo modello è un punto fisso ma non è l'assoluto "terminale".
Il Modello di Aczel: Hanno costruito l'universo "ultimo" di insiemi che permette i loop, dove qualsiasi grafo può essere trasformato in un insieme. Ciò ha richiesto un'assunzione matematica speciale (il Ridimensionamento Proposizionale).
La Ricetta dell'Uguaglianza: Hanno scoperto esattamente come definire la "somiglianza" per queste strutture infinite e circolari, mostrando che l'uguaglianza è semplicemente un altro tipo di struttura ad albero.
Formalizzazione: Non si sono limitati a scrivere tutto su carta; hanno costruito tutto all'interno di un programma per computer chiamato Agda, che controlla ogni passaggio logico per garantire che non ci siano errori.

Perché Questo è Importante?

L'articolo non pretende di risolvere problemi di ingegneria reale o questioni mediche. Al contrario, risolve un enigma fondamentale della matematica. Dimostra che possiamo costruire un universo logico e coerente dove "cerchi" e "loop" sono ammessi, utilizzando il linguaggio moderno della Teoria dei Tipi Omotopici. Colma il divario tra la teoria classica degli insiemi (che proibisce i loop) e la moderna logica dell'informatica (che ha bisogno di gestire strutture dati complesse e circolari come flussi di dati o sistemi di transizione).

In breve: hanno costruito due diversi "universi" dove le cose possono contenere se stesse, hanno dimostrato che funzionano secondo regole specifiche e hanno mostato esattamente come capire se due di queste entità autocontenute sono in realtà la stessa cosa.

Sintesi Tecnica: Coalgebre Terminali e Insiemi Non Ben Fondati in Teoria dei Tipi Omotopici

Enunciato del Probleamento
Il saggio affronta la sfida di modellare insiemi materiali non ben fondati all'interno della Teoria dei Tipi Omotopici (HoTT). Mentre la teoria degli insiemi ben fondati è stata modellata con successo in HoTT utilizzando i tipi induttivi superiori (dove l'uguaglianza è il tipo identità), la modellazione degli insiemi non ben fondati — insiemi che possono contenere se stessi o formare catene di appartenenza infinite — si è storicamente basata su setoid (dove l'uguaglianza è una relazione binaria separata) piuttosto che sul tipo identità. Gli autori mirano a costruire modelli di insiemi non ben fondati in HoTT in cui l'uguaglianza sia interpretata strettamente come il tipo identità, integrando così le nozioni classiche di coalgebra universale e teoria degli insiemi non ben fondati nelle strutture di ordine superiore supportate da HoTT. Nello specifico, il saggio cerca di costruire coalgebre terminali per endofunzioni di potenza ristrette per modellare l'Assioma di Anti-Fondazione di Aczel (AFA) e di costruire punti fissi alternativi che modellino l'Assioma di Anti-Fondazione di Scott (SAFA).

Metodologia
Gli autori utilizzano il framework della Teoria degli Insiemi Materiali Univalente e la teoria delle coalgebre per endofunzioni "wild" sull'universo dei tipi. La metodologia prevede tre approcci tecnici primari:

Dualizzazione degli Insiemi Iterativi: Gli autori costruiscono una gerarchia di tipi $V^n_\infty$ dualizzando la costruzione degli insiemi iterativi ( $V^n$ ). Mentre $V^n$ è l'algebra iniziale della endofunzione di potenza ristretta $P^n$ , $V^n_\infty$ è costruito come un sottotipo specifico del tipo M (la coalgebra terminale della endofunzione di potenza non ristretta $P^\infty$ ). Questo sottotipo è definito da un predicato coinduttivo che assicura che le mappe di branching ad ogni nodo siano troncate a un livello specifico.
Caratterizzazione dei Tipi Identità: Un passaggio tecnico cruciale consiste nel caratterizzare i tipi identità degli M-type. Gli autori dimostrano che il tipo identità tra due elementi di un M-type è equivalente a un M-type indicizzato (specificamente, la coalgebra terminale di una endofunzione polinomiale indicizzata derivata dallo "svolgimento" di una relazione). Questa caratterizzazione è essenziale per dimostrare la piccola dimensione locale (local smallness) dei modelli costruiti.
Adattamento della Costruzione Aczel–Mendler: Per costruire una vera coalgebra terminale per la endofunzione di potenza ristretta $P^0$ $P^{0}$ (che modella l'AFA), gli autori adattano il classico teorema di Aczel–Mendler alla teoria dei tipi. Questo adattamento richiede:
- La definizione di endofunzioni "U-based" (funzioni in cui i valori su tipi grandi sono colimiti di valori su tipi piccoli).
- L'utilizzo del sollevamento di relazioni (relation lifting) e del concetto di "precongruenze" per quotientare la coalgebra debolmente terminale.
- L'assunzione del ri dimensionamento proposizionale (propositional resizing) per garantire che i tipi risultanti dal quoziente siano localmente piccoli e che la costruzione valga per le endofunzioni a valori di insieme come $P^0$ .

Contributi Chiave e Risultati

Un Modello dell'Assioma di Anti-Fondazione di Scott (SAFA): Gli autori costruiscono un tipo $V^0_\infty$ che è un punto fisso della endofunzione di potenza ristretta $P^0$ , ma che non è né l'algebra iniziale né la coalgebra terminale. Dimostrano che questo tipo, equipaggiato con la relazione di appartenenza indotta, soddisfa l'Assioma di Anti-Fondazione di Scott. In questo modello, l'uguaglianza è il tipo identità, e il modello è "semplice" (qualsiasi due omoformismi in esso sono uguali) ma non terminale.
Generalizzazione a Tipi Superiori: La costruzione è generalizzata a una gerarchia di tipi $V^n_\infty$ per ogni livello di troncamento $n$ . Questi modelli soddisfano gli assiomi $k$ -SAFA generalizzati per tutti i $k \le n$ . Il saggio dimostra che questi modelli soddisfano gli standard assiomi della teoria degli insiemi (insieme vuoto, separazione, unione, ecc.) ai livelli di troncamento appropriati, a condizione che i modelli siano localmente piccoli.
Caratterizzazione dei Tipi Identità degli M-type: Il saggio fornisce una piena caratterizzazione del tipo identità di un M-type come M-type indicizzati (Teorema 2.15). Questo risultato è utilizzato per dimostrare che i modelli costruiti sono localmente piccoli, una condizione necessaria affinché possano fungere da validi modelli di teoria degli insiemi materiali in HoTT.
Un Modello dell'Assioma di Anti-Fondazione di Aczel (AFA): Assumendo l'assioma del ri dimensionamento proposizionale, gli autori costruiscono una coalgebra terminale per la endofunzione di potenza ristretta $P^0$ (e più generalmente per endofunzioni $U$ -based). Questa coalgebra terminale funge da modello dell'AFA di Aczel, dove ogni grafo ha una decorazione unica.
Non-Terminalità di $V^0_\infty$ : Il saggio dimostra esplicitamente che $V^0_\infty$ non è la coalgebra terminale per $P^0$ . Fornisce un controesempio mostrando che possono esistere distinti omoformismi di coalgebra da un grafo specifico verso $V^0_\infty$ , distinguendolo dalla coalgebra terminale costruita tramite il metodo Aczel–Mendler.

Significatività e Rivendicazioni
Il saggio rivendica di fornire i primi modelli di insiemi materiali non ben fondati in HoTT in cui l'uguaglianza è il tipo identità, andando oltre i modelli basati su setoid del passato.

Distinzione tra AFA e SAFA: Il lavoro chiarisce la relazione tra gli assiomi di anti-fondazione di Aczel e di Scott all'interno del contesto di HoTT. Mostra che mentre la coalgebra terminale (che richiede il ri dimensionamento proposizionale) valida l'AFA, il punto fisso co-iterativo (costruibile senza ri dimensionamento) valida la SAFA. Gli autori osservano che nel caso non troncato ( $\infty$ ), AFA e SAFA coincidono, ma divergono ai livelli di troncamento inferiori.
Natura Costruttiva: La costruzione del modello SAFA ( $V^n_\infty$ ) è pienamente costruttiva e non dipende da assiomi impredicativi come il ri dimensionamento proposizionale.
Formalizzazione: Tutti i risultati principali sono formalizzati nell'assistente di prova Agda, utilizzando sia lo standard Agda che Cubical Agda (per la Sezione 6), garantendo la correttezza degli complessi argomenti homotopici.
Domande Aperte: Gli autori notano con modestia che l'esistenza della coalgebra terminale per $P^0$ senza ri dimensionamento proposizionale rimane una questione aperta. Non pretendono di aver risolto se tale costruzione sia possibile o se la sua esistenza implichi principi classici, ma evidenziano questo punto come una primaria motivazione per il lavoro futuro.

In sintesi, il saggio estende con successo la teoria degli insiemi non ben fondati all'ambiente di ordine superiore di HoTT, fornendo modelli distinti per diversi assiomi di anti-fondazione e stabilendo le necessarie basi tecniche riguardanti gli M-type e le strutture di coalgebra.