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.