Multi-clocked Guarded Recursion Beyond {\omega}

TL;DR

This paper extends the presheaf model of multi-clocked guarded recursion to higher ordinals, enabling the correctness of encodings of complex coinductive types and predicates to be verified in set-theoretic models.

Contribution

It generalizes the extensional presheaf model of multi-clocked guarded recursion to higher ordinals, supporting more complex coinductive types and predicates.

Findings

Extended model verifies correctness of encodings involving finite powersets and distributions.

Supports coinductive predicates with existential quantification.

Bridges results from Clocked Cubical Type Theory to set-theoretic interpretations.

Abstract

Type theories with multi-clocked guarded recursion provide a flexible framework for programming with coinductive types encoding productivity in types. Combining this with solutions to general guarded domain equations one can also construct relatively simple denotational models of programming languages with advanced features. These constructions have previously been explored in the setting of extensional type theory through a presheaf model, which proves correctness of encodings of W-types. That model has been adapted to presheaves of cubical sets (functors into the category of cubical sets), where the model verifies correctness of encodings also of coinductive types whose definitions involve quotient inductive types such as finite powersets or finite distributions. Likewise the cubical model also verifies correctness of coinductive predicates defined using existential quantification and allows the results to be related to the global world of cubical sets. This paper looks at how to extend the extensional presheaf model of multi-clocked guarded recursion to higher ordinals, so that correctness of encodings of coinductive types can be extended from W-types to those involving finite powersets and finite distributions, as well as coinductive predicates involving existential quantification. This extension will allow results previously proved in Clocked Cubical Type Theory to be interpreted in a model based on set-theory, proving the correctness of these results as understood in their usual set theoretic interpretation.