my forest
strict constructions
+76
-9
+1
-3
trees/dt/dt-001Z.tree
+1
-3
trees/dt/dt-001Z.tree
+2
-5
trees/dt/dt-0038.tree
+2
-5
trees/dt/dt-0038.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\taxon{Exercise}
4
-
\p{Prove that the #{+ : \mathbf{Cpo} \times \mathbf{Cpo} \rightarrow \mathbf{Cpo}} is a lawful [bifunctor](dm-000M), as a consequence of the [weak universal property](dt-003B).
5
-
\solnblock{
6
-
\p{TODO}
7
-
}
3
+
\taxon{Theorem}
4
+
\p{#{+ : \mathbf{Cpo} \times \mathbf{Cpo} \rightarrow \mathbf{Cpo}} is a lawful [bifunctor](dm-000M).
8
5
}
+15
trees/dt/dt-003E.tree
+15
trees/dt/dt-003E.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Strict Constructions}
4
+
\p{When giving a semantics to a call-by-name (or "lazy") language, the constructions [#{\contto} for functions](dt-002F), [#{\times} for products](dt-0021) and [#{+} for sums](dt-0031) are exactly what we want. To properly capture call-by-value (or "strict") languages, however, we also need [strict](dt-000K) versions of these constructions.}
5
+
\transclude{dt-003F}
6
+
\transclude{dt-003G}
7
+
\transclude{dt-003H}
8
+
\transclude{dt-003J}
9
+
\transclude{dt-003I}
10
+
\upshotblock{
11
+
[[dt-003I]] has products, exponentials, \em{and sums} (as it doesn't suffer from the [problem](dt-0039) that #{\textbf{Cpo}} does).
12
+
}
13
+
\transclude{dt-003K}
14
+
\transclude{dt-003L}
15
+
+6
trees/dt/dt-003F.tree
+6
trees/dt/dt-003F.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Construction}
4
+
\title{The [cpo](dt-001D) of [strict](dt-000K) [continuous](dt-001J) functions}
5
+
##{A \strictto B = \Set{ f \in A \contto B \mid f(\bot) = \bot }}
6
+
\p{The [ordering](dm-0000) and [lubs](dt-0017) are, \em{mutatis mutandis}, as with the non-strict \ref{dt-002L}.}
+6
trees/dt/dt-003G.tree
+6
trees/dt/dt-003G.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Construction}
4
+
\title{Smash products of [cpos](dt-001D)}
5
+
##{A \otimes B = \Set{ (a,b) \in A \times B \mid a \neq \bot \land b \neq \bot } \cup \Set{ \bot_{A\otimes B}}}
6
+
\p{The [ordering](dm-0000) and [lubs](dt-0017) are, \em{mutatis mutandis}, as with the non-strict \ref{dt-0021}. This operator is called a \em{smash product} because the two #{\bot} values from #{A} and #{B} are "smashed" into one #{\bot} value.}
+6
trees/dt/dt-003H.tree
+6
trees/dt/dt-003H.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Construction}
4
+
\title{Smash sums of [cpos](dt-001D)}
5
+
##{A \oplus B = \Set{ (t,x) \in A + B \mid x \neq \bot } \cup \Set{ \bot_{A\oplus B} }}
6
+
\p{The [ordering](dm-0000) and [lubs](dt-0017) are, \em{mutatis mutandis}, as with the non-strict \ref{dt-0031}. This operator is called a \em{smash sum} because the two #{\bot} values from #{A} and #{B} are "smashed" into one #{\bot} value.}
+6
trees/dt/dt-003I.tree
+6
trees/dt/dt-003I.tree
···
1
+
\title{The [category](dm-000G) #{\mathbf{Cpo_\bot}}}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\p{
5
+
The [category](dm-000G) #{\mathbf{Cpo_\bot}} is the [category](dm-000G) where the objects are [cpos](dt-001D), the morphisms are [\em{strict} continuous functions](dt-003F) between these [cpos](dt-001D), and composition and identity are [as in #{\mathbf{Cpo}}](dt-002B).
6
+
}
+12
trees/dt/dt-003J.tree
+12
trees/dt/dt-003J.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Theorem}
3
+
\title{Isomorphisms with strict constructions}
4
+
\author{liamoc}
5
+
\p{
6
+
The [strict cpo constructions](dt-003E) satisfy \em{all} the usual [isomorphisms](dt-002E), including:
7
+
\ul{
8
+
\li{ #{(A \strictto B) \times (A \strictto C)\;\; \simeq\;\; A \strictto (B\otimes C)}}
9
+
\li{ #{(A \otimes B \strictto C) \;\; \simeq\;\; A \strictto (B \strictto C)}}
10
+
\li{ #{(A \strictto C) \times (B \strictto C)\;\; \simeq\;\; (A\oplus B) \strictto C}}
11
+
}
12
+
}
+9
trees/dt/dt-003K.tree
+9
trees/dt/dt-003K.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{The lifting operator for [cpos](dt-001D)}
4
+
\taxon{Definition}
5
+
\p{
6
+
The \em{lifting operator} #{(\cdot)_\bot} adds a new #{\bot} value to a [cpo](dt-001D). That is, for a [cpo](dt-001D) #{X}:
7
+
##{ X_\bot = X \cup \Set{\bot} \quad \text{(where $\bot \notin X$)}}
8
+
For all #{x \in X} (including #{\bot_X}), our new bottom value #{\bot \sqsubseteq x}.
9
+
}
+11
trees/dt/dt-003L.tree
+11
trees/dt/dt-003L.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\title{Isomorphisms with lifting}
5
+
\p{With [the lifting operator](dt-003K), we can relate the lazy constructions like [product](dt-0021) and [sum](dt-0031) with [strict](dt-000K) constructions like [smash product](dt-003G) and [sum](dt-003H) via [isomorphism](dt-002E):
6
+
\ul{
7
+
\li{ #{A\contto B \simeq A_\bot \strictto B}}
8
+
\li{ #{A + B \;\; \simeq A_\bot \oplus B_\bot}}
9
+
\li{ #{(A \times B)_\bot \simeq A_\bot \otimes B_\bot } }
10
+
}
11
+
}
+2
-1
trees/dt/dt-macros.tree
+2
-1
trees/dt/dt-macros.tree
···
34
34
\def\rparen{\startverb)\stopverb}
35
35
\def\scase[x][y]{\lsquare\x,\y\rsquare}
36
36
\def\op-cl-int[x][y]{\lsquare\x,\y\rparen}
37
-
\def\contto{\twoheadrightarrow}
37
+
\def\contto{\twoheadrightarrow}
38
+
\def\strictto{\mathbin{\circ\startverb\hspace{-0.4em}\stopverb\twoheadrightarrow}}