💻 computer science

A formalization of System I with type Top in Agda

Questo lavoro presenta una variante del Sistema I con il tipo Top e ne offre una formalizzazione completa in Agda, includendo le dimostrazioni di progressione e normalizzazione forte.

Autori originali: Agustín Séttimo, Cristian Sottile, Cecilia Manzino

Pubblicato 2026-03-26

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Agustín Séttimo, Cristian Sottile, Cecilia Manzino

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 un mondo di mattoncini da costruzione (i programmi) e regole precise su come possono combinarsi tra loro (i tipi). In questo mondo, di solito, se due mattoncini hanno forme leggermente diverse, non possono essere usati insieme, anche se alla fine fanno esattamente la stessa cosa.

Questo articolo parla di un progetto chiamato System I, che è come un nuovo manuale di istruzioni per questi mattoncini. La grande idea è: "Se due cose sono matematicamente identiche nella loro funzione, trattiamole come se fossero la stessa cosa, anche se sembrano diverse".

Ecco una spiegazione semplice di cosa hanno fatto gli autori, usando delle metafore:

1. Il Problema: La rigidità dei mattoncini

Immagina di avere una scatola con due oggetti: una mela e una pera. In un sistema normale, se chiedi "dammi una mela", non puoi prendere la pera, anche se sono entrambi frutti.
In informatica, questo succede con le funzioni. Se hai una funzione che prende prima un numero e poi una parola, e un'altra che prende prima la parola e poi il numero, i computer tradizionali le vedono come cose diverse. Ma per un umano, sono quasi la stessa cosa!

System I dice: "Basta rigidità! Se posso trasformare la mela in una pera e viceversa senza perdere nulla, allora sono la stessa cosa". Questo permette di scrivere programmi più flessibili, dove l'ordine delle cose non conta più.

2. La Nuova Regola: Il "Top" (Il Tutto)

Gli autori hanno aggiunto una nuova regola speciale chiamata Top (o "Tutto").
Pensa al Top come a una "scatola vuota magica" o a un "passo universale".

Se hai una scatola vuota e ci metti dentro un oggetto, è come se avessi solo l'oggetto (la scatola non aggiunge peso).
Se devi dare un oggetto a qualcuno che accetta "qualsiasi cosa" (il Top), puoi dargli anche la scatola vuota.

Hanno aggiunto questa regola al sistema per renderlo più completo, ma c'era un problema: come si fa a gestire tutto questo senza che il sistema impazzisca e si blocchi all'infinito?

3. La Soluzione: I "Biglietti d'Identità" (I Testimoni)

Qui arriva la parte geniale. Quando nel sistema normale dici "questa cosa è uguale a quell'altra", lo fai con un semplice "sì". Ma nel loro sistema, per essere sicuri che tutto funzioni, hanno deciso di scrivere un biglietto d'identità ogni volta che trasformi una cosa nell'altra.

Senza biglietti: Se trasformo una mela in una pera, lo faccio e basta.
Con i biglietti (il loro sistema): Ogni volta che trasformo una mela in una pera, devo attaccare un adesivo che dice: "Ho usato la regola 'scambio'".

Perché è importante? Perché se non avessimo questi adesivi, il computer potrebbe continuare a scambiare mela e pera all'infinito senza mai fermarsi (un loop infinito). Gli adesivi servono a dire: "Ok, ho fatto lo scambio una volta. Ora ho usato quel biglietto, non posso usarlo di nuovo per lo stesso scopo". Questo garantisce che il programma finisca sempre (un concetto chiamato normalizzazione forte).

4. La Prova: Costruire il Castello in Agda

Hanno usato un linguaggio di programmazione chiamato Agda per costruire questo sistema.
Immagina Agda non come un semplice linguaggio di codice, ma come un architetto matematico super-pignolo.

Non puoi dire "costruisci un muro" a meno che non gli mostri esattamente come ogni mattone si incastra con gli altri.
Se c'è anche solo un millimetro di errore nella logica, Agda ti dice: "No, non funziona".

Gli autori hanno usato Agda per:

Disegnare il sistema: Definire esattamente come funzionano le regole.
Dimostrare che non crolla: Hanno provato matematicamente che, seguendo queste regole, nessun programma può girare all'infinito. Ogni programma, prima o poi, arriva a una soluzione finale (un "valore").
Creare un esecutore: Hanno scritto un programma che prende un codice, lo riduce passo dopo passo (come se fosse un gioco di logica) e ti dice il risultato finale.

5. Perché è utile?

Immagina di avere un assistente personale che non solo esegue i tuoi comandi, ma capisce che se dici "mela prima, pera dopo" o "pera prima, mela dopo", intendi la stessa cosa.

Per i programmatori: Significa poter scrivere codice in modo più naturale, senza preoccuparsi dell'ordine esatto degli argomenti.
Per i matematici: Significa che le prove sono più robuste. Se due cose sono equivalenti, sono la stessa prova.

In sintesi

Questo articolo è come la ricetta per un nuovo tipo di cucina (il calcolo lambda) dove gli ingredienti possono essere scambiati liberamente se sono "equivalenti". Gli autori hanno:

Aggiunto un ingrediente speciale (il Top).
Inventato un sistema di etichette per assicurarsi che lo scambio non diventi un caos infinito.
Usato un architetto infallibile (Agda) per costruire la cucina e dimostrare che, se segui le regole, il pasto sarà sempre pronto e mai interrotto.

È un lavoro che unisce la magia della matematica pura con la pratica della programmazione, rendendo i computer un po' più "intelligenti" nel capire le equivalenze.

1. Il Problema e il Contesto

Il lavoro si inserisce nel campo dei calcoli lambda tipati modulo isomorfismi, un'area di ricerca che mira a identificare tipi isomorfi come equivalenti. In linguaggi di programmazione e sistemi di prova, questo permette di trattare programmi con sintassi diversa ma semantica equivalente come identici (ad esempio, scambiando l'ordine degli argomenti in una funzione: $A \to B \to C \equiv B \to A \to C$ ).

Il sistema di riferimento è System I, un calcolo lambda semplicemente tipato con coppie (prodotti cartesiani) in cui i tipi isomorfi sono considerati uguali. Tuttavia, l'estensione di tali sistemi presenta sfide significative:

Non determinismo e conservazione dei tipi: Le regole di riduzione classiche (come la proiezione basata sulla posizione) diventano problematiche quando l'ordine degli elementi in una coppia può cambiare grazie agli isomorfismi.
Terminazione (Strong Normalization): L'introduzione di nuove regole di equivalenza e la possibilità di espansioni infinite (come l'espansione $\eta$ ) minacciano la proprietà di normalizzazione forte, ovvero la garanzia che ogni sequenza di riduzione termini.
Assenza di un tipo Top: I sistemi precedenti spesso non includevano un tipo base "Top" (o $\top$ ), che corrisponde alla proposizione "Vero" in logica, limitando l'espressività e la capacità di modellare certi costrutti logici.
Formalizzazione: La complessità delle equivalenze tra termini rende difficile la verifica manuale delle proprietà di sicurezza e terminazione.

2. Metodologia

Gli autori hanno adottato un approccio rigoroso basato sulla formalizzazione interattiva utilizzando il linguaggio di dimostrazione Agda. Le scelte metodologiche chiave includono:

Estensione del Sistema: Hanno introdotto una variante di System I che include il tipo Top ( $\top$ ) come tipo base, aggiungendo nuovi isomorfismi specifici (es. $A \times \top \equiv A$ , $\top \to A \equiv A$ , $A \to \top \equiv \top$ ).
Rappresentazione Intrinseca dei Termini: A differenza di approcci estrinseci (dove i termini e i tipi sono definiti separatamente), hanno utilizzato una rappresentazione intrinseca in Agda. In questo schema, ogni termine è costruito direttamente come una derivazione di tipo; di conseguenza, ogni termine ben formato è automaticamente tipato.
Indici di De Bruijn: Per gestire le variabili, sono stati utilizzati indici di De Bruijn invece di nomi, rendendo la formalizzazione più compatta e gestibile per quanto riguarda la sostituzione e il legame delle variabili.
Tracciamento Esplicito degli Isomorfismi: Per risolvere il problema del non determinismo e garantire la terminazione, hanno introdotto witness espliciti (costruttori sintattici) che tracciano quale isomorfismo è stato applicato per convertire un termine. Un termine non è più solo $t$ , ma può essere $[\rho] \equiv t$ , dove $\rho$ è la prova dell'isomorfismo.
Relazioni di Riduzione Dirette: Invece di definire la riduzione come una relazione modulo equivalenza (che può portare a cicli infiniti), hanno diretto le relazioni di equivalenza verso relazioni di riscrittura. Le equivalenze tra termini ( $\Leftrightarrow$ ) sono state definite per eliminare o semplificare i costruttori di isomorfismo, agendo come passi di riduzione.

3. Contributi Chiave

I principali contributi del lavoro sono:

Definizione del Calcolo Esteso: Una specifica completa di System I con il tipo Top, inclusi nuovi isomorfismi e regole di congruenza per gestire le trasformazioni sintattiche necessarie alla formalizzazione.
Formalizzazione Completa in Agda:
- Definizione della sintassi, della semantica e delle regole di tipizzazione.
- Implementazione delle sostituzioni e delle riduzioni ( $\beta$ -riduzione e proiezioni) adattate per gestire gli isomorfismi.
Dimostrazione di Progress (Avanzamento):
- Dimostrazione che ogni termine chiuso e tipato è o un valore (normal form) o può compiere un passo di riduzione.
- Gestione dei casi complessi dove i termini contengono costruttori di isomorfismo, garantendo che non rimangano "bloccati" (stuck).
Dimostrazione di Strong Normalization (Normalizzazione Forte):
- Utilizzo di una tecnica di riducibilità (basata sul lavoro di Tait e Girard, adattata da Schäfer e Kovács) per dimostrare che ogni sequenza di riduzione termina.
- La prova è costruttiva: definisce un predicato di normalizzazione forte ($SN$) e dimostra che ogni termine tipato soddisfa questo predicato.
Implementazione di una Funzione di Valutazione:
- Grazie alla prova di normalizzazione forte, è stato possibile definire una funzione di valutazione totale in Agda che, dato un termine chiuso, restituisce la sequenza di riduzione fino al valore finale.

4. Risultati

Terminazione Garantita: È stato provato che il calcolo esteso con Top e witness espliciti è fortemente normalizzante. Questo risolve il problema potenziale di non terminazione introdotto dagli isomorfismi e dalle espansioni $\eta$ .
Correttezza della Semantica: La relazione di riduzione definita ( $\twoheadrightarrow$ ) preserva i tipi (subject reduction) e garantisce che i termini non si blocchino (progress).
Esempio Pratico: Gli autori hanno dimostrato l'efficacia del sistema valutando il termine $\Omega = (\lambda x. x x)(\lambda x. x x)$ , che in un sistema standard non tipato diverge. Nel loro sistema, grazie alla gestione esplicita degli isomorfismi e al tipo Top, il termine è tipabile e la valutazione termina correttamente restituendo il valore $\star$ (il termine di tipo Top).
Codice Disponibile: L'intero codice sorgente in Agda è stato reso pubblico su GitHub, fornendo una base verificabile per futuri lavori.

5. Significato e Impatto

Questo lavoro è significativo per diversi motivi:

Prima Formalizzazione di Normalizzazione Modulo Isomorfismi: È la prima versione conosciuta di una formalizzazione completa della prova di normalizzazione per un calcolo lambda modulo isomorfismi, un compito notoriamente complesso a causa dell'esplosione dei casi di riduzione.
Validazione della Teoria: La formalizzazione in Agda conferma che le scelte teoriche (come l'uso di witness espliciti e la direzione delle regole di equivalenza) sono coerenti e sufficienti per garantire proprietà di sicurezza fondamentali.
Implicazioni Logiche: Dal punto di vista della corrispondenza Curry-Howard, la normalizzazione forte garantisce la consistenza logica del sistema. Se ogni prova termina, non è possibile derivare una contraddizione.
Fondamento per Estensioni Future: Il lavoro apre la strada all'adattamento di queste tecniche ad altri sistemi, come il System I polimorfico (System F modulo isomorfismi) o varianti non tipate come il distributive $\lambda$ -calculus. Inoltre, suggerisce direzioni per rimuovere i witness sintattici in favore di inferenza automatica degli isomorfismi.

In sintesi, il paper fornisce un ponte solido tra la teoria dei tipi modulo isomorfismi e la pratica della verifica formale, dimostrando che sistemi con equivalenze tipologiche complesse possono essere resi sicuri, terminanti e implementabili.