Person. Paul Taylor [paultaylor]

Honorary Senior Research Fellow
University of Birmingham
https://paultaylor.eu/

Backlinks

Presentation. Baby steps in higher domain theory [00RN]

April 5, 2024
Jon Sterling with contributions from Leoni Pugh
Homotopy Type Theory and Computing – Classical and Quantum

I present some preliminary results obtained with Leoni Pugh concerning partial map classifiers in higher domain theory, realised in a version of Riehl and Shulman’s simplicial type theory assuming Phoa’s principle for the simplicial interval.

This is joint work with my masters/Part III student Leoni Pugh.

Slide. What is domain theory?

April 5, 2024
Jon Sterling

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.

Slide. Domains for computer science

April 5, 2024
Jon Sterling

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:

Logic: “Any observably true property of \(u\) is also true of \(v\).”
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}\).

Slide. Recursion as passage to the (co)limit

April 5, 2024
Jon Sterling

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”.

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

Slide. Denotational semantics in domains

April 5, 2024
Jon Sterling

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.

Slide. 2-dimensional domain theory for concurrency (I)

April 5, 2024
Jon Sterling

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.

Slide. 2-dimensional domain theory for concurrency (II)

April 5, 2024
Jon Sterling

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).

Slide. Towards \(\infty \)-bicategories of domains

April 5, 2024
Jon Sterling

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.

Slide. Simplicial homotopy type theory

April 5, 2024
Jon Sterling

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.

Segal types are internally orthogonal to \(\mathbb {H}^2_1\hookrightarrow \mathbb {I}_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.

Slide. Lifting and partial map classifiers

April 5, 2024
Jon Sterling

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

\[ L{\mathopen {}\left (A\right )\mathclose {}} :\equiv \mathchoice {\textstyle \sum _{{\mathopen {}\left (p:\mathcal {O}\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (p:\mathcal {O}\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (p:\mathcal {O}\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (p:\mathcal {O}\right )\mathclose {}}}}A^p \]

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.

Slide. Right-handed universal property of partial map classifiers

April 5, 2024
Jon Sterling

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:

Slide. Phoa’s principle in higher domain theory

April 5, 2024
Jon Sterling

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

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\).
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.

Slide. The higher Phoa principle (Leoni Pugh)

April 5, 2024
Jon Sterling

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

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}\).
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.

Slide. The Phoa principle vs. synthetic quasicoherence

April 5, 2024
Jon Sterling

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?

Slide. The partial map classifier of a synthetic \({\mathopen {}\left (\infty ,1\right )\mathclose {}}\)-category

April 5, 2024
Jon Sterling

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.

Slide. Is the partial map classifier a Sierpiński cone? (I)

April 5, 2024
Jon Sterling

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

(In categories, this means: free cocompletion by an initial object.)

Slide. Is the partial map classifier a Sierpiński cone? (II)

April 5, 2024
Jon Sterling

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:

Slide. Is the partial map classifier a Sierpiński cone? (III)

April 5, 2024
Jon Sterling

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

First take a pushout with the appropriate weight:
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 {}}\).

(Recall that Rezk types are defined by localising at just two maps.)

Slide. Is the partial map classifier a Sierpiński cone? (IV)

April 5, 2024
Jon Sterling

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.

Slide. Is the partial map classifier a Sierpiński cone? (V) [012P]

April 5, 2024
Jon Sterling

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\):

\[ \begin {aligned} L{\mathopen {}\left (A\right )\mathclose {}} &\to C \\ {\mathopen {}\left \langle i,a\right \rangle \mathclose {}} &\mapsto \operatorname {colim}_{\bot {\mathopen {}\left (i=1\right )\mathclose {}}} {\mathopen {}\left [f{\mathopen {}\left (\bot \right )\mathclose {}} \mid p:i=1\hookrightarrow f{\mathopen {}\left (\eta {\mathopen {}\left (a{\mathopen {}\left (p\right )\mathclose {}}\right )\mathclose {}}\right )\mathclose {}}\right ]\mathclose {}} \end {aligned} \]

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.

Slide. Analytic vs. synthetic domain theory (I)

April 5, 2024
Jon Sterling

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

Recursion is implemented by sequential colimits.
Thus domains must be suitably cocomplete objects.
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.)

Slide. Analytic vs. synthetic domain theory (II)

April 5, 2024
Jon Sterling

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 \).

Slide.

April 5, 2024
Jon Sterling

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 {}}\).

Slide. Analytic vs. synthetic domain theory (III)

April 5, 2024
Jon Sterling

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.

Slide.

April 5, 2024
Jon Sterling

thanks!

Question. The Phoa axiom and synthetic quasicoherence [008W]

September 12, 2023

Can the Phoa axiom in synthetic domain theory be deduced from synthetic quasicoherence? I believe that Paul Taylor may have commented on something in this direction once in MathOverflow, but I do not know if anyone has proved this. I think it could be an interesting test-case. In cases where we have a clean understanding of the geometric theory in question (as in simplicial sets), this might be feasible; but I wonder about more sophisticated models of synthetic domain theory.