Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Multi-clocked Guarded Recursion Beyond ω

Rasmus Ejlers Møgelberg

TL;DR

The paper addresses the challenge of relating guarded, multi-clocked recursive constructions to conventional set-theoretic semantics. It extends extensional presheaf models to higher ordinals, enabling encodings of coinductive types beyond W-types and allowing existential predicates to be interpreted in Set. It provides semantic and syntactic conditions for when functors (notably those arising from algebraic theories like finite powersets and finite distributions) commute with clock quantification and for when existential quantification can interchange with clock quantification. The results yield conservativity over Set and demonstrate that Clocked Type Theory results can be interpreted semantically in a set-theoretic framework, with implications for formalizing probabilistic and nondeterministic languages in proof assistants beyond cubical type theory.

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.

Multi-clocked Guarded Recursion Beyond ω

TL;DR

The paper addresses the challenge of relating guarded, multi-clocked recursive constructions to conventional set-theoretic semantics. It extends extensional presheaf models to higher ordinals, enabling encodings of coinductive types beyond W-types and allowing existential predicates to be interpreted in Set. It provides semantic and syntactic conditions for when functors (notably those arising from algebraic theories like finite powersets and finite distributions) commute with clock quantification and for when existential quantification can interchange with clock quantification. The results yield conservativity over Set and demonstrate that Clocked Type Theory results can be interpreted semantically in a set-theoretic framework, with implications for formalizing probabilistic and nondeterministic languages in proof assistants beyond cubical type theory.

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.

Paper Structure

This paper contains 18 sections, 7 theorems, 38 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Clocked Type Theory
  3. Axioms
  4. Universes
  5. Encoding Coinductive Types
  6. Applications
  7. Coalgebra
  8. Modelling Programming Languages with Probabilistic Choice
  9. Weak Bisimilarity
  10. Summary Requirements
  11. The Presheaf Model
  12. Universes
  13. Conservativity Over $\mathsf{Set}$
  14. Algebraic data types
  15. A Semantic Condition
  16. ...and 3 more sections

Key Result

Theorem 2

Let $F : (I \to \operatorname{U}_{\Delta}) \to (I \to \operatorname{U}_{\Delta})$ be a functor commuting with universal quantification over clocks. There is a unique object $\mu^\kappa X. F(\triangleright^\kappa X)$ in $(I \to \operatorname{U}_{\Delta, \kappa})$ satisfying $F(\triangleright^\kappa(\

Figures (2)

  • Figure 1: Selected typing rules for Clocked Type Theory bahr2017clocksclottmodel.
  • Figure 2: Selected typing rules for universes.

Theorems & Definitions (16)

  • Definition 1
  • Theorem 2: atkey13icfpMogelberg14
  • Definition 3: GDTTmodel
  • Proposition 4
  • Theorem 5
  • Example 6
  • Example 7
  • Theorem 8
  • Example 9
  • Example 10
  • ...and 6 more