my forest
add scott domains
+317
-3
assets/c3po.png
assets/c3po.png
This is a binary file and will not be displayed.
+34
-2
trees/dt/dt-001Y.tree
+34
-2
trees/dt/dt-001Y.tree
···
1
+
\import{dt-macros}
1
2
\taxon{Lecture Notes}
2
3
\title{Domain theory}
3
4
\author{liamoc}
···
14
15
\title{Scott Domains}
15
16
\transclude{dt-0040}
16
17
\subtree{
17
-
\title{Algebraicity and Ideals}
18
+
\title{Algebraicity and ideals}
19
+
\transclude{dt-0041}
20
+
\transclude{dt-0042}
21
+
\transclude{dt-0043}
22
+
\transclude{dt-0045}
23
+
\transclude{dt-0044}
24
+
\transclude{dt-0047}
25
+
\transclude{dt-0048}
26
+
\transclude{dt-0046}
27
+
\transclude{dt-0049}
18
28
}
19
29
\subtree{
20
-
\title{Getting Closure}
30
+
\title{Getting closure}
31
+
\transclude{dt-004A}
32
+
\transclude{dt-004B}
33
+
\transclude{dt-004C}
34
+
\problemblock{
35
+
#{\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}!
36
+
}
37
+
38
+
\transclude{dt-004D}
39
+
\transclude{dt-004E}
40
+
\transclude{dt-004F}
41
+
\transclude{dt-004G}
42
+
\transclude{dt-004H}
43
+
\transclude{dt-004I}
44
+
45
+
\scope{
46
+
\put\transclude/toc{false}
47
+
\put\transclude/numbered{false}
48
+
\subtree{\taxon{Thesis}
49
+
\p{Our semantic domains are [Scott domains](dt-004G).}
50
+
}}
51
+
52
+
21
53
}
22
54
}
23
55
\subtree{
+1
-1
trees/dt/dt-003Z.tree
+1
-1
trees/dt/dt-003Z.tree
···
2
2
\author{liamoc}
3
3
\title{Both infinite and compact}
4
4
\taxon{Exercise}
5
-
\p{Find a set in the [cpo of submonoids](dt-003Y) of #{(\mathbb{N},0,+)} that is \em{both} infinite and [compact](dt-003U)}
5
+
\p{Find a set in the [cpo of submonoids](dt-003Y) of #{(\mathbb{N},0,+)} that is \em{both} infinite and [compact](dt-003U).}
6
6
7
7
\solnblock{
8
8
\p{Take #{E \triangleq \Set{ n \in \mathbb{N} \mid n\ \text{is even}}}. Let #{Y \subseteq \pow{\mathbb{N}}} be directed and #{E \subseteq \bigcup Y}. Since #{2 \in E} there must exist #{y \in Y} such that #{2 \in Y}. Since #{(y,0,+)} is a [monoid](dm-000O), every positive multiple of #{2} is also in #{y}, thus #{E \subseteq y} and therefore #{E} is [compact](dt-003U).}
+1
trees/dt/dt-0040.tree
+1
trees/dt/dt-0040.tree
···
30
30
\p{In the example cpo #{X} above, all the elements except #{\infty} and #{x} would be [compact](dt-003U). Thus, compactness better captures our notion of an element representing a finite amount of information. This understanding of [compact](dt-003U) elements is a generalisation of the notion of a finite element from the theory of algebraic lattices.}
31
31
\transclude{dt-003V}
32
32
\transclude{dt-003X}
33
+
\transclude{dt-003Y}
33
34
\transclude{dt-003Z}
+12
trees/dt/dt-0041.tree
+12
trees/dt/dt-0041.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\title{Algebraicity}
5
+
\p{A [cpo](dt-001D) is \em{algebraic} iff every element is the [lub](dt-0017) of its [compact](dt-003U) approximations. That is, a [cpo](dt-001D) #{D} is \em{algebraic} iff for all #{x \in D},
6
+
\ol{
7
+
\li{#{\downset{x} = \Set{ y \in \compact{D} \mid y \sqsubseteq x }} is [directed](dt-0010);}
8
+
\li{#{x = \bigsqcup\downset{x}}}
9
+
}
10
+
\strong{Note}: It's common in semantics to consider only algebraic [cpos](dt-001D) with a \em{countable} set of [compact](dt-003U) elements. Such [cpos](dt-001D) are called \em{#{\omega}-algebraic}.}
11
+
12
+
\p{ \strong{Aside}: Plotkin provides an equivalent definition of #{\omega}-algebraic [cpos](dt-001D) in which [directed sets](dt-0010) are replaced with [#{\omega}-chains](dt-000W) throughout. [Hutton](haskellhutt) claims this is less appealing, as the definition speaks of \em{an} [#{\omega}-chain](dt-000W) of [compact](dt-003U) approximations, rather than \em{the} [directed set](dt-0010) of such.}
+7
trees/dt/dt-0042.tree
+7
trees/dt/dt-0042.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Example}
3
+
\title{#{\omega}-algebraic cpos}
4
+
\author{liamoc}
5
+
\p{
6
+
Many standard examples of [cpos](dt-001D) are #{\omega}-[algebraic](dt-0041) [cpos](dt-001D): finite cpos, subsets #{\pow{X}} of a set #{X}, partial functions #{\mathbb{N} \nrightarrow \mathbb{N}} and [submonoids of a monoid](dt-003Y). In general, any [cpo](dt-001D) of subalgebras (e.g. subgroups of a group, subrings of a ring etc.) is #{\omega}-[algebraic](dt-0041). This is the origin of the terminology.
7
+
}
+20
trees/dt/dt-0043.tree
+20
trees/dt/dt-0043.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\taxon{Counterexample}
4
+
\author{liamoc}
5
+
\title{Non-algebraic cpo}
6
+
\<html:div>[class]{sidefigure}{
7
+
\tex{\usepackage{tikz-cd}\usetikzlibrary{decorations.pathreplacing}\usepackage{amsmath}}{
8
+
\begin{tikzcd}
9
+
\infty\\
10
+
1\ar[u,thick,-,dotted] & & x\ar[ull,thick,-]\\
11
+
0\ar[u,thick,-] \\
12
+
& \bot \ar[ul,thick,-]\ar[uur,thick,-]
13
+
\end{tikzcd}
14
+
}
15
+
}
16
+
\p{In the [cpo](dt-001D) on the right (seen also in \ref{dt-0040}), the element #{x} is not the [lub](dt-0017) of its [compact](dt-003U) approximations. The only [compact](dt-003U) element that approximates #{x} is #{\bot}, and the [least upper bound](dt-0017) of the set #{\Set{\bot}} is just #{\bot}, not #{x}. That is:
17
+
##{\downset{x} = \Set{\bot}}
18
+
but:
19
+
##{x \neq \bigsqcup\Set{\bot}}
20
+
}
+22
trees/dt/dt-0044.tree
+22
trees/dt/dt-0044.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Exercise}
4
+
\p{Let #{f : D \contto E} be a [continuous](dt-001J) function between [algebraic](dt-0041) [cpos](dt-001D). Define:
5
+
##{G_f = \Set{ (a,b) \in \compact{D} \times \compact{E} \mid b \sqsubseteq f(a) }}
6
+
Then for all #{x \in D}, prove that:
7
+
##{
8
+
f(x) = \bigsqcup\ \Set{ b \mid (a,b) \in G_f \land a \sqsubseteq x }
9
+
}
10
+
}
11
+
\solnblock{
12
+
##{
13
+
\begin{array}{lclr}
14
+
f(x) & = & f(\bigsqcup \downset{x}) & \text{($D$ is {algebraic})}\\
15
+
&=&\bigsqcup\ \{ f(a) \mid a \in \downset{x} \} & \text{($f$ is continuous)}\\
16
+
&=&\bigsqcup\ \left\{ \bigsqcup \downset{f(a)} \mid a \in \downset{x} \right\} & \text{($E$ is {algebraic})}\\
17
+
&=&\bigsqcup\ \Set{ b \in \compact{E} \mid b \sqsubseteq f(a) \land a \in \downset{x}} & \text{(lubs and defn of $\downarrow$)}\\
18
+
&=&\bigsqcup\ \Set{ b \mid (a,b) \in G_f \land a \sqsubseteq x }&\text{(defn of $G_f$)}
19
+
\end{array}
20
+
}
21
+
}
22
+
\p{This is powerful. For example, the [continuous](dt-001J) function #{f : \pow{\mathbb{N}} \contto \pow{\mathbb{N}}} on an \em{uncountable} [cpo](dt-001D) #{\pow{\mathbb{N}}} is completely determined by the \em{countable} relation #{G_f}.}
+32
trees/dt/dt-0045.tree
+32
trees/dt/dt-0045.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\title{Nothing suddenly invented at infinity}
5
+
\p{Let #{D} and #{E} be [algebraic](dt-0041) [cpos](dt-001D). Then a function #{f : D \rightarrow E} is [continuous](dt-001J) iff, for all #{x \in D}: ##{f(x) = \bigsqcup\ \Set{ f(a) \mid a \in \downset{x} }}
6
+
In other words, in an [algebraic](dt-0041) [cpo](dt-001D), [continuous functions](dt-001J) are completely defined by their behaviour for [compact](dt-003U) arguments.}
7
+
\p{This makes precise our earlier slogan in \ref{dt-001J}, that [continuous functions](dt-001J) don't suddenly behave differently for infinite (i.e. non-[compact](dt-003U)) elements.}
8
+
\proofblock{
9
+
First, assuming #{f} is [continuous](dt-001J), we show that #{f(x) = \bigsqcup\ \Set{ f(a) \mid a \in \downset{x} }}:
10
+
##{
11
+
\begin{array}{lclr}
12
+
f(x) & = & f(\bigsqcup \downset{x}) & \text{($D$ is {algebraic})}\\
13
+
&=&\bigsqcup\ \{ f(a) \mid a \in \downset{x} \} & \text{($f$ is continuous)}\\
14
+
\end{array}
15
+
}
16
+
It remains to show that if #{f(x) = \bigsqcup\ \Set{ f(a) \mid a \in \downset{x} }}, then #{f} is [continuous](dt-001J). Using the [alternative definition](dt-001O), we shall first show that #{f} is [monotone](dt-000J). Let #{a \sqsubseteq b} for #{a,b \in D}. Then #{\downset{a} \subseteq \downset{b}} and thus #{\Set{f(x) \mid x \in \downset{a}} \subseteq \Set{f(x) \mid x \in \downset{b}}}, therefore:
17
+
##{
18
+
\begin{array}{lclr}
19
+
f(a) &=&\bigsqcup\ \Set{ f(x) \mid x \in \downset{a} } & \text{(assumption)}\\
20
+
& \sqsubseteq &\bigsqcup\ \Set{ f(x) \mid x \in \downset{b} } & \text{(from above)}\\
21
+
& = & f(b) & \text{(assumption)}\\
22
+
\end{array}
23
+
}
24
+
Next, let #{X \subseteq D} be [directed](dt-0010).
25
+
##{\begin{array}{lclr}
26
+
f(\bigsqcup X) &=&\bigsqcup\ \Set{ f(x) \mid x \in \downset{\bigsqcup X} } & \text{(assumption)}\\
27
+
&=&\bigsqcup\ \Set{ f(x) \mid x \in \compact{X} \land x \sqsubseteq \bigsqcup X } & \text{(defn.~of $\downarrow$)}\\
28
+
&=&\bigsqcup\ \Set{ f(x) \mid \exists y \in X.\ x \in \compact{X} \land x \sqsubseteq y } & \text{(compactness)}\\
29
+
&=&\bigsqcup\ \Set{ f(x) \mid \exists y \in X.\ x \in \downset{y}} & \text{(defn.~of $\downarrow$)}\\
30
+
&=&\bigsqcup\ \Set{ f(x) \mid x \in X} & \text{(algebraicity)}\\
31
+
\end{array}}
32
+
}
+9
trees/dt/dt-0046.tree
+9
trees/dt/dt-0046.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\title{Ideal completion}
4
+
\author{liamoc}
5
+
\p{The \em{ideal completion} of a set #{A}, written sometimes as #{\mathsf{Id}(A)}, is the set of all [ideal](dt-0048) subsets of #{A}, i.e.:
6
+
##{
7
+
\mathsf{Id}(A) = \Set{ X \subseteq A \mid X\ \text{is ideal}}
8
+
}
9
+
}
+4
trees/dt/dt-0047.tree
+4
trees/dt/dt-0047.tree
+4
trees/dt/dt-0048.tree
+4
trees/dt/dt-0048.tree
+7
trees/dt/dt-0049.tree
+7
trees/dt/dt-0049.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\title{Representation theorem for [algebraic](dt-0041) [cpos](dt-001D)}
5
+
\p{ Every [algebraic](dt-0041) [cpo](dt-001D) #{D} is [isomorphic](dt-002E) to the [ideal completion](dt-0046) of its [compact](dt-003U) elements, ordered by subset inclusion. That is, #{\mathsf{Id}(K(D))} is an [algebraic](dt-0041) [cpo](dt-001D) such that #{D \simeq \mathsf{Id}(K(D))
6
+
}.
7
+
}
+6
trees/dt/dt-004A.tree
+6
trees/dt/dt-004A.tree
+9
trees/dt/dt-004B.tree
+9
trees/dt/dt-004B.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\title{Compact basis for algebraic cpos}
5
+
\p{ If #{X} is a [basis](dt-004A) for #{A}, then #{A} is [algebraic](dt-0041) and #{\compact{A} = X}.
6
+
}
7
+
\proofblock{
8
+
\p{If #{a \in \compact{A}}, then #{\bigsqcup M = a} where #{M = \Set{ x \in X \mid x \sqsubseteq a }}, as #{X} is a [basis](dt-004A). Since #{a} is [compact](dt-003U), #{a \sqsubseteq b} for some #{b \in M}. But since #{a} is the [lub](dt-0017) of #{M}, #{b \sqsubseteq a} as well. By [antisymmetry](dm-0003) #{a = b}, hence #{a \in X}. Thus #{\compact{A} \subseteq X}, so #{\compact{A} = X} and #{A} is [algebraic](dt-0041).
9
+
}}
+37
trees/dt/dt-004C.tree
+37
trees/dt/dt-004C.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\author{liamoc}
4
+
\taxon{Theorem}
5
+
\title{Closure of algebraic cpos under product}
6
+
\p{If #{D} and #{E} are [algebraic](dt-0041) [cpos](dt-001D), then so is their product construction #{D \times E}.}
7
+
\proofblock{
8
+
\p{In the following proof, we show that #{\compact{D} \times \compact{E}} is a [basis](dt-004A) for the [product](dt-0021) #{D \times E} and thereby show via \ref{dt-004B} that #{D \times E} is [algebraic](dt-0041) if #{D} and #{E} are.}
9
+
\ol{
10
+
\li{
11
+
#{\compact{D} \times \compact{E} \subseteq \compact{D \times E}}: Let #{(x,y) \in \compact{D} \times \compact{E}}. To show that #{(x,y)} is [compact](dt-003U), let us assume that #{(x,y) \in \bigsqcup X} where #{X \subseteq D \times E} is [directed](dt-0010). We must show that there exists some element #{e} of #{X} such that our #{(x,y) \sqsubseteq e}. As #{(x,y) \in \bigsqcup X}, by the definition of [lub](dt-0017) on [products](dt-0021) we can conclude that:
12
+
##{\begin{array}{lcl}
13
+
x & \sqsubseteq & \bigsqcup \pi_0\lsquare X\rsquare \\
14
+
y & \sqsubseteq & \bigsqcup \pi_1[X]
15
+
\end{array}}
16
+
Here we use the notation #{f[X]} to indicate the image of a function on a set, i.e. #{\Set{ f(v) \mid v \in X }}.\br
17
+
18
+
Since #{x} and #{y} are both [compact](dt-003U), there must exist #{x' \in \pi_0\lsquare X\rsquare} and #{y' \in \pi_1\lsquare X\rsquare} such that #{x \sqsubseteq x'} and #{y \sqsubseteq y'}. While it does not follow that #{(x', y') \in X}, we know that there must exist a pair #{(a,b) \in X} such that #{x' \sqsubseteq a} and #{y' \sqsubseteq b} as #{X} is [directed](dt-0010). Hence #{(a,b)} can be our element #{e \in X} that is approximated by #{(x,y)}, i.e. #{(x,y) \sqsubseteq (a,b)}.
19
+
}
20
+
\li{
21
+
#{\downset{x,y}} is directed for all #{(x,y) \in D \times E}:
22
+
##{\begin{array}{lcl}
23
+
\downset{x,y} &= & \Set{ (a,b) \in \compact{D} \times \compact{E} \mid (a,b) \sqsubseteq (x,y) } \\
24
+
& = & \{ a \in \compact{D} \mid a \sqsubseteq x \} \times \Set{ b \in \compact{E} \mid b \sqsubseteq y }\\
25
+
& = & \downset{x} \times \downset{y}
26
+
\end{array}}
27
+
Because #{D} and #{E} are [algebraic](dt-0041), #{\downset{x}} and #{\downset{y}} are [directed](dt-0010). As directedness is closed under [product](dt-002K), #{\downset{x,y}} is [directed](dt-0010) too.
28
+
}
29
+
\li{#{(x,y) = \bigsqcup\downset{x,y}}
30
+
Starting from the right hand side:
31
+
##{\begin{array}{lclr}
32
+
\bigsqcup \downset{x,y} & = & \bigsqcup(\downset{x} \times \downset{y}) & \text{(part 2)}\\
33
+
& = & (\bigsqcup(\downset{x}, \bigsqcup\downset{y})) & \text{(lub on products)}\\
34
+
& = & (x,y) & \text{($D$, $E$ are {algebraic})}
35
+
\end{array}}}
36
+
}
37
+
}
+18
trees/dt/dt-004D.tree
+18
trees/dt/dt-004D.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Aside}
3
+
\author{liamoc}
4
+
\title{Scott's original solution: using complete lattices}
5
+
\p{The lack of closure of [algebraicity](dt-0041) under the ([continuous](dt-001J)) function arrow, [strict](dt-000K) or non-[strict](dt-000K), is not satisfying as it means that our semantic domains are not guaranteed to be [algebraic](dt-0041) even if they are composed from [algebraic](dt-0041) [cpos](dt-001D). Instead, we must replace [algebraic](dt-0041) [cpos](dt-001D) with something stronger still.}
6
+
\p{Scott's original solution to this lack of closure was to use a \em{complete lattice} instead of [cpos](dt-001D), i.e. requiring [lubs](dt-0017) for all subsets, not just [directed](dt-0010) ones. This solves the problem with #{\contto} but introduces new problems:
7
+
\ol{
8
+
\li{ Complete lattices need a \em{top} element #{\top}, but adding a fictitious top (representing inconsistent information) to [cpos](dt-001D) like #{\mathbb{B}_\bot} is strange.}
9
+
\li{ Extending the functions that capture our primitive semantic operationsto complete lattices can spoil nice algebraic properties. Consider these two possible implementations of #{\mathsf{ite}}, the function for the semantics of an #{\syn{if}} expression:
10
+
##{
11
+
\mathsf{ite}(\top,x,y) = x \sqcup y\quad\quad\quad \quad\quad \mathsf{ite}(\top,x,y) = \top
12
+
}
13
+
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) }
14
+
And the second definition above results in the failure of this equation that removes redundant checks:
15
+
##{\mathsf{ite}(b,x,x) = x}
16
+
}
17
+
\li{ The power domain construction (TODO) does not generalise to complete lattices, so semantics for non-deterministic programs are difficult in this setting. }
18
+
}}
+5
trees/dt/dt-004E.tree
+5
trees/dt/dt-004E.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{Consistent completeness}
5
+
\p{A [poset](dm-0004) #{A} is \em{consistent complete} (or \em{bounded complete}) iff #{\bigsqcup X} exists for all [consistent](dt-0013) #{X \subseteq A}. That is, any set with \em{an} [upper bound](dm-000C) (a [consistent](dt-0013) set) has a [\em{least} upper bound](dt-0017).}
+43
trees/dt/dt-004F.tree
+43
trees/dt/dt-004F.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\taxon{Example}
4
+
\author{liamoc}
5
+
\title{Consistent completeness vs directed completeness}
6
+
\figure{
7
+
\tableW{
8
+
\tr{
9
+
\td{
10
+
\tex{\usepackage{tikz-cd}}{\begin{tikzcd}[column sep=1em]
11
+
\quad \\
12
+
2 \ar[u,-,thick,dotted] \\
13
+
1 \ar[u,-,thick] \\
14
+
0 \ar[u,-,thick] \\
15
+
\end{tikzcd}}
16
+
}
17
+
\td{
18
+
\tex{\usepackage{tikz-cd}}{\begin{tikzcd}[column sep=1em]
19
+
\quad\\
20
+
\bullet && \bullet \\
21
+
\bullet \ar[u,-,thick]\ar[urr,-,thick] && \bullet \ar[ull,-,thick]\ar[u,-,thick] \\
22
+
&\bullet \ar[ul,-,thick]\ar[ur,-,thick] \\
23
+
\end{tikzcd}
24
+
}}
25
+
}
26
+
\tr{
27
+
\td{
28
+
[consistent complete](dt-004E)
29
+
}
30
+
\td{
31
+
not [consistent complete](dt-004E)
32
+
}
33
+
}
34
+
\tr{
35
+
\td{
36
+
not [directed complete](dt-001D)
37
+
}
38
+
\td{
39
+
[directed complete](dt-001D)
40
+
}
41
+
}
42
+
}
43
+
}
+26
trees/dt/dt-004G.tree
+26
trees/dt/dt-004G.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\taxon{Definition}
4
+
\title{Scott domain}
5
+
\author{liamoc}
6
+
7
+
\<html:img>[class]{sidefigure}[src]{\route-asset{assets/c3po.png}}
8
+
9
+
\p{A [cpo](dt-001D) #{D} is a \em{Scott domain} iff:
10
+
\ol{
11
+
\li{ #{D} is [#{\omega}-algebraic](dt-0041), }
12
+
\li{ #{D} is [consistent complete](dt-004E), }
13
+
}
14
+
In other words, \em{Scott domains} can be summed up by the acronym:
15
+
}
16
+
\<html:div>[class]{constrainfigure}{
17
+
\tex{\usepackage{tikz}\usepackage{amsmath}}{
18
+
\begin{tikzpicture}
19
+
\node (a) at (5,3) {\Large $\text{ac}^3\text{po}$};
20
+
\node (b1) at (0,-1) {\Large $\omega$-\textbf{\textcolor{orange}{a}}lgebraic };
21
+
\node (b2) at (4,-1) {\Large \textbf{\textcolor{orange}{c}}onsistent-\textbf{\textcolor{orange}{c}}omplete };
22
+
\node (b3) at (9.2,-1) {\Large \textbf{\textcolor{orange}{c}}omplete \textbf{\textcolor{orange}{p}}artial \textbf{\textcolor{orange}{o}}rder };
23
+
\draw[thick,-] (b1) -- (a) (b2) -- (a) (b3) -- (a);
24
+
\end{tikzpicture}
25
+
}
26
+
}
+3
trees/dt/dt-004H.tree
+3
trees/dt/dt-004H.tree
···
1
+
\taxon{Remark}
2
+
\author{liamoc}
3
+
\p{The second requirement in \ref{dt-004G} can, in light of the first, be expressed equivalently as: #{x \sqcup y} exists for all [consistent](dt-0013) #{x,y \in D}. This is useful when needing to show that a given [cpo](dt-001D) is a [Scott domain](dt-004G).}
+5
trees/dt/dt-004I.tree
+5
trees/dt/dt-004I.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Theorem}
3
+
\author{liamoc}
4
+
\p{[Scott domains](dt-004G) are closed under all our [cpo](dt-001D) constructions, including [sums](dt-0031) #{+}, [products](dt-0021) #{\times}, [continuous functions](dt-002L) #{\contto}, [smash sums](dt-003H) #{\oplus}, [smash products](dt-003G) #{\otimes} and [strict functions](dt-003F) #{\strictto}.
5
+
}
+8
trees/dt/dt-macros.tree
+8
trees/dt/dt-macros.tree
···
21
21
\subtree{\taxon{Upshot}
22
22
\body
23
23
}}}
24
+
\def\problemblock[body]{\scope{
25
+
\put\transclude/toc{false}
26
+
\put\transclude/numbered{false}
27
+
\subtree{\taxon{Problem}
28
+
\body
29
+
}}}
24
30
\def\solnblock[body]{\scope{
25
31
\put\transclude/toc{false}
26
32
\put\transclude/numbered{false}
···
28
34
\subtree{\taxon{Solution}
29
35
\body
30
36
}}}
37
+
\def\downset[body]{#{\mathop{\downarrow}(\body)}}
38
+
\def\downsetB[body]{#{\mathop{\downarrow}\left(\body\right)}}
31
39
\def\pow[body]{#{\mathcal{P}(\body)}}
32
40
\def\sems[body]{#{\llbracket \body \rrbracket}}
33
41
\def\nat{#{\mathbb{N}}}