my forest
add first part of recursive domains
+270
-5
+2
-5
trees/dt/dt-001Y.tree
+2
-5
trees/dt/dt-001Y.tree
···
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
\transclude{dt-0005}
7
7
\transclude{dt-001Z}
8
-
\subtree{
9
-
\taxon{Lecture}
10
-
\title{Recursively Defined Domains}
11
-
\p{todo}
12
-
}
8
+
\transclude{dt-004Z}
13
9
\subtree{
14
10
\taxon{Lecture}
15
11
\title{Scott Domains}
···
41
37
\transclude{dt-004G}
42
38
\transclude{dt-004H}
43
39
\transclude{dt-004I}
40
+
\transclude{dt-004O}
44
41
45
42
\scope{
46
43
\put\transclude/toc{false}
+13
trees/dt/dt-004J.tree
+13
trees/dt/dt-004J.tree
···
1
+
\import{dt-macros}
2
+
\title{Why we need recursively defined domains}
3
+
\author{liamoc}
4
+
\p{ We saw recursive domain equations with higher-order procedures in \ref{dt-0007}, but there are numerous other examples where they come up. }
5
+
\transclude{dt-004L}
6
+
\transclude{dt-004M}
7
+
\p{How can we find solutions to such recursive equations? How can we guarantee the existence of a (least) solution?
8
+
}
9
+
\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).}
10
+
\transclude{dt-004N}
11
+
\p{
12
+
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.
13
+
}
+9
trees/dt/dt-004K.tree
+9
trees/dt/dt-004K.tree
+11
trees/dt/dt-004L.tree
+11
trees/dt/dt-004L.tree
···
1
+
\import{dt-macros}
2
+
\title{Recursive algebraic data types}
3
+
\author{liamoc}
4
+
\p{Suppose we have a language with recursive data types, such as this #{\mathit{List}} type in Haskell-style syntax:
5
+
##{
6
+
\textbf{data}\ \mathit{List} = \mathsf{Nil} \mid \mathsf{Cons}\ (\mathit{Int} \times \mathit{List}) }
7
+
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}):
8
+
##{
9
+
L \simeq \mathbf{1} + (\mathbb{Z}_\bot \times L)
10
+
}
11
+
}
+11
trees/dt/dt-004M.tree
+11
trees/dt/dt-004M.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Untyped higher-order languages}
4
+
\p{
5
+
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.}
6
+
\transclude{dt-004K}
7
+
\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}:
8
+
##{
9
+
D \simeq D\contto D
10
+
}
11
+
}
+13
trees/dt/dt-004N.tree
+13
trees/dt/dt-004N.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Example}
3
+
\author{liamoc}
4
+
\title{Recursive domain equations as endofunctors}
5
+
\p{This recursive equation for lists:
6
+
##{
7
+
L \simeq \mathbf{1} + (\mathbb{Z}_\bot \times L)
8
+
}
9
+
Can be expressed as the least fixed point of this mapping (specifically an [endofunctor](dt-004T)) #{\mathcal{F}} on [cpos](dt-001D):
10
+
##{
11
+
\mathcal{F}(A) \triangleq \mathbf{1} + (\mathbb{Z}_\bot \times A)
12
+
}
13
+
}
+23
trees/dt/dt-004O.tree
+23
trees/dt/dt-004O.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{From a cpo to the [category #{\mathbf{Cpo}}](dt-002B)}
4
+
\problemblock{
5
+
\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.}
6
+
}
7
+
\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}.}
8
+
\scope{
9
+
\put\transclude/toc{false}
10
+
\put\transclude/numbered{false}
11
+
\subtree{
12
+
\title{Initiality}
13
+
\taxon{Categorical Aside}
14
+
\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.}
15
+
}
16
+
}
17
+
\transclude{dt-004P}
18
+
\transclude{dt-004T}
19
+
\transclude{dt-004U}
20
+
\transclude{dt-004V}
21
+
\transclude{dt-004W}
22
+
\transclude{dt-004X}
23
+
\transclude{dt-004Y}
+6
trees/dt/dt-004P.tree
+6
trees/dt/dt-004P.tree
+11
trees/dt/dt-004Q.tree
+11
trees/dt/dt-004Q.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\title{#{\omega}-chains of cpos in the category #{\mathbf{Cpo}}}
5
+
\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:}
6
+
\figure{
7
+
\tex{\usepackage{tikz-cd}}{
8
+
\begin{tikzcd}
9
+
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
10
+
\end{tikzcd}
11
+
}}
+11
trees/dt/dt-004R.tree
+11
trees/dt/dt-004R.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\title{Upper bounds in the category #{\mathbf{Cpo}}}
4
+
\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}}):}
5
+
\figure{\tex{\usepackage{tikz-cd}}{
6
+
\begin{tikzcd}
7
+
& & & A & \\
8
+
& & & & \cdots\\
9
+
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
10
+
\end{tikzcd}
11
+
}}
+17
trees/dt/dt-004S.tree
+17
trees/dt/dt-004S.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\title{Least upper bounds in the category #{\mathbf{Cpo}}}
5
+
\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}}):}
6
+
\figure{
7
+
\tex{\usepackage{tikz-cd}}{
8
+
\begin{tikzcd}
9
+
& & & B & \\
10
+
& & & & \cdots\\
11
+
& & & A \ar[uu,thick,dashed,"k"] & \\
12
+
& & & & \cdots\\
13
+
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
14
+
\end{tikzcd}
15
+
}}
16
+
\p{The least upper bound of such an #{\omega}-chain is also called its \em{colimit}.}
17
+
\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}.}
+10
trees/dt/dt-004T.tree
+10
trees/dt/dt-004T.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{Endofunctors on #{\textbf{Cpo}}}
5
+
\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:}
6
+
\ol{
7
+
\li{If #{f : A \contto B} then #{\mathcal{F}(f) : \mathcal{F}(A)\contto \mathcal{F}(B)} }
8
+
\li{#{\mathcal{F}(\mathsf{id}_A : A\contto A) = \mathsf{id}_{\mathcal{F}(A)} : \mathcal{F}(A)\contto \mathcal{F}(A)}}
9
+
\li{#{\mathcal{F}(f \circ g) = \mathcal{F}(f) \circ \mathcal{F}(g)}}
10
+
}
+6
trees/dt/dt-004U.tree
+6
trees/dt/dt-004U.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Remark}
3
+
\author{liamoc}
4
+
\p{
5
+
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}}.
6
+
}
+22
trees/dt/dt-004V.tree
+22
trees/dt/dt-004V.tree
···
1
+
\import{dt-macros}
2
+
\title{Cocontinuous endofunctors}
3
+
\taxon{Definition}
4
+
\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):
5
+
\figure{
6
+
\tex{\usepackage{tikz-cd}}{
7
+
\begin{tikzcd}
8
+
& & & A & \\
9
+
& & & & \cdots\\
10
+
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
11
+
\end{tikzcd}
12
+
}}
13
+
Then #{\mathcal{F}(A)} is a [colimit](dt-004S) for the following [chain](dt-004Q):
14
+
\figure{
15
+
\tex{\usepackage{tikz-cd}}{
16
+
\begin{tikzcd}[row sep=3.6em]
17
+
& & & \mathcal{F}(A) & \\
18
+
& & & & \cdots\\
19
+
\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
20
+
\end{tikzcd}
21
+
}}
22
+
}
+11
trees/dt/dt-004W.tree
+11
trees/dt/dt-004W.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\title{Fixed points of [endofunctors on #{\mathbf{Cpo}}](dt-004T)}
5
+
\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}. }
6
+
\scope{
7
+
\put\transclude/toc{false}
8
+
\put\transclude/numbered{false}
9
+
\subtree{\taxon{Note}
10
+
\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).
11
+
}}}
+13
trees/dt/dt-004X.tree
+13
trees/dt/dt-004X.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Theorem}
4
+
\title{Fixed point theorem for endofunctors on #{\mathbf{Cpo}}}
5
+
\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):}
6
+
\figure{
7
+
\tex{\usepackage{tikz-cd}}{\begin{tikzcd}[column sep=5.2em]
8
+
\mathbf{1} \ar[r,"\lambda x.\bot"] &
9
+
\mathcal{F}(\mathbf{1}) \ar[r,"\mathcal{F}(\lambda x.\bot)"] &
10
+
\mathcal{F}(\mathcal{F}(\mathbf{1})) \ar[r,"\mathcal{F}(\mathcal{F}(\lambda x.\bot))"] &
11
+
\mathcal{F}(\mathcal{F}(\mathcal{F}(\mathbf{1}))) \ar[r,thick,-,dotted] & \quad
12
+
\end{tikzcd}
13
+
}}
+74
trees/dt/dt-004Y.tree
+74
trees/dt/dt-004Y.tree
···
1
+
\taxon{Example}
2
+
\import{dt-macros}
3
+
\author{liamoc}
4
+
\title{Binary Numbers}
5
+
\p{
6
+
Consider the Haskell-style data type:
7
+
##{
8
+
\textbf{data}\ \mathit{Bin} = \mathsf{Zero}\ \mathit{Bin} \mid \mathsf{Empty} \mid \mathsf{One}\ \mathit{Bin}
9
+
}
10
+
So, e.g. #{\mathsf{One}\ (\mathsf{Zero}\ (\mathsf{One}\ \mathsf{Empty})) : \mathit{Bin}}.}
11
+
\p{ The recursive domain equation is, expressed as a fixed point:
12
+
##{
13
+
B \simeq \mathcal{F}(B)\quad\text{where}\ \mathcal{F}(X) = X + \mathbf{1} + X
14
+
}
15
+
We wish to show that #{\mathcal{F}} is a [cocontinuous endofunctor](dt-004V).}
16
+
\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)). }
17
+
18
+
\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:}
19
+
##{
20
+
\begin{array}{l}
21
+
\mathcal{F}(f) : \mathcal{F}(A)\contto \mathcal{F}(B)\\
22
+
\mathcal{F}(f) \triangleq f + \mathsf{id}_\textbf{1} + f
23
+
\end{array}
24
+
}
25
+
\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):}
26
+
\figure{
27
+
\tex{\usepackage{tikz-cd}}{
28
+
\begin{tikzcd}[column sep=5.2em]
29
+
\mathbf{1} \ar[r,"\lambda x.\bot"] &
30
+
\mathcal{F}(\mathbf{1}) \ar[r,"\mathcal{F}(\lambda x.\bot)"] &
31
+
\mathcal{F}(\mathcal{F}(\mathbf{1})) \ar[r,"\mathcal{F}(\mathcal{F}(\lambda x.\bot))"] &
32
+
\mathcal{F}(\mathcal{F}(\mathcal{F}(\mathbf{1}))) \ar[r,thick,-,dotted] & \quad
33
+
\end{tikzcd}
34
+
}}
35
+
\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. }
36
+
\figure{
37
+
\tex{\usepackage{tikz}}{
38
+
\begin{tikzpicture}
39
+
\node[draw, fill=white, rounded corners] (b1) at (0,0) {$\bot$};
40
+
\draw[->,ultra thick,dotted] (6,1.5) -- (10.5,1.5);
41
+
\draw[fill=white!95!black, rounded corners=2em] (6,-1) -- (10,3.5) -- (2,3.5) -- cycle;
42
+
\draw[fill=white!97!black, rounded corners=2em,dashed] (6,-0.8) -- (8.1,1.5) -- (3.9,1.5) -- cycle;
43
+
\draw[->,ultra thick] (2,0.5) -- (4.8,0.5);
44
+
\draw[fill=white!97!black, rounded corners=2em] (2,-0.8) -- (3.8,1.5) -- (0.2,1.5) -- cycle;
45
+
\node[draw, fill=white, dashed, rounded corners] (b2) at (2,0) {$\bot$};
46
+
\draw[->,ultra thick] (b1) -- (b2);
47
+
\node (a1) at (1.2,1) {$\mathsf{Z}(\bot)$};
48
+
\node (a2) at (2,1.04) {$\mathsf{E}$};
49
+
\node (a3) at (2.8,1) {$\mathsf{O}(\bot)$};
50
+
\draw[-] (b2) -- (a2);
51
+
\draw[-] (b2) -- (a3);
52
+
\draw[-] (b2) -- (a1);
53
+
\node (b2) at (6,0) {$\bot$};
54
+
\node (a1) at (5,1) {$\mathsf{Z}(\bot)$};
55
+
\node (a2) at (6,1.04) {$\mathsf{E}$};
56
+
\node (a3) at (7,1) {$\mathsf{O}(\bot)$};
57
+
\draw[-] (b2) -- (a2);
58
+
\draw[-] (b2) -- (a3);
59
+
\draw[-] (b2) -- (a1);
60
+
\node (c1) at (3.3,3) {\footnotesize $\mathsf{Z}(\mathsf{Z}(\bot))$};
61
+
\node (c2) at (4.3,3) {\footnotesize $\mathsf{Z}(\mathsf{E})$};
62
+
\node (c3) at (5.3,3) {\footnotesize $\mathsf{Z}(\mathsf{O}(\bot))$};
63
+
\draw[-] (a1) -- (c2);
64
+
\draw[-] (a1) -- (c3);
65
+
\draw[-] (a1) -- (c1);
66
+
\node (c1) at (6.7,3) {\footnotesize $\mathsf{O}(\mathsf{Z}(\bot))$};
67
+
\node (c2) at (7.7,3) {\footnotesize $\mathsf{O}(\mathsf{E})$};
68
+
\node (c3) at (8.7,3) {\footnotesize $\mathsf{O}(\mathsf{O}(\bot))$}; \draw[-] (a3) -- (c2);
69
+
\draw[-] (a3) -- (c3);
70
+
\draw[-] (a3) -- (c1);
71
+
\end{tikzpicture}
72
+
}}
73
+
\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!).
74
+
}
+7
trees/dt/dt-004Z.tree
+7
trees/dt/dt-004Z.tree
···
1
+
\taxon{Lecture}
2
+
\author{liamoc}
3
+
\title{Recursively Defined Domains}
4
+
\p{This lecture is based on material from [[haskellhutt]], [[jlongley]],[[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
5
+
\transclude{dt-004J}
6
+
\transclude{dt-004O}
7
+
\p{\strong{TODO: Retraction pairs stuff}}