nLab synthetic domain theory




Synthetic domain theory, as its name suggests, is a synthetic axiomatization of domain theory, typically in toposes. The slogan for synthetic domain theory is that “domains are sets”, or more precisely, “domains are certain intuitionistic sets” in that one works in an intuitionistic set theory with certain anti-classical axioms and defines a notion of domain internally. These synthetic domains act like the analytic notions in that domains support arbitrary fixed points and solutions to non-well-founded recursive domain equations.


Specific axioms of SDT vary, but a category for synthetic domain theory is typically a topos equipped with a dominance Σ\Sigma. From this dominance, a Σ\Sigma-partial map classifier can be constructed called the “lift” monad LAL A. The lift monad has initial and final algebras (as a functor, rather than a monad) called ω\omega and ω¯\overline\omega respectively, with an induced monomorphism ωω¯\omega \to \overline \omega. Then it is required that the induced function Σ ω¯Σ ω\Sigma^{\overline \omega} \to \Sigma^\omega has an inverse.

An intuition is that maps out of ω\omega are a synthetic notion of ω\omega-chains (as in ω \omega -CPOs) and maps out of ω¯\overline \omega are ω\omega-chains with a limit point. Requiring the inverse above then amounts to requiring that every chain in Σ\Sigma has a unique limit point.


There are two main classes of models of synthetic domain theory: realizability toposes and Grothendieck toposes.

A Grothendieck topos model that is very closely related to the analytic notion of ω\omega-CPO is given by taking sheaves with respect to the canonical topology on the full subcategory of ω\omega-CPO whose objects are finite products of ω¯\overline \omega, i.e., the ordinal ω+1\omega + 1. This model embeds ω\omega-CPO and the embedding preserves (among other things) limits, coproducts and the natural numbers object. The ω\omega-CPOs can be characterized as certain ¬¬\neg\neg-separated sheaves.


Last revised on October 28, 2022 at 00:41:24. See the history of this page for a list of all contributions to it.