Multi-clocked Guarded Recursion Beyond {\omega}

Resumen Técnico: Recursión Guardada Multireloj más allá de $\omega$

Planteamiento del Problema
Las teorías de tipos con recursión guardada multireloj (como la Teoría de Tipos con Reloj o CloTT) proporcionan un marco flexible para la programación con tipos coinductivos y la construcción de modelos denotacionales de lenguajes de programación que presentan constructos avanzados como la no determinación y la elección probabilística. Si bien estas teorías han sido modeladas con éxito mediante presheaves sobre el topos de árboles (indexados por $\omega$) y, más recientemente, mediante presheaves de conjuntos cúbicos, persiste una brecha al intentar relacionar estos resultados con el "mundo real" de la teoría de conjuntos estándar.

Específicamente, las interpretaciones estándar de la teoría de conjuntos suelen fallar al no preservar la conmutatividad de la cuantificación de relojes con ciertos functores (como el functor de potencias finitas $P_f$ y el functor de distribución finita $D_f$) y la cuantificación existencial. En el topos de árboles, la cuantificación existencial no siempre se externaliza como existencia en conjuntos, y los functores como $P_f$ y $D_f$ no conmutan con la cuantificación de relojes en el modelo estándar. Por consiguiente, los resultados probados en la Teoría de Tipos Cúbica con Reloj (por ejemplo, respecto a las leyes distributivas entre mónadas o la equivalencia contextual en FPC Probabilístico) se interpretan actualmente como enunciados sobre mónadas en hsets dentro del modelo cúbico, dejando su validez en la categoría de conjuntos estándar ($\mathbf{Set}$) sin verificar.

Metodología
El artículo investiga cómo extender el modelo de presheaf extensional de la recursión guardada multireloj a ordinales superiores ($\rho > \omega$) para restaurar las propiedades de conmutatividad necesarias. La metodología consiste en:

1. Extensión del Modelo: Generalizar el modelo de presheaf de CloTT (originalmente definido por Mannaa et al. para $\rho = \omega$) para que esté indexado por un ordinal límite regular arbitrario $\rho$. El modelo se construye en la categoría de presheaves sobre una categoría de objetos de tiempo $T_\rho$, donde los objetos son pares de conjuntos de relojes finitos y mapas hacia $\rho$.
2. Análisis Semántico de la Conmutatividad: El artículo analiza las condiciones bajo las cuales la cuantificación universal sobre relojes ($\forall \kappa$) conmuta con:
   • Functores generados por teorías algebraicas (específicamente mónadas como $P_f$ y $D_f$).
   • Cuantificación existencial ($\exists$).
3. Condiciones Sintácticas y Semánticas:
   • Para Functores: El artículo establece que un functor $F$ conmuta con límites indexados por $\rho^{op}$ (y, por tanto, con la cuantificación de relojes) si $F$ es $\kappa$-accesible, preserva intersecciones $\kappa$-pequeñas y preserva pullbacks de monomorfismos, siempre que $\rho$ contenga un ordinal de cardinalidad $\kappa$.
   • Para Teorías Algebraicas: Se identifica una condición sintáctica: las teorías algebraicas no deben contener "ecuaciones de descarte" (ecuaciones donde el conjunto de variables libres en los dos términos difiere). Esto asegura que la mónada generada satisfaga las condiciones semánticas mencionadas anteriormente.
   • Para la Cuantificación Existencial: El artículo demuestra que $\forall \kappa$ conmuta con $\exists$ sobre un tipo $X$ si las fibras de $X$ tienen una cardinalidad estrictamente menor que el ordinal de indexación $\rho$. También aborda cuantificaciones existenciales "esencialmente únicas", donde el testigo es único hasta un número finito de pasos de retraso.

Contribuciones Clave y Resultados

• Conservatividad sobre Set: El artículo establece y demuestra explícitamente la conservatividad del modelo de la Teoría de Tipos con Reloj sobre el modelo estándar de la teoría de conjuntos. Esto implica que cualquier enunciado expresable en el lenguaje interno de $\mathbf{Set}$ que sea demostrable en CloTT también es verdadero en $\mathbf{Set}$.
• Conmutatividad de las Mónadas: El artículo proporciona condiciones semánticas y un criterio sintáctico (ausencia de ecuaciones de descarte) para que las mónadas generadas por teorías algebraicas conmuten con la cuantificación de relojes. Esto valida el uso de $P_f$ y $D_f$ en el modelo de conjuntos, siempre que el ordinal de indexación $\rho$ sea suficientemente grande (por ejemplo, $\omega_1$ para operaciones contables).
• Conmutatividad de la Cuantificación Existencial: El artículo demuestra que, al elegir un ordinal regular suficientemente grande (por ejemplo, $\omega_1$ o superior), la cuantificación universal sobre relojes conmuta con la cuantificación existencial sobre conjuntos de cardinalidad menor que $\rho$. Esto resuelve el problema de la externalización de las pruebas existenciales desde el topos de árboles hacia $\mathbf{Set}$.
• Interpretación de Trabajos Previos: El artículo muestra que las aplicaciones previamente formalizadas en la Teoría de Tipos Cúbica con Reloj —específicamente:
  • Modelado algebraico de sistemas no deterministas y probabilísticos.
  • Razonamiento sobre bisimilitud débil y leyes distributivas entre mónadas.
  • Pruebas de equivalencia contextual para FPC Probabilístico.
    —pueden interpretarse en el modelo de conjuntos indexado por un ordinal suficientemente grande. Esto prueba la corrección de estos resultados bajo su interpretación estándar de la teoría de conjuntos.

Significado
El artículo sostiene que, al variar el ordinal de indexación del modelo, se puede cerrar la brecha entre la lógica interna de la recursión guardada (que maneja la productividad y la coinducción de manera elegante) y el mundo externo de la teoría de conjuntos estándar.

La significancia principal es que permite que los resultados probados utilizando la maquinaria de la Teoría de Tipos Cúbica con Reloj sean validados en la teoría de conjuntos estándar sin depender de las propiedades específicas de los conjuntos cúbicos. Esto sugiere que la base semántica para formalizar aplicaciones que involucran no determinación, probabilidad y predicados coinductivos puede establecerse en asistentes de pruebas que no dependen de la teoría de tipos cúbicos, siempre que el modelo subyacente utilice un ordinal de indexación suficientemente grande. El artículo señala que, aunque la metateoría utilizada para estas pruebas es la teoría de conjuntos clásica, los resultados proporcionan una justificación teórica de conjuntos rigurosa para la corrección de las codificaciones de tipos coinductivos que involucran tipos inductivos de cociente y cuantificación existencial.