my forest
progress on retraction pairs
+183
-2
+4
trees/dm/dm-000S.tree
+4
trees/dm/dm-000S.tree
···
1
+
\taxon{Definition}
2
+
\author{liamoc}
3
+
\title{Contravariant functor}
4
+
\p{A \em{contravariant} [functor](dm-000J) #{\mathcal{F}} is a [functor](dm-000J) that, instead of associating a morphism #{X \xrightarrow{m} Y} with a morphism #{\mathcal{F}(X) \xrightarrow{\mathcal{F}(m)} \mathcal{F}(Y)}, it instead gives a morphism #{\mathcal{F}(Y) \xrightarrow{\mathcal{F}(m)} \mathcal{F}(X)$}. Alternatively, it can be viewed as a functor from the [dual category](dm-000Q).}
+1
-1
trees/dt/dt-004M.tree
+1
-1
trees/dt/dt-004M.tree
···
2
2
\author{liamoc}
3
3
\title{Untyped higher-order languages}
4
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.}
5
+
If we take [PCF](dt-003T), \em{discard} the type system, [#{\textbf{fix}}](dt-001Q), 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
6
\transclude{dt-004K}
7
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
8
##{
+2
-1
trees/dt/dt-004O.tree
+2
-1
trees/dt/dt-004O.tree
+1
trees/dt/dt-004Z.tree
+1
trees/dt/dt-004Z.tree
+5
trees/dt/dt-0050.tree
+5
trees/dt/dt-0050.tree
···
1
+
\import{dt-macros}
2
+
\title{Constructing endofunctors}
3
+
\author{liamoc}
4
+
\p{If we have a mapping on [cpos](dt-001D) #{\mathcal{F} : \textbf{Cpo} \rightarrow \textbf{Cpo}} that is made up of the primitives #{\times}, #{+}, #{\otimes}, #{\oplus}, #{\mathbf{1}} and #{(\cdot)_\bot}, we can generate a corresponding \em{morphism mapping} on continuous functions #{\mathcal{F} : (A\contto B) \rightarrow (\mathcal{F}(A)\contto \mathcal{F}(B))} by using the corresponding morphism mappings of each of these operators. Thus any such mapping can be turned into an [endofunctor](dt-004T).}
5
+
\transclude{dt-0051}
+11
trees/dt/dt-0051.tree
+11
trees/dt/dt-0051.tree
···
1
+
\import{dt-macros}
2
+
\title{Making endofunctors for algebraic data types}
3
+
\taxon{Example}
4
+
\author{liamoc}
5
+
\p{ ##{
6
+
\begin{array}{llr}
7
+
\textsf{Object mapping} & \textsf{Morphism mapping}\\[0.2em]
8
+
\mathcal{F}(X) = X + \mathbf{1} & \mathcal{F}(f) = f + \mathsf{id}_\mathbf{1} & \quad\quad\text{((co)-natural numbers)} \\
9
+
\mathcal{F}(X) = \mathbf{1} + (\mathbb{Z}_\bot \times X) & \mathcal{F}(f) = \mathsf{id}_\mathbf{1} + (\mathsf{id}_{\mathbb{Z}_\bot} \times f) & \text{((co)-lists of integers)}\\
10
+
\end{array}
11
+
}}
+12
trees/dt/dt-0052.tree
+12
trees/dt/dt-0052.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{From #{\textbf{Cpo}} to #{\textbf{Cpo}^{\textbf{R}}}}
4
+
\transclude{dt-0053}
5
+
\transclude{dt-0054}
6
+
\transclude{dt-0055}
7
+
\transclude{dt-0056}
8
+
\transclude{dt-0057}
9
+
\transclude{dt-0058}
10
+
\transclude{dt-0059}
11
+
\transclude{dt-005A}
12
+
\transclude{dt-005B}
+13
trees/dt/dt-0053.tree
+13
trees/dt/dt-0053.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Problem}
3
+
\author{liamoc}
4
+
\title{Contravariance in the function arrow}
5
+
\p{We cannot get morphism mappings in [the category #{\textbf{Cpo}}](dt-002B) as easily as \ref{dt-0050} when our object mapping makes use of the function operators #{\strictto} and #{\contto}, as they are [contravariant](dm-000S) in their first argument. This means the [functor](dm-000J) that they extend to is not #{\textbf{Cpo} \rightarrow \textbf{Cpo}} but #{\textbf{Cpo}^\textsf{op} \rightarrow \textbf{Cpo}}, where #{\textbf{Cpo}^\textsf{op} } is the [dual category](dm-000Q) of #{\textbf{Cpo}}. The morphisms end up the wrong way around. }
6
+
7
+
\p{As an example, consider #{\mathcal{F}(X) = X\contto\mathbb{Z}_\bot}. Then, recalling [the morphism mapping of the #{\contto} functor](dt-002X):
8
+
##{
9
+
\inferrule{f : A \contto B \quad g : C\contto D}{f\contto g : (B\contto C)\contto (A\contto D)}
10
+
}
11
+
We can generate a morphism mapping for #{\mathcal{F}}: ##{\mathcal{F}(f)\; =\; f\contto\mathsf{id}_{\mathbb{Z}_\bot}\; =\; (\lambda h.\ \mathsf{id}_{\mathbb{Z}_\bot}\circ h \circ f)\; = \;(\lambda h.\ h \circ f) }
12
+
However, this mapping has the wrong type. For #{f : A\contto B}, then #{\mathcal{F}(f) : (B\contto \mathbb{Z}_\bot) \rightarrow (A\contto \mathbb{Z}_\bot)}, which is #{\mathcal{F}(B)\contto\mathcal{F}(A)}, not the required #{\mathcal{F}(A)\contto \mathcal{F}(B)}. This is because the generated functor is [contravariant](dm-000S), not [covariant](dm-000J).
13
+
}
+14
trees/dt/dt-0054.tree
+14
trees/dt/dt-0054.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\title{Retraction pair}
4
+
\author{liamoc}
5
+
\p{A \em{retraction pair} #{(f,g)} on [cpos](dt-001D) #{A} to #{B} consists of two [continuous](dt-001J) functions #{A \rpair{f}{g} B}
6
+
such that:
7
+
\ol{
8
+
\li{#{g \circ f = \mathsf{id}_A\quad} (i.e. #{\forall x \in A.\ g(f(x)) = x })}
9
+
\li{ #{f \circ g \sqsubseteq \mathsf{id}_B\quad} (i.e. #{\forall y \in B.\ f(g(y)) \sqsubseteq y })}
10
+
}
11
+
In this retraction pair, #{f} is called a \em{embedding} and #{g} is called a \em{projection}.
12
+
}
13
+
\p{
14
+
Retraction pairs are weakenings of [isomorphisms](dt-002E). Intuitively, going #{A \contto B\contto A}, all information is \em{preserved} due to requirement 1, but going #{B\contto A\contto B}, we \em{may lose} some information (hence the use of #{\sqsubseteq} in requirement 2). }
+46
trees/dt/dt-0055.tree
+46
trees/dt/dt-0055.tree
···
1
+
\import{dt-macros}
2
+
\import{table-macros}
3
+
\taxon{Example}
4
+
\author{liamoc}
5
+
\title{Examples and counterexamples of retraction pairs}
6
+
\p{Here are two examples of [retraction pairs](dt-0054):
7
+
\figure{
8
+
\tex{\usepackage{tikz-cd}}{
9
+
\begin{tikzcd}
10
+
& z \ar[dl, thick,->] \\
11
+
b \ar[r,thick,<->] & y \ar[u,-] \\
12
+
a\ar[u,-]\ar[r,thick,<->] & x \ar[u,-]
13
+
\end{tikzcd}
14
+
$\quad\qquad\qquad$
15
+
\begin{tikzcd}
16
+
& z \ar[dl, thick,<->] \\
17
+
b & y \ar[dl, thick,->] \ar[u,-] \\
18
+
a\ar[u,-]\ar[r,thick,<->] & x \ar[u,-]
19
+
\end{tikzcd}}}
20
+
(this demonstrates that there can be \em{many} [retraction pairs](dt-0054) #{A \rpair{f}{g} B})}
21
+
\p{The following, however, are \em{not} [retraction pairs](dt-0054) #{A \rpair{f}{g} B}:
22
+
\figure{
23
+
\tableW{\tr{\td{
24
+
\tex{\usepackage{tikz-cd}}{
25
+
\begin{tikzcd}
26
+
& z \ar[dl, thick,<->] \\
27
+
b \ar[r,thick,<-] & y \ar[u,-] \\
28
+
a\ar[u,-]\ar[r,thick,<->] & x \ar[u,-]
29
+
\end{tikzcd}
30
+
}}\td{
31
+
\tex{\usepackage{tikz-cd}}{
32
+
\begin{tikzcd}
33
+
& z \ar[dl, thick,->] \\
34
+
b \ar[dr, thick,->] & y \ar[l, thick,->] \ar[u,-] \\
35
+
a\ar[u,-]\ar[r,thick,<->] & x \ar[u,-]
36
+
\end{tikzcd}
37
+
}}}
38
+
\tr{
39
+
\td{
40
+
(#{y \mapsto b \mapsto z} but #{z \not\sqsubseteq y})
41
+
}
42
+
\td{
43
+
(#{b \mapsto x \mapsto a} but #{a \neq b})
44
+
}
45
+
}
46
+
}}}
+13
trees/dt/dt-0056.tree
+13
trees/dt/dt-0056.tree
···
1
+
\import{dt-macros}
2
+
\title{Composition of retraction pairs}
3
+
\taxon{Definition}
4
+
\author{liamoc}
5
+
\p{We can compose [retraction pairs](dt-0054) by composing their \em{embedding} and \em{projection}:}
6
+
\figure{
7
+
\tex{\usepackage{tikz-cd}\usepackage{amsmath}\usepackage{amssymb}}{
8
+
\begin{tikzcd}
9
+
A \ar[r,"f",yshift=0.2em] & B \ar[l,"g", ,yshift=-0.2em]
10
+
\ar[r,"h",yshift=0.2em] & C \ar[l,"i", ,yshift=-0.2em] &\leadsto &
11
+
A \ar[r,"h \circ f",yshift=0.2em] & C \ar[l,"g \circ i",yshift=-0.2em] &\quad
12
+
\end{tikzcd}
13
+
}}
+10
trees/dt/dt-0057.tree
+10
trees/dt/dt-0057.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Corollary}
3
+
\title{Derived products of retraction pairs}
4
+
\p{It follows from the definition of [retraction pairs](dt-0054) that, for a pair #{\rpair{f}{g}}:
5
+
\ol{
6
+
\li{ #{f} and #{g} are [strict](dt-000K), i.e. #{f(\bot) = \bot} and #{g(\bot) = \bot}.}
7
+
\li{ #{g} is \em{uniquely determined} by #{f} and vice-versa, so if another [retraction pair](dt-0054) #{\rpair{f}{g'}} exists, then #{g = g'}. To see why, remember that #{f} and #{g} must be [continuous](dt-001J) and therefore [monotonic](dt-000J).}
8
+
\li{ #{A} is [isomorphic](dt-002E) to the range of #{f}, i.e. #{A \simeq \Set{ f(x) \mid x \in A} \subseteq B}.}
9
+
}
10
+
}
+5
trees/dt/dt-0058.tree
+5
trees/dt/dt-0058.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\title{The category #{\textbf{Cpo}^\textbf{R}}}
4
+
\author{liamoc}
5
+
\p{The category #{\textbf{Cpo}^\textbf{R}} is the [category](dm-000G) where the objects are [cpos](dt-001D), the morphisms are [retraction pairs](dt-0054), composition is as in \ref{dt-0056} and identity is just the [retraction pair](dt-0054) #{A \rpair{\lambda x. x}{\lambda x. x} A}. }
+8
trees/dt/dt-0059.tree
+8
trees/dt/dt-0059.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\title{Information ordering in #{\textbf{Cpo}^\textbf{R}}}
5
+
\p{
6
+
The third point in \ref{dt-0057} suggests a notion of approximation, or [information ordering](dt-000B), for [cpos](dt-001D). Rather than say, as we did in \ref{dt-004O}, that for [cpos](dt-001D) #{A} and #{B}, #{A \sqsubseteq B} iff there exists a [continuous function](dt-001J) #{A\contto B}, we now say:
7
+
\figure{#{A \sqsubseteq B} iff there exists a [retraction pair](dt-0054) #{A \rpair{f}{g} B}}
8
+
}
+4
trees/dt/dt-005A.tree
+4
trees/dt/dt-005A.tree
···
1
+
\title{Generalising to #{\textbf{Cpo}^\textbf{R}}}
2
+
\author{liamoc}
3
+
\p{All of our other notions for #{\textbf{Cpo}} naturally generalise to a setting with [retraction pairs](dt-0054) #{\textbf{Cpo}^\textbf{R}}: least elements, [#{\omega}-chains](dt-004Q), [upper bounds](dt-004R), [colimits](dt-004S), [cocontinuous endofunctors](dt-004V) and so on.}
4
+
\transclude{dt-005C}
+18
trees/dt/dt-005B.tree
+18
trees/dt/dt-005B.tree
···
1
+
\taxon{Theorem}
2
+
\title{Fixed point theorem for endofunctors on #{\textbf{Cpo}^\textbf{R}}}
3
+
\p{Every [cocontinuous endofunctor](TODO) #{\mathcal{F}} on #{\mathbf{Cpo}^\textbf{R}} has a least fixed point, given by the [colimit](TODO) of the ascending [#{\omega}-chain](dt-005C):
4
+
\figure{
5
+
\tex{\usepackage{tikz-cd}}{\begin{tikzcd}
6
+
\mathbf{1} \ar[r,"f_0",->,yshift=0.2em]\ar[r,"g_0"', <-,yshift=-0.2em] &
7
+
\mathcal{F}(\mathbf{1}) \ar[r,"f_1",->,yshift=0.2em]\ar[r,"g_1"', <-,yshift=-0.2em] &
8
+
\mathcal{F}(\mathcal{F}(\mathbf{1})) \ar[r,"f_2",->,yshift=0.2em]\ar[r,"g_2"', <-,yshift=-0.2em] &
9
+
\mathcal{F}(\mathcal{F}(\mathcal{F}(\mathbf{1}))) \ar[r,-,dashed,yshift=0.2em]\ar[r,dashed,-,yshift=-0.2em] &
10
+
\cdots
11
+
\end{tikzcd}}}
12
+
Where the [retraction pairs](dt-0054) #{(f_i, g_i)} are defined by:
13
+
##{
14
+
\begin{array}{lcl}
15
+
(f_0,g_0) & \triangleq & (\lambda x. \bot, \lambda x. \bot)\\
16
+
(f_{i+1},g_{i+1}) & \triangleq & \mathcal{F}(f_i,g_i) \\
17
+
\end{array}
18
+
}}
+15
trees/dt/dt-005C.tree
+15
trees/dt/dt-005C.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\title{#{\omega}-chains of cpos in the category #{\mathbf{Cpo}^\textbf{R}}}
5
+
\p{An [#{\omega}-chain](dt-000W) of [cpos](dt-001D) in the [category #{\mathbf{Cpo}^\textbf{R}}](dt-0058) consists of a family of [cpos](dt-001D) #{\Set{D_i \mid i \in \mathbb{N} }}, together with a family of [retraction pairs](dt-0054) #{ D_i \rpair{f_i}{g_i} D_{i+1}}, shown below:}
6
+
\figure{
7
+
\tex{\usepackage{tikz-cd}}{
8
+
\begin{tikzcd}
9
+
D_0 \ar[r,"f_0",->,yshift=0.2em]\ar[r,"g_0"', <-,yshift=-0.2em] &
10
+
D_1 \ar[r,"f_1",->,yshift=0.2em]\ar[r,"g_1"', <-,yshift=-0.2em] &
11
+
D_2 \ar[r,"f_2",->,yshift=0.2em]\ar[r,"g_2"', <-,yshift=-0.2em] &
12
+
D_3 \ar[r,-,dashed,yshift=0.2em]\ar[r,dashed,-,yshift=-0.2em] &
13
+
\cdots
14
+
\end{tikzcd}
15
+
}}