From bf8561a844fd71122305c31f9fa87131d052f1ee Mon Sep 17 00:00:00 2001 From: Liam O'Connor Date: Fri, 18 Apr 2025 07:14:53 +1000 Subject: [PATCH] strict constructions --- trees/dt/dt-001Z.tree | 4 +--- trees/dt/dt-0038.tree | 7 ++----- trees/dt/dt-003E.tree | 15 +++++++++++++++ trees/dt/dt-003F.tree | 6 ++++++ trees/dt/dt-003G.tree | 6 ++++++ trees/dt/dt-003H.tree | 6 ++++++ trees/dt/dt-003I.tree | 6 ++++++ trees/dt/dt-003J.tree | 12 ++++++++++++ trees/dt/dt-003K.tree | 9 +++++++++ trees/dt/dt-003L.tree | 11 +++++++++++ trees/dt/dt-macros.tree | 3 ++- 11 files changed, 76 insertions(+), 9 deletions(-) create mode 100644 trees/dt/dt-003E.tree create mode 100644 trees/dt/dt-003F.tree create mode 100644 trees/dt/dt-003G.tree create mode 100644 trees/dt/dt-003H.tree create mode 100644 trees/dt/dt-003I.tree create mode 100644 trees/dt/dt-003J.tree create mode 100644 trees/dt/dt-003K.tree create mode 100644 trees/dt/dt-003L.tree diff --git a/trees/dt/dt-001Z.tree b/trees/dt/dt-001Z.tree index 5186bcd..9a1ee83 100644 --- a/trees/dt/dt-001Z.tree +++ b/trees/dt/dt-001Z.tree @@ -7,9 +7,7 @@ \transclude{dt-002K} \transclude{dt-002Z} \transclude{dt-0030} -\subtree{ -\title{Strict Constructions} -} +\transclude{dt-003E} \subtree{ \title{PCF} } diff --git a/trees/dt/dt-0038.tree b/trees/dt/dt-0038.tree index a2cecd7..6ab3b2c 100644 --- a/trees/dt/dt-0038.tree +++ b/trees/dt/dt-0038.tree @@ -1,8 +1,5 @@ \import{dt-macros} \author{liamoc} -\taxon{Exercise} -\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). -\solnblock{ -\p{TODO} -} +\taxon{Theorem} +\p{#{+ : \mathbf{Cpo} \times \mathbf{Cpo} \rightarrow \mathbf{Cpo}} is a lawful [bifunctor](dm-000M). } diff --git a/trees/dt/dt-003E.tree b/trees/dt/dt-003E.tree new file mode 100644 index 0000000..073eda4 --- /dev/null +++ b/trees/dt/dt-003E.tree @@ -0,0 +1,15 @@ +\import{dt-macros} +\author{liamoc} +\title{Strict Constructions} +\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.} +\transclude{dt-003F} +\transclude{dt-003G} +\transclude{dt-003H} +\transclude{dt-003J} +\transclude{dt-003I} +\upshotblock{ + [[dt-003I]] has products, exponentials, \em{and sums} (as it doesn't suffer from the [problem](dt-0039) that #{\textbf{Cpo}} does). +} +\transclude{dt-003K} +\transclude{dt-003L} + diff --git a/trees/dt/dt-003F.tree b/trees/dt/dt-003F.tree new file mode 100644 index 0000000..f7b1128 --- /dev/null +++ b/trees/dt/dt-003F.tree @@ -0,0 +1,6 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Construction} +\title{The [cpo](dt-001D) of [strict](dt-000K) [continuous](dt-001J) functions} +##{A \strictto B = \Set{ f \in A \contto B \mid f(\bot) = \bot }} +\p{The [ordering](dm-0000) and [lubs](dt-0017) are, \em{mutatis mutandis}, as with the non-strict \ref{dt-002L}.} diff --git a/trees/dt/dt-003G.tree b/trees/dt/dt-003G.tree new file mode 100644 index 0000000..02f77b6 --- /dev/null +++ b/trees/dt/dt-003G.tree @@ -0,0 +1,6 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Construction} +\title{Smash products of [cpos](dt-001D)} +##{A \otimes B = \Set{ (a,b) \in A \times B \mid a \neq \bot \land b \neq \bot } \cup \Set{ \bot_{A\otimes B}}} +\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.} diff --git a/trees/dt/dt-003H.tree b/trees/dt/dt-003H.tree new file mode 100644 index 0000000..879b3aa --- /dev/null +++ b/trees/dt/dt-003H.tree @@ -0,0 +1,6 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Construction} +\title{Smash sums of [cpos](dt-001D)} +##{A \oplus B = \Set{ (t,x) \in A + B \mid x \neq \bot } \cup \Set{ \bot_{A\oplus B} }} +\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.} diff --git a/trees/dt/dt-003I.tree b/trees/dt/dt-003I.tree new file mode 100644 index 0000000..de69dd6 --- /dev/null +++ b/trees/dt/dt-003I.tree @@ -0,0 +1,6 @@ +\title{The [category](dm-000G) #{\mathbf{Cpo_\bot}}} +\author{liamoc} +\taxon{Definition} +\p{ + 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). +} \ No newline at end of file diff --git a/trees/dt/dt-003J.tree b/trees/dt/dt-003J.tree new file mode 100644 index 0000000..1b7f8ef --- /dev/null +++ b/trees/dt/dt-003J.tree @@ -0,0 +1,12 @@ +\import{dt-macros} +\taxon{Theorem} +\title{Isomorphisms with strict constructions} +\author{liamoc} +\p{ +The [strict cpo constructions](dt-003E) satisfy \em{all} the usual [isomorphisms](dt-002E), including: +\ul{ +\li{ #{(A \strictto B) \times (A \strictto C)\;\; \simeq\;\; A \strictto (B\otimes C)}} +\li{ #{(A \otimes B \strictto C) \;\; \simeq\;\; A \strictto (B \strictto C)}} +\li{ #{(A \strictto C) \times (B \strictto C)\;\; \simeq\;\; (A\oplus B) \strictto C}} +} +} diff --git a/trees/dt/dt-003K.tree b/trees/dt/dt-003K.tree new file mode 100644 index 0000000..809e4e1 --- /dev/null +++ b/trees/dt/dt-003K.tree @@ -0,0 +1,9 @@ +\import{dt-macros} +\author{liamoc} +\title{The lifting operator for [cpos](dt-001D)} +\taxon{Definition} +\p{ + The \em{lifting operator} #{(\cdot)_\bot} adds a new #{\bot} value to a [cpo](dt-001D). That is, for a [cpo](dt-001D) #{X}: + ##{ X_\bot = X \cup \Set{\bot} \quad \text{(where $\bot \notin X$)}} + For all #{x \in X} (including #{\bot_X}), our new bottom value #{\bot \sqsubseteq x}. +} \ No newline at end of file diff --git a/trees/dt/dt-003L.tree b/trees/dt/dt-003L.tree new file mode 100644 index 0000000..581c3d4 --- /dev/null +++ b/trees/dt/dt-003L.tree @@ -0,0 +1,11 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Theorem} +\title{Isomorphisms with lifting} +\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): +\ul{ +\li{ #{A\contto B \simeq A_\bot \strictto B}} +\li{ #{A + B \;\; \simeq A_\bot \oplus B_\bot}} +\li{ #{(A \times B)_\bot \simeq A_\bot \otimes B_\bot } } +} +} \ No newline at end of file diff --git a/trees/dt/dt-macros.tree b/trees/dt/dt-macros.tree index 13ce132..b974c22 100644 --- a/trees/dt/dt-macros.tree +++ b/trees/dt/dt-macros.tree @@ -34,4 +34,5 @@ \def\rparen{\startverb)\stopverb} \def\scase[x][y]{\lsquare\x,\y\rsquare} \def\op-cl-int[x][y]{\lsquare\x,\y\rparen} -\def\contto{\twoheadrightarrow} \ No newline at end of file +\def\contto{\twoheadrightarrow} +\def\strictto{\mathbin{\circ\startverb\hspace{-0.4em}\stopverb\twoheadrightarrow}} \ No newline at end of file -- 2.51.2