Powerdomains

Powerdomains#

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 $\Diamond$ and $\Box$ 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

(2)#\[\begin{gather} (x\odot y)\odot z= x\odot (y\odot z)\\ x\odot y = y\odot x\\ x\odot x = x \end{gather}\]

What is axiomatised here is choice as a set of alternatives. Given a set $X$, we denote by $\mathcal PX$ 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#

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 PX$. A coalgebra morphism

\[ (X\stackrel \xi \to \mathcal PX) \stackrel f\longrightarrow (X'\stackrel {\xi'} \to \mathcal PX') \]

is a function $f:X\to X'$ satisfying

\[\mathcal Pf\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.

(3)#\[\begin{gather} \mathcal Pf\circ \xi \ \subseteq \ \xi'\circ f\\ xRy \ \Rightarrow \ f(x) R' f(y)\\ x'=f(x) \ \Rightarrow \ \forall y\in\xi(x)\,.\,\exists y'\in\xi'(x')\,.\,y'=f(x') \end{gather}\]

The following are equivalent conditions for $f$ being a backward simulation.

(4)#\[\begin{gather} \mathcal Pf\circ \xi \ \supseteq \ \xi'\circ f\\ f(x)R'y' \ \Rightarrow \ \exists y\,.\, xRy \ \& \ y'=f(y)\\ x'=f(x) \ \Rightarrow \ \forall y'\in\xi'(x')\,.\,\exists y\in\xi(x)\,.\,y'=f(x') \end{gather}\]

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.

(5)#\[\begin{gather} x\le x\odot y\\ x\ge x\odot y \end{gather}\]

Convex Powerdomain#

The functor

\[\mathcal P^\rm c:\sf Pos \to Pos\]

maps a poset $(X,\le)$ to the set of convex subsets $\mathcal PX$. The order on convex subsets is defined as follows. [3] [4]

(6)#\[\begin{align} a\le b\ \quad \textrm{ if } \quad & \forall x\in a\,.\,\exists y\in b. x\le y \quad \textrm{ and }\\ &\forall y\in b\,.\,\exists x\in a. x\le y\\ \end{align}\]

If $X$ is discrete then $\mathcal P^\rm c X$ is just $\mathcal PX$ and $\le$ is equality.

Lower Powerdomain#

The functor

\[\mathcal D:\sf Pos \to Pos\]

maps a poset $(X,\le)$ to the set of downward closed subsets (downsets) $\mathcal DX$. The order on subsets $a,b\subseteq X$ is defined as [5] [6]

(7)#\[\begin{align} a\le b\ \quad \textrm{ if } \quad & \forall x\in a\,.\,\exists y\in b. x\le y \end{align}\]

which amounts to inclusion of downsets. If $X$ is discrete then $\mathcal DX$ is $\mathcal PX$ ordered by $\subseteq$.

Upper Powerdomain#

The functor $\mathcal U:\sf Pos \to Pos$ maps a poset $(X,\le)$ to the set of upward closed subsets (upsets) $\mathcal UX$. The order on upsets is defined as [7]

(8)#\[\begin{align} a\le b\ \quad \textrm{ if } \quad & \forall y\in b\,.\,\exists x\in a. x\le y \end{align}\]

which amounts to reverse inclusion of upsets. If $X$ is discrete then $\mathcal UX$ is $\mathcal PX$ ordered by $\supseteq$.

Coalgebras#

As noted above, coalgebras $X\to\mathcal PX$ 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'\le x R y \le y'}{x'R y'}\]

$(X,R)$ is an $\mathcal D$-coalgebra iff

\[\frac{x'\ge x R y \ge y'}{x'R y'}\]

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^\rm 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 $\bf R$ on the disjoint union $X+Y$.
Because of the universal property of the coproduct, there always will be a coalgebra ${\bf R}\to T{\bf R}$ where $T$ is either $\mathcal U$ or $\mathcal D$.
$R$ is a (bi)simulation iff ${\bf R}\to T{\bf 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:\sf Set\to Set$ induces a notion of $T$-bisimulation.

What about simulations?

We first note that each functor $T:\sf Ord\to Ord$ induces a notion of $T$-(bi)simulation.[10] I write (bi)simulation here because technically this notion works much in the same way for $\sf Set$-functors and for $\sf Ord$-functors. But for $\sf Ord$-functors, it encompasses both simulations and bisimulations, depending on the functor.

A general way to introduce notions of simulation for $\sf Set$ functors is as follows. Let $T:\sf Set\to Set$ be a functor. Extend $T$ to a functor $T':\sf Ord\to Ord$.[11] Then restrict $T'$-(bi)simulation to $T$-coalgebras.

Example: Let $T=\mathcal P$. We can let $T'$ be one of $\mathcal P^\rm 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 $\Box$ and $\Diamond$ 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^\rm c 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 DX$ 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 DX=[X^\rm 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 DX\to\mathcal DX$.

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” $\Box$ and $\Diamond$. 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 PX$$

is a coalgebra. We rewrite the usual definition of the semantics of $\Box$ and $\Diamond$ in terms of the coalgebra structure $\xi$ as follows.

(9)#\[\begin{gather} \Box a = \xi^{-1}(\{b\subseteq X \mid b\subseteq a\})\\ \Diamond a = \xi^{-1}(\{b\subseteq X \mid a\cap b\not=\emptyset\}) \end{gather}\]

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

(10)#\[\begin{gather} x\in \Box a \quad \Longleftrightarrow \quad \forall y\in\xi(x)\,.\, y\in a\\ x\in \Diamond a \quad \Longleftrightarrow \quad \exists y\in\xi(x)\,.\, y\in a \end{gather}\]

We can now extend propositional logic by unary operators for $\Box$ and $\Diamond$ (and all equations they satisfy in all coalgebras). This is known as the modal logic $\bf 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 $\bf K$ is invariant under coalgebra morphisms. Every logic that contains classical propositional logic and is invariant under bisimulation is equivalent to $\bf K$ on finite coalgebras. $\bf K$ characterises elements of coalgebras up to bisimilarity on finite coalgebras. $\bf 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 PX$ and $X'\stackrel {\xi'} \to \mathcal PX'$ a relation $R\subseteq X\times X'$ is called a bisimulation if

(11)#\[\begin{align} x Rx' \ \ \textrm{ only if } \quad & \forall y\in \xi(x)\,.\,\exists y'\in\xi'(x')\,.\, x'Ry' \quad \textrm {and}\\ & \forall y'\in \xi'(x')\,.\,\exists y\in\xi(x)\,.\, x'Ry'\\ \end{align}\]

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 ${\bf K}^\Box$ and ${\bf K}^\Diamond$ (this is not standard notation) for the negation-free fragment of $\bf K$ that only contains $\Box$ (respectively $\Diamond$) formulas. It now turns out that preservation of ${\bf K}^\Box$-formulas and preservation of ${\bf K}^\Diamond$-formulas each corresponds to one direction of the definition of bisimulation.

As the Exercise on (bi)simulation above shows, ${\bf K}^\Diamond$-formulas are invariant under forward-simulation and ${\bf K}^\Box$-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 DX$ are downsets ordered according to $\ a\le b \ \Leftrightarrow\ a\subseteq b$ and the elements of $\mathcal UX$ are upsets ordered as $\ a\le b \ \Leftrightarrow\ a\supseteq b$ .

$T$	$\mathcal D$	$\mathcal U$
also known as	Hoare powerdomain	Smyth powerdomain
$\odot$	$\cup$	$\cup$
$a\le b\in TX$	$\forall x\in a\,.\,\exists y\in b\,.\, x\le y$	$\forall y\in b\,.\,\exists x\in a\,.\, x\le y$
semilattice + …	$a\le a\odot b$	$a \odot b \le a$
(bi)simulation	forward	backward
logic	$\Diamond$	$\Box$
$X\stackrel R \longrightarrow TX$	$\frac{x'\ge x\,R\,y'\ge y}{x'\,R\,y'}$	$\frac{x'\le x\,R\,y'\le y}{x'\,R\,y'}$
	angelic	demonic

Maybe the most principled way to remember that $\mathcal U$ gives $\Box$ and $\mathcal D$ gives $\Diamond$ 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.

…

\(T\)	\(\mathcal D\)	\(\mathcal U\)
also known as	Hoare powerdomain	Smyth powerdomain
\(\odot\)	\(\cup\)	\(\cup\)
\(a\le b\in TX\)	\(\forall x\in a\,.\,\exists y\in b\,.\, x\le y\)	\(\forall y\in b\,.\,\exists x\in a\,.\, x\le y\)
semilattice + …	\(a\le a\odot b\)	\(a \odot b \le a\)
(bi)simulation	forward	backward
logic	\(\Diamond\)	\(\Box\)
\(X\stackrel R \longrightarrow TX\)	\(\frac{x'\ge x\,R\,y'\ge y}{x'\,R\,y'}\)	\(\frac{x'\le x\,R\,y'\le y}{x'\,R\,y'}\)
	angelic	demonic

Powerdomains

Contents