Discussing "First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees"

(Link). Slightly confusingly, the authors earlier published a shorter conference article with the same name.

Authors: Lars Birkedal (IT University of Copenhagen), Rasmus Ejlers Møgelberg (IT University of Copenhagen), Jan Schwinghammer (Saarland University), and Kristian Støvring (University of Copenhagen)

Reference: Birkedal, L., Møgelberg, R. E., Schwinghammer, J., & Støvring, K. (2012). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science, 8.

Why this paper? Cited by A Formal Logic for Formal Category Theory, Classifying topoi in synthetic guarded domain theory, and A metalanguage for cost-aware denotational semantics

This paper, which has been very influential on a chunk of my career, nicely pieces together some practically minded applications in program verification with the more abstract world of category theory.

The practical motivations are very similar to the step-indexing paper I discussed a few weeks ago, namely type systems with recursive features that appear difficult to reason about without getting trapped in unsolvable circularities. In the key example of this paper, a programming language with higher-order store (i.e. the ability to store typed programs in memory) forces one to define the meaning of types in terms of the meaning of the store, but also to define the meaning of the store in terms of the meanings of types! In the step-indexing approach, one works around these circularities by invoking a natural number that decreases towards zero as the program computes; this paper does something quite similar, but in the name of “avoiding tedious calculations with step indices” it instead asks us to work in a topos which naturally supports this sort of notion of steps.

A topos is, very roughly, a ‘mathematical universe’ (or category) which contains the mathematical machinery one would expect to have in set theory. For example, a subobject classifier is an object of truth values. We might expect to have just the two values, True and False – and indeed there are toposes for which this is so – but in the topos of this paper, the topos of trees, one can see the subobject classifier as the set of all natural numbers, along with the infinite value ω. One can consider 0 as False, ω as True, and each positive integer n as ‘not falsified by the first n steps of computation’ (this is not quite how this paper presents things, but is the point of view taken for example by a later paper of mine). This is quite a nice way to think about computations that unfold over time: consider two streams (infinite lists); they are 1-equal if their first elements agree, 2-equal if their first two elements agree, and so on to only reach ω, or ‘true’, equality if there is no index on which they will ever be unequal. In other words, working inside the topos of trees gives you access to a logic that allows you to talk about certain aspects of computer programs that are harder to describe with more conventional logic. In particular, instead of working directly with the indices, one instead can do a lot with a modality (new logical connective) called ‘later’ than helps hide those details away while preserving the ability to make the sort of arguments for which one would otherwise explicitly involve step indices.

As well as the logical point of view which comes from working with the subobject classifier, one can also use the topos of trees as a denotational semantics (mathematical meaning) for types in various ways, whether one is reasoning about a typed programming language, or using dependent type theory to construct a formal mathematical argument. Looked at through this prism, instead of viewing a type as standing in for its set of elements, one can view types as an infinite series of sets that become more and more precise or informative over time. For example, the type of streams is not merely the set of infinite sequences, but instead an infinite string of sets that at step 1 reveal only their first elements, at step 2 reveal their first two elements, and so on. The modality `later’ now reappears in slightly different guise as a type-former; one needs to check that self-references are guarded by later in order to ensure one has a meaningful recursive type definition. This idea of checking syntax for guardedness in order to ensure that recursive definitions are good is quite old, but usually takes place at the level of the syntax of terms. By lifting this check to the level of types we get the advantages that well-behaved type systems usually confer, particularly modularity – the ability to stick any two good programs together, provided their types agree, without their combination going wrong.