Multi-clocked Guarded Recursion Beyond {\omega}

Resumo Técnico: Recursão Guardada com Múltiplos Relógios Além de $\omega$

Enunciado do Problema
Teorias de tipos com recursão guardada de múltiplos relógios (como a Clocked Type Theory, CloTT) fornecem um arcabouço flexível para a programação com tipos coindutivos e para a construção de modelos denotacionais de linguagens de programação que apresentam construtos avançados, como não-determinismo e escolha probabilística. Embora estas teorias tenham sido modeladas com sucesso usando presheaves sobre o topos de árvores (indexados por $\omega$) e, mais recentemente, presheaves de conjuntos cúbicos (cubical sets), permanece uma lacuna ao relacionar estes resultados com o "mundo real" da teoria dos conjuntos padrão.

Especificamente, as interpretações de teoria dos conjuntos padrão frequentemente falham em preservar a comutatividade da quantificação de relógio com certos funtores (como o funtor de potência finita $P_f$ e o funtor de distribuição finita $D_f$) e com a quantificação existencial. No topos de árvores, a quantificação existencial nem sempre se externaliza para a existência em conjuntos, e funtores como $P_f$ e $D_f$ não comutam com a quantificação de relógio no modelo padrão. Consequentemente, resultados provados na Clocked Cubical Type Theory (por exemplo, sobre leis distributivas entre monads ou equivalência contextual em Probabilistic FPC) são atualmente interpretados como afirmações sobre monads em hsets dentro do modelo cúbico, deixando sua validade no modelo padrão da categoria de conjuntos ($\mathbf{Set}$) não verificada.

Metodologia
O artigo investiga como estender o modelo de presheaf extensivo de recursão guardada de múltiplos relógios para ordinais superiores ($\rho > \omega$) para restaurar as necessárias propriedades de comutatividade. A metodologia envolve:

1. Extensão do Modelo: Generalizar o modelo de presheaf da CloTT (originalmente definido por Mannaa et al. para $\rho = \omega$) para ser indexado por um ordinal limite regular arbitrário $\rho$. O modelo é construído na categoria de presheaves sobre uma categoria de objetos de tempo $T_\rho$, onde os objetos são pares de conjuntos de relógios finitos e mapas para $\rho$.
2. Análise Semântica de Comutatividade: O artigo analisa as condições sob as quais a quantificação universal sobre relógios ($\forall \kappa$) comuta com:
   • Funtores gerados por teorias algébricas (especificamente monads como $P_f$ e $D_f$).
   • Quantificação existencial ($\exists$).
3. Condições Sintáticas e Semânticas:
   • Para Funtores: O artigo estabelece que um funtor $F$ comuta com limites indexados por $\rho^{op}$ (e, portanto, com a quantificação de relógio) se $F$ for $\kappa$-acessível, preservar interseções $\kappa$-pequenas e preservar pullbacks de monomorfismos, desde que $\rho$ contenha um ordinal de cardinalidade $\kappa$.
   • Para Teorias Algébricas: Uma condição sintática é identificada: as teorias algébricas não devem conter "equações de descarte" (drop equations) (equações onde o conjunto de variáveis livres nos dois termos difere). Isso garante que a monad gerada satisfaça as condições semânticas acima.
   • Para Quantificação Existencial: O artigo prova que $\forall \kappa$ comuta com $\exists$ sobre um tipo $X$ se as fibras de $X$ tiverem cardinalidade estritamente menor que o ordinal de indexação $\rho$. O artigo também aborda quantificações existenciais "essencialmente únicas", onde o testemunho é único até um número finito de passos de atraso (delay steps).

Contribuições Principais e Resultados

• Conservatividade sobre Set: O artigo declara e prova explicitamente a conservatividade do modelo de Clocked Type Theory sobre o modelo de teoria de tipos padrão de conjuntos. Isso implica que qualquer afirmação expressável na linguagem interna de $\mathbf{Set}$ que seja provável em CloTT também é verdadeira em $\mathbf{Set}$.
• Comutatividade de Monads: O artigo fornece condições semânticas e um critério sintático (ausência de equações de descarte) para que monads geradas por teorias algébricas comutem com a quantificação de relógio. Isso valida o uso de $P_f$ e $D_f$ no modelo de teoria dos conjuntos, desde que o ordinal de indexação $\rho$ seja suficientemente grande (por exemplo, $\omega_1$ para operações contáveis).
• Comutatividade da Quantificação Existencial: O artigo demonstra que, ao escolher um ordinal regular suficientemente grande (por exemplo, $\omega_1$ ou superior), a quantificação universal sobre relógios comuta com a quantificação existencial sobre conjuntos de cardinalidade menor que $\rho$. Isso resolve o problema de externalizar provas existenciais do topos de árvores para $\mathbf{Set}$.
• Interpretação de Trabalhos Anteriores: O artigo mostra que aplicações anteriormente formalizadas em Clocked Cubical Type Theory — especificamente:
  • Modelagem coalgebrica de sistemas não-determinísticos e probabilísticos.
  • Raciocínio sobre bisimilaridade fraca e leis distributivas entre monads.
  • Provas de equivalência contextual para Probabilistic FPC.
    — podem ser interpretadas no modelo de teoria dos conjuntos indexado por um ordinal suficientemente grande. Isso prova a correção destes resultados sob sua interpretação padrão de teoria dos conjuntos.

Significância
O artigo afirma que, ao variar o ordinal de indexação do modelo, é possível preencher a lacuna entre a lógica interna da recursão guardada (que lida com produtividade e coindução elegantemente) e o mundo externo da teoria dos conjuntos padrão.

A principal significância é que isso permite que resultados provados usando o aparato da Clocked Cubical Type Theory sejam validados na teoria dos conjuntos padrão sem depender das propriedades específicas de conjuntos cúbicos. Isso sugere que a base semântica para formalizar aplicações envolvendo não-determinismo, probabilidade e predicados coindutivos pode ser estabelecida em assistentes de prova que não dependem de teoria de tipos cúbicos, desde que o modelo subjacente utilize um ordinal de indexação suficientemente grande. O artigo observa que, embora a metateoria usada para estas provas seja a teoria dos conjuntos clássica, os resultados fornecem uma justificativa rigorosa em teoria dos conjuntos para a correção de codificações de tipos coindutivos envolvendo tipos indutivos de quociente e quantificação existencial.