Directed proof-relevant logical relations in simplicial HoTT

Technische Samenvatting: Gericht Bewijs-Relevantie Logische Relaties in Simpliciale HoTT

Probleemstelling
Traditionele bewijs-relevante logische relaties (vaak geformuleerd via categorische gluing) interpreteren typen als families van berekenbare termen, waarbij berekenbaarheidspredicaten families van typen zijn in plaats van louter proposities. In ekwationele presentaties van typentheorie wordt oordeelskundige gelijkheid gerepresenteerd door meta-niveau gelijkheid, en rusten logische relaties op een "sluiting onder expansie" lemma: als een term $M$ reduceert naar $M'$, en $M'$ is berekenbaar, dan is $M$ berekenbaar. Deze benadering behandelt computation echter als een symmetrische relatie (via gelijkheid) of vertrouwt op handmatige bewijzen van achterwaartse sluiting. Het internaliseert niet inherent de gerichte aard van reductie, waarbij termen naar andere termen stappen ($M \to M'$) maar niet noodzakelijkerwijs andersom. Dit artikel adresseert de uitdaging om een bewijs-relevante logische relatie te construeren die gerichte reducties intern accountt, zonder te vertrouwen op externe reductierelaties of bewijs-irrelevante expansie-lemma's.

Methodologie
De auteurs ontwikkelen hun raamwerk binnen de simpliciale homotopie-type Theorie (HoTT), een gerichte uitbreiding van HoTT die een gerichte interval en ongelijkheidstypen ($x \leq_A y$) bevat.

1. Gerichte Syntaxis via Gerichte QIIT's:
   De object-taal syntaxis wordt gepresenteerd als een gerichte quotient inductief-inductieve type (gerichte QIIT). In tegenstelling tot standaard QIIT's, die quotienten door oordeelskundige gelijkheden (pad-constructoren), bevat deze syntaxis gerichte constructoren die ongelijkheidstypen genereren. Bijvoorbeeld, de $\beta$-reductie voor producten wordt geïnternaliseerd als een ongelijkheid:
   $$\times\beta_1 : \text{fst}(\text{pair } a \, b) \leq a$$
   De syntaxis is geconstrueerd als een "dunne Segal-type", wat garandeert dat reducties componeren en dat ongelijkheden tussen dezelfde eindpunten uniek zijn (bewijs-irrelevant), wat een pre-orde modelleert in plaats van een algemene categorie.

2. Contravariantie als Bewijs-Relevante Expansie:
   Het kerninzicht van de theoretische basis is dat contravariante families in de simpliciale typentheorie exact de structuur bieden die nodig is voor bewijs-relevante sluiting onder expansie. In deze setting is een berekenbaarheidspredicaat $A^\bullet$ voor een type $A$ niet alleen een familie van typen; het moet een contravariante familie zijn.

   • Definitie: Een familie $C: X \to \mathcal{U}$ is contravariant als voor elke ongelijkheid $f: x \leq_X y$ en getuige $v: C(y)$, het type van lifts $\sum_{u:C(x)} u \leq_{C(f)} v$ contractibel is.
   • Implicatie: Deze contractibiliteit garandeert een unieke, functoriele "achterwaartse transport"-operatie $f^*: C(y) \to C(x)$. Deze operatie internaliseert het expansie-lemma: bewijs van berekenbaarheid kan achterwaarts langs reducties worden getransporteerd op een manier die identiteiten en compositie automatisch respecteert.

3. Afhandeling van Afhankelijke Typen en Universa:
   Het uitbreiden hiervan naar afhankelijke typen introduceert een conflict: type-conversie vereist symmetrische gelijkheid, maar de syntaxis biedt enkel gerichte ongelijkheden.

   • Discretisering: De auteurs discretiseren de type-universum ($Ty$) door een constructor toe te voegen die type-ongelijkheden in gelijkheden verandert ($A \leq Ty B \implies A = Ty B$). Dit maakt standaard type-conversie mogelijk terwijl gerichte reducties voor termen behouden blijven.
   • Vlakke Modaliteit: Om bewijs-relevantie voor universum-predicaten te behouden zonder de discretie te verliezen, gebruiken de auteurs de vlakke modaliteit ($\flat$) uit de crisp type theory. Berekenbaarheidspredicaten voor universa worden opgeslagen als vlakke codes. Omdat $\flat X$ discreet is, klappen ongelijkheden tussen predicaten in tot gelijkheden, wat de uniciteit vereist voor de universum-berekenbaarheidsgetuige waarborgt.

Belangrijkste Bijdragen

1. Gerichte Quotient Syntaxis: Een formalisering van typentheorie-syntaxis waarbij oordeelskundige reducties worden geïnternaliseerd als gerichte ongelijkheden via gerichte QIIT's.
2. Contravariantie als Expansie: De identificatie van contravariante families in de simpliciale typentheorie als de bewijs-relevante generalisatie van het expansie-lemma, wat ingebouwde functorialiteit en universele eigenschappen biedt voor achterwaarts transport.
3. Unaire Logische Relatie Model: Een constructie van een unaire logische relatie model dat gerichte Boolean canoniciteit bewijst: elke gesloten Boolean term $M$ voldoet aan $M \leq \text{true}$ of $M \leq \text{false}$.
4. Mechanisatie: Een proof-of-concept mechanisatie in Cubical Agda voor het simpel-getypeerde fragment (producten, functies, Booleans), die de haalbaarheid van de gerichte benadering demonstreert.
5. Uitbreiding naar Afhankelijke Typen en Universa: Een oplossing voor afhankelijke typen met discretisering van typen en de vlakke modaliteit om universum-predicaten te hanteren.
6. Binaire Parametriciteit: Een adaptatie van de methode naar binaire logische relaties, waarbij verticale reducties (contravariantie) worden gescheiden van horizontale parametriciteit, geïllustreerd door een argument voor representatie-onafhankelijkheid van queues.

Resultaten

• Gerichte Canoniciteit: Het fundamentele theorem van logische relaties wordt vastgesteld voor de gerichte setting. Voor elke gesloten Boolean term $M$ levert het model een getuige dat $M$ reduceert naar een canonieke boolean.
• Representatie-onafhankelijkheid: De binaire logische relatie scheidt de verticale dimensie (reductie/contravariantie) succesvol van de horizontale dimensie (parametriciteit), waardoor een bewijs-relevante account van representatie-onafhankelijkheid mogelijk is waarbij de relatie een span is in plaats van een zig-zag.
• Mechanisatie: Het simpel-getypeerde fragment, inclusief de constructie van de gerichte syntaxis en het logische relatie model, is geformaliseerd in Cubical Agda.

Betekenis en Claims
Het artikel claimt een type-theoretische internalisering te bieden van het idee dat logische relaties zowel canoniciteit als parametriciteit moeten valideren, zelfs wanneer syntaxis wordt gepresenteerd door reducties in plaats van gelijkheden.

• Theoretische Unificatie: Het verenigt het operationele beeld van computation (gerichte reductie) met het semantische beeld van logische relaties (bewijs-relevante gluing) door gebruik te maken van de native gerichte structuur van de simpliciale typentheorie.
• Nieuwe Rol voor Contravariantie: Het verheft contravariante families van een instrument voor synthetische categorietheorie naar een fundamenteel mechanisme voor logische relaties, waarbij ad-hoc expansie-lemma's worden vervangen door een universele eigenschap.
• Bescheidenheid: De auteurs merken op dat het resultaat in zijn conclusie "niet verrassend" is (logische relaties zouden moeten werken voor reducties), maar significant in zijn internalisering. Ze erkennen dat de afhankelijke uitbreiding aanzienlijke transport-uitdagingen met zich meebrengt en dat de huidige mechanisatie beperkt is tot het simpel-getypeerde geval. Ze beweren niet alle problemen met betrekking tot identiteitstypen in gerichte settings te hebben opgelost, wat wijst op toekomstig werk met betrekking tot fase-onderscheidingen of monadische modaliteiten.

Het werk demonstreert dat de simpliciale typentheorie niet alleen een instrument is voor synthetische $\infty$-categorietheorie, maar ook een levensvatbare metatheorie voor het redeneren over de reductie-semantiek van programmeertalen en typentheorieën.