Definitional Inversion, Without Normalisation

Stel je voor dat je een enorme, magische bibliotheek bouwt waar elk boek een wiskundig bewijs is, en de planken zelf van logica zijn gemaakt. Dit is de wereld van afhankelijke typesystemen (dependent type systems), de geheime motor achter moderne bewijsassistenten zoals Lean en programmeertalen zoals Idris. In deze wereld zijn de regels ongelooflijk streng: als je een "kat" op een plank probeert te zetten met het label "getallen", moet het beveiligingssysteem van de bibliotheek (de type checker) onmiddellijk "Error!" schreeuwen en je stoppen. Deze veiligheid rust op een concept genaamd definitionele gelijkheid (definitional equality), wat de manier is waarop de bibliotheek beslist of twee dingen essentieel hetzelfde zijn. Bijvoorbeeld: is een "vierkant" gewoon een "rechthoek met gelijke zijden"? Als het systeem "ja" zegt, behandelt het ze als identiek.

Het controleren van deze regels is echter lastig. Traditioneel moesten wiskundigen, om te bewijzen dat de bibliotheek veilig is, aantonen dat elk boek kan worden vereenvoudigd tot zijn meest eenvoudige, meest basale vorm (een proces dat normalisatie wordt genoemd). Maar veel moderne, krachtige bibliotheken zijn ontworpen om oneindig of zelfverwijzend te zijn, wat betekent dat ze niet kunnen worden vereenvoudigd tot een definitieve stop. Het is als het proberen te plat te slaan van een fractal; je blijft steeds meer detail vinden. Een lange tijd konden we, als een systeem niet kon worden vereenvoudigd, niet bewijzen dat het veilig was. Dit artikel introduceert een nieuwe manier om de veiligheid van de bibliotheek te controleren zonder eerst de fractal te hoeven afplatten.

---

De Oneindige Puzzel en de Magische Spiegel

Beschouw een afhankelijk typesysteem als een gigantische, zelfcontrolerende puzzel. De stukjes zijn types (zoals "getallen" of "functies"), en het doel is om ervoor te zorgen dat wanneer je twee stukjes aan elkaar klikt, ze perfect passen. De meest cruciale regel in deze puzzel is definitionele inversie (definitional inversion). Dit is de logica die zegt: "Als twee complexe structuren er hetzelfde uitzien, moeten hun onderdelen ook hetzelfde zijn." Bijvoorbeeld, als je twee functietypes hebt die identiek zijn, bewijst het artikel dat hun inputtypes en outputtypes ook identiek moeten zijn. Dit is cruciaal omdat het de computer in staat stelt om complexe code veilig af te breken in kleinere stukjes zonder in de war te raken.

Decennialang was de enige manier om te bewijzen dat deze stukjes pasten het gebruik van een methode genaamd confluentie (controleren of verschillende paden van vereenvoudiging leiden tot hetzelfde resultaat) of logische relaties (een complexe manier om te vergelijken hoe termen zich gedragen). Maar deze oude instrumenten liepen tegen een muur aan. Confluentie valt uiteen wanneer je bepaalde "extensionele" regels toevoegt (zoals $\eta$-wetten, die zeggen dat een functie volledig wordt gedefinieerd door wat hij doet, en niet door hoe hij is geschreven). Logische relaties vereisen meestal dat het systeem "normaliserend" is (in staat is om te stoppen met vereenvoudigen), wat veel krachtige, real-world programmeertalen die oneindige loops of zelfverwijzende types toestaan, uitsluit.

De Nieuwe Aanpak: Een Kaart van Mogelijkheden

De auteurs, een team van computerwetenschappers en wiskundigen, stellen een frisse strategie voor die gebaseerd is op domeintheorie (domain theory). In plaats van te proberen de puzzelstukjes te dwingen tot één enkele definitieve vorm, bouwen zij een kaart van alle mogheden gedrag.

Stel je voor dat je probeert een mysterieus wezen in een donker bos te identificeren.

• De Oude Manier: Je wacht tot het wezen stopt met bewegen en zijn ware, definitieve vorm onthult. Als het wezen nooit stopt met bewegen (omdat het een oneindige loop is), kun je het niet identificeren, en is het bos onveilig.
• De Nieuwe Manier: Je wacht niet tot het wezen stopt. In plaats daarvan observeer je de voetafdrukken. Je merkt op dat het een "linkervoet"-afdruk achterlaat, dan een "rechtervoet"-afdruk, en dan weer een "linkervoet"-afdruk. Zelfs als het wezen nooit stopt met lopen, kun je de vorm ervan afleiden door naar het patroon van zijn stappen te kijken.

In de taal van het artikel zijn deze "voetafdrukken" compacte elementen of eindige observaties. De auteurs construeren een wiskundig "domein" (een gestructureerde ruimte) waar elk type niet wordt gerepresenteerd door een definitief antwoord, maar door de verzameling van alle eindige zaken die we over het kunnen observeren. Ze gebruiken een techniek genaamd finitaire projectoren om dit domein in hanteerbare brokken te snijden.

Wat Ze Hebben Gevonden

Met deze "voetafdruk"-methode is het team erin geslaagd te bewijzen dat definitionele inversie standhoudt, zelfs in systemen die:

1. Nooit stoppen met vereenvoudigen (niet-normaliserend), zoals systemen met een "type-in-type" regel (waarbij een type zichzelf kan bevatten).
2. $\eta$-wetten bevatten, welke lastige regels die functies en paren intuïtiever laten gedragen maar traditionele bewijsmethoden doorbreken.

Ze hebben dit gedemonstreerd op een kleine, kernversie van een type theory genaamd MLTT$\eta$ (Martin-Löf Type Theory met $\eta$-wetten). Ze lieten zien dat zelfs in dit chaotische, potentieel oneindige systeem, als twee types gelijk zijn, hun bouwstenen ook gelijk moeten zijn. Dit is een grote prestatie omdat het bewijst dat het "veiligheidsnet" van het typesysteem werkt, zelfs wanneer het systeem de ruimte krijgt om rommelig en oneindig te zijn.

Waarom Dit Belangrijk Is

De auteurs hebben niet alleen een puzzel opgelost voor een klein speelgoedsysteem; ze hebben aangetoond dat hun methode robuust is. Ze hebben hun bewijs uitgebreid naar:

• Afhankelijke sommen (paren van data).
• Unit types (een type met slechts één waarde).
• Vaste-punt combinatoren (instrumenten die oneindige recursie mogelijk maken).
• Natuurlijke getallen met patroonmatching.
• Identiteitstypes (bewijzen dat twee dingen hetzelfde zijn).
• Bewijs-irrelevante proposities (waarbij de inhoud van een bewijs er niet toe doet, alleen dat het bestaat).

Ze hebben zelfs een model gebouwd voor een "universum van strikte proposities", waarmee ze aantonen dat hun techniek de complexe kenmerken kan hanteren die te vinden zijn in real-world tools zoals Lean, Agda en Rocq.

De Limieten en de Toekomst

Het artikel is zeer duidelijk over wat het niet doet. Het bewijst niet dat deze systemen "normaliserend" zijn (dat ze altijd stoppen). Sterker nog, het werkt expliciet voor systemen die niet stoppen. Het lost ook het probleem van "neutrals" (variabelen die nog niet zijn ingevuld) niet op dezelfde manier op als het dat doet voor gesloten termen, hoewel het hint naar hoe dat in de toekomst mogelijk kan worden gedaan.

De auteurs hebben hun wiskundige bewijzen al omgezet in code, en hebben deze drie keer geverifieerd in drie verschillende bewijsassistenten (Agda, Lean en Rocq). Dit suggereert dat hun methode niet alleen een theoretisch idee is, maar een praktisch hulpmiddel.

De Kernboodschap

Dit artikel is alsof je de bouwers van de magische bibliotheek een nieuwe bril geeft. Voorheen konden ze de veiligheid van de bibliotheek alleen controleren als de boeken statisch en af waren. Nu kunnen ze de veiligheid controleren van boeken die nog steeds geschreven worden, of boeken die zichzelf eeuwig verwijzen. Door te focussen op het observeerbare gedrag (de voetafdrukken) in plaats van de definitieve bestemming (de stop), hebben ze de deur geopend naar het verifiëren van de meest krachtige, complexe en potentieel oneindige typesystemen die we ons kunnen voorstellen. Dit legt de basis voor "Lean4Lean" en "MetaRocq"—projecten waarbij bewijsassistenten hun eigen code verifiëren—waardoor de instrumenten die we gebruiken om wiskunde en software te bouwen, nog betrouwbaarder worden.