Definition. Strictness [dt-000K]

Liam O'Connor

A function $f : X \rightarrow Y$ on pointed posets $X$ and $Y$ is strict if it preserves the bottom value, i.e. $f(\bot _X) = \bot _Y$ .

Context

Monotonic functions [dt-000H]

Liam O'Connor

If we model our semantic domains for values with pointed posets, then programs are modelled by functions between such posets. But, not all functions are suitable:

Example. The halting query [dt-000I]

Liam O'Connor

The function $H : \mathbb {B}_\bot \rightarrow \mathbb {B}_\bot$ seems to let us solve the halting problem, assuming $\bot$ represents non-termination: $H(v) \; = \; \begin {cases} F & \text {if}\ v = \bot \\ T & \text {otherwise} \end {cases}$

It stands to reason that the amount of information we get out of our functions should grow as we increase the amount of information we put into them. Such functions are called monotonic with respect to our information ordering.

Definition. Monotonicity [dt-000J]

Liam O'Connor

A function $f : X \rightarrow Y$ between posets $X$ and $Y$ is monotone (or monotonic) if, for all $x, y \in X$ : $x \sqsubseteq y\; \text {implies}\; f(x) \sqsubseteq f(y)$

Definition. Strictness [dt-000K]

Liam O'Connor

A function $f : X \rightarrow Y$ on pointed posets $X$ and $Y$ is strict if it preserves the bottom value, i.e. $f(\bot _X) = \bot _Y$ .

Thesis.

Liam O'Connor

Computable functions are monotonic (observe that $H$ is not).

Exercise. [dt-000N]

Liam O'Connor

Consider the functions $\mathbb {B}_\bot \rightarrow \mathbb {B}_\bot$ . Which ones are monotonic? There are a total of 27 such functions but only three significant classes.

Solution.

Liam O'Connor

The three classes are the nine strict functions (which map $\bot$ to $\bot$ ), which are all monotonic, the two non-strict constant functions (which ignore their input and return $\mathit {T}$ and $\mathit {F}$ respectively), which are also monotonic, and the 16 non-monotonic functions.

Exercise. [dt-000O]

Liam O'Connor

Let $\mathbf {K}_K$ denote the chain of values $x_1, x_2, x_3, \dots , x_K$ where $a \leq b$ implies $x_a \sqsubseteq x_b$ . There is one monotonic function $\mathbf {K}_1 \rightarrow \mathbf {K}_1$ :

And there are three monotonic functions $\mathbf {K}_2 \rightarrow \mathbf {K}_2$ :

Write down the monotonic functions $\mathbf {K}_3 \rightarrow \mathbf {K}_3$ .

Solution.

Liam O'Connor

When drawn as a diagram like the above, the monotonic functions are all those whose lines do not cross.

Write a simple recursive program to calculate the number of monotonic functions $\mathbf {K}_n \rightarrow \mathbf {K}_m$ .

Solution.

Liam O'Connor

In Haskell:

monotonics :: Int -> Int -> Int
monotonics n 1 = 1
monotonics n m = sum [monotonics (n-x) (m-1) | x <- [0..n]]

Backlinks

Exercise. [dt-000N]

Liam O'Connor

Consider the functions $\mathbb {B}_\bot \rightarrow \mathbb {B}_\bot$ . Which ones are monotonic? There are a total of 27 such functions but only three significant classes.

Solution.

Liam O'Connor

The three classes are the nine strict functions (which map $\bot$ to $\bot$ ), which are all monotonic, the two non-strict constant functions (which ignore their input and return $\mathit {T}$ and $\mathit {F}$ respectively), which are also monotonic, and the 16 non-monotonic functions.

Corollary. Derived products of retraction pairs [dt-0057]

It follows from the definition of retraction pairs that, for a pair $\xtofrom [g]{f}$ :

$f$ and $g$ are strict, i.e. $f(\bot ) = \bot$ and $g(\bot ) = \bot$ .
$g$ is uniquely determined by $f$ and vice-versa, so if another retraction pair $\xtofrom [g']{f}$ exists, then $g = g'$ . To see why, remember that $f$ and $g$ must be continuous and therefore monotonic.
$A$ is isomorphic to the range of $f$ , i.e. $A \simeq \{ f(x) \mid x \in A\} \subseteq B$ .

Theorem. Isomorphisms with lifting [dt-003L]

Liam O'Connor

With the lifting operator, we can relate the lazy constructions like product and sum with strict constructions like smash product and sum via isomorphism:

$A\twoheadrightarrow B \simeq A_\bot \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B$
$A + B \simeq A_\bot \oplus B_\bot$
$(A \times B)_\bot \simeq A_\bot \otimes B_\bot$

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.

Strict Constructions [dt-003E]

Liam O'Connor

When giving a semantics to a call-by-name (or "lazy") language, the constructions $\twoheadrightarrow$ for functions, $\times$ for products and $+$ for sums are exactly what we want. To properly capture call-by-value (or "strict") languages, however, we also need strict versions of these constructions.

Construction. The cpo of strict continuous functions [dt-003F]

Liam O'Connor

A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B = \{ f \in A \twoheadrightarrow B \mid f(\bot ) = \bot \}

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-002L].

Construction. Smash products of cpos [dt-003G]

Liam O'Connor

A \otimes B = \{ (a,b) \in A \times B \mid a \neq \bot \land b \neq \bot \} \cup \{ \bot _{A\otimes B}\}

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-0021]. This operator is called a smash product because the two $\bot$ values from $A$ and $B$ are "smashed" into one $\bot$ value.

Construction. Smash sums of cpos [dt-003H]

Liam O'Connor

A \oplus B = \{ (t,x) \in A + B \mid x \neq \bot \} \cup \{ \bot _{A\oplus B} \}

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-0031]. This operator is called a smash sum because the two $\bot$ values from $A$ and $B$ are "smashed" into one $\bot$ value.

Theorem. Isomorphisms with strict constructions [dt-003J]

Liam O'Connor

The strict cpo constructions satisfy all the usual isomorphisms, including:

$(A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B) \times (A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)\;\; \simeq \;\; A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } (B\otimes C)$
$(A \otimes B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C) \;\; \simeq \;\; A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } (B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)$
$(A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C) \times (B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)\;\; \simeq \;\; (A\oplus B) \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C$

Definition. The category $\mathbf {Cpo_\bot }$ [dt-003I]

Liam O'Connor

The category $\mathbf {Cpo_\bot }$ is the category where the objects are cpos, the morphisms are strict continuous functions between these cpos, and composition and identity are as in $\mathbf {Cpo}$ .

Upshot.

Liam O'Connor

\mathbf {Cpo_\bot }

has products, exponentials, and sums (as it doesn't suffer from the problem that

\textbf {Cpo}

does).

Definition. The lifting operator for cpos [dt-003K]

Liam O'Connor

The lifting operator $(\cdot )_\bot$ adds a new $\bot$ value to a cpo. That is, for a cpo $X$ : $X_\bot = X \cup \{\bot \} \quad \text {(where $\bot \notin X$)}$ For all $x \in X$ (including $\bot _X$ ), our new bottom value $\bot \sqsubseteq x$ .

Theorem. Isomorphisms with lifting [dt-003L]

Liam O'Connor

With the lifting operator, we can relate the lazy constructions like product and sum with strict constructions like smash product and sum via isomorphism:

$A\twoheadrightarrow B \simeq A_\bot \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B$
$A + B \simeq A_\bot \oplus B_\bot$
$(A \times B)_\bot \simeq A_\bot \otimes B_\bot$

Construction. The cpo of strict continuous functions [dt-003F]

Liam O'Connor

A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B = \{ f \in A \twoheadrightarrow B \mid f(\bot ) = \bot \}

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-002L].

Related

The bottom value [dt-000A]

Liam O'Connor

Following Scott, we introduce a special bottom value $\bot$ to our semantic domains. $\bot \ \text {represents}\ \begin {cases}\text {an undefined value;}\\\text {an error value;}\\\text {a \emph {non-terminating} computation.} \end {cases}$