finished domain theory!

trees/dm/dm-000T.tree

···
+\taxon{Definition}
+\author{liamoc}
+\title{Kleisli category}
+\p{For a [monad](dm-000U) #{(\mathcal{M}, \mu, \eta) } over the [category](dm-000G) #{\mathbf{C}}, the \em{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}.
+ } 

trees/dm/dm-000U.tree

···
+\import{table-macros}
+\author{liamoc}
+\title{Monad}
+\taxon{Definition}
+\p{
+A \em{monad} on the [category](dm-000G) #{\textbf{C}} consists of an [endofunctor](dm-000J) #{\mathcal{M} : \textbf{C} \rightarrow \textbf{C}} and two operations (\em{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](dm-000L) commute:
+\figure{
+	\table{\tr{
+	\td{
+	\tex{\usepackage{tikz-cd}}{
+	\begin{tikzcd}
+	\mathcal{M}(\mathcal{M}(\mathcal{M}(X))) \ar[r,"\mathcal{M}(\mu_X)"]
+	 \ar[d,"\mu_{\mathcal{M}(X)}"'] & \mathcal{M}(\mathcal{M}(X)) \ar[d,"\mu_X"] \\
+	\mathcal{M}(\mathcal{M}(X)) \ar[r,"\mu_X"]& \mathcal{M}(X)
+	\end{tikzcd}	
+	}	
+	}
+	\td{
+		\tex{\usepackage{tikz-cd}}{\begin{tikzcd}
+		\mathcal{M}(X) \ar[r,"\eta_{\mathcal{M}(X)}"]
+			 \ar[d,"\mathcal{M}(\eta_X)"']\ar[dr,equal] & \mathcal{M}(\mathcal{M}(X)) \ar[d,"\mu_X"] \\
+			\mathcal{M}(\mathcal{M}(X)) \ar[r,"\mu_X"]& \mathcal{M}(X)
+			\end{tikzcd}}
+	}	
+	}}
+}
+In equational form, these laws are 
+\ol{
+\li{ #{\mu_X \circ \mathcal{M}(\mu_X) = \mu_X \circ \mu_{\mathcal{M}(X)}} }
+\li{ #{\mu_X \circ \mathcal{M}(\eta_X) =  \mu_X \circ \eta_{\mathcal{M}(X)} = \mathsf{id}_{\mathcal{M}(X)}} }
+}
+ In computer science, #{\eta_X} is sometimes called \em{unit, pure,} or \em{return}, and #{\mu_X} is usually called \em{join}. 
+ }

trees/dm/dm-000V.tree

···
+\title{Preorder}
+\p{A binary relation #{(\preceq) \subseteq X \times X} is a \em{preorder} if it is, for all #{x, y, z \in X}:
+\ul{
+\li{ [reflexive](dm-0001): #{x \preceq x}, }
+\li{ [transitive](dm-0002): #{x \preceq y} and #{y \preceq z} implies #{x \preceq z},}
+}
+A preorder that is also [antisymmetric](dm-0003) is a [partial order](dm-0000).
+}
+

trees/dm/dm-000W.tree

···
+\author{liamoc}
+\title{Equivalence relation}
+\p{A binary relation #{(\approx) \subseteq X \times X} is an \em{equivalence relation} if it is, for all #{x, y, z \in X}:
+\ul{
+\li{ [reflexive](dm-0001): #{x \approx x}, }
+\li{ [transitive](dm-0002): #{x \approx y} and #{y \approx z} implies #{x \approx z},}
+\li{ [symmetric](dm-000Y): #{x \approx y} implies #{y \approx x}}
+}
+}

trees/dm/dm-000X.tree

···
+\taxon{Definition}
+\title{Equivalence class}
+\author{liamoc}
+\p{Given an [equivalence relation](dm-000W) #{\approx} on a set #{S}, the set #{S} can be completely partitioned into subsets (\em{equivalence classes}) such that two elements #{x} and #{y} belong to the same \em{equivalence class} if and only if #{x \approx y}.}

trees/dm/dm-000Y.tree

···
+\title{Symmetry}
+\author{liamoc}
+\taxon{Definition}
+\p{ A binary relation #{\mathcal{R}} is \em{symmetric} iff, for all #{x} and #{y}, #{x\ \mathcal{R}\ y} implies #{y\ \mathcal{R}\ x}.}

trees/dt/dt-001Y.tree

···
 \title{Domain theory}
 \author{liamoc}
 \p{These lecture notes are based on the material I used to teach the [[typesig-dt]] course at the [[uoe]] in 2024.}
+\scope{
+\put\transclude/expanded{false}
 \transclude{dt-0005}
 \transclude{dt-001Z}
 \transclude{dt-004Z}
-\subtree{
-\taxon{Lecture}
-\title{Scott Domains}
-\transclude{dt-0040}
-\subtree{
-\title{Algebraicity and ideals}
-\transclude{dt-0041}
-\transclude{dt-0042}
-\transclude{dt-0043}
-\transclude{dt-0045}
-\transclude{dt-0044}
-\transclude{dt-0047}
-\transclude{dt-0048}
-\transclude{dt-0046}
-\transclude{dt-0049}
-}
-\subtree{
-\title{Getting closure}
-\transclude{dt-004A}
-\transclude{dt-004B}
-\transclude{dt-004C}
-\problemblock{
-#{\omega}-[algebraic](dt-0041) [cpos](dt-001D) are closed under all of our constructions ([products](dt-0021) and [sums](dt-0031), including [strict versions of these](dt-003E)) \strong{except} functions #{\contto} and strict functions #{\strictto}!
-}
-
-\transclude{dt-004D}
-\transclude{dt-004E}
-\transclude{dt-004F}
-\transclude{dt-004G}
-\transclude{dt-004H}
-\transclude{dt-004I}
-
-\scope{
-\put\transclude/toc{false}
-\put\transclude/numbered{false}
-\subtree{\taxon{Thesis}
-\p{Our semantic domains are [Scott domains](dt-004G).}
-}}
-
-
-}
-}
-\subtree{
-\taxon{Lecture}
-\title{Non-determinism}
-\p{todo}
+\transclude{dt-005V}
 }

trees/dt/dt-001Z.tree

···
 \taxon{Lecture}
 \title{Constructions on [cpos](dt-001D) and PCF}
 \author{liamoc}
-\p{This lecture is based on material from [[haskellhutt]], [[jlongley]],[[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
+\p{This lecture is based on material from [[haskellhutt]], [[jlongley]], [[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
 \transclude{dt-002K}
 \transclude{dt-002Z}
 \transclude{dt-0030}

trees/dt/dt-004Z.tree

···
 \taxon{Lecture}
 \author{liamoc}
-\title{Recursively Defined Domains}
-\p{This lecture is based on material from [[haskellhutt]], [[jlongley]],[[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
+\title{Recursively defined domains and #{\lambda}-calculus}
+\p{This lecture is based on material from [[haskellhutt]], [[jlongley]], [[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
 \transclude{dt-004J}
 \transclude{dt-004O}
 \transclude{dt-0052}

trees/dt/dt-005P.tree

···
+\import{dt-macros}
+\author{liamoc}
+\taxon{Example}
+\title{Flat domains as monads}
+\p{The [flat domain](dt-0008) [lifting operation](dt-003K) #{(\cdot)_\bot} forms a [monad](dm-000U), 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}.}

trees/dt/dt-005Q.tree

···
+\import{dt-macros}
+\taxon{Definition}
+\author{liamoc}
+\title{Monadic semantics for #{\mathcal{C}}}
+\p{We define our semantics generically in terms of a [monad](dm-000U) #{(\mathcal{M},\mu,\eta)}, using the [Kleisli composition operator](dm-000T) 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}
+}
+}

trees/dt/dt-005R.tree

···
+\import{dt-macros}
+\title{The \cal{C} Language}
+\taxon{Definition}
+\author{liamoc}
+\p{ Using notation similar to \em{Backus-Naur Form} (BNF):
+##{
+\begin{array}{lcl}
+\cal{E} & \Coloneqq & n \mid x \mid \cal{E}_1 + \cal{E}_2 \mid \cal{E}_1 - \cal{E}_2\\
+\cal{B} & \Coloneqq & \syn{false} \mid \syn{true} \mid \neg \cal{B} \mid \cal{E}_1 = \cal{E}_2\\
+\cal{C} & \Coloneqq & \syn{skip} \mid x := \cal{E} \mid \cal{C}_1 ; \cal{C}_2 \mid \syn{if}\ \cal{B}\ \syn{then}\ \cal{C}_1\ \syn{else}\ \cal{C}_2 \mid \syn{while}\ \cal{B}\ \syn{do}\ \cal{C}\ \syn{od}\\
+x & \in & \cal{V}\; \textit{(variables)}\\
+n & \in & \nat
+\end{array}
+}
+}

trees/dt/dt-005S.tree

···
+\import{dt-macros}
+\taxon{Example}
+\title{Instantiating #{\mathcal{C}} with the lifting monad}
+\author{liamoc}
+\p{
+Instantiating our [monadic semantics](dt-005Q) where the [monad](dm-000U) #{\mathcal{M}} is [flat domain lifting](dt-005P), we recover our [original semantics](dt-0004) of #{\mathcal{C}}.
+}

trees/dt/dt-005T.tree

···
+\import{dt-macros}
+\taxon{Example}
+\author{liamoc}
+\title{Instantiating #{\mathcal{C}} with exceptions}
+\p{
+	Let us instantiate our [monadic semantics](dt-005Q) with the [monad](dm-000U) #{\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.}
+\p{Then we may extend our [language](dt-005R) with lightweight exception constructs:
+	##{\mathcal{C} ::= \dots \mid \syn{throw} \mid \syn{try}\ \mathcal{C}_1\ \syn{catch}\ \mathcal{C}_2}
+and define their semantics, leaving our [existing semantics](dt-005Q) unchanged:	
+	##{
+\begin{array}{lcl}
+\llbracket \syn{throw} \rrbracket\ \sigma &=& \mathsf{fail} \\
+\llbracket \syn{try}\ c_1\ \syn{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}
+	}
+}

trees/dt/dt-005U.tree

···
+\import{dt-macros}
+\title{Introduction to nondeterminism}
+\author{liamoc}
+\p{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 \em{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}.}
+
+\p{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.
+}

trees/dt/dt-005V.tree

···
+\import{dt-macros}
+\taxon{Lecture}
+\author{liamoc}
+\title{Monadic semantics, Scott domains and nondeterminism}
+\p{This lecture is based on material from [[cgunter]], [[gwinskel]], [[haskellhutt]], [[kaie]], [[dexterkozen]], [[andrewmyers]], [[jlongley]], [[danascott]], and [[jstoy]].}
+\transclude{dt-005Z}
+\subtree{
+\title{Nondeterminism}
+\transclude{dt-005U}
+\transclude{dt-0060}
+}
+\transclude{dt-005W}
+\transclude{dt-0061}
+\transclude{dt-0064}
+\transclude{dt-0067}

trees/dt/dt-005W.tree

···
+\import{dt-macros}
+\author{liamoc}
+\title{Scott domains}
+\transclude{dt-0040}
+\transclude{dt-005X}
+\transclude{dt-005Y}

trees/dt/dt-005X.tree

···
+\author{liamoc}
+\title{Algebraicity and ideals}
+\transclude{dt-0041}
+\transclude{dt-0042}
+\transclude{dt-0043}
+\transclude{dt-0045}
+\transclude{dt-0044}
+\transclude{dt-0047}
+\transclude{dt-0048}
+\transclude{dt-0046}
+\transclude{dt-0049}

trees/dt/dt-005Y.tree

···
+\import{dt-macros}
+\author{liamoc}
+\title{Getting closure}
+\transclude{dt-004A}
+\transclude{dt-004B}
+\transclude{dt-004C}
+\problemblock{
+#{\omega}-[algebraic](dt-0041) [cpos](dt-001D) are closed under all of our constructions ([products](dt-0021) and [sums](dt-0031), including [strict versions of these](dt-003E)) \strong{except} functions #{\contto} and strict functions #{\strictto}!
+}
+
+\transclude{dt-004D}
+\transclude{dt-004E}
+\transclude{dt-004F}
+\transclude{dt-004G}
+\transclude{dt-004H}
+\transclude{dt-004I}
+
+\scope{
+\put\transclude/toc{false}
+\put\transclude/numbered{false}
+\subtree{\taxon{Thesis}
+\p{Our semantic domains are [Scott domains](dt-004G).}
+}}

trees/dt/dt-005Z.tree

···
+\import{dt-macros}
+\title{Generalising our semantics}
+\author{liamoc}
+\p{We return to [the #{\mathcal{C}} language](dt-005R) we saw [previously](dt-0000):}
+\transclude{dt-005R}
+\p{If we wish to add other kinds of effects (beyond mutation of state) to our language, this will necessarily affect the semantic domain. Rather than rewrite the entire semantics for each possible setting, we will generalise the semantics to work over any instance of an algebraic structure, called a [monad](dm-000U).}
+\transclude{dm-000U}
+\transclude{dt-005P}
+\p{Sometimes it is more convenient to work with the [Kleisli composition](dm-000T) operator, rather than the operations #{\mu} and #{\eta} directly.}
+\transclude{dm-000T}
+\transclude{dt-005Q}
+\transclude{dt-005S}
+\transclude{dt-005T}

trees/dt/dt-0060.tree

···
+\import{dt-macros}
+\author{liamoc}
+\title{Instantiating our semantics for nondeterminism}
+\p{
+Our [initial semantics](dt-0004) for #{\mathcal{C}} (without loops) was functions on states #{\Sigma \rightarrow \Sigma}. When adding loops, we used a [cpo](dt-001D) #{\Sigma \contto \Sigma_\bot} for our semantic domain. Since \em{non-deterministic} programs can have more than one outcome, a natural choice of semantic domain would be #{\Sigma \contto \mathcal{P}(\Sigma_\bot) \setminus \emptyset}, i.e., functions from an initial state to a non-empty set of possible outcomes. }
+
+\p{We can provide #{\eta} and #{\mu} operations for our proposed [monad](dm-000U) 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](dt-001D), and all our operations [continuous](dt-001J). 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 #{\Set{ \sigma }} would be considered \em{less} informative than the program that may diverge #{\Set{ \bot, \sigma }}. This would make most of our operations non-[continuous](dt-001J).}
+\p{
+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 \em{powerdomain}. However, for these orderings to produce valid [partial orders](dm-0000), we require a certain  [theorem](dt-0049) that only applies to a certain class of [cpos](dt-001D), called "[algebraic](dt-0041)" cpos. Thus, we will first introduce a richer class of cpos, called \em{Scott domains}, and then return to the problem of non-determinism.}

trees/dt/dt-0061.tree

···
+\import{dt-macros}
+\author{liamoc}
+\title{The Hoare powerdomain}
+\p{We write #{\mathcal{P}_f^\ast(S)} to denote finite non-empty subsets of #{S}. Let #{X, Y \in \mathcal{P}_f^\ast(\compact{A})} be finite, non-empty sets of compact elements of a Scott domain #{A}. The \em{Hoare powerdomain} construction is based on the following ordering:
+##{
+X \preceq_H Y\quad \text{iff}\quad (\forall x \in X.\ \exists y \in Y.\ x \sqsubseteq_A y)
+}
+The intuition behind this is that "Anything #{X} can do, #{Y} can do better". This ordering has some desirable properties: The least element is #{\Set{\bot }}, as we might expect. It also satisfies the equation #{X \preceq_H X \cup Y}, which intuitively means that a non-deterministic choice is considered to have \em{more} information than any of its components. When specialised to the case where #{A} is a [flat domain](dt-0008) like #{\Sigma_\bot}, it simplifies to:
+##{
+X \preceq_H Y\quad \text{iff}\quad X \setminus \Set{\bot } \subseteq Y
+}
+This is, however, not a proper order, but a [preorder](dm-000V), as it fails [antisymmetry](dm-0003). Even in the [flat domain](dt-0008) case, #{\Set{ x, \bot } \preceq_H \Set{x }} and #{\Set{ x } \preceq_H \Set{x, \bot }} but they are not equal. However, any [preorder](dm-000V) \em{does} induce an [equivalence relation](dm-000W), where #{X \approx_H Y} iff #{X \preceq_H Y} and #{Y \preceq_H X}. Furthermore, if we take the [ideal completion](dt-0046) of #{\mathcal{P}_f^\ast(K(A))} with respect to the [preorder](dm-000V) #{\preceq_H} (i.e., the set of all #{\preceq_H}-[downwards-closed](dt-0047) [directed](dt-0010) subsets of #{\mathcal{P}_f^\ast(\compact{A})}), we can order them by inclusion to obtain an [algebraic](dt-0041) domain with [compact](dt-003U) elements which correspond to [equivalence classes](dm-000X) of elements under #{\approx_H}. We have a [lub](dt-0017) operation for these [ideals](dt-0048):
+##{
+A \sqcup_H B = \Set{ X \cup Y \mid X \in A \land Y \in B }
+}
+}
+\transclude{dt-0062}
+\transclude{dt-0063}

trees/dt/dt-0062.tree

···
+\import{dt-macros}
+\author{liamoc}
+\taxon{Example}
+\title{Hoare powerdomain of #{\mathbb{N}_\bot}}
+\p{
+	Let us find the [Hoare powerdomain](dt-0061) of #{\mathbb{N}_\bot}. Note that #{\mathbb{N}_\bot} is a [flat domain](dt-0008) so all elements are [compact](dt-003U), i.e. #{\compact{\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](dt-0048) subsets are [downwards closed](dt-0047), we can identify an [ideal](dt-0048) #{I \in \mathsf{Id}({\mathcal{P}_f^\ast(\mathbb{N}_\bot)})} with its union #{\bigcup I}. The [ideals](dt-0048) of #{\mathcal{P}^\ast_f(\mathbb{N}_\bot)} are then [isomorphic](dt-002E) to domain #{\mathcal{P}(\mathbb{N})} of all subsets of #{\mathbb{N}} under subset inclusion.
+}

trees/dt/dt-0063.tree

···
+\import{dt-macros}
+\taxon{Remark}
+\author{liamoc}
+\title{Angelic nondeterminism}
+\p{
+Consider the following three programs:
+\ol{
+\li{#{ x := 1}}
+\li{ #{\textsf{while}\ \textsf{true}\ \textsf{do}\ \textsf{skip}}}
+\li{#{ \textsf{while}\ \textsf{true}\ \textsf{do}\ \textsf{skip}\ \textsf{od} + x := 1 }}
+}
+Given a state #{\sigma}, let #{\sigma' = \sigma(x \mapsto 1)}. Then, the possible results of these programs are #{\Set{ \sigma' }}, #{\Set{ \bot }}, and #{\Set{\sigma', \bot }} respectively. Because the [Hoare construction](dt-0061) identifies #{\approx_H}-equivalent sets, the Hoare powerdomain semantics will consider programs 1 and 3 to be the same. That is, the non-determinism is \em{angelic}. The bad outcome (#{\bot}) is only said to happen if it is \em{inevitable}. 
+}

trees/dt/dt-0064.tree

···
+\import{dt-macros}
+\author{liamoc}
+\title{The Smyth powerdomain}
+\p{As before, let #{X, Y \in \mathcal{P}_f^\ast(\compact{A})} be finite, non-empty sets of [compact](dt-003U) elements of a [Scott domain](dt-004G) #{A}. The \em{Smyth powerdomain} construction is based on the following [preorder](dm-000V):
+##{
+X \preceq_S Y\quad \text{iff}\quad (\forall y \in Y.\ \exists x \in X.\ x \sqsubseteq_A y)
+}
+The intuition here is "Everything #{Y} can do, #{X} can do worse". It satisfies the equation #{X \cup Y \preceq_S X}, which intuitively means that a non-deterministic choice is considered to have \em{less} information than any of its components. When applied to a [flat domain](dt-0008), it simplifies to:
+##{
+X \preceq_S Y\quad\text{iff}\quad \bot \in X \lor Y \subseteq X
+}
+As with the [Hoare powerdomain](dt-0061), this fails to be a [partial order](dm-0000), but we can use the same [ideal completion](dt-0046) trick to induce an [algebraic](dt-0041) domain where [compact elements](dt-003U) correspond to [equivalence classes](dm-000X) of elements under #{\approx_S} (where #{X \approx_S Y} is, as with #{\approx_H}, just defined as #{X \preceq_S Y \land Y \preceq_S X}). }
+\transclude{dt-0065}
+\transclude{dt-0066}

trees/dt/dt-0065.tree

···
+\import{dt-macros}
+\author{liamoc}
+\taxon{Example}
+\title{Smyth powerdomain of #{\mathbb{N}_\bot}}
+\p{Firstly note that, as [ideals](dt-0048) are [downwards-closed](dt-0047), any #{\preceq_S}-[ideal](dt-0048) subsets of #{\mathcal{P}^\ast_f(\mathbb{N}_\bot)} will contain \em{all} finite subsets of #{\mathbb{N}_\bot} that contain #{\bot}.  Let us call those sets \em{trivial}. So, a set in #{\mathcal{P}^\ast_f(\mathbb{N}_\bot)} is \em{non-trivial} if it does not contain #{\bot} and an ideal subset of #{\mathcal{P}^\ast_f(\mathbb{N}_\bot)} is \em{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](dt-0048) #{I \in \mathsf{Id}({\mathcal{P}_f^\ast(\mathbb{N}_\bot)})} with the [down-closure](dt-0047) of the \em{intersection} of its non-trivial elements. The smaller this set is, the larger the ideal #{I}. Hence, and confusingly, the non-trivial [ideals](dt-0048) in the powerdomain (ordered by subset inclusion) correspond to finite subsets of #{\mathbb{N}} ordered by \em{superset} inclusion. As all \em{trivial} sets are identified, we just need to throw in the unique trivial [ideal](dt-0048), and we can see that the \em{Smyth} powerdomain of #{\mathbb{N}} is [isomorphic](dt-002E) to the domain of sets #{\Set{ \mathbb{N} } \cup \mathcal{P}_f^\ast(\mathbb{N})} ordered by subset inclusion.}

trees/dt/dt-0066.tree

···
+\import{dt-macros}
+\author{liamoc}
+\taxon{Remark}
+\title{Demonic nondeterminism}
+\p{Note that all sets that contain #{\bot} are considered equivalent by the [Smyth](dt-0064) construction #{\approx_S}. Thus, this models \em{demonic} non-determinism: Of the three programs in \ref{dt-0063}, the [Smyth](dt-0064) semantics considers 2 and 3 to be the same. Thus, the \em{possibility} of divergence #{\bot} is no different from \em{inevitable} divergence.
+}

trees/dt/dt-0067.tree

···
+\import{dt-macros}
+\author{liamoc}
+\title{The Plotkin powerdomain}
+\p{As before, let #{X, Y \in \mathcal{P}_f^\ast(\compact{A})} be finite, non-empty sets of [compact elements](dt-003U) of a [Scott domain](dt-004G) #{A}. The \em{Plotkin powerdomain} construction is based on the following \em{preorder}, simply combining the orderings from the [Hoare](dt-0061) and [Smyth](dt-0064) constructions:
+##{
+X \preceq_P Y\quad \text{iff}\quad X \preceq_H Y \land X \preceq_S Y
+}
+This ordering is also called the \em{Egli-Milner} ordering.  On a [flat domain](dt-0008), it simplifies to:
+#{A\sqsubseteq B\quad\text{iff}\quad A = B \lor (\bot \in A \land (A \setminus \{\bot\})\subseteq B)}
+Note that this \em{is} antisymmetric in the case of a [flat domain](dt-0008), and the [lub](dt-0017) of a [chain](dt-000V) of sets can be found by taking the union of all elements of the chain if all elements contain $\bot$. If not, then the element without $\bot$ will be the [least upper bound](dt-0017).}
+\p{
+The failures of [antisymmetry](dm-0003) can only be observed in domains of height higher than one. Consider a set #{\Set{x,y}} containing two elements. According to the induced equivalence from this [preorder](dm-000V) #{\approx_P}, this set would be considered equal to the set that contains those two elements \em{plus} any elements that lie between them on the [information ordering](dt-000B): ##{\Set{x,y} \approx_P \Set{ z \mid x \sqsubseteq z \sqsubseteq y }}
+The \em{Plotkin powerdomain} is sometimes called the \em{convex powerdomain}, due to the similarity of this to the geometric definition of convexity.  Thus, we use the [ideal completion](dt-0046) trick (as with the [Hoare](dt-0061) and [Smyth](dt-0064) constructions) here to arrive at a definition of powerdomain that distinguishes between all three programs outlined in \ref{dt-0063}.} 
+\subtree{
+\taxon{Aside}
+\p{
+There is a beautiful algebraic characterisation of Plotkin powerdomains in [[mhennessy]] [[plotkin]]'s paper, [[hennessy-plotkin-1979]].
+% Full Abstraction for a Simple Parallel Programming Language}. In
+%Mathematical Foundations of Computer Science 1979, Proceedings, Olomouc, Czechoslovakia, September 3-7,
+%1979 (LNCS, Vol. 74), Springer, 108–120		
+}
+}

trees/people/andrewmyers.tree

···
+\title{Andrew Myers}
+\taxon{Person}
+\meta{institution}{[[cornell]]}
+\meta{position}{Professor}
+\meta{external}{https://www.cs.cornell.edu/andru/}
+\meta{orcid}{0000-0001-5819-7588}

trees/people/dexterkozen.tree

···
+\title{Dexter Kozen}
+\taxon{Person}
+\meta{institution}{[[cornell]]}
+\meta{position}{Professor Emeritus}
+\meta{external}{https://www.cs.cornell.edu/~kozen/}
+\meta{orcid}{0000-0002-8007-4725}

trees/people/mhennessy.tree

···
+\title{Matthew Hennessy}
+\taxon{Person}
+\meta{position}{Research Professor}
+\meta{external}{https://www.scss.tcd.ie/Matthew.Hennessy}
+\meta{institution}{[[tcd]]}
+

trees/people/plotkin.tree

···
+\title{Gordon Plotkin}
+\taxon{Person}
+\meta{position}{Professor}
+\meta{external}{https://homepages.inf.ed.ac.uk/gdp/}
+\meta{institution}{[[uoe]]}
+

trees/places/cornell.tree

···
+\title{Cornell University}
+\taxon{Institution}
+\meta{external}{https://www.cornell.edu/}
+\meta{venue}{Ithaca, New York, USA}

trees/places/mfcs79.tree

···
+\import{conf-name-macros}
+\taxon{Conference}
+\title{\conf-name{MFCS '79}{Mathematical Foundations of Computer Science 1979}}
+\date{1979-09}
+\meta{venue}{Olomouc, Czechoslovakia}
+\meta{doi}{10.1007/3-540-09526-8}

trees/places/tcd.tree

···
+\title{Trinity College, Dublin}
+\taxon{Institution}
+\meta{venue}{Dublin, Ireland}
+\meta{external}{https://www.tcd.ie}

trees/refs/hennessy-plotkin-1979.tree

···
+\title{Full abstraction for a simple parallel programming language}
+\taxon{Reference}
+\meta{venue}{[[mfcs79]]}
+\author{mhennessy}
+\author{plotkin}
+\date{1979-09-07}
+\meta{doi}{10.1007/3-540-09526-8_8}
+\tag{refereed}