Constructing (Co)inductive Types via Large Sizes

1. Probleemstelling

Bewijsassistenten (bijv. Agda, Lean, Rocq) vertrouwen op afhankelijke typetheorie om consistentie en beslisbaarheid te garanderen. Een kritieke vereiste is dat alle recursieve functies totaal (terminerend) moeten zijn en dat alle corecursieve functies productief moeten zijn.

• Huidige Beperkingen: De meeste systemen handhaven totaliteit via syntactische controles (bijv. structurele recursie of size-change termination). Deze controles zijn vaak restrictief, niet-modulair en gevoelig voor code-refactoring.
• Grootte-gebaseerde Types (Sized Types): Een type-gebaseerd alternatief gebruikt "groottes" (ordinaalgetallen) om types te annoteren, waardoor terminatie kan worden bewezen via goed-geordende induktie op grootte.
• De Agda-inkonsistentie: Agda implementeert grootte-gebaseerde types, maar introduceert een grootste grootte ($\infty$) om het volledige inductieve/co-inductieve type te definiëren als zijn benadering bij $\infty$. Dit leidt tot een logische inkonsistentie: het systeem bewijst $\infty < \infty$, wat de irreflexiviteit van strikt goed-geordende relaties schendt.
• Vorige Theoretische Werk: Vorige pogingen om dit op te lossen met parametrische kwantoren (existential $\exists$ voor inductief, universeel $\forall$ voor co-inductief) waren beperkt. Specifiek konden ze alleen finitely-branching (eindig vertakkende) inductieve types construeren, omdat het grootte-type werd geïnterpreteerd als de verzameling natuurlijke getallen ($\mathbb{N}$), wat limietordinaalgetallen mist die noodzakelijk zijn voor oneindig vertakkende structuren.

Doel: Een consistente typetheorie construeren die alle (co)inductieve types (inclusief oneindig vertakkende) ondersteunt met behulp van grootte-gebaseerde types en parametrische kwantoren, zonder te vertrouwen op een inkonsistente grootste grootte.

2. Methodologie

De auteurs breiden Martin-Löf Type Theory (MLTT) uit met specifieke functies om deze constructie te realiseren en bewijzen de consistentie ervan via een realiseringsmodel.

A. De Uitgebreide Typetheorie

De theorie omvat standaard MLTT-functies (universa, $\Sigma$, $\Pi$, identiteitstypes) plus:

1. Een Type van Groottes (Size):
   • Uitgerust met een nul ($0$) en opvolger ($\uparrow i$).
   • Geordend door een preorde ($\leq$) gecodeerd als een puur proposition.
   • Cruciaal: Size is een groot type (niet in het universum $U$), maar kwantisatie erover kan kleine types opleveren.
2. Parametrische Kwantoren:
   • $\exists i. A(i)$ (Existentieel): Vertegenwoordigt de vereniging van benaderingen. Termen zijn paren $\langle s, a \rangle$, maar de grootte $s$ is geabstraheerd (kan niet worden gepatroneerd). Eliminatie is beperkt tot kleine types.
   • $\forall i. A(i)$ (Universeel): Vertegenwoordigt de doorsnede van benaderingen. Functies werken uniform op elke grootte.
   • Parametriciteitsaxioma's: De theorie bevat axioma's die stellen dat deze kwantoren commuteren met typeconstructoren (bijv. $\Pi x:A. \exists i. B(x,i) \simeq \exists i. \Pi x:A. \exists j < i. B(x,j)$). Dit internaliseert het idee dat groottes uniform worden behandeld.
3. Goed-geordende Induktie (fix):
   • Een fixpuntoperator die definitie door induktie op groottes toestaat: $fix\ f : \forall i. A(i)$ gegeven $f : \forall i. ((\forall j < i. A(j)) \to A(i))$.
   • De $\beta$-regel is propositioneel (niet definitorisch) om de beslisbaarheid van typecontrole te behouden.

B. Constructie van (Co)inductieve Types

De auteurs coderen (co)inductieve types als initiële algebra's en finale coalgebra's voor polynomiale endofunctoren ($F$).

1. Ordinaalgetal-Benaderingen: Zij definiëren grootte-geïndexeerde functoren $F[\exists -]$ en $F[\forall -]$. Met behulp van de fix-operator construeren zij initiële algebra's ($\mu_3 F$) en finale coalgebra's ($\nu_2 F$) voor deze grootte-geïndexeerde functoren. Deze vertegenwoordigen het type getrimd op een specifieke grootte.
2. Volledige Types via Kwantorisatie:
   • Inductieve Types: Gedefinieerd als $\mu F := \exists i. (\mu_3 F) i$. De existentiële kwantor verzamelt alle termen die begrensd zijn door een bepaalde grootte.
   • Co-inductieve Types: Gedefinieerd als $\nu F := \forall i. (\nu_2 F) i$. De universele kwantor zorgt ervoor dat termen op elke diepte waarneembaar zijn.
3. Omgaan met Oneindig Vertakkende Types: De kerninnovatie is het aantonen dat polynomiale functoren zwak commuteren met de existentiële kwantor. Dit vereist het bestaan van limietordinaalgetallen (suprema van reeksen groottes), wat onmogelijk is als groottes slechts $\mathbb{N}$ zijn.

C. Consistentiebewijs: Realiseringsmodel

Om te bewijzen dat de theorie consistent is, construeren de auteurs een realiseringsmodel gebaseerd op Hyland's Effective Topos.

• Interpretatie van Types:
  • Kleine Types: Geïnterpreteerd als Partiële Equivalentierelaties (PERs) op natuurlijke getallen (berekenbare data).
  • Grote Types: Geïnterpreteerd als Assemblies (verzamelingen met berekenbaarheidsrelaties).
• Interpretatie van Size:
  • Het type Size wordt geïnterpreteerd als $\nabla \omega_1$, waarbij $\omega_1$ het eerste overaftelbare ordinaalgetal is (de verzameling van alle aftelbare ordinaalgetallen).
  • Het krijgt de "volledige" realiseringsrelatie, wat betekent dat morfismen alle groottes uniform moeten behandelen (parametriciteit).
• Validatie:
  • Omdat $\omega_1$ limietordinaalgetallen bevat, valideert het model de parametriciteitsaxioma's die vereist zijn voor oneindig vertakkende inductieve types.
  • Het model valideert Impredicativiteit (kwantisatie over grote types levert kleine types op) en Uniciteit van Identiteitsbewijzen (UIP), zelfs al neemt de syntaxis deze niet aan. Dit toont aan dat de syntaxis compatibel is met sterkere theorieën (zoals Homotopy Type Theory) zonder hierdoor beperkt te worden.

3. Belangrijkste Bijdragen

1. Algemene Constructie van (Co)inductieve Types: In tegenstelling tot eerdere parametrische benaderingen die beperkt waren tot finitely-branching types, construeert dit werk alle (co)inductieve types, inclusief oneindig vertakkende (bijv. Brouwer-ordinaalgetallen, modellen van constructieve verzamelingstheorie).
2. Oplossing voor Agda's Inkonsistentie: Door de inkonsistente "grootste grootte" ($\infty$) te vervangen door parametrische kwantoren over een groot type van groottes, bieden de auteurs een consistente alternatief voor Agda's huidige implementatie.
3. Parametrische Kwantoren als Mechanisme: Zij tonen aan dat het internaliseren van parametriciteit via $\exists$ en $\forall$ over groottes effectief de noodzakelijke abstractie afdwingt om niet-terminerend gedrag en logische inkonsistenties te voorkomen.
4. Robuust Realiseringsmodel: De constructie van een model waarin Size wordt geïnterpreteerd als $\omega_1$ biedt een rigoureuze semantische rechtvaardiging voor de theorie en bewijst dat de parametriciteitsaxioma's consistent zijn.

4. Resultaten

• Theoretische Soundness: Het artikel bewijst dat de initiële algebra en finale coalgraaf voor elke polynomiale endofunctie bestaan binnen de uitgebreide theorie.
• Consistentie: Het realiseringsmodel bevestigt dat de theorie consistent is. Het toont aan dat de axioma's voor parametrische kwantoren gelden wanneer groottes worden geïnterpreteerd als een overaftelbaar ordinaalgetal.
• Compatibiliteit: De constructies vertrouwen niet op UIP of impredicativiteit in de syntaxis, waardoor de resultaten compatibel zijn met Homotopy Type Theory (HoTT), ondanks dat het model aan deze eigenschappen voldoet.

5. Betekenis en Toekomstig Werk

• Impact op Bewijsassistenten: Dit werk biedt een weg om grootte-gebaseerde types te implementeren in bewijsassistenten (zoals Agda) zonder de huidige inkonsistentie veroorzaakt door de $\infty$-grootte. Het staat modulair en compositieel terminatiecontrole toe.
• Computatiegedrag: De auteurs erkennen dat hoewel de theorie consistent is, de huidige syntaxis geen computationeel gedrag heeft voor de parametriciteitsaxioma's (het zijn axioma's, geen reductieregels). Toekomstig werk moet dit verbinden met interne parametriciteit (bijv. via bridgetypes of cubical type theory) om beslisbaarheid en canoniciteit in de praktijk te waarborgen.
• Beslisbaarheid van Ongelijkheid: Het model impliceert dat ongelijkheid op groottes niet algemeen beslisbaar is (vanwege suprema). De auteurs suggereren een hybride aanpak (definitorische versus propositionele ongelijkheid) voor praktische implementatie.
• Generalisatie: Het model zou potentieel kunnen worden gegeneraliseerd naar andere partiële combinatoire algebra's of geïntegreerd met effecten en univocaliteit.

Kortom, het artikel slaagt erin de kloof te overbruggen tussen de theoretische behoefte aan parametrische grootte-gebaseerde types en de praktische vereiste van consistentie, waardoor de constructie van complexe (co)inductieve types mogelijk wordt binnen een sound type-theoretisch raamwerk.