Example. Consistent completeness vs directed completeness [dt-004F]

Liam O'Connor


consistent complete	not consistent complete
not directed complete	directed complete

Context

Getting closure [dt-005Y]

Liam O'Connor

Definition. Basis [dt-004A]

Liam O'Connor

A set of compact elements $X \subseteq \mathsf {K}(A)$ is a basis for a cpo $A$ iff for all $x\in A$ , $x= \bigsqcup \{a \in X \mid a \sqsubseteq x\}$ .

Theorem. Compact basis for algebraic cpos [dt-004B]

Liam O'Connor

If $X$ is a basis for $A$ , then $A$ is algebraic and $\mathsf {K}(A) = X$ .

Proof.

Liam O'Connor

If $a \in \mathsf {K}(A)$ , then $\bigsqcup M = a$ where $M = \{ x \in X \mid x \sqsubseteq a \}$ , as $X$ is a basis. Since $a$ is compact, $a \sqsubseteq b$ for some $b \in M$ . But since $a$ is the lub of $M$ , $b \sqsubseteq a$ as well. By antisymmetry $a = b$ , hence $a \in X$ . Thus $\mathsf {K}(A) \subseteq X$ , so $\mathsf {K}(A) = X$ and $A$ is algebraic.

Theorem. Closure of algebraic cpos under product [dt-004C]

Liam O'Connor

If $D$ and $E$ are algebraic cpos, then so is their product construction $D \times E$ .

Proof.

Liam O'Connor

In the following proof, we show that $\mathsf {K}(D) \times \mathsf {K}(E)$ is a basis for the product $D \times E$ and thereby show via Theorem [dt-004B] that $D \times E$ is algebraic if $D$ and $E$ are.

$\mathsf {K}(D) \times \mathsf {K}(E) \subseteq \mathsf {K}(D \times E)$ : Let $(x,y) \in \mathsf {K}(D) \times \mathsf {K}(E)$ . To show that $(x,y)$ is compact, let us assume that $(x,y) \in \bigsqcup X$ where $X \subseteq D \times E$ is directed. We must show that there exists some element $e$ of $X$ such that our $(x,y) \sqsubseteq e$ . As $(x,y) \in \bigsqcup X$ , by the definition of lub on products we can conclude that: $\begin {array}{lcl} x & \sqsubseteq & \bigsqcup \pi _0[ X] \\ y & \sqsubseteq & \bigsqcup \pi _1[X] \end {array}$ Here we use the notation $f[X]$ to indicate the image of a function on a set, i.e. $\{ f(v) \mid v \in X \}$ .

Since $x$ and $y$ are both compact, there must exist $x' \in \pi _0[ X]$ and $y' \in \pi _1[ X]$ such that $x \sqsubseteq x'$ and $y \sqsubseteq y'$ . While it does not follow that $(x', y') \in X$ , we know that there must exist a pair $(a,b) \in X$ such that $x' \sqsubseteq a$ and $y' \sqsubseteq b$ as $X$ is directed. Hence $(a,b)$ can be our element $e \in X$ that is approximated by $(x,y)$ , i.e. $(x,y) \sqsubseteq (a,b)$ .
$\mathop {\downarrow }(x,y)$ is directed for all $(x,y) \in D \times E$ : $\begin {array}{lcl} \mathop {\downarrow }(x,y) &= & \{ (a,b) \in \mathsf {K}(D) \times \mathsf {K}(E) \mid (a,b) \sqsubseteq (x,y) \} \\ & = & \{ a \in \mathsf {K}(D) \mid a \sqsubseteq x \} \times \{ b \in \mathsf {K}(E) \mid b \sqsubseteq y \}\\ & = & \mathop {\downarrow }(x) \times \mathop {\downarrow }(y) \end {array}$ Because $D$ and $E$ are algebraic, $\mathop {\downarrow }(x)$ and $\mathop {\downarrow }(y)$ are directed. As directedness is closed under product, $\mathop {\downarrow }(x,y)$ is directed too.
$(x,y) = \bigsqcup \mathop {\downarrow }(x,y)$ Starting from the right hand side: $\begin {array}{lclr} \bigsqcup \mathop {\downarrow }(x,y) & = & \bigsqcup (\mathop {\downarrow }(x) \times \mathop {\downarrow }(y)) & \text {(part 2)}\\ & = & (\bigsqcup (\mathop {\downarrow }(x), \bigsqcup \mathop {\downarrow }(y))) & \text {(lub on products)}\\ & = & (x,y) & \text {($D$, $E$ are {algebraic})} \end {array}$

Problem.

Liam O'Connor

\omega

-algebraic cpos are closed under all of our constructions (products and sums, including strict versions of these) except functions

\twoheadrightarrow

and strict functions

\mathbin {\circ \hspace{-0.4em}\twoheadrightarrow }

!

Aside. Scott's original solution: using complete lattices [dt-004D]

Liam O'Connor

The lack of closure of algebraicity under the (continuous) function arrow, strict or non-strict, is not satisfying as it means that our semantic domains are not guaranteed to be algebraic even if they are composed from algebraic cpos. Instead, we must replace algebraic cpos with something stronger still.

Scott's original solution to this lack of closure was to use a complete lattice instead of cpos, i.e. requiring lubs for all subsets, not just directed ones. This solves the problem with $\twoheadrightarrow$ but introduces new problems:

Complete lattices need a top element $\top$ , but adding a fictitious top (representing inconsistent information) to cpos like $\mathbb {B}_\bot$ is strange.
Extending the functions that capture our primitive semantic operations to complete lattices can spoil nice algebraic properties. Consider these two possible implementations of $\mathsf {ite}$ , the function for the semantics of an $\mathsf {if}$ expression: $\mathsf {ite}(\top ,x,y) = x \sqcup y\quad \quad \quad \quad \quad \mathsf {ite}(\top ,x,y) = \top$ Either of these solutions results in the failure of useful and expected laws for $\mathsf {if}$ expressions. For example, the left definition above results in the failure of the common equation to eliminate unreachable cases: $\mathsf {ite}(b, \mathsf {ite}(b,x,y),z) = \mathsf {ite}(b,x,z)$ And the second definition above results in the failure of this equation that removes redundant checks: $\mathsf {ite}(b,x,x) = x$
The powerdomain construction does not generalise to complete lattices, so semantics for non-deterministic programs are difficult in this setting.

Definition. Consistent completeness [dt-004E]

Liam O'Connor

A poset $A$ is consistent complete (or bounded complete) iff $\bigsqcup X$ exists for all consistent $X \subseteq A$ . That is, any set with an upper bound (a consistent set) has a least upper bound.

Example. Consistent completeness vs directed completeness [dt-004F]

Liam O'Connor


consistent complete	not consistent complete
not directed complete	directed complete

Definition. Scott domain [dt-004G]

Liam O'Connor

A cpo $D$ is a Scott domain iff:

$D$ is $\omega$ -algebraic,
$D$ is consistent complete,

In other words, Scott domains can be summed up by the acronym:

Remark. [dt-004H]

Liam O'Connor

The second requirement in Definition [dt-004G] can, in light of the first, be expressed equivalently as: $x \sqcup y$ exists for all consistent $x,y \in D$ . This is useful when needing to show that a given cpo is a Scott domain.

Theorem. Closure of Scott domains [dt-004I]

Liam O'Connor

Scott domains are closed under all our cpo constructions, including sums $+$ , products $\times$ , continuous functions $\twoheadrightarrow$ , smash sums $\oplus$ , smash products $\otimes$ and strict functions $\mathbin {\circ \hspace{-0.4em}\twoheadrightarrow }$ .

Thesis.

Liam O'Connor

Our semantic domains are Scott domains.

Related

Definition. Complete partial order [dt-001D]

Liam O'Connor

A complete partial order or cpo (more specifically a directed complete partial order or dcpo) is a poset where lubs exist for the empty set and for all directed subsets. That is, a cpo is a poset $A$ such that:

$A$ has a bottom element $\bot \in A$ , that is the lub of the empty set, and
$\bigsqcup X$ exists for all directed $X \subseteq A$ .

Definition. Consistent completeness [dt-004E]

Liam O'Connor

A poset $A$ is consistent complete (or bounded complete) iff $\bigsqcup X$ exists for all consistent $X \subseteq A$ . That is, any set with an upper bound (a consistent set) has a least upper bound.