💻 computer science

Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda

Questo articolo presenta una formalizzazione della costruzione dei numeri reali di Cauchy nella Teoria dei Tipi Omotopica in Cubical Agda, dimostrando che tale approccio evita la scelta numerabile, l'overhead dei setoidi e i problemi di tracciamento dei livelli di universo intrinseci ad altre definizioni costruttive, verificando al contempo il tipo senza postulati.

Autori originali: Jackson Brough

Pubblicato 2026-04-29

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Jackson Brough

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 cercare di costruire un righello perfetto e infinito per misurare tutto nell'universo. Nel mondo della matematica classica, questo righello è facile da descrivere: basta prendere tutte le possibili misurazioni "approssimate" (come 3,1; 3,14; 3,141; ecc.) e dire: "Se due sequenze di misurazioni si avvicinano sempre di più, rappresentano lo stesso punto sul righello".

Tuttavia, nella Matematica Costruttiva — uno stile di matematica che insiste sul fatto che devi essere in grado di effettivamente costruire o calcolare la cosa di cui stai parlando — questo approccio semplice si scontra con un muro. Per dimostrare che il tuo righello è completo, devi fare una scelta magica: devi scegliere una misurazione specifica da un elenco infinito di opzioni per rappresentare il punto finale. La matematica costruttiva dice: "Nessuna magia consentita. Se non puoi mostrarmi come l'hai scelta, non hai ancora costruito il righello".

Per decenni, i matematici hanno dovuto compromettere. O hanno usato trucchi di "contabilità" che rendevano ogni calcolo disordinato, oppure hanno costruito il righello in un modo che richiedeva il tracciamento di complessi "livelli di universo" (come tenere il punteggio di quanto sono grandi le tue scatole).

Il Nuovo Progetto (Reali del Libro HoTT)
Questa tesi presenta un nuovo progetto per costruire il righello, tratto dal famoso libro Homotopy Type Theory (HoTT). Invece di costruire il righello incollando pezzi insieme e poi cercando di lisciarli, questo metodo costruisce il righello e le regole di "lisciatura" simultaneamente.

Pensaci come alla costruzione di una casa in cui i muri e il progetto vengono disegnati esattamente nello stesso momento.

I Mattoni: Si inizia con numeri semplici e noti (come le frazioni).
La Colla: Si aggiunge una regola speciale che dice: "Se due punti sono abbastanza vicini, sono effettivamente lo stesso punto".
La Magia: Poiché la regola della "vicinanza" è integrata nella definizione della casa stessa, non è necessario fare quelle scelte magiche in seguito. La casa è completa nel momento in cui si finisce di posare i mattoni.

La Sfida: Il Traduttore per Computer
L'autore, Jackson Brough, ha preso questo progetto teorico e ha cercato di tradurlo in un linguaggio che un computer possa comprendere e verificare: Cubical Agda.

Immagina di cercare di spiegare una complessa coreografia a un robot che comprende solo istruzioni rigide e letterali.

Il Problema: I precedenti tentativi di tradurre questo progetto fallirono perché il linguaggio informatico non disponeva delle giuste "mosse" (in particolare, non poteva gestire la definizione simultanea del righello e delle regole di vicinanza). I traduttori dovevano dire: "Assumiamo che questa mossa esista", il che è barare in matematica.
La Soluzione: Cubical Agda è un robot più nuovo e intelligente che nativamente comprende queste mosse complesse. Permette all'autore di scrivere il progetto esattamente come è stato progettato, senza barare.

Cosa è Accaduto Durante la Traduzione?
La tesi non riguarda solo la digitazione del codice; riguarda ciò che è accaduto quando l'autore ha cercato di far comprendere la matematica al computer. La rigidità del computer ha costretto l'autore a trovare lacune nascoste nella spiegazione originale:

La Mappa "Alternativa": Il libro originale descriveva come verificare se due punti sono vicini. Ma quando l'autore ha cercato di scrivere il codice, ha realizzato che il metodo del libro era come un "senso unico". Si potevano provare i punti vicini, ma non si poteva facilmente lavorare all'indietro per vedere perché. L'autore ha dovuto costruire una seconda mappa "computazionale" (chiamata relazione alternativa) che agisce come una retromarcia, permettendo al computer di calcolare effettivamente la risposta.
L'Ingrediente Mancante: Il libro descriveva una regola per costruire funzioni (come la moltiplicazione) come se il computer potesse "ricordare" l'elenco originale delle approssimazioni. La prima versione del codice dell'autore aveva dimenticato questa memoria. Il computer l'ha respinta. L'autore ha dovuto riscrivere la regola per trasportare esplicitamente la memoria lungo il percorso, rendendosi conto che il testo originale era stato troppo vago per una macchina.
Il Puzzle a Variabili Multiple: Il libro accennava che le regole per i singoli numeri potevano essere facilmente applicate a coppie o terzine di numeri. Il computer non ne era convinto. L'autore ha dovuto dimostrare un nuovo lemma specifico che mostrava che, se una regola funziona per una variabile, funziona anche per due, a condizione che vengano controllate una alla volta.

Il Risultato
Il prodotto finale è una vasta libreria di codice open-source (oltre 13.000 righe) che dimostra che i reali del libro HoTT funzionano perfettamente.

Dimostra che questi numeri formano un campo ordinato completo (si possono aggiungere, sottrarre, moltiplicare, dividere e confrontare).
Dimostra che il righello è "Archimedeo" (il che significa che non importa quanto piccolo sia un intervallo, si può sempre trovare una frazione che ci sta dentro).
Soprattutto, fa tutto questo senza barare. Il computer ha controllato ogni singolo passaggio e il codice funziona senza alcuna "assunzione magica".

In Sintesi
Questa tesi è la storia di come un'idea matematica alta e bella sia stata portata a sopravvivere nel mondo rigoroso e letterale della verifica informatica. Facendo ciò, l'autore non ha solo costruito un righello digitale; ha lucidato lo stesso progetto, rivelando dettagli nascosti e rendendo la teoria più forte e precisa di quanto non fosse prima. Il codice è ora disponibile per chiunque voglia utilizzarlo come una solida base per future scoperte matematiche.

1. Enunciato del Problema

La matematica costruttiva mira a fornire interpretazioni computazionali per le dimostrazioni matematiche, ma la costruzione dei numeri reali ( $\mathbb{R}$ ) ha storicamente richiesto compromessi significativi:

Costruzione Classica di Cauchy: Richiede l'Assioma della Scelta Numerabile per selezionare rappresentanti dalle classi di equivalenza delle successioni di Cauchy al fine di dimostrare la completezza di Cauchy. Questo approccio è non costruttivo.
Costruzione Setoidale di Bishop: Evita la scelta lavorando con successioni di Cauchy equipaggiate con una relazione di equivalenza esplicita (setoidi). Tuttavia, ciò introduce un persistente onere di gestione (bookkeeping overhead), richiedendo dimostrazioni di congruenza esplicite per ogni operazione e teorema, il che complica le strutture algebriche.
Tagli di Dedekind: Nella teoria dei tipi predicativa, i tagli di Dedekind richiedono il tracciamento dei livelli di universo (i reali vivono un livello sopra i loro tagli), rendendo gli sviluppi ingombranti.

Il Libro HoTT (Homotopy Type Theory) propone una soluzione: definire i numeri reali come un Tipo Induttivo-Induttivo Superiore (HIIT). Questa costruzione evita la scelta, elimina l'onere dei setoidi identificando i reali $\epsilon$ -vicini tramite costruttori di percorso e evita il tracciamento dei livelli di universo. Tuttavia, le formalizzazioni precedenti (ad esempio, quella di Gilbert in Rocq) erano incomplete perché gli assistenti alla dimostrazione mancavano del supporto nativo per gli HIIT, costringendo l'autore a postulare i costruttori di percorso e le loro regole di computazione invece di derivarli.

2. Metodologia

La tesi presenta una formalizzazione completa e verificata da macchina dei reali del Libro HoTT utilizzando Cubical Agda, un assistente alla dimostrazione basato sulla Teoria dei Tipi Cubica.

Supporto Nativo: Cubical Agda supporta nativamente i Tipi Induttivi Superiori (HIT) e le definizioni Induttive-Induttive. Ciò permette all'autore di definire i reali e la relazione di vicinanza simultaneamente senza postulati, garantendo che i costruttori di percorso abbiano regole di computazione native.
Ambito della Formalizzazione: Il lavoro formalizza oltre 13.000 righe di codice, coprendo:
1. La definizione HIIT di $\mathbb{R}$ e della relazione di vicinanza ( $\sim_\epsilon$ ).
2. Principi di induzione e ricorsione.
3. Proprietà della relazione di vicinanza (riflessività, simmetria, disuguaglianza triangolare, arrotondamento).
4. Principi di estensione per mappe Lipschitziane e non espansive.
5. La costruzione delle operazioni algebriche (addizione, negazione, min/max, moltiplicazione, reciproco).
6. Teoria dell'ordine (disuguaglianze strette/non strette, separazione).
7. La dimostrazione che $\mathbb{R}$ forma un campo ordinato Archimedeo.
Strumentazione: L'autore ha utilizzato Claude Code (agente AI di Anthropic) per assistere nella navigazione della vasta libreria standard di Cubical Agda e nella conversione di schizzi di dimostrazione informali in termini Agda formali, accelerando significativamente lo sviluppo di dimostrazioni complesse come quella della costruzione del reciproco.

3. Contributi Chiave

A. La Prima Formalizzazione Completa dei Reali HoTT

Questa è la prima formalizzazione dei reali del Libro HoTT che non si basa su postulati. I tentativi precedenti dovevano assumere l'esistenza dei costruttori di percorso; questo lavoro li deriva direttamente dalla teoria dei tipi di Cubical Agda, garantendo che tutte le regole di computazione valgano definizionalmente.

B. Risoluzione delle Lacune di Formalizzazione

Il processo di formalizzazione ha rivelato questioni sottili nella presentazione informale del Libro HoTT che richiedevano affinamento matematico:

Relazione di Vicinanza Alternativa: La definizione induttiva della vicinanza ( $\sim$ ) fornisce condizioni sufficienti ma non necessarie per estrarre testimoni. La formalizzazione costruisce rigorosamente una relazione ausiliaria ( $\approx$ ) che calcola sui costruttori e dimostra $\sim \iff \approx$ , permettendo l'analisi dei casi sulle ipotesi di vicinanza.
Principio di Ricorsione Potenziato: La notazione del testo informale per il principio di ricorsione assumeva tacitamente l'accesso all'approssimazione del dominio ( $x_\epsilon$ ) all'interno dell'ipotesi induttiva. La formalizzazione ha richiesto la riformulazione esplicita del principio di ricorsione per trasportare sia l'approssimazione che l'assegnazione del codominio, un dettaglio mancato nelle trascrizioni iniziali naive.
Continuità Multi-variabile: Il Libro HoTT implica che la continuità separata sia sufficiente per estendere le identità a più variabili. La formalizzazione ha dimostrato questo esplicitamente (Lemma 2.3.4), mostrando che la continuità separata è sufficiente per estendere identità binarie e ternarie da $\mathbb{Q}$ a $\mathbb{R}$ .

C. Costruzione di Moltiplicazione e Reciproco

La moltiplicazione e il reciproco non sono globalmente Lipschitziani, quindi non possono essere definiti tramite semplici principi di estensione. La tesi adotta la strategia locale-globale di Gilbert:

Definire operazioni su domini ristretti dove esistono limiti Lipschitziani (ad esempio, fissando un limite su un fattore).
Dimostrare che queste definizioni locali concordano sulle sovrapposizioni.
Utilizzare il Teorema di Kraus (mappe dalle troncature proposizionali agli insiemi) per eliminare la dipendenza dal limite specifico, ottenendo una definizione globale.
Questo approccio è stato implementato utilizzando il modulo SetElim della libreria standard di Cubical Agda.

D. Efficienza Computazionale

A differenza della costruzione di quoziente classica in Lean (dove $2+2=4$ sui reali non è vero definizionalmente), la costruzione HoTT in Cubical Agda permette all'aritmetica su input razionali di calcolare definizionalmente. Ad esempio, rational(2) + rational(2) = rational(4) si riduce direttamente a refl (riflessività) nel type checker.

4. Risultati

Campo Ordinato Archimedeo: La formalizzazione dimostra con successo che il tipo costruito $\mathbb{R}$ soddisfa tutti gli assiomi di un campo ordinato Archimedeo, inclusa l'esistenza di inversi per gli elementi separati dallo zero.
Disponibilità del Codice: L'intera base di codice (circa 13.500 righe) è open source e passa il controllo dei tipi senza buchi o postulati utilizzando l'ultima libreria standard di Cubical Agda.
Sviluppo Assistito da AI: La tesi dimostra l'efficacia dell'uso di agenti di codifica basati su LLM per la matematica formale, specificamente per navigare grandi librerie e tradurre strategie di dimostrazione di alto livello in termini di tipi dipendenti di basso livello.

5. Significato

Fondamentale per l'Analisi Costruttiva: Questo lavoro fornisce una base robusta e verificata da macchina per l'analisi costruttiva all'interno del programma delle Fondazioni Univalenti. Rimuove l'onere della "gestione" (bookkeeping) dei setoidi e l'onere della "scelta" dei quozienti classici.
Evoluzione degli Assistenti alla Dimostrazione: Convalida Cubical Agda come ambiente superiore per la matematica basata su HIIT rispetto a sistemi come Rocq (Coq) che mancano del supporto nativo per gli HIT.
Lavori Futuri: La formalizzazione prepara il terreno per estendere l'analisi costruttiva a strutture più complesse (ad esempio, integrazione di Riemann, equazioni differenziali) e generalizzare concetti come i localizzatori (strutture che permettono la computazione sui reali) a spazi metrici più ampi.
Insight Metodologico: La tesi sottolinea che la formalizzazione non è meramente un esercizio di verifica, ma un'attività matematica che può scoprire assunzioni implicite e affinare teoremi in modi che la sola lettura informale non può fare.

In sintesi, la tesi di Jackson Brough colma il divario tra l'eleganza teorica dei numeri reali del Libro HoTT e la matematica pratica ed eseguibile, fornendo una fondazione verificata, computazionalmente efficiente e priva di postulati per l'analisi reale nella teoria dei tipi.