nLab synthetic guarded domain theory

Contents

Contents

Idea

Synthetic guarded domain theory (SGDT), is a field of synthetic mathematics that provides an alternative to synthetic domain theory, where all guarded recursive definitions have (guarded) fixed points.

More generally, the aim of synthetic domain theory is roughly that computability should be built in the logic. As a result, constructions on domains would be set-theoretic with no extra structure and proofs of continuity are for free. However, such a theory would yield an unrestricted fixed-point combinator at all types which would render the theory itself inconsistent when viewed as a logical system.

SGDT solves this problem by introducing a notion of “time”. For a type AA, A\triangleright A is the type of computations available one step from now. The \triangleright modality (pronounced “later”) yields a restricted fixed-point operator

fix:(AA)A\text{fix} : (\triangleright A \to A) \to A

at all types AA, which is consistent when viewing this theory as a logical framework. In particular, it corresponds to Löb's theorem.

A model of SGDT

The original model of (single-clock) SGDT is the category of presheaves over ω\omega, the first infinite ordinal. The objects of this category, also known as the topos of trees, here named 𝒮\mathcal{S}, are contravariant set-valued functors X:ω opSetX : \omega^{\text{op}} \to \text{Set} which have the following shape

X(1)r 1X(2)r 2r n1X(n)r nX(1) \xleftarrow{r_1} X(2)\xleftarrow{r_2} \dots \xleftarrow{r_{n-1}} X(n)\xleftarrow{r_{n}} \dots

where the maps r ir_i, for iω opi \in \omega^{\text{op}}, are the restriction maps induced by the functor XX. The arrows of this category are natural transformations between two functors (satisfying the naturality condition).

The later modality \triangleright is an endofunctor in this category defined as A(1)=1\triangleright A (1) = 1 and A(n+1)=A(n)\triangleright A (n+1) = A(n), for an object AA. Furthermore, for every object XX there exists an obvious map next:XX\text{next} : X\to \triangleright X witnessing the fact that everything that is available now is also available later.

Inspired by terminology used in the metric spaces (see below), every map XXX \to X in Set ω op\text{Set}^{\omega^\text{op}} is called non-expansive while a map f:XXf : X \to X is contractive if it factors through the next\text{next} map, i.e. there exists a map g:XXg : \triangleright X \to X such that f=gnextf = g \circ \text{next}.

 Fixed-point construction

A \triangleright-algebra (X,f)(X, f) yields a natural transformation with components f 1:1X(1)f_1 : 1 \to X(1) and f i:X(i)X(i+1)f_i : X(i) \to X(i+1) commuting with the restriction maps of the object XX. It can therefore be thought of as an ω\omega-chain as follows

1f 1X(1)f 2X(2)X(n)1 \xrightarrow{f_1} X(1) \xrightarrow{f_2} X(2) \dots \to X(n) \dots

The morphism fix f:1X\text{fix}_f : 1 \to X is itself a natural transformation whose components are f 1f i1f i:1X(i)f_1 \circ \dots f_{i-1} \circ f_{i} : 1 \to X(i), for all iω opi \in \omega^{\text{op}} satisfying

fix f=fnext(fix f)\text{fix}_f = f \circ \text{next} \circ (\text{fix}_f)

The idea here is that the recursive call is guarded by the next\text{next} map.

Relation with the metric spaces

The category of complete bisected ultrametric spaces (BiCUlt) is a coreflective subcategory of the topos of trees (Proposition 5.1).

BiCUltι𝒮 \text{BiCUlt} \underoverset {\underset{}{\leftarrow}}{\overset{\iota}{\hookrightarrow}}{\bot } \mathcal{S}

Moreover, the inclusion functor restricts to an equivalence of categories when considering objects in 𝒮\mathcal{S} whose restriction maps are surjective, which are sometimes called the total objects or flabby sheaves.

First, recall that every point in a ball \mathcal{B} of an ultrametric space is at its centre while intersecting balls are contained into each other which means that closed 2 n2^{-n}-balls partition a space. Thus, we can partition a metric space (X,d)(X, d) by defining a family of equivalence relation

x= nyd(x,y)2 nx =_n y \Leftrightarrow d(x,y) \le 2^{-n}

for all nn \in \mathbb{N}. This family is also known as Complete Ordered Family of Equivalences (c.o.f.e) (Di Gianantonio and Miculan, 2003). Intuitively, xx and yy are equal at nn if they belong to the same 2 n2^{-n}-ball.

The inclusion functor ι:BiCUlt𝒮\iota: \text{BiCUlt} \hookrightarrow \mathcal{S} takes a metric space (X,d)(X,d) in CBUlt into the presheaf of its space decompositions

(X/= 1)(X/= 2)(X/= n)(X/=_1) \leftarrow (X/=_2) \leftarrow \dots \leftarrow (X/=_n) \leftarrow \dots

where each restriction map (X/= (n+1))(X/= n)(X/=_{(n+1)}) \to (X/=_{n}) takes a 2 (n+1)2^{-(n+1)}-ball to the 2 n2^{-n}-ball that contains it.

The inclusion functor has a right adjoint 𝒮BiCUlt\mathcal{S} \to \text{BiCUlt} which maps a presheaf XX to the homset 𝒮(1,X)\mathcal{S}(1, X) (the global elements of XX). This is also the limit of XX when seen as a diagram in Set. The metric on 𝒮(1,X)\mathcal{S}(1, X) is defined as

d(x,y)={2 ni<n.x j()=y j()}d(x,y) = \bigsqcap \{ 2^{-n} \mid \forall i \lt n . x_j(\star) = y_j(\star) \}

for natural transformations x,y:1Xx, y : 1 \to X. Intuitively, this metric is the greatest lower bound on which the elements of XX agree.

A summary of these results can be found in Bizjak’s Ph.D. thesis (Bizjak 16, Section 1.2).

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.

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)

  • Daniele 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 (doi)

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

  • Aleš Bizjak, On Semantics and Applications of Guarded Recursion. PhD thesis, Aarhus University (pdf)

  • Pietro Di Gianantonio, Marino Miculan, A Unifying Approach to Recursive and Co-recursive Definitions. In Geuvers, Wiedijk, editors, Proceedings of TYPES’02. LNCS 2646, 2003.

  • Guarded Cubical Agda

  • Jonathan Sterling, Bibliography of Guarded Domain Theory

Last revised on November 23, 2022 at 23:24:30. See the history of this page for a list of all contributions to it.