Multi-clocked Guarded Recursion Beyond {\omega}

Technische Samenvatting: Multi-clocked Guarded Recursion voorbij $\omega$

Probleemstelling
Typetheorieën met multi-clocked guarded recursion (zoals Clocked Type Theory, CloTT) bieden een flexibel kader voor het programmeren met coinductieve typen en het construeren van denotationele modellen van programmeertalen die geavanceerde constructen bevatten zoals non-determinisme en probabilistische keuze. Hoewel deze theorieën succesvol gemodelleerd zijn met presheaves over de topos van bomen (geïndexeerd door $\omega$) en, recenter, presheaves van cubical sets, blijft er een kloof bestaan in het relateren van deze resultaten aan de "echte wereld" van de standaard verzamelingenleer.

Specifiek falen standaard verzamelingenleerlijke interpretaties vaak in het behouden van de commutativiteit van klok-kwantificatie met bepaalde functoren (zoals de eindige machtsverzamelfunctie $P_f$ en de eindige distributiefunctie $D_f$) en existentiële kwantificatie. In de topos van bomen kwantificeert existentiële kwantificatie niet altijd naar existentie in verzamelingen, en functoren zoals $P_f$ en $D_f$ communiceren niet met klok-kwantificatie in het standaardmodel. Bijgevolg worden resultaten bewezen in Clocked Cubical Type Theory (bijv. betreffende distributieve wetten tussen monaden of contextuele equivalentie in Probabilistic FPC) momenteel geïnterpreteerd als uitspraken over monaden op hsets binnen het cubical model, terwijl hun geldigheid in de standaard categorie van verzamelingen ($\mathbf{Set}$) ongeverifieerd blijft.

Methodologie
Dit artikel onderzoekt hoe de extensieve presheaf-model van multi-clocked guarded recursion kan worden uitgebreid naar hogere ordinaalgetallen ($\rho > \omega$) om de noodzakelijke commutativiteitseigenschappen te herstellen. De methodologie omvat:

1. Modelextensie: Het generaliseren van het presheaf-model van CloTT (oorspronkelijk gedefinieerd door Mannaa et al. voor $\rho = \omega$) om te worden geïndexeerd door een willekeurige reguliere limietordinaal $\rho$. Het model wordt geconstrueerd in de categorie van presheaves over een categorie van tijdsobjecten $T_\rho$, waarbij objecten paren zijn van eindige kloksets en afbeeldingen naar $\rho$.
2. Semantische Analyse van Commutativiteit: Het artikel analyseert de voorwaarden waaronder universele kwantificatie over klokken ($\forall \kappa$) commuteert met:
   • Functoren gegenereerd door algebraïsche theorieën (specifiek monaden zoals $P_f$ en $D_f$).
   • Existentiële kwantificatie ($\exists$).
3. Syntactische en Semantische Voorwaarden:
   • Voor Functoren: Het artikel stelt vast dat een functor $F$ commuteert met $\rho^{op}$-geïndexeerde limieten (en dus klok-kwantificatie) indien $F$ $\kappa$-toegankelijk is, $\kappa$-kleine intersecties behoudt en pullbacks van monomorfismen behoudt, mits $\rho$ een ordinaal bevat met cardinaliteit $\kappa$.
   • Voor Algebraïsche Theorieën: Een syntactische voorwaarde wordt geïdentificeerd: algebraïsche theorieën mogen geen "drop equations" bevatten (vergelijkingen waarbij de verzameling vrije variabelen in de twee termen verschilt). Dit zorgt ervoor dat de gegenereerde monade de semantische voorwaarden hierboven voldoet.
   • Voor Existentiële Kwantificatie: Het artikel bewijst dat $\forall \kappa$ commuteert met $\exists$ over een type $X$ indien de vezels van $X$ een cardinaliteit hebben die strikt kleiner is dan de indexerende ordinaal $\rho$. Het behandelt ook "essentieel unieke" existentiële kwantificaties, waarbij de getuige uniek is tot een eindig aantal vertragingsstappen.

Belangrijkste Bijdragen en Resultaten

• Conservativiteit over Set: Het artikel stelt expliciet de conservativiteit van het Clocked Type Theory-model over het standaard verzamelingenleerlijke model van typetheorie vast en bewijst dit. Dit impliceert dat elke uitspraak die expressief is in de interne taal van $\mathbf{Set}$ en bewezen is in CloTT, ook waar is in $\mathbf{Set}$.
• Commutativiteit van Monaden: Het artikel biedt semantische voorwaarden en een syntactisch criterium (afwezigheid van drop equations) voor monaden gegenereerd door algebraïsche theorieën om te communiceren met klok-kwantificatie. Dit valideert het gebruik van $P_f$ en $D_f$ in het verzamelingenleerlijke model, mits de indexerende ordinaal $\rho$ voldoende groot is (bijv. $\omega_1$ voor tellbare operaties).
• Commutativiteit van Existentiële Kwantificatie: Het artikel demonstreert dat door een voldoende grote reguliere ordinaal $\rho$ te kiezen (bijv. $\omega_1$ of hoger), universele kwantificatie over klokken commuteert met existentiële kwantificatie over verzamelingen met een cardinaliteit kleiner dan $\rho$. Dit lost het probleem op van het externaliseren van existentiële bewijzen van de topos van bomen naar $\mathbf{Set}$.
• Interpretatie van Voorgaand Werk: Het artikel toont aan dat toepassingen die eerder zijn geformaliseerd in Clocked Cubical Type Theory — specifiek:
  • Coalgebraische modellering van non-deterministische en probabilistische systemen.
  • Redeneren over zwakke bisimilariteit en distributieve wetten tussen monaden.
  • Contextuele equivalentiebewijzen voor Probabilistic FPC.
    — kunnen worden geïnterpreteerd in het verzamelingenleerlijke model geïndexeerd door een voldoende grote ordinaal. Dit bewijst de correctheid van deze resultaten onder hun standaard verzamelingenleerlijke interpretatie.

Significantie
Het artikel claimt dat door de indexerende ordinaal van het model te variëren, men de kloof kan overbruggen tussen de interne logica van guarded recursion (die productiviteit en coinductie elegant afhandelt) en de externe wereld van de standaard verzamelingenleer.

De primaire significantie is dat dit het mogelijk maakt om resultaten die bewezen zijn met de machinerie van Clocked Cubical Type Theory te valideren in de standaard verzamelingenleer zonder te vertrouwen op de specifieke eigenschappen van cubical sets. Dit suggereert dat de semantische basis voor het formaliseren van toepassingen betrokken bij non-determinisme, probabiliteit en coinductieve predicaten kan worden gevestigd in bewijsassistenten die niet afhankelijk zijn van cubical type theory, mits het onderliggende model een voldoende grote indexerende ordinaal gebruikt. Het artikel merkt op dat hoewel de metatheorie gebruikt voor deze bewijzen klassieke verzamelingenleer is, de resultaten een rigoureuze verzamelingenleerlijke rechtvaardiging bieden voor de correctheid van coderingen van coinductieve typen die betrokken zijn bij quotient inductive types en existentiële kwantificatie.