nLab synthetic guarded domain theory

Contents

Contents

Idea

Synthetic guarded domain theory, is a field of synthetic mathematics that provides an alternative to synthetic domain theory, where all guarded recursive definitions have fixed points. It provides a simple setting in which to carry out constructions using the technique of step-indexing in programming language semantics. In the same way that synthetic domain theory is inspired by classical domain theory based on cpos and continuous maps, synthetic guarded domain theory is inspired by metric (or guarded) domain theory based on various kinds of metric space and nonexpansive maps.

Axiomatics

Palombi and Sterling provide the following simple axiomatization of a model of (single-clock) synthetic guarded domain theory:

  1. An elementary topos EE with natural numbers object.

  2. with a left exact endofunctor \triangleright

  3. with a natural transformation next:1\text{next} \;\colon\; 1 \to \triangleright satisfying next=next\triangleright\text{next} = \text{next}\triangleright

  4. supporting Löb-induction, i.e., ϕ:Ω|ϕϕϕ\phi : \Omega|\triangleright \phi \Rightarrow \phi \vdash \phi in the internal logic of EE.

Then “multi-clock” SGDT is simply a topos EE with an object of clocks K:EK \colon E such that the slice E/KE/K is a model of single-clock SGDT.

Type Theory

Mathematics in synthetic guarded domain theory can be formalized in the internal language of SGDT models. Several presentations have been proposed such as:

Agda includes an implementation of some portions of clocked cubical type theory under the name Guarded Cubical Agda.

Models

The most basic model of SGDT is given by the topos of trees, the category of presheaves on ω\omega, the first infinite ordinal. The topos of trees establishes the relationship between synthetic guarded domain theory and metric domain theory: the category of complete, bisected, ultrametric spaces embeds into the topos of trees as the full subcategory spanned by flabby objects (Proposition 5.1, there called “total” objects).

References

  • Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring, First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8 4 (2012) [doi:10.2168/LMCS-8(4:1)2012]

  • Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. Møgelberg, Lars Birkedal. Guarded Dependent Type Theory with Coinductive Types. FoSSaCS 2016 (doi)

  • Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. LICS 2022 (preprint)

  • Daniela Palombi and Jonathan Sterling, Classifying topoi in synthetic guarded domain theory: The universal property of multi-clock guarded recursion. Mathematical Foundations of Program Semantics 2022 (preprint)

  • Marco Paviotti, Denotational semantics in Synthetic Guarded Domain Theory. PhD thesis, IT University of Copenhagen (pdf)

  • Guarded Cubical Agda

  • Jonathan Sterling, Bibliography of Guarded Domain Theory

Last revised on August 4, 2022 at 17:56:24. See the history of this page for a list of all contributions to it.