Definition. Down-closure [dt-0047]

Liam O'Connor

Given a poset $Y$ , a set $X \subseteq Y$ is down-closed iff, for all $x \in X$ , any $y \sqsubseteq x$ is in $X$ .

Context

Algebraicity and ideals [dt-005X]

Liam O'Connor

Definition. Algebraicity [dt-0041]

Liam O'Connor

A cpo is algebraic iff every element is the lub of its compact approximations. That is, a cpo $D$ is algebraic iff for all $x \in D$ ,

$\mathop {\downarrow }(x) = \{ y \in \mathsf {K}(D) \mid y \sqsubseteq x \}$ is directed;
$x = \bigsqcup \mathop {\downarrow }(x)$

Note: It's common in semantics to consider only algebraic cpos with a countable set of compact elements. Such cpos are called $\omega$ -algebraic.

Aside: Plotkin provides an equivalent definition of $\omega$ -algebraic cpos in which directed sets are replaced with $\omega$ -chains throughout. Hutton claims this is less appealing, as the definition speaks of an $\omega$ -chain of compact approximations, rather than the directed set of such.

Example. $\omega$ -algebraic cpos [dt-0042]

Liam O'Connor

Many standard examples of cpos are $\omega$ -algebraic cpos: finite cpos, subsets $\mathcal {P}(X)$ of a set $X$ , partial functions $\mathbb {N} \nrightarrow \mathbb {N}$ and submonoids of a monoid. In general, any cpo of subalgebras (e.g. subgroups of a group, subrings of a ring etc.) is $\omega$ -algebraic. This is the origin of the terminology.

Counterexample. Non-algebraic cpo [dt-0043]

Liam O'Connor

In the cpo on the right (seen also in § [dt-0040]), the element $x$ is not the lub of its compact approximations. The only compact element that approximates $x$ is $\bot$ , and the least upper bound of the set $\{\bot \}$ is just $\bot$ , not $x$ . That is: $\mathop {\downarrow }(x) = \{\bot \}$ but: $x \neq \bigsqcup \{\bot \}$

Theorem. Nothing suddenly invented at infinity [dt-0045]

Liam O'Connor

Let $D$ and $E$ be algebraic cpos. Then a function $f : D \rightarrow E$ is continuous iff, for all $x \in D$ : $f(x) = \bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \}$ In other words, in an algebraic cpo, continuous functions are completely defined by their behaviour for compact arguments.

This makes precise our earlier slogan in Definition [dt-001J], that continuous functions don't suddenly behave differently for infinite (i.e. non-compact) elements.

Proof.

Liam O'Connor

First, assuming

f

is continuous, we show that

f(x) = \bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \}

:

\begin {array}{lclr} f(x) & = & f(\bigsqcup \mathop {\downarrow }(x)) & \text {($D$ is {algebraic})}\\ &=&\bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \} & \text {($f$ is continuous)}\\ \end {array}

It remains to show that if

f(x) = \bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \}

, then

f

is continuous. Using the alternative definition, we shall first show that

f

is monotone. Let

a \sqsubseteq b

for

a,b \in D

. Then

\mathop {\downarrow }(a) \subseteq \mathop {\downarrow }(b)

and thus

\{f(x) \mid x \in \mathop {\downarrow }(a)\} \subseteq \{f(x) \mid x \in \mathop {\downarrow }(b)\}

, therefore:

\begin {array}{lclr} f(a) &=&\bigsqcup \ \{ f(x) \mid x \in \mathop {\downarrow }(a) \} & \text {(assumption)}\\ & \sqsubseteq &\bigsqcup \ \{ f(x) \mid x \in \mathop {\downarrow }(b) \} & \text {(from above)}\\ & = & f(b) & \text {(assumption)}\\ \end {array}

Next, let

X \subseteq D

\begin {array}{lclr} f(\bigsqcup X) &=&\bigsqcup \ \{ f(x) \mid x \in \mathop {\downarrow }(\bigsqcup X) \} & \text {(assumption)}\\ &=&\bigsqcup \ \{ f(x) \mid x \in \mathsf {K}(X) \land x \sqsubseteq \bigsqcup X \} & \text {(defn.~of $\downarrow $)}\\ &=&\bigsqcup \ \{ f(x) \mid \exists y \in X.\ x \in \mathsf {K}(X) \land x \sqsubseteq y \} & \text {(compactness)}\\ &=&\bigsqcup \ \{ f(x) \mid \exists y \in X.\ x \in \mathop {\downarrow }(y)\} & \text {(defn.~of $\downarrow $)}\\ &=&\bigsqcup \ \{ f(x) \mid x \in X\} & \text {(algebraicity)}\\ \end {array}

Exercise. [dt-0044]

Liam O'Connor

Let $f : D \twoheadrightarrow E$ be a continuous function between algebraic cpos. Define: $G_f = \{ (a,b) \in \mathsf {K}(D) \times \mathsf {K}(E) \mid b \sqsubseteq f(a) \}$ Then for all $x \in D$ , prove that: $f(x) = \bigsqcup \ \{ b \mid (a,b) \in G_f \land a \sqsubseteq x \}$

Solution.

Liam O'Connor

\begin {array}{lclr} f(x) & = & f(\bigsqcup \mathop {\downarrow }(x)) & \text {($D$ is {algebraic})}\\ &=&\bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \} & \text {($f$ is continuous)}\\ &=&\bigsqcup \ \left \{ \bigsqcup \mathop {\downarrow }(f(a)) \mid a \in \mathop {\downarrow }(x) \right \} & \text {($E$ is {algebraic})}\\ &=&\bigsqcup \ \{ b \in \mathsf {K}(E) \mid b \sqsubseteq f(a) \land a \in \mathop {\downarrow }(x)\} & \text {(lubs and defn of $\downarrow $)}\\ &=&\bigsqcup \ \{ b \mid (a,b) \in G_f \land a \sqsubseteq x \}&\text {(defn of $G_f$)} \end {array}

This is powerful. For example, the continuous function $f : \mathcal {P}(\mathbb {N}) \twoheadrightarrow \mathcal {P}(\mathbb {N})$ on an uncountable cpo $\mathcal {P}(\mathbb {N})$ is completely determined by the countable relation $G_f$ .

Definition. Down-closure [dt-0047]

Liam O'Connor

Given a poset $Y$ , a set $X \subseteq Y$ is down-closed iff, for all $x \in X$ , any $y \sqsubseteq x$ is in $X$ .

Definition. Ideal [dt-0048]

Liam O'Connor

A set is ideal iff it is both down-closed and directed.

Definition. Ideal completion [dt-0046]

Liam O'Connor

The ideal completion of a set $A$ , written sometimes as $\mathsf {Id}(A)$ , is the set of all ideal subsets of $A$ , i.e.: $\mathsf {Id}(A) = \{ X \subseteq A \mid X\ \text {is ideal}\}$

Theorem. Representation theorem for algebraic cpos [dt-0049]

Liam O'Connor

Every algebraic cpo $D$ is isomorphic to the ideal completion of its compact elements, ordered by subset inclusion. That is, $\mathsf {Id}(K(D))$ is an algebraic cpo such that $D \simeq \mathsf {Id}(K(D))$ .

Backlinks

Example. Hoare powerdomain of $\mathbb {N}_\bot$ [dt-0062]

Liam O'Connor

Let us find the Hoare powerdomain of $\mathbb {N}_\bot$ . Note that $\mathbb {N}_\bot$ is a flat domain so all elements are compact, i.e. $\mathsf {K}(\mathbb {N}_\bot ) = \mathbb {N}_\bot$ . Let us find examine the $\preceq _H$ -ideal subsets of $\mathcal {P}_f^\ast (\mathbb {N}_\bot )$ . If $v$ and $u$ both contain $\bot$ , then $v \preceq _H u$ iff $v \subseteq u$ . As ideal subsets are downwards closed, we can identify an ideal $I \in \mathsf {Id}({\mathcal {P}_f^\ast (\mathbb {N}_\bot )})$ with its union $\bigcup I$ . The ideals of $\mathcal {P}^\ast _f(\mathbb {N}_\bot )$ are then isomorphic to domain $\mathcal {P}(\mathbb {N})$ of all subsets of $\mathbb {N}$ under subset inclusion.

Definition. Ideal [dt-0048]

Liam O'Connor

A set is ideal iff it is both down-closed and directed.

Example. Smyth powerdomain of $\mathbb {N}_\bot$ [dt-0065]

Liam O'Connor

Firstly note that, as ideals are downwards-closed, any $\preceq _S$ -ideal subsets of $\mathcal {P}^\ast _f(\mathbb {N}_\bot )$ will contain all finite subsets of $\mathbb {N}_\bot$ that contain $\bot$ . Let us call those sets trivial. So, a set in $\mathcal {P}^\ast _f(\mathbb {N}_\bot )$ is non-trivial if it does not contain $\bot$ and an ideal subset of $\mathcal {P}^\ast _f(\mathbb {N}_\bot )$ is non-trivial if it contains a non-trivial set. Observe that for non-trivial sets $X$ and $Y$ , $X \preceq _S Y$ iff $X \supseteq Y$ . Thus, we can identify an ideal $I \in \mathsf {Id}({\mathcal {P}_f^\ast (\mathbb {N}_\bot )})$ with the down-closure of the intersection of its non-trivial elements. The smaller this set is, the larger the ideal $I$ . Hence, and confusingly, the non-trivial ideals in the powerdomain (ordered by subset inclusion) correspond to finite subsets of $\mathbb {N}$ ordered by superset inclusion. As all trivial sets are identified, we just need to throw in the unique trivial ideal, and we can see that the Smyth powerdomain of $\mathbb {N}$ is isomorphic to the domain of sets $\{ \mathbb {N} \} \cup \mathcal {P}_f^\ast (\mathbb {N})$ ordered by subset inclusion.

The Hoare powerdomain [dt-0061]

Liam O'Connor

We write $\mathcal {P}_f^\ast (S)$ to denote finite non-empty subsets of $S$ . Let $X, Y \in \mathcal {P}_f^\ast (\mathsf {K}(A))$ be finite, non-empty sets of compact elements of a Scott domain $A$ . The Hoare powerdomain construction is based on the following ordering: $X \preceq _H Y\quad \text {iff}\quad (\forall x \in X.\ \exists y \in Y.\ x \sqsubseteq _A y)$ The intuition behind this is that "Anything $X$ can do, $Y$ can do better". This ordering has some desirable properties: The least element is $\{\bot \}$ , as we might expect. It also satisfies the equation $X \preceq _H X \cup Y$ , which intuitively means that a non-deterministic choice is considered to have more information than any of its components. When specialised to the case where $A$ is a flat domain like $\Sigma _\bot$ , it simplifies to: $X \preceq _H Y\quad \text {iff}\quad X \setminus \{\bot \} \subseteq Y$ This is, however, not a proper order, but a preorder, as it fails antisymmetry. Even in the flat domain case, $\{ x, \bot \} \preceq _H \{x \}$ and $\{ x \} \preceq _H \{x, \bot \}$ but they are not equal. However, any preorder does induce an equivalence relation, where $X \approx _H Y$ iff $X \preceq _H Y$ and $Y \preceq _H X$ . Furthermore, if we take the ideal completion of $\mathcal {P}_f^\ast (K(A))$ with respect to the preorder $\preceq _H$ (i.e., the set of all $\preceq _H$ -downwards-closed directed subsets of $\mathcal {P}_f^\ast (\mathsf {K}(A))$ ), we can order them by inclusion to obtain an algebraic domain with compact elements which correspond to equivalence classes of elements under $\approx _H$ . We have a lub operation for these ideals: $A \sqcup _H B = \{ X \cup Y \mid X \in A \land Y \in B \}$

Example. Hoare powerdomain of $\mathbb {N}_\bot$ [dt-0062]

Liam O'Connor

Let us find the Hoare powerdomain of $\mathbb {N}_\bot$ . Note that $\mathbb {N}_\bot$ is a flat domain so all elements are compact, i.e. $\mathsf {K}(\mathbb {N}_\bot ) = \mathbb {N}_\bot$ . Let us find examine the $\preceq _H$ -ideal subsets of $\mathcal {P}_f^\ast (\mathbb {N}_\bot )$ . If $v$ and $u$ both contain $\bot$ , then $v \preceq _H u$ iff $v \subseteq u$ . As ideal subsets are downwards closed, we can identify an ideal $I \in \mathsf {Id}({\mathcal {P}_f^\ast (\mathbb {N}_\bot )})$ with its union $\bigcup I$ . The ideals of $\mathcal {P}^\ast _f(\mathbb {N}_\bot )$ are then isomorphic to domain $\mathcal {P}(\mathbb {N})$ of all subsets of $\mathbb {N}$ under subset inclusion.

Remark. Angelic nondeterminism [dt-0063]

Liam O'Connor

Consider the following three programs:

$x := 1$
$\textsf {while}\ \textsf {true}\ \textsf {do}\ \textsf {skip}$
$\textsf {while}\ \textsf {true}\ \textsf {do}\ \textsf {skip}\ \textsf {od} + x := 1$

Given a state

\sigma

, let

\sigma ' = \sigma (x \mapsto 1)

. Then, the possible results of these programs are

\{ \sigma ' \}

,

\{ \bot \}

, and

\{\sigma ', \bot \}

respectively. Because the Hoare construction identifies

\approx _H

-equivalent sets, the Hoare powerdomain semantics will consider programs 1 and 3 to be the same. That is, the non-determinism is angelic. The bad outcome (

\bot

) is only said to happen if it is inevitable.

Related

Definition. Poset [dm-0004]

Liam O'Connor

A partially ordered set, or poset for short, is a pair $(X, \sqsubseteq )$ of a set $X$ equipped with a partial order $(\sqsubseteq ) \subseteq X \times X$ .

Sometimes, when the ordering is arbitrary or clear from context, the set $X$ itself may be referred to as a poset.