my forest
actually finished?
+6
-2
+1
-1
trees/dt/dt-001Y.tree
+1
-1
trees/dt/dt-001Y.tree
···
4
4
\author{liamoc}
5
5
\p{These lecture notes are based on the material I used to teach the [[typesig-dt]] course at the [[uoe]] in 2024.}
6
6
\scope{
7
-
\put\transclude/expanded{false}
7
+
%\put\transclude/expanded{false}
8
8
\transclude{dt-0005}
9
9
\transclude{dt-001Z}
10
10
\transclude{dt-004Z}
+5
-1
trees/dt/dt-0067.tree
+5
-1
trees/dt/dt-0067.tree
···
7
7
}
8
8
This ordering is also called the \em{Egli-Milner} ordering. On a [flat domain](dt-0008), it simplifies to:
9
9
#{A\sqsubseteq B\quad\text{iff}\quad A = B \lor (\bot \in A \land (A \setminus \{\bot\})\subseteq B)}
10
-
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).}
10
+
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).}
11
11
\p{
12
12
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 }}
13
13
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}.}
14
+
\scope{
15
+
\put\transclude/toc{false}
16
+
\put\transclude/numbered{false}
14
17
\subtree{
15
18
\taxon{Aside}
16
19
\p{
···
20
23
%1979 (LNCS, Vol. 74), Springer, 108–120
21
24
}
22
25
}
26
+
}