Non-Derivability Results in Polymorphic Dependent Type Theory

Dit artikel toont aan dat in de pure polymorfe afhankelijke typetheorie ($\lambda$P2) de afleidbaarheid van inductie- en co-inductieprincipes voor kwotiënt- en co-inductieve typen onmogelijk is, en dat functieverlenging een cruciale voorwaarde is voor het bewijzen van inductie.

De kern

Titel: Waarom je niet kunt bewijzen wat je wilt in de wereld van wiskundige logica

Stel je voor dat je een gigantische, onfeilbare bouwset hebt. Dit is λP2 (een geavanceerde vorm van wiskundige logica). Met deze set kun je alles bouwen: van simpele blokken (data) tot ingewikkelde machines (functies). De uitvinder van deze set, Stefano Berardi, is de jarige die we vandaag vieren.

De auteur van dit artikel, Herman Geuvers, zegt: "Deze bouwset is geweldig, maar hij heeft een groot gebrek. Je kunt wel de blokken bouwen, maar je kunt niet altijd bewijzen dat ze echt werken zoals je denkt."

Hier is wat Geuvers ontdekt, vertaald in alledaags taal:

1. De "Magische" Blokken die niet werken

In deze wereld kun je een "natuurlijk getal" (1, 2, 3...) bouwen door te zeggen: "Een getal is iets dat je kunt herhalen." Dat klinkt slim, maar er zit een addertje onder het gras.

• Het probleem: Je kunt een machine bouwen die getallen telt, maar je kunt niet bewijzen dat deze machine altijd correct telt als je hem oneindig vaak gebruikt. In de wiskunde noemen we dit het "inductie-principe". Het is alsof je een ladder bouwt, maar je kunt niet bewijzen dat elke sport van de ladder stevig is, alleen dat de eerste sport er is.
• De ontdekking: Geuvers laat zien dat je, hoe slim je ook bent met je bouwset, dit bewijs nooit kunt vinden. Het is alsof je probeert een sleutel te maken die een deur opent, maar de deur is ontworpen zodat die sleutel er nooit in past.

2. De "Stream" (Stroom) die niet stopt

Stel je voor dat je een rivier (een 'stream') bouwt die oneindig doorstroomt. Je wilt dat deze rivier de "ultieme" rivier is, waar alle andere rivieren op lijken.

• Het probleem: Geuvers toont aan dat je in deze bouwset een rivier kunt maken die eruitziet als een echte stroom, maar die niet voldoet aan de regels van een echte, perfecte stroom. Twee rivieren kunnen er exact hetzelfde uitzien als je er even naar kijkt, maar als je ze van dichtbij bekijkt, blijken ze verschillend te zijn. De bouwset laat je niet toe om te zeggen: "Als ze er hetzelfde uitzien, zijn ze hetzelfde."

3. De "Groep" die niet bestaat

Soms wil je een groep mensen maken waarbij iedereen die op elkaar lijkt, als één persoon wordt behandeld. Dit noemen we een "quotiënt" (een soort samenvoeging).

• Het probleem: Geuvers bewijst dat je in de basis-bouwset geen echte, flexibele groepen kunt maken die voor elke situatie werken. Je kunt ze wel voor één specifieke situatie maken, maar niet als een universele regel. Het is alsof je probeert een universele paspoort te maken voor iedereen, maar de set heeft alleen paspoorten voor mensen met blauwe ogen.

4. De Oplossing: Wat ontbreekt er?

Aan de andere kant van het verhaal kijken we naar een uitgebreide versie van de bouwset. Wetenschappers hebben gezegd: "Als we drie nieuwe gereedschappen toevoegen, kunnen we de problemen oplossen."

1. Identiteitsgereedschap: Om te zeggen "dit is hetzelfde als dat".
2. Uniekheid: Om te zeggen "er is maar één manier om te zeggen dat iets hetzelfde is".
3. Functie-uitbreiding (FunExt): Dit is de magische sleutel. Het zegt: "Als twee machines voor elke input hetzelfde resultaat geven, dan zijn ze dezelfde machine."

Geuvers' grote ontdekking is dit: Zelfs als je de eerste twee gereedschappen toevoegt, werkt het nog steeds niet. Je kunt nog steeds geen bewijs vinden dat de getallenmachine werkt.
Pas als je de derde gereedschap (FunExt) toevoegt, werkt het.

De Metafoor: De Bouwmeester en de Magische Smeer

Stel je voor dat je een auto bouwt (de data).

• In de oude set (λP2) kun je de auto bouwen, maar je kunt niet bewijzen dat hij rijdt als je de motor start.
• Sommige mensen zeiden: "Voeg een nieuwe motor toe (Identity types) en een nieuwe brandstof (Σ-types)."
• Geuvers zegt: "Nee, dat helpt niet. Je hebt een magische smeermiddel nodig (Function Extensionality). Zonder die smeermiddel blijven de onderdelen vastzitten, ook al heb je de beste motor."

Conclusie

Dit artikel is een eerbetoon aan Stefano Berardi, een briljante wiskundige. Geuvers laat zien dat in de wereld van wiskundige logica:

1. Je niet alles kunt bewijzen wat je wilt, tenzij je specifieke, krachtige regels toevoegt.
2. De regel "Functie-uitbreiding" (FunExt) is de cruciale regel. Zonder die ene regel blijven de logische machines vastlopen, zelfs als je alles anders perfect bouwt.

Het is een verhaal over de grenzen van logica en hoe we, door slimme experimenten met "tegen-modellen" (situaties waar dingen niet werken), eindelijk begrijpen wat er echt nodig is om de wereld van wiskunde en computers te laten werken.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het artikel "Non-Derivability Results in Polymorphic Dependent Type Theory" van Herman Geuvers, geschreven in het Nederlands.

Titel: Non-Derivability Results in Polymorphic Dependent Type Theory

Auteur: Herman Geuvers (Radboud Universiteit Nijmegen & TU Eindhoven)
Context: Essay aangeboden aan Stefano Berardi ter gelegenheid van zijn 64e verjaardag (EPTCS 441, 2026).

---

1. Probleemstelling

In de pure Calculus of Constructions (CC) en zijn sub-systeem $\lambda P2$ (polymorfe afhankelijke type-theorie) kunnen data-types (zoals natuurlijke getallen, lijsten) en functies daarover worden gedefinieerd via impredicatieve coderingen (bijv. Church-cijfers). Hoewel deze coderingen krachtig zijn, blijken ze onvoldoende om fundamentele redeneerprincipes af te leiden.

Het centrale probleem is dat inductie (voor inductieve data-types) en co-inductie (voor co-inductieve data-types zoals streams) niet bewijsbaar zijn in het pure $\lambda P2$, ongeacht hoe slim de codering van de data-types is.
Recente werken (o.a. Awodey, Frey, Speight [1] en Geuvers [8]) hebben aangetoond dat deze principes wel bewijsbaar worden in een uitgebreide versie van $\lambda P2$ die de volgende eigenschappen bevat:

1. Identiteits-types (Identity Types).
2. Uniekheid van identiteitsbewijzen (UIP - Uniqueness of Identity Proofs).
3. Functionele extensionaliteit (FunExt).
4. $\Sigma$-types (sterke som-types).

De open vragen die dit artikel adresseert zijn:

• Zijn deze uitbreidingen allemaal noodzakelijk?
• Zijn quotient-types (kwotiënten) en co-inductieve types (zoals streams) met de juiste principes al definieerbaar in het pure $\lambda P2$?
• Is het mogelijk om een "slimme" codering te vinden die inductie of co-inductie mogelijk maakt zonder de genoemde uitbreidingen?

2. Methodologie

De auteur gebruikt een model-theoretische aanpak om onmogelijkheidsresultaten (non-derivability) te bewijzen. In plaats van te proberen een afleiding te vinden, construeert hij specifieke tegenmodellen waarin de principes niet gelden.

• Modelsoort: De modellen zijn van een syntactische aard en gebaseerd op Weakly Extensional Combinatory Algebras (WECA). Een specifiek voorbeeld is de verzameling van open $\lambda$-termen modulo $\beta$- of $\beta\eta$-gelijkheid.
• Polyset Structure: Types worden geïnterpreteerd als verzamelingen van "realizers" (elementen van de algebra). Een polyset is een collectie van deze verzamelingen die gesloten is onder afhankelijke producten.
• Strategie: Als er een model bestaat waarin een type (bijv. het type dat inductie representeert) leeg is (niet bevolkt), dan kan er geen gesloten term van dat type bestaan in de theorie. Dit bewijst dat het principe niet afleidbaar is.
• Uitbreidingen: Voor het onderzoek naar de noodzaak van FunExt en UIP, worden de modellen uitgebreid met constanten voor identiteits-types ($\text{refl}, J$) en $\Sigma$-types, met specifieke reductieregels.

3. Belangrijkste Bijdragen en Resultaten

Het artikel levert drie hoofdresultaten op die de noodzaak van bepaalde uitbreidingen bevestigen:

A. Geen Co-inductie voor Streams in $\lambda P2$

• Resultaat: De standaard, polymorf definieerbare stream-type (gebaseerd op existentiële codering) is geen finale co-algebra in $\lambda P2$.
• Bewijs: Er wordt een model geconstrueerd waarin twee streams $s_1$ en $s_2$ bestaan die bisimulair zijn (ze produceren dezelfde waarden en gedrag), maar niet gelijk zijn ($s_1 \neq s_2$).
• Conclusie: Omdat bisimilariteit niet impliceert dat de streams gelijk zijn, geldt het co-inductieprincipe niet. Er is dus geen manier om streams in puur $\lambda P2$ te definiëren met een geldig co-inductieprincipe.

B. Geen Parametrische Quotient-types in $\lambda P2$

• Resultaat: Parametrische quotient-types (waarbij de quotiënt-operatie polymorf is) zijn niet definieerbaar in $\lambda P2$.
• Definitie: Een parametrisch quotient vereist een functie cls die elementen naar hun equivalentieklassen afbeeldt, zodanig dat als $R(x,y)$ geldt, dan cls(x) = cls(y).
• Bewijs: In een model gebaseerd op de WECA van $\lambda$-termen, zou een dergelijke cls-functie constant moeten zijn om aan de eisen te voldoen. Dit leidt echter tot een contradictie (bijvoorbeeld: true zou gelijk moeten zijn aan false als ze in dezelfde klasse zitten).
• Nuance: Triviale quotienten (waarbij de relatie $R$ de identiteit is) bestaan wel, maar er zijn geen parametrische quotienten voor algemene relaties.

C. De Noodzaak van Functionele Extensionaliteit (FunExt)

• Resultaat: Zelfs als $\lambda P2$ wordt uitgebreid met $\Sigma$-types, Identiteits-types en UIP, is het nog steeds niet mogelijk om inductie voor natuurlijke getallen te bewijzen.
• Bewijs: De auteur construeert een model gebaseerd op $\Lambda_{id}$ (uitgebreide $\lambda$-calculus met refl en J). In dit model geldt UIP en zijn $\Sigma$-types en identiteits-types correct geïnterpreteerd. Echter, het type dat inductie voor natuurlijke getallen representeert, is leeg in dit model.
• Conclusie: Functionele Extensionaliteit (FunExt) is een cruciale en noodzakelijke voorwaarde om inductie (en daarmee ook sterke quotienten en co-inductie) bewijsbaar te maken. Zonder FunExt blijven deze principes onbereikbaar, zelfs met de andere uitbreidingen.

4. Significatie en Discussie

• Bevestiging van Grenzen: Het artikel bevestigt dat de impredicatieve codering van data-types in $\lambda P2$ fundamenteel beperkt is. Er is geen "slimme" codering die inductie of co-inductie kan redden zonder de theorie te verrijken.
• Rol van FunExt: Een van de belangrijkste inzichten is dat UIP en $\Sigma$-types onvoldoende zijn. Functionele extensionaliteit is de sleutelcomponent die het verschil maakt tussen een theorie waar inductie bewijsbaar is en een waar het niet is. Dit onderstreept het belang van FunExt in moderne type-theoretische formalisaties (zoals in Homotopy Type Theory en bewijsassistenten).
• Verband met Berardi: De resultaten sluiten naadloos aan bij het eerdere werk van Stefano Berardi over niet-parametrische modellen en de syntactische analyse van type-theorieën. Het toont aan dat de beperkingen van $\lambda P2$ die Berardi al eerder had geïdentificeerd, ook gelden voor complexere constructies zoals quotienten en co-inductie.
• Toekomstig Onderzoek: De auteur suggereert dat het interessant zou zijn om te onderzoeken of er überhaupt enige stream-type bestaat met een co-inductieprincipe in $\lambda P2$, of dat dit onmogelijk is voor elke mogelijke codering. Ook wordt de vraag gesteld of er niet-triviale niet-parametrische quotienten bestaan.

Samenvattend: Herman Geuvers bewijst dat in het pure $\lambda P2$ noch co-inductie voor streams, noch parametrische quotienten, noch inductie voor natuurlijke getallen bewijsbaar zijn. Zelfs met uitbreidingen zoals $\Sigma$-types en UIP blijft inductie onbereikbaar; Functionele Extensionaliteit is de essentiële ontbrekende schakel.