Getting closure [dt-005Y]
DefinitionBasis [dt-004A]
TheoremCompact basis for algebraic cpos [dt-004B]
If X is a basis for A, then A is algebraic and \mathsf {K}(A) = X.
Proof.
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.
TheoremClosure of algebraic cpos under product [dt-004C]
If D and E are algebraic cpos, then so is their product construction D \times E.
Proof.
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.
AsideScott's original solution: using complete lattices [dt-004D]
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.
DefinitionConsistent completeness [dt-004E]
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.
ExampleConsistent completeness vs directed completeness [dt-004F]
DefinitionScott domain [dt-004G]

A cpo D is a Scott domain iff:
- D is \omega -algebraic,
- D is consistent complete,
Remark [dt-004H]
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.
TheoremClosure of Scott domains [dt-004I]
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.
Our semantic domains are Scott domains.