Using notation similar to Backus-Naur Form (BNF): \begin {array}{lcl} \mathcal {E} & \Coloneqq & n \mid x \mid \mathcal {E}_1 + \mathcal {E}_2 \mid \mathcal {E}_1 - \mathcal {E}_2\\ \mathcal {B} & \Coloneqq & \mathsf {false} \mid \mathsf {true} \mid \neg \mathcal {B} \mid \mathcal {E}_1 = \mathcal {E}_2\\ \mathcal {C} & \Coloneqq & \mathsf {skip} \mid x := \mathcal {E} \mid \mathcal {C}_1 ; \mathcal {C}_2 \mid \mathsf {if}\ \mathcal {B}\ \mathsf {then}\ \mathcal {C}_1\ \mathsf {else}\ \mathcal {C}_2 \mid \mathsf {while}\ \mathcal {B}\ \mathsf {do}\ \mathcal {C}\ \mathsf {od}\\ x & \in & \mathcal {V}\; \textit {(variables)}\\ n & \in & \mathbb {N} \end {array}

A monad on the category \textbf {C} consists of an endofunctor \mathcal {M} : \textbf {C} \rightarrow \textbf {C} and two operations (natural transformations) for all \mathbf {C}-objects X: \mu _X : \mathcal {M}(\mathcal {M}(X)) \rightarrow \mathcal {M}(X) and \eta _X : X \rightarrow \mathcal {M}(X), such that the following diagrams commute:

1. \mu _X \circ \mathcal {M}(\mu _X) = \mu _X \circ \mu _{\mathcal {M}(X)}
2. \mu _X \circ \mathcal {M}(\eta _X) = \mu _X \circ \eta _{\mathcal {M}(X)} = \mathsf {id}_{\mathcal {M}(X)}

The flat domain lifting operation (\cdot )_\bot forms a monad, where the endofunctor \mathcal {M}(X) = X_\bot , the operation \mu _X : (X_\bot )_\bot \rightarrow X_\bot collapses the two \bot values, and \eta _X : X \rightarrow X_\bot is simply \eta _X(x) = x.

For a monad (\mathcal {M}, \mu , \eta ) over the category \mathbf {C}, the Kleisli category has the same objects as \mathbf {C}, but the morphisms A \xrightarrow {h} B are those morphisms h of \mathbf {C} that have the form A \xrightarrow {h} \mathcal {M}(B). Composition is defined as follows, for morphisms A \xrightarrow {f} \mathcal {M}(B) and B \xrightarrow {g} \mathcal {M}(C): g \circ _K f = \mu _C \circ \mathcal {M}(g) \circ f Identity morphisms for this category are just \eta .

We define our semantics generically in terms of a monad (\mathcal {M},\mu ,\eta ), using the Kleisli composition operator for \mathcal {M}: \begin {array}{l} \mathsf {ite} : (\Sigma \rightarrow \mathbb {B}) \times (\Sigma \rightarrow \mathcal {M}(\Sigma )) \times (\Sigma \rightarrow \mathcal {M}(\Sigma )) \rightarrow (\Sigma \rightarrow \mathcal {M}(\Sigma ))\\ \mathsf {ite}(b,t,e)(\sigma ) = \begin {cases}t(\sigma ) & \text {if}\ b(\sigma ) = T \\ e(\sigma ) & \text {otherwise} \end {cases} \end {array} \begin {array}{lcl} \llbracket \cdot \rrbracket _\mathcal {C} : \mathcal {C} \rightarrow \Sigma \rightarrow \mathcal {M}(\Sigma )\\[0.4em] \llbracket \mathsf {skip} \rrbracket _\mathcal {C} & = & \eta _\Sigma \\ \llbracket x := e \rrbracket _\mathcal {C} & = & \boldsymbol {\lambda } \sigma .\ \eta _\Sigma (\sigma \left (x \mapsto \llbracket e \rrbracket _\mathcal {E}\right )) \\ \llbracket c_1 ; c_2 \rrbracket _\mathcal {C} & = & \llbracket c_2 \rrbracket _\mathcal {C} \circ _K \llbracket c_1 \rrbracket _\mathcal {C} \\[0.3em] \llbracket \textsf {if}\ b\ \textsf {then}\ c_1\ \textsf {else}\ c_2 \rrbracket _\mathcal {C} & = & \mathsf {ite}(\llbracket b \rrbracket _\mathcal {B},\llbracket c_1 \rrbracket _\mathcal {C},\llbracket c_2 \rrbracket _\mathcal {C})\\ \llbracket \textsf {while}\ b\ \textsf {do}\ c\ \textsf {od} \rrbracket _\mathcal {C} & = & \mathbf {\mathbf {fix}}(\boldsymbol {\lambda } f.\ \mathsf {ite}(\llbracket b \rrbracket _\mathcal {B}, f \circ _K \llbracket c \rrbracket _\mathcal {C}, \eta _\Sigma ) ) \end {array}

Instantiating our monadic semantics where the monad \mathcal {M} is flat domain lifting, we recover our original semantics of \mathcal {C}.

Let us instantiate our monadic semantics with the monad \mathcal {M}(X) = X_\bot \oplus \mathbf {1}, where the added value (from \mathbf {1}) is called \mathsf {fail}. The operation \mu _X : (X_\bot \oplus \mathbf {1})_\bot \oplus \mathbf {1} \rightarrow X_\bot \oplus \mathbf {1} collapses the two possible \bot values to \bot and the two possible \mathsf {fail} values to \mathsf {fail}, and the operation \eta _X : X \rightarrow X_\bot \oplus \mathbf {1} is the straightforward injection.

Then we may extend our language with lightweight exception constructs: \mathcal {C} ::= \dots \mid \mathsf {throw} \mid \mathsf {try}\ \mathcal {C}_1\ \mathsf {catch}\ \mathcal {C}_2 and define their semantics, leaving our existing semantics unchanged: \begin {array}{lcl} \llbracket \mathsf {throw} \rrbracket \ \sigma &=& \mathsf {fail} \\ \llbracket \mathsf {try}\ c_1\ \mathsf {catch}\ c_2 \rrbracket \ \sigma &=& \begin {cases} \llbracket c_2 \rrbracket \ \sigma & \text {if}\ \llbracket c_1 \rrbracket \ \sigma = \mathsf {fail} \\ \llbracket c_1 \rrbracket \ \sigma & \text {otherwise}\end {cases} \end {array}

When modelling programming languages we sometimes require a way to be imprecise about some aspects of a program — usually, this takes the form of non-determinism. Non-determinism can be hard for beginners to grasp, but it typically has to be employed when modelling real programs. For example, suppose we had a greeting program that differed depending on the physical location of the computer: \begin {array}{l} \textsf {\textbf {if}}\ \mathit {currentLocation}() = \text {Korea}\ \textsf {\textbf {then}} \\ \quad \textsf {\textbf {say}}\ \text {``안녕하세요''} \\ \textsf {\textbf {else}} \\ \quad \textsf {\textbf {say}}\ \text {``Hello!''}\\ \textsf {\textbf {fi}} \end {array} If we wanted to mathematically model the behaviour of this program, it would be frightfully inconvenient to include the geography of Earth and the computer's physical location in our model. That's where non-determinism comes in. If we abstract away from the geographical details, and instead regard the program as choosing between the two options based on some unspecified criteria, then we can get away with modelling less, at the cost of some detail: \begin {array}{l} \textsf {\textbf {if}}\ \mathit {???}\ \textsf {\textbf {then}} \\ \quad \textsf {\textbf {say}}\ \text {``안녕하세요''} \\ \textsf {\textbf {else}} \\ \quad \textsf {\textbf {say}}\ \text {``Hello!''}\\ \textsf {\textbf {fi}} \end {array} Such underspecified conditionals are usually called non-deterministic choice, where our conditional \textsf {\textbf {if}}\ \mathit {???}\ \textsf {\textbf {then}}\ P\ \textsf {\textbf {else}}\ Q\ \textsf {\textbf {fi}} is written simply as P + Q.

While we tend to view our physical machines as deterministic automata, the state upon which each decision is deterministically made includes a number of external things which are tedious to model mathematically. We can also use non-determinism to ignore details that we don't care about for our particular domain — a common example is memory allocation, where it is very convenient (for some programs) to think of memory as infinite, and allocation as an operation that can potentially fail, without specifying exactly when and how this failure can occur. This is normally modelled as a choice between successful allocation and a failure state.

Our initial semantics for \mathcal {C} (without loops) was functions on states \Sigma \rightarrow \Sigma . When adding loops, we used a cpo \Sigma \twoheadrightarrow \Sigma _\bot for our semantic domain. Since non-deterministic programs can have more than one outcome, a natural choice of semantic domain would be \Sigma \twoheadrightarrow \mathcal {P}(\Sigma _\bot ) \setminus \emptyset , i.e., functions from an initial state to a non-empty set of possible outcomes.

We can provide \eta and \mu operations for our proposed monad for non-determinism \mathcal {M}(X) = \mathcal {P}(X_\bot ) \setminus \emptyset : \begin {array}{l} \eta : X \rightarrow \mathcal {P}(X_\bot ) \setminus \emptyset \\ \eta (x) = \{ x \}\\ \mu : \mathcal {P}{((\mathcal {P}(X_\bot ) \setminus \emptyset )_\bot )}\rightarrow \mathcal {P}(X_\bot ) \setminus \emptyset \\ \mu (S) = (\bigcup _{X \neq \bot \in S} X) \cup (S \cap \{ \bot \}) \end {array} And, with this semantics, we can easily add a denotation for a non-deterministic choice operator, in terms of union: \llbracket c_1 + c_2 \rrbracket _\mathcal {C} = \lambda \sigma . \llbracket c_1 \rrbracket _\mathcal {C} \sigma \cup \llbracket c_2 \rrbracket _\mathcal {C} \sigma Unfortunately this is only the beginning of our troubles. While we have given a valuation function above, its definition uses \textbf {fix}, and therefore our domain \Sigma \rightarrow \mathcal {M}(\Sigma ) must be a cpo, and all our operations continuous. It is not clear how to order elements of \mathcal {P}(X_\bot ) \setminus \emptyset . A natural choice of ordering would be subset inclusion \subseteq . However, as we lack \emptyset , there is no least element for this ordering. Furthermore, simply using \subseteq as our ordering would mean that the deterministic, terminating program that always returns a single state \{ \sigma \} would be considered less informative than the program that may diverge \{ \bot , \sigma \}. This would make most of our operations non-continuous.

Instead, we shall examine three separate orderings on this set, each of which carries a different view of non-determinism. More generally, we wish to come up with a construction analogous to the powerset operator \mathcal {P}, but for our semantic domains — a powerdomain. However, for these orderings to produce valid partial orders, we require a certain theorem that only applies to a certain class of cpos, called "algebraic" cpos. Thus, we will first introduce a richer class of cpos, called Scott domains, and then return to the problem of non-determinism.

We begin by formalising the notion of an element in a cpo representing a finite amount of information.

Following the above intuition, we might be tempted to say that the "infinite" elements of a cpo are those which are the lub of an interesting set, but this notion is too weak. Consider this cpo X:

In the example cpo X above, all the elements except \infty and x would be compact. Thus, compactness better captures our notion of an element representing a finite amount of information. This understanding of compact elements is a generalisation of the notion of a finite element from the theory of algebraic lattices.

ExampleCompact elements with infinitely many approximations [dt-003X]

• Liam O'Connor

Compact elements may still have an infinite number of approximations. Consider the cpo \mathbb {N} \cup \{ \infty , \infty + 1 \}, where we have tacked on an additional top element \infty + 1 to our normal cpo of natural numbers extended with infinity. Then, while \infty is not compact, \infty + 1 is compact — it is not the lub of an interesting directed set. If \infty + 1 is the lub of a set X then \infty + 1 must be in the set X. Nonetheless, there are an infinite number of approximations to \infty + 1, i.e., elements x such that x \sqsubseteq \infty + 1.

As an aside, requiring that our compact elements have a truly finite number of approximations is the basis for the theory of Berry domains and stable functions.

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.

Consider the following three programs:

1. x := 1
2. \textsf {while}\ \textsf {true}\ \textsf {do}\ \textsf {skip}
3. \textsf {while}\ \textsf {true}\ \textsf {do}\ \textsf {skip}\ \textsf {od} + x := 1

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.

Note that all sets that contain \bot are considered equivalent by the Smyth construction \approx _S. Thus, this models demonic non-determinism: Of the three programs in Remark [dt-0063], the Smyth semantics considers 2 and 3 to be the same. Thus, the possibility of divergence \bot is no different from inevitable divergence.