A Short Review of Powerdomains

(draft … references to be added) … (up)

Powerdomains can be seen as modelling non-determinstic choice. They appear in various areas of mathematics and computer science.

We review the basic relationships between lower/upper powerdomains, forward and backward simulation, and

$◊$ and

$◻$ modalities.

It may be worth to read the Summary first.

An Axiomatic Account of Choice

A somewhat minimal axiomatisation of a "choice" operator

$\odot$ is

$$\begin{array}{c}(x\odot y)\odot z=x\odot (y\odot z)\\ x\odot y=y\odot x\\ x\odot x=x\end{array}$$

What is axiomatised here is choice as a set of alternatives. Given a set

$X$, we denote by

$\mathcal{P}X$ the set of subsets of

$X$ and by

${\mathcal{P}}_{\omega }X$ the set of finite subsets of

$X$. A set with an operation

$\odot$ satisfying the three equations above is known as a semi-lattice.

Facts:

• ${\mathcal{P}}_{\omega }X$ is the free semi-lattice over
  $X$.
• $({\mathcal{P}}_{\omega },\eta ,\mu )$ with
  $\eta (x)=\{x\}$ and
  $\mu (A)=\bigcup A$ where
  $A\subseteq {\mathcal{P}}_{\omega }X$ is a monad and the algebras for the monad are the semi-lattices.
• Semi-lattices can be equipped with an order in two ways. The first corresponds to taking
  ${\mathcal{P}}_{\omega }X$ with inclusion of subsets and the second to reverse inclusion.
  • The operation
    $\odot$ is the join in the poset generated by
    $x\le x\odot y$.
  • The operation
    $\odot$ is the meet in the poset generated by
    $x\ge x\odot y$.
• Similarly,
  $\mathcal{P}$ gives us complete semi-lattices. The initial algebra for the functor
  $\mathcal{P}$ is our usual set-theoretic universe, while the final coalgebra fo the functor
  $\mathcal{P}$ is Aczel's universe of non-well founded sets. ^[1]

Remark: Semi-lattices exist in many categories. This often allows us to generalise non-determinism.

Coalgebras for the Powerset Functor

(this section can be skipped)

More often than not, the reason to investigate choice is to model dynamic scenarios where agents change state by making choices. Such dynamical systems are known as coalgebras for the powerset functor and also as transition systems in process algebra and as non-determinstic automata in the theory of automata and formal languages and as Kripke frames in the theory of modal logic.

Mathematically, a coalgebra is a function

$X\to \mathcal{P}X$. A coalgebra morphism

$$(X\stackrel{\xi }{\to }\mathcal{P}X)\stackrel{f}{⟶}(X^{\prime }\stackrel{{\xi }^{\prime }}{\to }\mathcal{P}{X}^{\prime })$$

is a function

$f:X\to X^{\prime }$ satisfying

$$\mathcal{P}f\circ \xi =\xi \circ f.$$

In other words,

$f$ makes the following square commute.

Of course, a coalgebra on

$X$ is nothing but a set with a relation

$R\subseteq X\times X$. But coalgebra morphisms do not only preserve the relation but also reflect it in a particular way. Key to this is the following.

Exercise on (bi)simulation: We write

$xRy$ for

$y\in \xi (x)$. The following are equivalent conditions for

$f$ being a forward simulation.

$$\begin{array}{c}\mathcal{P}f\circ \xi \subseteq {\xi }^{\prime }\circ f\\ xRy\Rightarrow f(x)R^{\prime }f(y)\\ x^{\prime }=f(x)\Rightarrow \mathrm{\forall }y\in \xi (x).\mathrm{\exists }{y}^{\prime }\in {\xi }^{\prime }(x^{\prime }).y^{\prime }=f(x^{\prime })\end{array}$$

The following are equivalent conditions for

$f$ being a backward simulation.

$$\begin{array}{c}\mathcal{P}f\circ \xi \supseteq {\xi }^{\prime }\circ f\\ f(x)R^{\prime }{y}^{\prime }\Rightarrow \mathrm{\exists }y.xRy\mathrm{\&}{y}^{\prime }=f(y)\\ x^{\prime }=f(x)\Rightarrow \mathrm{\forall }{y}^{\prime }\in {\xi }^{\prime }(x^{\prime }).\mathrm{\exists }y\in \xi (x).y^{\prime }=f(x^{\prime })\end{array}$$

The advantage of the first conditions is that they are parametric in the functor^[2], the second condition is how so-called zig-zag morphisms or p-morphisms or bounded morphisms are defined in modal logic and the third conditions establish the following important fact that will continue to play a role in this note (we will give a precise definition of bisimulation later).

Fact: A function is a coalgebra morphism iff its graph is a bisimulation.

Powerdomains on Posets

The "domain" in powerdomain comes from domain theory and the theory of programming languages. It is well-known that in order to model recursively defined programs and datatypes in general one needs to extend the types-as-sets paradigm to types-as-domains. There are different ways to define domains. Typically, they involve some kind of complete order or complete metric that supports the taking of certain limits to interpret recursively defined functions. In this section, I simplify by ignoring completeness and only look at domains as ordered sets.

Functors

The powerset functor gives rise to three different powerdomains on the category of partial orders according to whether we enforce one of one of the following two alternatives.

$$\begin{array}{c}x\le x\odot y\\ x\ge x\odot y\end{array}$$

• The functor

  $${\mathcal{P}}^{\mathrm{c}}:\mathsf{P}\mathsf{o}\mathsf{s}\to \mathsf{P}\mathsf{o}\mathsf{s}$$ maps a poset
  $(X,\le )$ to the set of convex subsets
  $\mathcal{P}X$. The order on convex subsets is defined as follows. ^{[3] [4]}
  
  $$\begin{array}{rl}a\le b\text{ if }& \mathrm{\forall }x\in a.\mathrm{\exists }y\in b.x\le y\text{ and }\\ & \mathrm{\forall }y\in b.\mathrm{\exists }x\in a.x\le y\end{array}$$

  If

  $X$ is discrete then
  ${\mathcal{P}}^{\mathrm{c}}\mathrm{X}$ is just
  $\mathcal{P}X$ and
  $\le$ is equality.

• The functor

  $$\mathcal{D}:\mathsf{P}\mathsf{o}\mathsf{s}\to \mathsf{P}\mathsf{o}\mathsf{s}$$ maps a poset
  $(X,\le )$ to the set of downward closed subsets (downsets)
  $\mathcal{D}X$. The order on subsets
  $a,b\subseteq X$ is defined as ^{[5] [6]}
  
  $$\begin{array}{rl}a\le b\text{ if }& \mathrm{\forall }x\in a.\mathrm{\exists }y\in b.x\le y\end{array}$$

  which amounts to inclusion of downsets. If

  $X$ is discrete then
  $\mathcal{D}X$ is
  $\mathcal{P}X$ ordered by
  $\subseteq$.

• The functor

  $\mathcal{U}:\mathsf{P}\mathsf{o}\mathsf{s}\to \mathsf{P}\mathsf{o}\mathsf{s}$ maps a poset
  $(X,\le )$ to the set of upward closed subsets (upsets)
  $\mathcal{U}X$. The order on upsets is defined as ^[7]
  
  $$\begin{array}{rl}a\le b\text{ if }& \mathrm{\forall }y\in b.\mathrm{\exists }x\in a.x\le y\end{array}$$

  which amounts to reverse inclusion of upsets. If

  $X$ is discrete then
  $\mathcal{U}X$ is
  $\mathcal{P}X$ ordered by
  $\supseteq$.

Coalgebras

As noted above, coalgebras

$X\to \mathcal{P}X$ are in bijective correspondence with Kripke frames

$(X,R)$. This continues to hold in the ordered setting under appropriate conditions on the relation

$R$.

$(X,R)$ is an

$\mathcal{U}$-coalgebra iff

$R$ is a weakening relation, that is, iff

$$\frac{x^{\prime }\le xRy\le y^{\prime }}{x^{\prime }R{y}^{\prime }}$$

$(X,R)$ is an

$\mathcal{D}$-coalgebra iff

$$\frac{x^{\prime }\ge xRy\ge y^{\prime }}{x^{\prime }R{y}^{\prime }}$$

Example: Let

$X=\{x,y\}$ be a Kripke frame where

$x$ has no successor and

$y$ is reflexive. We can turn

$X$ into a

$\mathcal{U}$-coalgebra by setting

$x\le y$ and into a

$\mathcal{D}$-coalgebra by setting

$x\ge y$.

(Bi)simulations

As for set-functors, any functor on ordered sets gives rise to a canonical notion of (bi)simulation, cospan bisimulation. In case of

${\mathcal{P}}^{\mathrm{c}}$-coalgebras (bi)simulation is bisimulation, in case of

$\mathcal{U}$-coalgebras (bi)simulation is backward simulation and in case of

$\mathcal{D}$-coalgebras (bi)simulation is forward simulation.

Fact: The largest preorder on a

$\mathcal{U}$-coalgebra (

$\mathcal{D}$-coalgebra) compatible with the coalgebra structure is the largest backward-simulation (forward simulation) on that coalgebra. ^[8]

To understand this better it helps to know more about coalgebraic (bi)similarity. But I will try to shortcut this here, with more details available at cospan (bi)simulation.

In order to define the notion of (bi)simulation induced by

$\mathcal{U}$ or

$\mathcal{D}$ we proceed as follows.

• A relation
  $R$ from
  $X$ to
  $Y$ will be represented as an order
  $\mathbf{R}$ on the disjoint union
  $X+Y$.
• Because of the universal property of the coproduct, there always will be a coalgebra
  $\mathbf{R}\to T\mathbf{R}$ where
  $T$ is either
  $\mathcal{U}$ or
  $\mathcal{D}$.
• $R$ is a (bi)simulation iff
  $\mathbf{R}\to T\mathbf{R}$ is monotone.

Recall from the definition of

$\mathcal{D}$ and

$\mathcal{U}$ how these functors act on ordered sets.^[9] Instantiating this procedure it is not difficult to see the following.

Proposition on

$\mathcal{D}$- and

$\mathcal{U}$-(bi)simulation:

$\mathcal{D}$-(bi)simulation is forward-simulation and

$\mathcal{U}$-(bi)simulation is backward-simulation.

Simulations for Set-Coalgebras

Each functor

$T:\mathsf{S}\mathsf{e}\mathsf{t}\to \mathsf{S}\mathsf{e}\mathsf{t}$ induces a notion of

$T$-bisimulation.

What about simulations?

We first note that each functor

$T:\mathsf{O}\mathsf{r}\mathsf{d}\to \mathsf{O}\mathsf{r}\mathsf{d}$ induces a notion of

$T$-(bi)simulation.^[10] I write (bi)simulation here because technically this notion works much in the same way for

$\mathsf{S}\mathsf{e}\mathsf{t}$-functors and for

$\mathsf{O}\mathsf{r}\mathsf{d}$-functors. But for

$\mathsf{O}\mathsf{r}\mathsf{d}$-functors, it encompasses both simulations and bisimulations, depending on the functor.

A general way to introduce notions of simulation for

$\mathsf{S}\mathsf{e}\mathsf{t}$ functors is as follows. Let

$T:\mathsf{S}\mathsf{e}\mathsf{t}\to \mathsf{S}\mathsf{e}\mathsf{t}$ be a functor. Extend

$T$ to a functor

$T^{\prime }:\mathsf{O}\mathsf{r}\mathsf{d}\to \mathsf{O}\mathsf{r}\mathsf{d}$.^[11] Then restrict

$T^{\prime }$-(bi)simulation to

$T$-coalgebras.

Example: Let

$T=\mathcal{P}$. We can let

$T^{\prime }$ be one of

${\mathcal{P}}^{\mathrm{c}}$ or

$\mathcal{U}$ or

$\mathcal{D}$ to capture bisimulation or forward simulation or backward simulation.

Remark: The ordered setting is the right one if we want to exploit that the structures at hand support an order-duality. In the example,

$\mathcal{U}$ and

$\mathcal{D}$ capture

$◻$ and

$◊$ separately and both extend

$\mathcal{P}$.

Powerdomains via Generators and Relations

The finitary versions of the three powerdomains can be generated as follows. The way we describe algebras by generators and relation is the same as over sets, with the only difference that we now require

$\odot$ to be order-preserving (monotone).

If

$X$ is a finite poset, then the finitely generated convex subsets

${\mathcal{P}}_{\omega }^{\mathrm{c}}\mathrm{X}$ are ismorphic to the free semi-lattice over

$X$. Convexity is captured by the requirement that

$\odot$ is montone. ^[12]

If

$X$ is a finite poset, then the finitely generated downsets

${\mathcal{D}}_{\omega }X$ are ismorphic to the free semi-lattice over

$X$ satisfying

$x\le x\odot y$, or, equivalently, the free join semi-lattice over

$X$.

If

$X$ is a finite poset, then the finitely generated upsets

${\mathcal{U}}_{\omega }X$ are ismorphic to the free semi-lattice over

$X$ satisfying

$x\odot y\le x$, or, equivalently, the free meet semi-lattice over

$X$.

To remember how taking upsets and downsets interacts with the order, it is helpful to know the following.

Facts: Let

$X$ be a preorder.

$\mathcal{D}X$ is the free complete join semi lattice over

$X$.

$\mathcal{D}$ is a monad on preorders (and also on posets). The unit

$X\to \mathcal{D}X=[X^{\mathrm{o}},2]$ is the order enriched Yoneda embedding.^[13] The Yoneda embedding is a free completion by colimits (joins). The

$x\le x\odot y$ play the role of the arrows into the colimit (coproduct, join). (The Yoneda embedding preserves all limits (meets) that may already exist in

$X$.) The multiplication of the monad is the free extension of the identity

$\mathcal{D}X\to \mathcal{D}X$.

Modal Logic

We have seen that coalgebra morphisms express a particular back-and-forth condition. It is interesting to study its logical ramifications.

The key questions are: Which logic is invariant under coalgebra morphisms (bisimulation)? Which logic is invariant under forward (or backward) simulation?

The Logic of Bisimulation

The answer is given by the "bounded quantifiers"

$◻$ and

$◊$. Usually they are considered as syntactic operations on formulas. But I want to treat them here as operations on "semantic" propositions, that is, on subsets of

$X$ where

$$\xi :X\to \mathcal{P}X$$

is a coalgebra. We rewrite the usual definition of the semantics of

$◻$ and

$◊$ in terms of the coalgebra structure

$\xi$ as follows.

$$\begin{array}{c}◻a={\xi }^{-1}(\{b\subseteq X\mid b\subseteq a\})\\ ◊a={\xi }^{-1}(\{b\subseteq X\mid a\cap b\ne \mathrm{\varnothing }\})\end{array}$$

Exercise: The following are a direct consequence of the definition above.

$$\begin{array}{c}x\in ◻a⟺\mathrm{\forall }y\in \xi (x).y\in a\\ x\in ◊a⟺\mathrm{\exists }y\in \xi (x).y\in a\end{array}$$

We can now extend propositional logic by unary operators for

$◻$ and

$◊$ (and all equations they satisfy in all coalgebras). This is known as the modal logic

$\mathbf{K}$.

Here are some classic results of modal logic. I use "coalgebra" instead of "Kripke frame" to indicate that these results generalise.

Facts: The modal logic

$\mathbf{K}$ is invariant under coalgebra morphisms. Every logic that contains classical propositional logic and is invariant under bisimulation is equivalent to

$\mathbf{K}$ on finite coalgebras.

$\mathbf{K}$ characterises elements of coalgebras up to bisimilarity on finite coalgebras.

$\mathbf{K}$ is the bisimulation-invariant fragment of first-order logic.

The notion of bisimilarity can be defined in different ways. From a coalgebraic point of view I find the following the most elegant.

Two elements of two

$\mathcal{P}$-coalgebras are bisimilar (or behaviourally equivalent) iff they can be connected by some zig-zag of morphisms. ^[14]

The advantage of this definition is that it captures the informal idea that coalgebra-morphisms preserve behaviour and that it is parametric in the functor. But we also want a more combinatorial characterisation:

Given two coalgebras

$X\stackrel{\xi }{\to }\mathcal{P}X$ and

$X^{\prime }\stackrel{{\xi }^{\prime }}{\to }\mathcal{P}{X}^{\prime }$ a relation

$R\subseteq X\times X^{\prime }$ is called a bisimulation if

$$\begin{array}{rl}xR{x}^{\prime }\text{ only if }& \mathrm{\forall }y\in \xi (x).\mathrm{\exists }{y}^{\prime }\in {\xi }^{\prime }(x^{\prime }).x^{\prime }R{y}^{\prime }\text{and}\\ & \mathrm{\forall }{y}^{\prime }\in {\xi }^{\prime }(x^{\prime }).\mathrm{\exists }y\in \xi (x).x^{\prime }R{y}^{\prime }\end{array}$$

Facts: Two elements of two coalgebras are bisimilar iff there is a bisimulation relating them. If two elements of two coalgebras are bisimular then they satisfy the same modal formulas. The converse is true on finite coalgebras (or if we extend modal logic by infinitary conjunctions).

Logics of Simulation

A finer analysis, separating forward and backward simulation, is possible. It also sheds light on the ordered generalisations of the powerset functor.

Let me write

${\mathbf{K}}^{◻}$ and

${\mathbf{K}}^{◊}$ (this is not standard notation) for the negation-free fragment of

$\mathbf{K}$ that only contains

$◻$ (respectively

$◊$) formulas. It now turns out that preservation of

${\mathbf{K}}^{◻}$-formulas and preservation of

${\mathbf{K}}^{◊}$-formulas each corresponds to one direction of the definition of bisimulation.

As the Exercise on (bi)simulation above shows,

${\mathbf{K}}^{◊}$-formulas are invariant under forward-simulation and

${\mathbf{K}}^{◻}$-formulas are invariant under backward-simulation.

On the other hand, we know from the Proposition on

$\mathcal{D}$- and

$\mathcal{U}$-(bi)simulation that

$\mathcal{D}$-(bi)simulation is forward-simulation and

$\mathcal{U}$-(bi)simulation is backward simulation.

We now assembled all the pieces needed for the table below.

Summary

To read the table recall that, for a poset

$X$, the elements of

$\mathcal{D}X$ are downsets ordered according to

$a\le b\iff a\subseteq b$ and the elements of

$\mathcal{U}X$ are upsets ordered as

$a\le b\iff a\supseteq b$ .

$T$	$\mathcal{D}$	$\mathcal{U}$
also known as	Hoare powerdomain	Smyth powerdomain
$\odot$	$\cup$	$\cap$
$a\le b\in TX$	$\mathrm{\forall }x\in a.\mathrm{\exists }y\in b.x\le y$	$\mathrm{\forall }y\in b.\mathrm{\exists }x\in a.x\le y$
semilattice + …	$a\le a\odot b$	$a\odot b\le a$
(bi)simulation	forward	backward
logic	$◊$	$◻$
$X\stackrel{R}{⟶}TX$	$\frac{x^{\prime }\ge xR{y}^{\prime }\ge y}{x^{\prime }R{y}^{\prime }}$	$\frac{x^{\prime }\le xR{y}^{\prime }\le y}{x^{\prime }R{y}^{\prime }}$
	angelic	demonic

Maybe the most principled way to remember that

$\mathcal{U}$ gives

$◻$ and

$\mathcal{D}$ gives

$◊$ is via a direct analysis of the predicate liftings of these functors, see my note on monotone predicate liftings.

A choice satisfying

$a\le a\odot b$ is sometimes called angelic because, whatever

$a\odot b$ is, it is better than what I have,

$a$. Dually, a demon would make sure that

$a\odot b$ is not better than

$a$ and not better than

$b$.

Generalisations

The basic ideas we have seen so far generalise in many directions.

In domain theory we are typically interested in directed complete partial orders with the Scott topology.

Domains can be seen as particular topological spaces. Many different topological spaces support some kind of powerspace, often called the Vietoris construction.

Vietoris defined a powerdomain on certain topological spaces. A good introduction to the topic is this talk by Guram Bezhanishvili. (Passcode: ?D3q#^mw).

The theory can also be developed internally in a topos.

Many results on powerdomains generalise to quantale enriched categories. And some even survive the move to categories or higher categories. The analogy here is that the powerset functor, or rather

$\mathcal{U}$ and

$\mathcal{D}$, generalise to taking presheaves.

…

Further Reading

(very incomplete)

Topology

Vietoris

Johnstone: Stone Spaces. 1982. See in particular Chapter III.4. On page 112 one finds the definitions of

$◻$ (called

$t$) and

$◊$ (called

$m$). This also works for ordered compact Hausdorff spaces and many other settings, see Guram Bezhanishvili's talk.

G. Bezhanishvili: Talk on The hit-or-miss toplogy. (Passcode: ?D3q#^mw).

Modal Logic

van Benthem, Segerberg, Goldblatt, …

Domain Theory

Plotkin 1976, Smyth 1978 ^[15], Plotkin 1980, Apt-Plotkin 1981, Winskel 1985 ^[16], Section 6.2 of Abramsky-Jung 1994, Martin-Curtis-Rewitzky 2007, Section 3 of Goubault-Larreque 2010, …

Coalgebra

Aczel: Non-well founded set theory. Aczel-Mendler, …

Barwise, Moss: Vicious Circles.

Baltag: A structural theory of sets.

Rutten: Universal coalgebra.

Jacobs, Hughes-Jacobs, …

Pattinson

Litak etal

…

More references can also be found in the following papers. Kurz-Palmigiano Coalgebras and Modal Expansions of Logics, Kapulkin-Kurz-Velebil Expressiveness of Positive Coalgebraic Logic, Bilkova-Kurz-Petrisan-Velebil Relation lifting, with an application to the many-valued cover modality, Balan-Kurz-Velebil Positive Fragments of Coalgebraic Logics.

---

1. To make this claim precise, one needs to extend sets with classes and extend the powerset functor continuously. ↩︎

2. All functors can be extended to functors on ordered sets, see Positive Fragments of Coalgebraic Logics. ↩︎

3. Note how the back-and-forth pattern of bisimulations appears again. ↩︎

4. We could have defined this powerdomain as the set of all subsets instead of restricting to convex subsets. Then

   $\mathcal{P}X$ is a preorder but may not be a partial order. This gives the right definition of the "convex" powerdomain on preorders. In fact, for a preorder
   $(X,\le )$ and
   $a,b\subseteq X$ we have
   $a\le b$ iff they have the same posetal quotients of their convex closures. ↩︎

5. Note that the definition of the order

   $\le$ makes sense for aribtray subsets of
   $X$ (but may only be a preorder then). ↩︎

6. The justification for choosing this half of the convex powerdomain is the following. Two subsets

   $a,b\subseteq X$ are in the relation
   $a\le b$ iff the downset closure of
   $a$ is a subset of the downset closure of
   $b$. It follows that if
   $X$ is a poset then the order
   $\le$ is also a poset when restricted to downsets. ↩︎

7. As before, the definition of the order makes sense for aribtrary subsets

   $a,b\subseteq X$ (and we can use this observation to extend the powerset functor to preorders). Note that
   $a\le b$ iff the upset of
   $b$ is a subset of the upset of
   $a$. It follows that if
   $X$ is a poset then the order
   $\le$ is also a poset when restricted to upsets. ↩︎

8. Compatible means that the quotient by the preorder is again a coalgebra. ↩︎

9. The order on

   $\mathcal{D}X$ is given by
   $$\begin{array}{rl}a\le b\text{ if }& \mathrm{\forall }x\in a.\mathrm{\exists }y\in b.x\le y\end{array}$$

   and the order on

   $\mathcal{U}X$ by
   
   $$\begin{array}{rl}a\le b\text{ if }& \mathrm{\forall }y\in b.\mathrm{\exists }x\in a.x\le y\end{array}$$ ↩︎

10. I like to write

    $\mathsf{O}\mathsf{r}\mathsf{d}$ if I do not want to commit to using preorders or posets. If you want to be specific let
    $\mathsf{O}\mathsf{r}\mathsf{d}$ be the category of preorders. ↩︎

11. Let

    $D:\mathsf{S}\mathsf{e}\mathsf{t}\to \mathsf{O}\mathsf{r}\mathsf{d}$ be the "discrete" embedding.
    $T^{\prime }$ is an extension of
    $T$ if there is a natural transformation
    $DT\to T^{\prime }D$. For example, if
    $T=\mathcal{P}$ and
    $T^{\prime }=\mathcal{U}$, then we have the bijection
    $(\mathcal{P}X,=)\to (\mathcal{U},\subseteq )$. ↩︎

12. Add more detail … ↩︎

13. This deserves more explanation … ↩︎

14. See the note on Coalgebraic (Bi)Similarity for more. ↩︎

15. On page 26 we find
    

    ↩︎

16. On page 128 we find
    

    ↩︎