💻 computer science

A formalization of System I with type Top in Agda

Dit artikel presenteert een variant van System I met het type Top en bevat een volledige formalisatie in Agda, inclusief bewijzen van voortgang en sterke normalisatie.

Oorspronkelijke auteurs: Agustín Séttimo, Cristian Sottile, Cecilia Manzino

Gepubliceerd 2026-03-26

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Agustín Séttimo, Cristian Sottile, Cecilia Manzino

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een enorme bibliotheek hebt waar boeken op de plank staan. In de wereld van de informatica (en wiskunde) zijn deze boeken programma's en de regels voor hoe ze op de plank moeten staan zijn typen.

Normaal gesproken is een boek met de titel "Hoe je een taart bakt" heel anders dan een boek "Hoe je een taart bakt, stap voor stap". In de meeste programmeertalen zijn dit twee totaal verschillende boeken. Maar wat als we zeggen: "Wacht even, deze twee boeken vertellen precies hetzelfde verhaal, alleen in een andere volgorde"? Dan zouden ze eigenlijk hetzelfde boek moeten zijn.

Dit is het idee achter System I, een manier van programmeren waarbij je verschillende vormen van hetzelfde idee als gelijk behandelt. De auteurs van dit paper, Agustín, Cristian en Cecilia, hebben nu een nieuwe versie van dit systeem bedacht en het volledig in een computerprogramma (Agda) nagemaakt om te bewijzen dat het werkt.

Hier is de uitleg, vertaald naar alledaagse taal:

1. Het Probleem: De Verwarde Bibliotheek

Stel je voor dat je een robot hebt die boeken moet sorteren.

Als je de robot vraagt om een boek te halen dat "A en B" bevat, en er ligt een boek "B en A", dan zegt de robot: "Die zijn niet hetzelfde! Ik kan die niet vinden."
In de echte wereld weten we dat "A en B" hetzelfde is als "B en A".
System I is de robot die dit wel snapt. Hij zegt: "Ah, dit is hetzelfde boek, ik kan het omwisselen."

Maar er is een probleem: als je de robot te veel vrijheid geeft om boeken om te wisselen, kan hij in een oneindige lus raken. Hij wisselt boek A om naar B, dan B naar A, dan weer A naar B... en hij stopt nooit. Dit noemen we in de computerwereld een "eindeloze lading" (geen strong normalization).

2. De Oplossing: De "Top"-Stempel en de Bewijskaartjes

De auteurs voegen een nieuw boek toe aan de bibliotheek: Top. Dit is een heel speciaal boek dat altijd waar is (zoals "Het is vandaag dag").

De uitdaging: Hoe zorg je dat de robot niet vastloopt als hij dit nieuwe boek moet verwerken?
De truc: Ze laten de robot niet zomaar boeken omwisselen. Ze geven hem kaartjes (witnesses).
- Als je wilt zeggen dat boek A gelijk is aan boek B, moet je een kaartje tonen met de reden waarom (bijvoorbeeld: "commutatie" of "associatie").
- De robot mag alleen een boek veranderen als hij het juiste kaartje heeft.
- Belangrijker nog: elke keer dat hij een kaartje gebruikt, wordt het kaartje "opgebruikt" of veranderd. Hij kan het niet oneindig vaak gebruiken om hetzelfde boek heen en weer te wisselen. Dit zorgt ervoor dat de robot uiteindelijk stopt met zoeken en een antwoord geeft.

3. De "Agda"-Bouwplaat

De auteurs hebben dit hele systeem niet alleen bedacht, maar het ook nagemaakt in een taal die heet Agda.

Denk aan Agda als een super-strict bouwpakket (zoals LEGO, maar dan voor wiskundigen).
In dit pakket kun je geen fouten maken. Als je een stukje bouwt dat niet klopt, past het gewoon niet in de rest.
Ze hebben laten zien dat als je een programma (een boek) in dit systeem bouwt, het altijd afgerond wordt. Het bouwt zichzelf nooit in een kluwen waaruit je niet meer kunt komen.

4. Waarom is dit belangrijk? (De Analogie van de Eetkamer)

Stel je voor dat je een recept hebt voor een taart.

Systeem zonder isomorfie: Je moet de ingrediënten in de exacte volgorde toevoegen die op het recept staat. Als je suiker en eieren verwisselt, zegt de computer: "Fout! Dit werkt niet."
Systeem I: De computer zegt: "Geen probleem, suiker en eieren zijn verwisselbaar, het resultaat is hetzelfde."
Het nieuwe systeem (met Top): Ze hebben een nieuwe regel toegevoegd: "Als je een ingrediënt niet nodig hebt (zoals 'Top', wat niets toevoegt), mag je het weglaten of toevoegen, zolang je maar laat zien waarom."

De grote prestatie van dit paper is dat ze bewezen hebben dat je, zelfs met al deze vrijheden, nooit in een situatie terechtkomt waar je taart nooit klaar wordt. De robot (de computer) zal altijd stoppen met bakken en je een taart geven.

5. Het Grote Bewijs: "Progress" en "Strong Normalization"

De auteurs hebben twee dingen bewezen in hun bouwpakket:

Progress (Vooruitgang): Elke keer dat de robot een stap zet, komt hij dichter bij het eindresultaat. Hij stopt nooit halverwege met een "ik weet het niet"-gehalte, tenzij hij al klaar is.
Strong Normalization (Sterke Normalisatie): Dit is het belangrijkste. Het betekent dat er geen enkele weg is die de robot kan kiezen die hem oneindig laat ronddraaien. Of je nu de suiker eerst doet of de eieren, of je nu het boek "A en B" omwisselt naar "B en A", je komt altijd op hetzelfde punt uit en stopt altijd.

Samenvatting

Dit paper is als een garantiecertificaat voor een heel slimme, flexibele robot.

Wat hebben ze gedaan? Ze hebben een nieuwe, slimmere robot gebouwd die boeken (programma's) kan herschrijven zonder de betekenis te verliezen.
Hoe hebben ze het gedaan? Ze hebben elke herschrijving vastgelegd op een kaartje, zodat de robot niet in een cirkel kan lopen.
Wat is het resultaat? Ze hebben in een computerprogramma bewezen dat deze robot altijd stopt en een goed resultaat levert.

Dit is een enorme stap voor programmeurs en wiskundigen, omdat het betekent dat we veiliger en flexibeler kunnen programmeren zonder bang te hoeven zijn dat onze software in een oneindige lus vastloopt. Ze hebben de "theorie" omgezet in een "onweerlegbaar bewijs" met de hulp van de computer.

Probleemstelling

De studie van type-isomorfieën is een groeiend onderzoeksgebied met toepassingen in programmeertalen en bewijssystemen. Door isomorfe types als gelijk te beschouwen, kunnen programma's met verschillende syntaxis maar equivalente semantiek worden geïdentificeerd. Dit stelt echter complexe uitdagingen aan de vormgeving van lambda-calculi:

Determinisme en Typebehoud: In systemen zoals System I (een simply-typed lambda calculus met paren modulo isomorfieën) leidt het identificeren van isomorfe types tot non-determinisme in de reductie. Bijvoorbeeld, door de commutativiteit van paren ( $A \times B \equiv B \times A$ ) is het niet langer duidelijk welk element van een paar wordt geselecteerd door projectie.
Normalisatie: Het toevoegen van nieuwe typeconstructoren (zoals Top) en het handhaven van sterke normalisatie (dat elke reductieketen eindigt) vereist zorgvuldige keuzes in de reductieregels en de behandeling van isomorfieën op termniveau.
Formalisatie: Bestaande systemen zijn vaak moeilijk volledig te formaliseren in bewijsassistenten zoals Agda, vooral vanwege de complexe interactie tussen type-isomorfieën, substitutie en de noodzaak van expliciete getuigen (witnesses) voor typeconversies.

Methodologie

De auteurs hebben een variant van System I ontwikkeld die het type Top (de eenheidstype) omvat en deze volledig hebben geformaliseerd in Agda. De methodologische aanpak kenmerkt zich door:

Intrinsieke Typing: In plaats van extrinsieke termen (waarbij termen en types los van elkaar worden gedefinieerd), gebruiken de auteurs een intrinsieke benadering. Termen zijn direct gedefinieerd als bewijs van een type in een context. Dit garandeert dat elke gedefinieerde term correct getypeerd is.
Expliciete Getuigen (Witnesses): Om de conversieregel ( $A \equiv B \vdash t : A \Rightarrow t : B$ ) te hanteren, wordt een expliciete syntactische constructor [ρ]≡t gebruikt, waarbij ρ een getuige is van de isomorfie. Dit maakt de toepassing van isomorfieën syntax-gestuurd en voorkomt ambiguïteit.
De Bruijn Indexen: Variabelen worden weergegeven met De Bruijn-indexen om de formalisatie compacter te maken en naamproblemen te vermijden.
Reductie en Equivalentie: De reductierelatie ( $\leadsto$ ) wordt gedefinieerd als de vereniging van de klassieke $\beta$ -reductie en een equivalentierelatie ( $\Leftrightarrow$ ) die specifiek is ontworpen om isomorfieën op termniveau te elimineren. In tegenstelling tot eerdere werken waar equivalentie en reductie gescheiden waren, worden hier corresponderende termen van isomorfe types direct als een reductiestap behandeld.
Normalisatiebewijs: Voor het bewijs van sterke normalisatie gebruiken de auteurs de techniek van "reducibility" (Tait/Girard), aangepast volgens de methode van Schäfer en Kovács. Dit maakt gebruik van een interpretatie van termen in een verzameling van sterk genormaliseerde termen ($SN$), uitgebreid met een predicat $P$ om de inductie te faciliteren.

Belangrijkste Bijdragen

Extensie van System I met Top: De auteurs introduceren een calculus die het type Top bevat, inclusief de bijbehorende isomorfieën (zoals $A \times \top \equiv A$ en $A \to \top \equiv \top$ ). Ze passen de regels aan om een deterministische en genormaliseerde calculus te garanderen.
Volledige Formalisatie in Agda: Het artikel presenteert een complete implementatie in Agda, inclusief de syntaxis, type-regels, semantiek en de bewijzen. De code is beschikbaar in een open-source repository.
Bewijs van Progress en Sterke Normalisatie:
- Progress: Bewezen dat elke gesloten, getypeerde term ofwel een waarde is of kan reduceren.
- Sterke Normalisatie: Bewezen dat elke reductieketen vanuit een getypeerde term eindigt. Dit is cruciaal omdat de aanwezigheid van Top en isomorfieën normaal gesproken oneindige reducties (zoals de term $\Omega$ ) zou kunnen toelaten. De auteurs tonen aan dat hun aanpak met expliciete getuigen dit voorkomt.
Implementatie van Evaluatie: Omdat sterke normalisatie is bewezen, kunnen de auteurs een totale evaluatiefunctie definiëren die een reductieketen produceert van een term tot een waarde.

Resultaten

Correctheid: De formalisatie bevestigt dat de variant van System I met Top en expliciete getuigen zowel progress als sterke normalisatie bezit.
Behandeling van $\Omega$ : De auteurs demonstreren hoe de term $\Omega = (\lambda x.x)(\lambda x.x)$ , die in een calculus zonder getuigen en met Top vaak tot een probleem leidt, in hun systeem correct wordt gereduceerd tot ⋆ (de waarde van Top). Dit wordt mogelijk gemaakt door de specifieke reductieregels die isomorfieën systematisch elimineren.
Efficiëntie van de Methode: De gebruikte aanpak van Schäfer/Kovács bleek zeer geschikt voor Agda, omdat deze minder complex is dan klassieke reducibility-bewijzen en beter aansluit bij constructieve logica.

Betekenis en Impact

Voor Programmeertalen: Het werk biedt een theoretische basis voor programmeertalen die isomorfieën gebruiken om code flexibeler te maken (bijvoorbeeld het willekeurig ordenen van argumenten). De garantie van sterke normalisatie is essentieel voor de betrouwbaarheid van dergelijke talen.
Voor Bewijssystemen: Het illustreert hoe "proof-irrelevance" (het behandelen van verschillende bewijzen van dezelfde stelling als gelijk) kan worden geïmplementeerd zonder de logica inconsistent te maken.
Voor Formele Methodologie: Dit is, naar weten van de auteurs, de eerste volledige formalisatie van een normalisatiebewijs voor een lambda-calculus modulo isomorfieën in een bewijsassistent. Het toont aan dat complexe systemen met type-isomorfieën rigoureus kunnen worden geverifieerd.
Toekomstperspectief: De formalisatie vormt een fundament voor verdere uitbreidingen, zoals polymorfe systemen (System F modulo isomorfieën) of het verwijderen van de syntactische getuigen ten gunste van type-inferentie.

Samenvattend biedt dit artikel een robuust, formeel bewezen raamwerk voor het werken met type-isomorfieën in een simply-typed lambda calculus, waarbij de valkuilen van non-determinisme en oneindige reducties worden overwonnen door een zorgvuldig ontworpen syntactische structuur en een geavanceerde normalisatiemethode.