From 57e6298ef51b6e83e9315e4fe9871aa82fd63cc3 Mon Sep 17 00:00:00 2001 From: Liam O'Connor Date: Wed, 14 May 2025 01:25:47 +1000 Subject: [PATCH] add first part of recursive domains --- trees/dt/dt-001Y.tree | 7 ++-- trees/dt/dt-004J.tree | 13 ++++++++ trees/dt/dt-004K.tree | 9 ++++++ trees/dt/dt-004L.tree | 11 +++++++ trees/dt/dt-004M.tree | 11 +++++++ trees/dt/dt-004N.tree | 13 ++++++++ trees/dt/dt-004O.tree | 23 ++++++++++++++ trees/dt/dt-004P.tree | 6 ++++ trees/dt/dt-004Q.tree | 11 +++++++ trees/dt/dt-004R.tree | 11 +++++++ trees/dt/dt-004S.tree | 17 ++++++++++ trees/dt/dt-004T.tree | 10 ++++++ trees/dt/dt-004U.tree | 6 ++++ trees/dt/dt-004V.tree | 22 +++++++++++++ trees/dt/dt-004W.tree | 11 +++++++ trees/dt/dt-004X.tree | 13 ++++++++ trees/dt/dt-004Y.tree | 74 +++++++++++++++++++++++++++++++++++++++++++ trees/dt/dt-004Z.tree | 7 ++++ 18 files changed, 270 insertions(+), 5 deletions(-) create mode 100644 trees/dt/dt-004J.tree create mode 100644 trees/dt/dt-004K.tree create mode 100644 trees/dt/dt-004L.tree create mode 100644 trees/dt/dt-004M.tree create mode 100644 trees/dt/dt-004N.tree create mode 100644 trees/dt/dt-004O.tree create mode 100644 trees/dt/dt-004P.tree create mode 100644 trees/dt/dt-004Q.tree create mode 100644 trees/dt/dt-004R.tree create mode 100644 trees/dt/dt-004S.tree create mode 100644 trees/dt/dt-004T.tree create mode 100644 trees/dt/dt-004U.tree create mode 100644 trees/dt/dt-004V.tree create mode 100644 trees/dt/dt-004W.tree create mode 100644 trees/dt/dt-004X.tree create mode 100644 trees/dt/dt-004Y.tree create mode 100644 trees/dt/dt-004Z.tree diff --git a/trees/dt/dt-001Y.tree b/trees/dt/dt-001Y.tree index 94e6181..d49ff31 100644 --- a/trees/dt/dt-001Y.tree +++ b/trees/dt/dt-001Y.tree @@ -5,11 +5,7 @@ \p{These lecture notes are based on the material I used to teach the [[typesig-dt]] course at the [[uoe]] in 2024.} \transclude{dt-0005} \transclude{dt-001Z} -\subtree{ -\taxon{Lecture} -\title{Recursively Defined Domains} -\p{todo} -} +\transclude{dt-004Z} \subtree{ \taxon{Lecture} \title{Scott Domains} @@ -41,6 +37,7 @@ \transclude{dt-004G} \transclude{dt-004H} \transclude{dt-004I} +\transclude{dt-004O} \scope{ \put\transclude/toc{false} diff --git a/trees/dt/dt-004J.tree b/trees/dt/dt-004J.tree new file mode 100644 index 0000000..cfee1c2 --- /dev/null +++ b/trees/dt/dt-004J.tree @@ -0,0 +1,13 @@ +\import{dt-macros} +\title{Why we need recursively defined domains} +\author{liamoc} +\p{ We saw recursive domain equations with higher-order procedures in \ref{dt-0007}, but there are numerous other examples where they come up. } +\transclude{dt-004L} +\transclude{dt-004M} +\p{How can we find solutions to such recursive equations? How can we guarantee the existence of a (least) solution? +} +\p{We can start by generalising [the fixed point approach](dt-001I) we used for values (i.e. elements of [cpos](dt-001D)) to domains (i.e. [cpos](dt-001D) themselves).} +\transclude{dt-004N} +\p{ +To ensure that least fixed points exist, and to give us a means of finding them, we must now generalise all of the concepts we used for least fixed points on values ([information ordering](dt-000B), [least upper bounds](dt-0017), [continuity](dt-001J) etc.) to domains themselves. +} \ No newline at end of file diff --git a/trees/dt/dt-004K.tree b/trees/dt/dt-004K.tree new file mode 100644 index 0000000..c90c1c7 --- /dev/null +++ b/trees/dt/dt-004K.tree @@ -0,0 +1,9 @@ +\taxon{Definition} +\title{Untyped #{\lambda}-calculus} +\author{liamoc} +\p{ + Untyped #{\lambda}-calculus consists only of untyped (higher-order) functions: + ##{ + e \; \Coloneqq \; x \mid \lambda x. e \mid e_1\ e_2 +} +} \ No newline at end of file diff --git a/trees/dt/dt-004L.tree b/trees/dt/dt-004L.tree new file mode 100644 index 0000000..cdba6b9 --- /dev/null +++ b/trees/dt/dt-004L.tree @@ -0,0 +1,11 @@ +\import{dt-macros} +\title{Recursive algebraic data types} +\author{liamoc} +\p{Suppose we have a language with recursive data types, such as this #{\mathit{List}} type in Haskell-style syntax: +##{ +\textbf{data}\ \mathit{List} = \mathsf{Nil} \mid \mathsf{Cons}\ (\mathit{Int} \times \mathit{List}) } +As in [PCF](dt-003T), the denotation of a type #{\tau} is the domain which contains all the denotations of all closed expressions of type #{\tau}. What, then, is the domain that corresponds to #{\mathit{List}\ a}? We need a [cpo](dt-001D) #{L} that satisfies the below equation (where #{\mathbf{1}} is the [cpo](dt-001D) containing just one element #{\bot}): +##{ +L \simeq \mathbf{1} + (\mathbb{Z}_\bot \times L) +} +} \ No newline at end of file diff --git a/trees/dt/dt-004M.tree b/trees/dt/dt-004M.tree new file mode 100644 index 0000000..371c1bc --- /dev/null +++ b/trees/dt/dt-004M.tree @@ -0,0 +1,11 @@ +\import{dt-macros} +\author{liamoc} +\title{Untyped higher-order languages} +\p{ + If we take [PCF](dt-003T), \em{discard} the type system, #{\syn{fix}}, natural number primitives and any other superfluous features, and just boil our language down to a minimal, Turing-complete subset, we end up with the [untyped #{\lambda}-calculus](dt-004K) — a language consisting only of untyped functions.} +\transclude{dt-004K} +\p{Trying to give a semantics to the [untyped #{\lambda} calculus](dt-004K) poses an issue: we can no longer rely on the type of an expression to select an appropriate semantic domain. Instead, we we must pick a \em{single} domain #{D} which, since functions can be applied to themselves, must apparently include the set of functions #{D \contto D}: +##{ +D \simeq D\contto D +} +} diff --git a/trees/dt/dt-004N.tree b/trees/dt/dt-004N.tree new file mode 100644 index 0000000..ac5953a --- /dev/null +++ b/trees/dt/dt-004N.tree @@ -0,0 +1,13 @@ +\import{dt-macros} +\taxon{Example} +\author{liamoc} +\title{Recursive domain equations as endofunctors} +\p{This recursive equation for lists: +##{ +L \simeq \mathbf{1} + (\mathbb{Z}_\bot \times L) +} +Can be expressed as the least fixed point of this mapping (specifically an [endofunctor](dt-004T)) #{\mathcal{F}} on [cpos](dt-001D): +##{ +\mathcal{F}(A) \triangleq \mathbf{1} + (\mathbb{Z}_\bot \times A) +} +} \ No newline at end of file diff --git a/trees/dt/dt-004O.tree b/trees/dt/dt-004O.tree new file mode 100644 index 0000000..14ef8cf --- /dev/null +++ b/trees/dt/dt-004O.tree @@ -0,0 +1,23 @@ +\import{dt-macros} +\author{liamoc} +\title{From a cpo to the [category #{\mathbf{Cpo}}](dt-002B)} +\problemblock{ + \p{The following definitions are \strong{insufficient} when using [function](dt-002L) constructions in our domain equations (#{\contto} and #{\strictto}), but it will suffice for our purposes for now.} +} +\p{Let us say (for now) that a [cpo](dt-001D) #{A} \em{approximates} a [cpo](dt-001D) #{B} (i.e. #{A \sqsubseteq B}) iff there is a [continuous function](dt-001J) #{f : A\contto B}. Then, there is a least element for this ordering: the one-element [cpo](dt-001D) #{\mathbf{1} = \Set{ \bot }}, as the [continuous function](dt-001J) #{(\lambda x. \bot) : \mathbf{1} \contto A} exists for any [cpo](dt-001D) #{A}.} +\scope{ +\put\transclude/toc{false} +\put\transclude/numbered{false} +\subtree{ +\title{Initiality} +\taxon{Categorical Aside} +\p{The [category #{\mathbf{Cpo}}](dt-002B) has no initial object. The [cpo](dt-001D) #{\mathbf{1}} is terminal; but also serves as a "pseudo" initial object due to the above.} +} +} +\transclude{dt-004P} +\transclude{dt-004T} +\transclude{dt-004U} +\transclude{dt-004V} +\transclude{dt-004W} +\transclude{dt-004X} +\transclude{dt-004Y} \ No newline at end of file diff --git a/trees/dt/dt-004P.tree b/trees/dt/dt-004P.tree new file mode 100644 index 0000000..4073282 --- /dev/null +++ b/trees/dt/dt-004P.tree @@ -0,0 +1,6 @@ +\import{dt-macros} +\author{liamoc} +\title{Colimits in the [category #{\mathbf{Cpo}}](dt-002B)} +\transclude{dt-004Q} +\transclude{dt-004R} +\transclude{dt-004S} \ No newline at end of file diff --git a/trees/dt/dt-004Q.tree b/trees/dt/dt-004Q.tree new file mode 100644 index 0000000..ea7dddd --- /dev/null +++ b/trees/dt/dt-004Q.tree @@ -0,0 +1,11 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Definition} +\title{#{\omega}-chains of cpos in the category #{\mathbf{Cpo}}} +\p{An [#{\omega}-chain](dt-000W) of [cpos](dt-001D) in the [category #{\mathbf{Cpo}}](dt-002B) consists of a family of [cpos](dt-001D) #{\Set{A_i \mid i \in \mathbb{N} }}, together with a family of [continuous functions](dt-001J) #{\Set{ f_i : A_i\contto A_{i+1} \mid i \in \mathbb{N}}}, shown below:} +\figure{ +\tex{\usepackage{tikz-cd}}{ +\begin{tikzcd} + A_0 \ar[r,thick,"f_0"'] & A_1 \ar[r,thick,"f_1"'] & A_2 \ar[r,thick,"f_2"'] & A_3 \ar[r,thick,-,dotted] & \quad +\end{tikzcd} +}} diff --git a/trees/dt/dt-004R.tree b/trees/dt/dt-004R.tree new file mode 100644 index 0000000..0165939 --- /dev/null +++ b/trees/dt/dt-004R.tree @@ -0,0 +1,11 @@ +\import{dt-macros} +\taxon{Definition} +\title{Upper bounds in the category #{\mathbf{Cpo}}} +\p{A [cpo](dt-001D) #{A} is an [upper bound](dm-000C) of an [#{\omega}-chain of cpos](dt-004Q) in [the category #{\mathbf{Cpo}}](dt-002B) if there is a family of [continuous functions](dt-001J) #{\Set{g_i : A_i \contto A \mid i \in \mathbb{N}}} such that the following diagram commutes (i.e. #{g_i = g_{i+1} \circ f_i} for all #{i \in \mathbb{N}}):} +\figure{\tex{\usepackage{tikz-cd}}{ +\begin{tikzcd} +& & & A & \\ +& & & & \cdots\\ + A_0 \ar[r,thick,"f_0"'] \ar[uurrr,"g_0"near start] & A_1 \ar[r,thick,"f_1"']\ar[uurr,"g_1"near start] & A_2 \ar[r,thick,"f_2"'] \ar[uur,"g_2"near start] & A_3 \ar[uu,"g_3"near start] \ar[r,thick,-,dotted] & \quad +\end{tikzcd} +}} \ No newline at end of file diff --git a/trees/dt/dt-004S.tree b/trees/dt/dt-004S.tree new file mode 100644 index 0000000..26e7096 --- /dev/null +++ b/trees/dt/dt-004S.tree @@ -0,0 +1,17 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Definition} +\title{Least upper bounds in the category #{\mathbf{Cpo}}} +\p{A [cpo](dt-001D) #{A} is the [\em{least} upper bound](dt-0017) of an [#{\omega}-chain of cpos](dt-004Q) if is both an [upper bound](dt-004R) and if there exists a \em{unique} #{k} for any other [upper bound](dt-004R) #{B} such that the following diagram commutes (i.e. #{h_i = g_i \circ k} for all #{i \in \mathbb{N}}):} +\figure{ +\tex{\usepackage{tikz-cd}}{ +\begin{tikzcd} +& & & B & \\ +& & & & \cdots\\ +& & & A \ar[uu,thick,dashed,"k"] & \\ +& & & & \cdots\\ + A_0 \ar[r,thick,"f_0"'] \ar[uuuurrr,"h_0", bend left] \ar[uurrr,"g_0"near start] & A_1 \ar[r,thick,"f_1"']\ar[uurr,"g_1"near start]\ar[uuuurr,"h_1", bend left] & A_2 \ar[r,thick,"f_2"'] \ar[uur,"g_2"near start] \ar[uuuur,"h_2", bend left] & A_3 \ar[uu,"g_3"near start] \ar[r,thick,-,dotted] \ar[uuuu,"h_3", bend left=3.5em] & \quad +\end{tikzcd} +}} +\p{The least upper bound of such an #{\omega}-chain is also called its \em{colimit}.} +\p{\strong{Note}: Uniqueness of lubs is up to isomorphism. That is, if #{A} and #{B} are both colimits of our #{\omega}-chain, then #{A \simeq B}.} diff --git a/trees/dt/dt-004T.tree b/trees/dt/dt-004T.tree new file mode 100644 index 0000000..42b790b --- /dev/null +++ b/trees/dt/dt-004T.tree @@ -0,0 +1,10 @@ +\import{dt-macros} +\taxon{Definition} +\author{liamoc} +\title{Endofunctors on #{\textbf{Cpo}}} +\p{An \em{endofunctor} on [the category #{\textbf{Cpo}}](dt-002B) is a [functor](dm-000J) #{\textbf{Cpo} \rightarrow \textbf{Cpo}}, i.e. a mapping #{\mathcal{F}} on [cpos](dt-001D) together with a mapping #{\mathcal{F}} on [continuous functions](dt-001J), such that:} +\ol{ +\li{If #{f : A \contto B} then #{\mathcal{F}(f) : \mathcal{F}(A)\contto \mathcal{F}(B)} } +\li{#{\mathcal{F}(\mathsf{id}_A : A\contto A) = \mathsf{id}_{\mathcal{F}(A)} : \mathcal{F}(A)\contto \mathcal{F}(A)}} +\li{#{\mathcal{F}(f \circ g) = \mathcal{F}(f) \circ \mathcal{F}(g)}} +} diff --git a/trees/dt/dt-004U.tree b/trees/dt/dt-004U.tree new file mode 100644 index 0000000..e8a3b56 --- /dev/null +++ b/trees/dt/dt-004U.tree @@ -0,0 +1,6 @@ +\import{dt-macros} +\taxon{Remark} +\author{liamoc} +\p{ +Observe that, given the [information ordering for cpos](dt-004O) where #{A \sqsubseteq B} if there exists a continuous function #{A \contto B}, the [functor](dm-000J) laws necessarily imply [monotonicity](dt-000J) for all [endofunctors](dt-004T) #{\mathcal{F}}. +} \ No newline at end of file diff --git a/trees/dt/dt-004V.tree b/trees/dt/dt-004V.tree new file mode 100644 index 0000000..3ed8432 --- /dev/null +++ b/trees/dt/dt-004V.tree @@ -0,0 +1,22 @@ +\import{dt-macros} +\title{Cocontinuous endofunctors} +\taxon{Definition} +\p{An [endofunctor](dt-004T) #{\mathcal{F}} is \em{cocontinuous} iff it preserves [colimits](dt-004S) of [#{\omega}-chains of cpos](dt-004Q). That is, given a [chain](dt-004Q) where #{A} is a [colimit](dt-004S): +\figure{ +\tex{\usepackage{tikz-cd}}{ +\begin{tikzcd} +& & & A & \\ +& & & & \cdots\\ + A_0 \ar[r,thick,"f_0"'] \ar[uurrr,"g_0"near start] & A_1 \ar[r,thick,"f_1"']\ar[uurr,"g_1"near start] & A_2 \ar[r,thick,"f_2"'] \ar[uur,"g_2"near start] & A_3 \ar[uu,"g_3"near start] \ar[r,thick,-,dotted] & \quad +\end{tikzcd} +}} +Then #{\mathcal{F}(A)} is a [colimit](dt-004S) for the following [chain](dt-004Q): +\figure{ +\tex{\usepackage{tikz-cd}}{ +\begin{tikzcd}[row sep=3.6em] +& & & \mathcal{F}(A) & \\ +& & & & \cdots\\ + \mathcal{F}(A_0) \ar[r,thick,"\mathcal{F}(f_0)"',->] \ar[uurrr,"\mathcal{F}(g_0)"near start] & \mathcal{F}(A_1) \ar[r,thick,"\mathcal{F}(f_1)"',->]\ar[uurr,"\mathcal{F}(g_1)"near start] & \mathcal{F}(A_2) \ar[r,thick,"\mathcal{F}(f_2)"',->] \ar[uur,"\mathcal{F}(g_2)"near start] & \mathcal{F}(A_3) \ar[uu,"\mathcal{F}(g_3)"near start] \ar[r,thick,-,dotted] & \quad +\end{tikzcd} +}} +} \ No newline at end of file diff --git a/trees/dt/dt-004W.tree b/trees/dt/dt-004W.tree new file mode 100644 index 0000000..ef9af80 --- /dev/null +++ b/trees/dt/dt-004W.tree @@ -0,0 +1,11 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Definition} +\title{Fixed points of [endofunctors on #{\mathbf{Cpo}}](dt-004T)} +\p{A [fixed point](dt-000S) of an [endofunctor on cpos](dt-004T) #{\mathcal{F}} is a [cpo](dt-001D) #{\mathcal{F}} such that #{\mathcal{F}(A) \simeq A}. } +\scope{ +\put\transclude/toc{false} +\put\transclude/numbered{false} +\subtree{\taxon{Note} +\p{In Scott's approach, which we follow here, our fixed points are up to [isomorphism](dt-002E) (suitable for languages with \em{isorecursive} types), but there are other approaches where they are equalities (suitable for languages with \em{equirecursive} types). +}}} \ No newline at end of file diff --git a/trees/dt/dt-004X.tree b/trees/dt/dt-004X.tree new file mode 100644 index 0000000..71b25cb --- /dev/null +++ b/trees/dt/dt-004X.tree @@ -0,0 +1,13 @@ +\import{dt-macros} +\author{liamoc} +\taxon{Theorem} +\title{Fixed point theorem for endofunctors on #{\mathbf{Cpo}}} +\p{ Every [cocontinuous endofunctor](dt-004V) #{\mathcal{F}} on [cpos](dt-001D) has a [least fixed point](dt-004W), given by the [colimit](dt-004S) of the [#{\omega}-chain](dt-004Q):} +\figure{ +\tex{\usepackage{tikz-cd}}{\begin{tikzcd}[column sep=5.2em] + \mathbf{1} \ar[r,"\lambda x.\bot"] & + \mathcal{F}(\mathbf{1}) \ar[r,"\mathcal{F}(\lambda x.\bot)"] & + \mathcal{F}(\mathcal{F}(\mathbf{1})) \ar[r,"\mathcal{F}(\mathcal{F}(\lambda x.\bot))"] & + \mathcal{F}(\mathcal{F}(\mathcal{F}(\mathbf{1}))) \ar[r,thick,-,dotted] & \quad +\end{tikzcd} +}} diff --git a/trees/dt/dt-004Y.tree b/trees/dt/dt-004Y.tree new file mode 100644 index 0000000..2b474f6 --- /dev/null +++ b/trees/dt/dt-004Y.tree @@ -0,0 +1,74 @@ +\taxon{Example} +\import{dt-macros} +\author{liamoc} +\title{Binary Numbers} +\p{ +Consider the Haskell-style data type: +##{ +\textbf{data}\ \mathit{Bin} = \mathsf{Zero}\ \mathit{Bin} \mid \mathsf{Empty} \mid \mathsf{One}\ \mathit{Bin} +} +So, e.g. #{\mathsf{One}\ (\mathsf{Zero}\ (\mathsf{One}\ \mathsf{Empty})) : \mathit{Bin}}.} +\p{ The recursive domain equation is, expressed as a fixed point: +##{ +B \simeq \mathcal{F}(B)\quad\text{where}\ \mathcal{F}(X) = X + \mathbf{1} + X +} +We wish to show that #{\mathcal{F}} is a [cocontinuous endofunctor](dt-004V).} +\p{We have a mapping #{\mathcal{F}} on [cpos](dt-001D) (objects of [the category #{\textbf{Cpo}}](dt-002B)), but for it to be a [functor](dm-000J) we additionally need a mapping #{\mathcal{F}} on [continuous functions](dt-001J) (morphisms of [the category #{\textbf{Cpo}}](dt-002B)). } + +\p{Recalling [our sum construction](dt-0031), we may remember that sums are already a [bifunctor](dm-000M) #{\textbf{Cpo} \times \textbf{Cpo} \rightarrow \textbf{Cpo}} (\ref{dt-0038}). Thus, our mapping on [continuous functions](dt-001J) #{\mathcal{F}} can be \em{derived} from our mapping on [cpos](dt-001D) #{\mathcal{F}} by using the morphism mapping from the sum construction (\ref{dt-0037}). Given a continuous function #{f : A \contto B}, our morphism mapping is:} +##{ +\begin{array}{l} +\mathcal{F}(f) : \mathcal{F}(A)\contto \mathcal{F}(B)\\ +\mathcal{F}(f) \triangleq f + \mathsf{id}_\textbf{1} + f +\end{array} +} +\p{Proof that this [endofunctor](dt-004T) is [cocontinuous](dt-004V) is left for the reader. Hence the semantics of the type #{\mathit{Bin}}, i.e. #{\llbracket \mathit{Bin} \rrbracket : \textbf{Cpo}} is the least fixed point of #{\mathcal{F}}, i.e. the [colimit](dt-004S) of the [#{\omega}-chain](dt-004Q):} +\figure{ +\tex{\usepackage{tikz-cd}}{ +\begin{tikzcd}[column sep=5.2em] + \mathbf{1} \ar[r,"\lambda x.\bot"] & + \mathcal{F}(\mathbf{1}) \ar[r,"\mathcal{F}(\lambda x.\bot)"] & + \mathcal{F}(\mathcal{F}(\mathbf{1})) \ar[r,"\mathcal{F}(\mathcal{F}(\lambda x.\bot))"] & + \mathcal{F}(\mathcal{F}(\mathcal{F}(\mathbf{1}))) \ar[r,thick,-,dotted] & \quad +\end{tikzcd} +}} +\p{Let us visualise this chain. Here the sum injections have been written as #{\textsf{Z, E, O}} rather than (combinations of) #{\textsf{inl}} and #{\textsf{inr}} to keep the connection with the Haskell data type clear. } +\figure{ +\tex{\usepackage{tikz}}{ +\begin{tikzpicture} + \node[draw, fill=white, rounded corners] (b1) at (0,0) {$\bot$}; + \draw[->,ultra thick,dotted] (6,1.5) -- (10.5,1.5); + \draw[fill=white!95!black, rounded corners=2em] (6,-1) -- (10,3.5) -- (2,3.5) -- cycle; + \draw[fill=white!97!black, rounded corners=2em,dashed] (6,-0.8) -- (8.1,1.5) -- (3.9,1.5) -- cycle; + \draw[->,ultra thick] (2,0.5) -- (4.8,0.5); + \draw[fill=white!97!black, rounded corners=2em] (2,-0.8) -- (3.8,1.5) -- (0.2,1.5) -- cycle; + \node[draw, fill=white, dashed, rounded corners] (b2) at (2,0) {$\bot$}; + \draw[->,ultra thick] (b1) -- (b2); + \node (a1) at (1.2,1) {$\mathsf{Z}(\bot)$}; + \node (a2) at (2,1.04) {$\mathsf{E}$}; + \node (a3) at (2.8,1) {$\mathsf{O}(\bot)$}; + \draw[-] (b2) -- (a2); + \draw[-] (b2) -- (a3); + \draw[-] (b2) -- (a1); + \node (b2) at (6,0) {$\bot$}; + \node (a1) at (5,1) {$\mathsf{Z}(\bot)$}; + \node (a2) at (6,1.04) {$\mathsf{E}$}; + \node (a3) at (7,1) {$\mathsf{O}(\bot)$}; + \draw[-] (b2) -- (a2); + \draw[-] (b2) -- (a3); + \draw[-] (b2) -- (a1); + \node (c1) at (3.3,3) {\footnotesize $\mathsf{Z}(\mathsf{Z}(\bot))$}; + \node (c2) at (4.3,3) {\footnotesize $\mathsf{Z}(\mathsf{E})$}; + \node (c3) at (5.3,3) {\footnotesize $\mathsf{Z}(\mathsf{O}(\bot))$}; + \draw[-] (a1) -- (c2); + \draw[-] (a1) -- (c3); + \draw[-] (a1) -- (c1); + \node (c1) at (6.7,3) {\footnotesize $\mathsf{O}(\mathsf{Z}(\bot))$}; + \node (c2) at (7.7,3) {\footnotesize $\mathsf{O}(\mathsf{E})$}; + \node (c3) at (8.7,3) {\footnotesize $\mathsf{O}(\mathsf{O}(\bot))$}; \draw[-] (a3) -- (c2); + \draw[-] (a3) -- (c3); + \draw[-] (a3) -- (c1); +\end{tikzpicture} +}} +\p{Thus, the #{n}th cpo in the chain contains binary numbers with at most #{n} defined digits. The [colimit](dt-004S) of the chain contains all binary numbers (finite, partial, and infinite!). +} \ No newline at end of file diff --git a/trees/dt/dt-004Z.tree b/trees/dt/dt-004Z.tree new file mode 100644 index 0000000..493ec3a --- /dev/null +++ b/trees/dt/dt-004Z.tree @@ -0,0 +1,7 @@ +\taxon{Lecture} +\author{liamoc} +\title{Recursively Defined Domains} +\p{This lecture is based on material from [[haskellhutt]], [[jlongley]],[[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].} +\transclude{dt-004J} +\transclude{dt-004O} +\p{\strong{TODO: Retraction pairs stuff}} \ No newline at end of file -- 2.51.2