Normalization for multimodal type theory

Deze paper bewijst normalisatie voor MTT, een algemeen multimodaal type-theoretisch kader, en toont aan dat het bepalen van typecontrole en conversie kan worden gereduceerd tot het vergelijken van modaliteiten, wat leidt tot een typecontrole-algoritme voor alle instanties van MTT.

De kern

Dit is een samenvatting van het wetenschappelijke artikel "Normalization for Multimodal Type Theory" van Daniel Gratzer, vertaald naar begrijpelijk Nederlands met behulp van creatieve analogieën.

De Kernboodschap in Eén Zin

De auteur heeft een manier bedacht om te bewijzen dat een zeer complexe, flexibele taal voor computerwiskunde (MTT) altijd "op orde" is, wat betekent dat computers deze taal betrouwbaar kunnen controleren en begrijpen, zelfs als de regels ervan enorm ingewikkeld zijn.

---

1. Het Probleem: De "Multimode" Chaos

Stel je voor dat je een taal leert om over de wereld te praten. Normaal gesproken zijn regels voor deze taal overal hetzelfde (als je "appel" zegt, bedoel je een fruit).

Maar in Modale Type Theory (MTT) hebben we te maken met verschillende "werelden" of modi.

• In wereld A is een "appel" misschien gewoon een fruit.
• In wereld B (bijvoorbeeld een wereld van tijd) is een "appel" iets dat in de toekomst bestaat.
• In wereld C (een wereld van geheimen) is een "appel" iets dat je niet mag zien.

De uitdaging is dat je regels moet hebben die werken als je van wereld A naar wereld B springt. Dit is als een tolk die niet alleen vertaalt, maar ook de regels van de wetten in elk land kent. Als je deze regels verkeerd toepast, stort het hele systeem in.

Vroeger was het bewijzen dat deze talen "stabiel" waren (dat ze geen fouten maken) als het proberen te bouwen van een kasteel van kaarten in een storm. Elke keer dat je een nieuwe wereld toevoegde, moest je alles opnieuw uitvinden.

2. De Oplossing: De "Normale" Vorm

In de computerwetenschap willen we weten of twee uitdrukkingen hetzelfde betekenen. Bijvoorbeeld: is (2 + 2) * 3 hetzelfde als 12?
Om dit te weten, moeten we de uitdrukkingen reduceren tot hun normale vorm.

• Analogie: Stel je voor dat je een rommelige kamer hebt vol met kleding, dozen en spullen. De "normale vorm" is de kamer die perfect is opgeruimd: elke kledingstuk hangt in de kast, elke doos is gelabeld.
• Als je twee kamers hebt die er heel anders uitzien, maar als je ze allebei perfect opruimt, zien ze er precies hetzelfde uit, dan waren ze oorspronkelijk hetzelfde.

Het probleem met MTT is dat het opruimen (de "normalisatie") zo complex was dat niemand zeker wist of het altijd lukte. Zonder die zekerheid kunnen computers de taal niet betrouwbaar controleren.

3. De Magische Techniek: "Synthetische Tait Computabiliteit"

Gratzer gebruikt een nieuwe techniek die hij "Synthetische Tait Computabiliteit" noemt. Laten we dit uitleggen met een metafoor.

Stel je voor dat je een spiegel wilt bouwen die niet alleen je afbeelding weerspiegelt, maar ook laat zien of je kleding netjes is.

• De oude manier: Je zou elke kledingstuk één voor één moeten controleren en een lijst maken van wat "netjes" is. Dit is extreem veel werk en foutgevoelig.
• De nieuwe manier (Gluing/Plakken): In plaats van alles handmatig te controleren, bouw je een magische spiegelwereld (een "geplakt model").
  • In deze spiegelwereld zijn de regels zo ontworpen dat "netjes zijn" automatisch gebeurt.
  • Als je een object uit de echte wereld in deze spiegelwereld plaatst, wordt het daar automatisch opgeruimd.
  • Als je het dan terugneemt, heb je je oorspronkelijke object, maar nu in de perfecte, opgeruimde vorm.

Gratzer heeft bewezen dat je deze "spiegelwereld" kunt bouwen voor MTT, zelfs met al die verschillende werelden (modi) en de complexe regels om tussen hen te reizen.

4. Waarom is dit belangrijk?

Dit bewijs is een doorbraak om drie redenen:

1. Betrouwbaarheid: Het betekent dat elke versie van deze taal die iemand ooit bedenkt (voor beveiliging, cryptografie, of het modelleren van tijd), automatisch controleerbaar is. Computers kunnen nu zeggen: "Ja, dit programma is correct" zonder twijfel.
2. Flexibiliteit: Omdat de techniek zo algemeen is, hoeven onderzoekers niet meer voor elke nieuwe "wereld" (bijvoorbeeld een nieuwe manier om tijd of geheime data te modelleren) opnieuw te bewijzen dat het werkt. Ze kunnen de "spiegelwereld" gewoon hergebruiken.
3. Efficiëntie: Het biedt een algoritme (een recept) voor computers om deze complexe taal te verwerken. Dit opent de deur voor betere programmeertools en veiligere software.

Samenvattend

Daniel Gratzer heeft een universele "opruimmachine" ontworpen voor een zeer ingewikkelde taal die verschillende werelden met elkaar verbindt. Hij heeft bewezen dat deze machine altijd werkt, ongeacht hoe gek de regels van de wereld zijn. Hierdoor kunnen we nu vertrouwen op computers om deze taal te gebruiken voor de meest geavanceerde en veilige toepassingen, zonder bang te hoeven zijn voor verborgen fouten.

Het is alsof hij een nieuwe soort kompas heeft uitgevonden dat altijd de juiste richting aangeeft, zelfs als je door een labyrint van verschillende dimensies loopt.

Technische samenvatting

Probleemstelling

De paper adresseert het ontbreken van een normalisatie-algoritme voor MTT (Multimodal Type Theory), een generalisatie van afhankelijke type-theorieën die modaliteiten (modi) en transformaties tussen deze modaliteiten ondersteunt. MTT is ontworpen om diverse specifieke modale theorieën te kunnen modelleren, zoals die voor guarded recursion, geïnternaliseerde parametriciteit en andere prototypische modale situaties.

Hoewel eerdere werken (Gratzer et al., 2020a) de correctheid (soundness) en canoniciteit van gesloten termen in MTT hadden bewezen, bleef de vraag of MTT een normalisatie-algoritme toelaat en of type-checking beslisbaar is, open. De complexiteit van MTT ligt in de rijke substitutiestructuur die voortkomt uit de onderliggende "mode theory" (een strikte 2-categorie). Deze structuur introduceert subtiele vergelijkingen tussen termen die het bewijzen van metatheoretische eigenschappen bemoeilijken. Traditionele methoden voor normalisatie, zoals Normalization-by-Evaluation (NbE), bleken te complex of niet direct toepasbaar op de multimodale structuur van MTT zonder de substitutiestructuur te vereenvoudigen op een manier die de theorie onbruikbaar maakt.

Methodologie

De auteur gebruikt een geavanceerde variant van Synthetic Tait Computability (STC), een abstracte aanpak voor het construeren van "gluing"-modellen (klevende modellen) om normalisatie te bewijzen. De kern van de methode bestaat uit de volgende stappen:

1. Synthetische Gluing: In plaats van een normalisatie-algoritme handmatig te definiëren en vervolgens correctheid te bewijzen, construeert de auteur een specifiek model van type-theorie (een "normalization cosmos") waarin normalisatie intrinsiek is. Dit wordt gedaan door een Artin-gluing toe te passen op een functor tussen categorieën van contexten.
2. Multimodal Synthetic Tait Computability (MSTC): De paper generaliseert STC naar de multimodale setting. Waar eerdere STC-bewijzen binnen één topos werkten, werkt deze paper binnen de interne taal van extensional MTT zelf. Dit stelt de auteur in staat om tegelijkertijd in een netwerk van topoi (één per modus) te werken.
   • De constructie maakt gebruik van lex idempotent monads (# en ``) die de open en gesloten deeltopoi binnen het ge-glueide model vertegenwoordigen.
   • Een cruciaal ingrediënt is de realignment axiom (heralignering), die het mogelijk maakt om objecten die slechts tot op isomorfisme overeenkomen met de syntactische structuur, strikt gelijk te maken aan de syntactische termen. Dit lost het probleem op dat connectieven in type-theorie vaak alleen tot op definitorische gelijkheid universele eigenschappen hebben.
3. Constructie van het Normalisatie-Cosmos:
   • De auteur definieert een "normalization cosmos" $\mathcal{G}$ als een ge-glueide presheaf-cosmos.
   • Binnen dit model worden termen geïnterpreteerd als paren bestaande uit een syntactisch object en een "proof-relevant predicate" (een predikaat dat aangeeft of een term een normaal vorm heeft).
   • De normalisatiefunctie wordt afgeleid uit de projectie van dit model naar de initiële syntactische model.

Belangrijkste Bijdragen

1. Normalisatie voor MTT: Het eerste bewijs dat MTT een normalisatie-algoritme toelaat. Dit geldt voor de volledige suite van connectieven: afhankelijke sommen, producten, booleaanse waarden, intensionele identiteitstypen, een universum en modale typen.
2. Beslisbaarheid van Type-checking: Het bewijs dat type-checking en conversie in MTT beslisbaar zijn, mits de gelijkheid van modaliteiten en 2-cellen in de onderliggende mode theory beslisbaar is. Dit is een fundamenteel resultaat voor de implementatie van MTT.
3. Generalisatie van STC: De introductie van Multimodal Synthetic Tait Computability (MSTC). Dit is een nieuwe methode die STC uitbreidt naar multimodale settingen, waarbij de modaliteiten van MTT worden gebruikt als metalanguage om de gluing-construktie zelf te definiëren.
4. Injectiviteit van Type-constructoren: Het bewijs dat type-constructoren in MTT injectief zijn (bijv. als $A \to B = C \to D$, dan is $A=C$ en $B=D$), wat essentieel is voor efficiënte implementaties.
5. Extensie met Crisp Inductie: De paper toont aan dat de normalisatiebewijsmethode robuust is en kan worden uitgebreid om crisp inductie-principes (voor identiteitstypen onder modaliteiten) te ondersteunen, zonder de geldigheid van normalisatie te verliezen.

Resultaten

• Theorema 6.4: Er bestaat een functie $nf_\Gamma(M, A)$ die een term $M$ van type $A$ in context $\Gamma$ afbeeldt op een normaal vorm $u$, zodanig dat:
  • Soundness: De decoding van de normaal vorm is gelijk aan de oorspronkelijke term ($|u| = M$).
  • Completeness: Als twee termen gelijk zijn ($M = N$), dan zijn hun normaal vormen identiek ($nf(M) = nf(N)$).
  • Idempotentie: Het normaliseren van een reeds normaal vorm levert dezelfde vorm op.
• Corollarium 6.10: Type-checking is beslisbaar als de mode theory beslisbaar is.
• Corollarium 6.11: Canoniciteit geldt voor MTT zonder de extra gelijkheid $1.{\mu} = 1$ die in eerdere werken nodig was om de constructie te "temmen".
• Theorema 7.2: Er wordt aangetoond dat "modal extensionality" (de equivalentie tussen modale gelijkheid en gelijkheid onder modaliteit) niet vanzelfsprekend is in intensionele MTT, maar dat crisp inductie wel consistent is met normalisatie.

Significantie

De resultaten van deze paper zijn van groot belang voor de theorie en praktijk van modale type-theorieën:

• Theoretische Voltooiing: Het sluit een belangrijke lacune in de literatuur door te bewijzen dat de flexibele MTT-structuur niet ten koste gaat van de fundamentele eigenschappen van type-theorieën, zoals normalisatie en beslisbaarheid.
• Implementatie: Het biedt de theoretische basis voor het bouwen van praktische type-checkers en compilers voor MTT en de vele specifieke calculi die erop gebaseerd zijn (zoals guarded recursion en parametriciteit). De noodzaak van een beslissingsprocedure voor de mode theory is een concrete, haalbare voorwaarde.
• Methodologische Doorbraak: De toepassing van MSTC toont aan dat het gebruik van de object-theorie (MTT) als metalanguage voor het bewijzen van eigenschappen van diezelfde theorie een krachtige en schaalbare techniek is. Dit maakt het mogelijk om complexe metatheoretische resultaten voor multimodale systemen te bewijzen die met traditionele, handmatige gluing-methoden ondoenlijk zouden zijn.
• Unificatie: Het resultaat verenigt diverse eerder handmatig bewezen resultaten voor specifieke modale theorieën onder één paraplu van een algemeen bewijs.

Kortom, dit werk transformeert MTT van een theoretisch raamwerk met onzekerheid over zijn computatie-eigenschappen naar een volledig onderbouwde, implementeerbare type-theorie met gegarandeerde normalisatie en type-checking.