Multi-clocked Guarded Recursion Beyond {\omega}

Sintesi Tecnica: Ricorsione Guardata Multi-clock oltre $\omega$

Enunciato del Probleo
Le teorie dei tipi con ricorsione guardata multi-clock (come la Clocked Type Theory, CloTT) forniscono un framework flessibile per la programmazione con tipi coinduttivi e la costruzione di modelli denotazionali di linguaggi di programmazione caratterizzati da costrutti avanzati come il non-determinismo e la scelta probabilistica. Sebbene queste teorie siano state modellate con successo utilizzando presheaves sulla topos di alberi (indicizzati da $\omega$) e, più recentemente, presheaves di cubical sets, rimane un divario nel relazionare questi risultati con il "mondo reale" della teoria degli insiemi standard.

Nello specifico, le interpretazioni basate sulla teoria degli insiemi standard spesso falliscono nel preservare la commutatività della quantificazione di clock con certi funtori (come il funtore del powerset finito $P_f$ e il funtore della distribuzione finita $D_f$) e la quantificazione esistenziale. Nella topos di alberi, la quantificazione esistenziale non sempre si estenalizza in esistenza negli insiemi, e i funtori come $P_f$ e $D_f$ non commutano con la quantificazione di clock nel modello standard. Di conseguenza, i risultati provati nella Clocked Cubical Type Theory (ad esempio, riguardanti le leggi distributive tra monadi o l'equivalenza contestuale in Probabilistic FPC) sono attualmente interpretati come affermazzioni su monadi su hsets all'interno del modello cubico, lasciando la loro validità nel modello standard della categoria degli insiemi ($\mathbf{Set}$) non verificata.

Metodologia
Il documento investiga come estendere il modello di presheaf estensionale della ricorsione guardata multi-clock a ordinali superiori ($\rho > \omega$) per ripristinare le necessarie proprietà di commutatività. La metodologia prevede:

1. Estensione del Modello: Generalizzare il modello di presheaf di CloTT (originariamente definito da Mannaa et al. per $\rho = \omega$) affinché sia indicizzato da un arbitrario ordinale limite regolare $\rho$. Il modello è costruito nella categoria di presheaves su una categoria di oggetti temporali $T_\rho$, dove gli oggetti sono coppie di insiemi di clock finiti e mappe verso $\rho$.
2. Analisi Semantica della Commutatività: Il documento analizza le condizioni sotto le quali la quantificazione universale su clock ($\forall \kappa$) commuta con:
   • Funtori generati da teorie algebriche (specificamente monadi come $P_f$ e $D_f$).
   • Quantificazione esistenziale ($\exists$).
3. Condizioni Sintattiche e Semantiche:
   • Per i Funtori: Il documento stabilisce che un funtore $F$ commuta con i limiti indicizzati da $\rho^{op}$ (e quindi con la quantificazione di clock) se $F$ è $\kappa$-accessibile, preserva le intersezioni $\kappa$-piccole e preserva i pullback di monomorfismi, a condizione che $\rho$ contenga un ordinale di cardinalità $\kappa$.
   • Per le Teorie Algebriche: Viene identificata una condizione sintattica: le teorie algebriche non devono contenere "drop equations" (equazioni in cui l'insieme delle variabili libere nei due termini differisce). Ciò assicura che la monade generata soddisfi le condizioni semantiche sopra descritte.
   • Per la Quantificazione Esistenziale: Il documento prova che $\forall \kappa$ commuta con $\exists$ su un tipo $X$ se le fibre di $X$ hanno cardinalità strettamente minore dell'ordinale di indicizzazione $\rho$. Affronta inoltre le quantificazioni esistenziali "essenzialmente uniche", dove il testimone è unico fino a un numero finito di passi di ritardo.

Contributi Chiave e Risultati

• Conservatività su Set: Il documento dichiara e prova esplicitamente la conservatività del modello di Clocked Type Theory rispetto al modello standard della teoria degli insiemi. Ciò implica che qualsiasi affermazione esprimibile nel linguaggio interno di $\mathbf{Set}$ che sia dimostrabile in CloTT è anche vera in $\mathbf{Set}$.
• Commutatività delle Monadi: Il documento fornisce condizioni semantiche e un criterio sintetico (assenza di drop equations) affinché le monadi generate da teorie algebriche commutino con la quantificazione di clock. Questo valida l'uso di $P_f$ e $D_f$ nel modello della teoria degli insiemi, a condizione che l'ordinale di indicizzazione $\rho$ sia sufficientemente grande (ad esempio, $\omega_1$ per operazioni countable).
• Commutatività della Quantificazione Esistenziale: Il documento dimostra che, scegliendo un ordinale regolare $\rho$ sufficientemente grande (ad esempio, $\omega_1$ o superiore), la quantificazione universale su clock commuta con la quantificazione esistenziale su insiemi di cardinalità minore di $\rho$. Ciò risolve il problema di l'esternalizzazione delle prove esistenziali dalla topos di alberi a $\mathbf{Set}$.
• Interpretazione del Lavoro Precedente: Il documento mostra che le applicazioni precedentemente formalizzate nella Clocked Cubical Type Theory — specificamente:
  • Modellazione coalgraica di sistemi non deterministici e probabilistici.
  • Ragionamento sulla bisimilarità debole e leggi distributive tra monadi.
  • Prove di equivalenza contestuale per Probabilistic FPC.
    — possono essere interpretate nel modello della teoria degli inseri indicizzato da un ordinale sufficientemente grande. Ciò prova la correttezza di questi risultati sotto la loro standard interpretazione nella teoria degli insiemi.

Significatività
Il documento sostiene che variando l'ordinale di indicizzazione del modello, è possibile colmare il divario tra la logica interna della ricorsione guardata (che gestisce elegantemente produttività e coinduzione) e il mondo esterno della teoria degli insiemi standard.

La significatività primaria è che permette di validare i risultati provati utilizzando il machinery della Clocked Cubical Type Theory nella teoria degli insiemi standard senza dipendere dalle proprietà specifiche dei cubical sets. Ciò suggerisce che la base semantica per formalizzare applicazioni che coinvolgono il non-determinismo, la probabilità e i predicati coinduttivi può essere stabilita in assistenti di prove che non dipendono dalla cubical type theory, a condizione che il modello sottostante utilizzi un ordinale di indicizzazione sufficientemente grande. Il documento nota che, sebbene la metateoria utilizzata per queste prove sia la teoria classica degli insiemi, i risultati forniscono una rigorosa giustificazione set-teoretica della correttezza delle codifiche di tipi coinduttivi che coinvolgono tipi induttivi quotient e quantificazione esistenziale.