Domain theory is “topology with an attitude”...

Not, to be clear, topology qua the study of topological spaces, but rather: topology qua the search for adequate notions of space.

Adequate for what? There are many viewpoints, and all of them are correct. But today, I speak about computer science.

A domain is a space in which computation happens.

The (generalised) points of a domain correspond to specific programs.

Points of a domain \(X\) are equipped with an information order \(u\sqsubseteq _X v\) that can be thought of in two ways:

1. Logic: “Any observably true property of \(u\) is also true of \(v\).”
2. Geometry: “We have a continuous transformation \(\alpha \colon \mathbb {I}\to X\) with \(\alpha {\mathopen {}\left (0\right )\mathclose {}} = u\) and \(\alpha {\mathopen {}\left (1\right )\mathclose {}} = v\).”

A reasonable “logic of observable properties” can always be obtained by saying that \(P\subseteq X\) is observable iff it is classified by \({\mathopen {}\left \{1\right \}\mathclose {}}\subseteq \mathbb {I}\).

With the information order, domains are naturally arranged into a (locally posetal) bicategory. Recursion is interpreted as sequential colimit, both at the “type level” and the “program level”.

1. A recursively defined domain is obtained as the pseudo-colimit of an \(\omega \)-chain of internal adjunctions (Cattani and Fiore).
2. A recursively defined program is obtained as a (local) colimit of an \(\omega \)-chain of generalised points.

Domains have served as the computational substrate for the denotational semantics of programming languages to enable computational reasoning about recursive processes.

The simplest kinds of domains, \(\omega \)-cpos and dcpos, have had the widest applicability for “working computer scientists”.

Some computational effects (e.g. exceptions, first-order store, non-determinism, etc.) dealt with elegantly in terms of these simple domains. Concurrency is another story.

In classical domain theory, observations are “propositional”: there is at most one way for an observation to happen (e.g. termination). Early attempts at concurrency semantics used domains of sets of traces.

Inadequate for concurrency: many different ways for a process to take a certain path. Two processes that realise the same set of traces may not be bisimilar, as bisimulation theory must “remember” the way that processes are glued together.

Let \(\alpha \) be an “action”, and consider the two processes \(\alpha \star \) and \(\alpha .\varnothing + \alpha \star \).

We have \(\mathbf {Traces}{\mathopen {}\left (\alpha \star \right )\mathclose {}} = {\mathopen {}\left \{\varepsilon , \alpha , \alpha .\alpha ,\ldots \right \}\mathclose {}}=\mathbf {Traces}{\mathopen {}\left (\alpha .\varnothing + \alpha \star \right )\mathclose {}}\).

But the process \(\alpha \star \) can never get stuck, whereas \(\alpha .\varnothing + \alpha \star \) gets stuck if it proceeds along the left branch.

Thus trace equivalence is highly un-physical. To deal with this, we generalise the information order to a category in which bisimulation can be expressed. Idea: non-determinism must be modelled by a van Kampen colimit (e.g. disjoint coproduct).

See Joyal, Nielsen and Winskel (1996) and Cattani and Winskel (2005).

Bicategories of concurrent domains abound (most examples arising from distributors, spans, or the like).

We are interested in \(\infty \)-bicategories, i.e. \({\mathopen {}\left (\infty ,2\right )\mathclose {}}\)-categories, of domains. Potential advantage: a domain of all domains (Paul Taylor).

To that end, we start by studying domain-theoretic concepts in the Riehl–Shulman framework for synthetic \(\infty \)-categories.

Riehl and Shulman introduced simplicial HoTT, a new type theory with judgemental structure that represents the \(n\)-simplex \(\mathbb {I}_n\subseteq \mathbb {I}^n\) and related figures (like the horn \(\mathbb {H}^2_1\subseteq \mathbb {I}_2\)) in the \(\infty \)-topos of simplicial spaces.

1. Segal types are internally orthogonal to \(\mathbb {H}^2_1\hookrightarrow \mathbb {I}_2\).
2. Rezk types are internally orthogonal to \(\mathbb {H}^2_1\hookrightarrow \mathbb {I}_2\) and \(\mathbb {E}\to \mathbf {1}\) where \(\mathbb {E}\) is the walking isomorphism.

Segal \(\sim \) precategory, Rezk \(\sim \) category.

The judgmental structure of simplicial HoTT can be distracting. Simpler(*): just axiomatise the theory of a strict interval in HoTT.

Domains are usually defined as the algebras for a partial map classifier (pseudo-)monad, where \(\mathcal {O}\) is a dominance containing \(\bot \).

The dominance \(\mathcal {O}\) is some kind of interval, as \(\bot \leq \top \). Leoni Pugh and I are studying the partial map classifier for the simplicial interval \(\mathbb {I}\) in simplicial homotopy type theory.

Maps \(X\to L{\mathopen {}\left (A\right )\mathclose {}}\) uniquely determine spans \(X\hookleftarrow U\to A\) whose left components are open, i.e. classified by \({\mathopen {}\left \{1\right \}\mathclose {}}\subseteq \mathbb {I}\), as follows:

Not much can be done until we assume Phoa’s principle, which is either of the following equivalent properties:

1. The boundary map \(\mathbb {I}^\mathbb {I}\to \mathbb {I}^2\) factors through an isomorphism \(\mathbb {I}^\mathbb {I}\cong \mathbb {I}_2\subseteq \mathbb {I}^2\).
2. For any function \(\phi \colon \mathbb {I}\to \mathbb {I}\), we have \(\phi {\mathopen {}\left (x\right )\mathclose {}} = \phi {\mathopen {}\left (0\right )\mathclose {}}\lor {\mathopen {}\left (x \land \phi {\mathopen {}\left (1\right )\mathclose {}}\right )\mathclose {}}\).

Probably cannot be deduced from the axiomatics of Riehl and Shulman, but true in the model.

We might name by the “higher Phoa principle” either of the following equivalent properties:

1. Each boundary map \(\mathbb {I}^{\mathbb {I}_n}\to \mathbb {I}^{n+1}\) factors through an isomorphism \(\mathbb {I}^{\mathbb {I}_n}\cong \mathbb {I}_{n+1}\subseteq \mathbb {I}^{n+1}\).
2. For any function \(\phi \colon \mathbb {I}_n\to \mathbb {I}\), we have: \[\phi {\mathopen {}\left (x_0,\ldots x_{n-1}\right )\mathclose {}}=\phi {\mathopen {}\left (0\ldots \right )\mathclose {}}\lor \bigvee _{1\leq i \leq n}{\mathopen {}\left (x_{n-i}\land \phi {\mathopen {}\left (0^{n-i}\ldots 1^i\right )\mathclose {}}\right )\mathclose {}}\]

Equivalence due to Leoni Pugh. In fact, Pugh shows that the ordinary Phoa principle implies the higher Phoa principle.

The higher Phoa principle is a Kock–Lawvere / “synthetic quasi-coherence” axiom that comes directly from the geometric theory of a strict interval, as a quotient of the theory of bounded distributive lattices (Gratzer).

Question. What are the other domain theoretic consequences of synthetic quasicoherence?

Assuming the higher Phoa principle, Leoni has deduced that if \(A\) is a Segal type, then so is \(L{\mathopen {}\left (A\right )\mathclose {}}\).

It is not difficult, using results of Buchholtz and Weinberger, to show that if \(A\) is Rezk, then so is \(L{\mathopen {}\left (A\right )\mathclose {}}\).

Thus, synthetic \({\mathopen {}\left (\infty ,1\right )\mathclose {}}\)-categories are closed under partial map classifiers: a necessary first step to a theory of higher domains.

In traditional domain theory, the partial map classifier has an additional left-handed universal property: the Sierpiński cone.

The scone’s universal property allows “case analysis” on whether a partial element is defined, even in constructive domain theory. When \(c_\bot \sqsubseteq _C c_\eta x\), we may define:

We can actually compute the scone \(\bot {\mathopen {}\left (A\right )\mathclose {}}\) in simplicial type theory.

1. First take a pushout with the appropriate weight:

   

2. Then compute the universal Rezk type \(\bot {\mathopen {}\left (A\right )\mathclose {}}\) equipped with a map \({\mathopen {}\left \{\bot \right \}\mathclose {}} \amalg _A {\mathbb {I}\times A} \to \bot {\mathopen {}\left (A\right )\mathclose {}}\).

When \(A\) is Rezk, we have a comparison map \(\bot {\mathopen {}\left (A\right )\mathclose {}} \to L{\mathopen {}\left (A\right )\mathclose {}}\). Pugh’s result lets us use the universal property of the scone:

Unfortunately, the present axiomatics do not seem to imply that \(\bot {\mathopen {}\left (A\right )\mathclose {}}\to L{\mathopen {}\left (A\right )\mathclose {}}\) is an equivalence.

In the case of dcpos, unique extensions of \(f\colon \bot {\mathopen {}\left (A\right )\mathclose {}}\to C\) along the comparison map \(\bot {\mathopen {}\left (A\right )\mathclose {}}\to L{\mathopen {}\left (A\right )\mathclose {}}\) are obtained by taking the colimits of diagrams \(\bot {\mathopen {}\left (i=1\right )\mathclose {}}\to C\):

Perhaps we can use the same idea.

Conjecture. The comparison map \(\bot {\mathopen {}\left (A\right )\mathclose {}}\to L{\mathopen {}\left (A\right )\mathclose {}}\) is left orthogonal to any Rezk type closed under colimits of shape \(\bot {\mathopen {}\left (i=1\right )\mathclose {}}\) in the sense of Bardomiano Martínez.

Complete Segal spaces would provide a model of higher analytic domain theory, where cocontinuity conditions are explicit:

1. Recursion is implemented by sequential colimits.
2. Thus domains must be suitably cocomplete objects.
3. And morphisms between domains must be suitably cocontinuous.

This is natural, but very painful. We would like a “DSL” for domain theory, where maps are automatically cocontinuous. (Dana Scott’s suggestion, 1980: synthetic domain theory.)

In synthetic domain theory, we expect a topos equipped with a full reflective subfibration of suitable “cocomplete” objects. This is, by definition, an orthogonality condition! “Cocontinuity” is thus automatic.

Let \(L{\mathopen {}\left (\omega \right )\mathclose {}} \to \omega \) be an initial algebra, and let \(\bar {\omega }\to L{\mathopen {}\left (\bar {\omega }\right )\mathclose {}}\) be a terminal coalgebra with its infinite point \(\infty \in \bar \omega \). We have a canonical comparison map \(\omega \hookrightarrow \bar \omega \).

Then a (pre)domain is a type that is internally orthogonal to every pullback of the comparison map \(\omega \hookrightarrow \bar \omega \) along an open subspace of \(\omega \).

Extending along \(\omega \hookrightarrow \bar \omega \) means: equip an “\(\omega \)-chain” with a “colimit”, given by evaluation of the extension at \(\infty \).

Stability of the left class under open immersions \(U\hookrightarrow \bar \omega \) implies that if \(X\) is a predomain, so is \(L{\mathopen {}\left (X\right )\mathclose {}}\).

In the 1990s, Fiore and Rosolini and Fiore and Plotkin studied the representation of analytic categories of domains in toposes of synthetic domains by taking sheaves, building on prior work of Scott.

We hope that we can also take \({\mathopen {}\left (\infty ,1\right )\mathclose {}}\)-sheaves on a dense generator of the category of \(\omega \)-cpos to obtain a model of higher synthetic domain theory. Our existing work on lifting should apply.

Open question. We must get a better understanding of models of SDT as classifying toposes in order to continue to synthetic quasicoherence.

Related to our current efforts, we hope also to investigate whether the formally (co)complete cuboidal sets of Fiore, Plotkin, and Power (1997) have a synthetic counterpart.

thanks!