my forest
finished products
+174
-36
+10
trees/dm-000M.tree
+10
trees/dm-000M.tree
···
1
+
\title{Bifunctor}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\p{
5
+
A binary [functor](dm-000J), or \em{bifunctor} from two [categories](dm-000G) #{\mathbf{A}} and #{\mathbf{B}} to a [category](dm-000G) #{\mathbf{C}} is a [functor](dm-000J) from the [product category](dm-000N) #{\mathbf{A} \times \mathbf{B}} to #{\mathbf{C}}. That is, a bifunctor #{F} consists of an \em{object mapping} #{F(a,b)} that maps an object #{a} of #{\mathbf{A}} and an object #{b} of #{\mathbf{B}} to an object of #{\mathbf{C}}, and a \em{morphism mapping} #{F(f,g)} that maps a morphism #{X_\textbf{A} \xrightarrow{f} Y_\textbf{A}} and a morphism #{X_\textbf{B} \xrightarrow{g} Y_\textbf{B}} to a morphism #{F(X_\textbf{A},X_\textbf{B}) \xrightarrow{F(f,g)} F(Y_\textbf{A},Y_\textbf{B}) } in #{\textbf{C}}, such that:
6
+
\ul{
7
+
\li{ For each object #{X} in #{\mathbf{A}} and #{Y} in #{\mathbf{B}}, the equation #{F(\mathsf{id}_X, \mathsf{id}_Y) = \mathsf{id}_{F(X,Y)}} holds in #{\mathbf{C}}. }
8
+
\li{ For a pair of morphisms #{X_\textbf{A} \xrightarrow{f_1} Y_\textbf{A} \xrightarrow{f_2} Z_\textbf{A}} in #{\mathbf{A}} and another pair #{X_\textbf{B} \xrightarrow{g_1} Y_\textbf{B} \xrightarrow{g_2} Z_\textbf{B}} in #{\mathbf{B}}, the equation #{F (f_2 \circ f_1, g_2 \circ g_1) = F(f_2,g_2) \circ F(f_1,g_1)} holds in #{\mathbf{C}}. }
9
+
}
10
+
}
+6
trees/dm-000N.tree
+6
trees/dm-000N.tree
···
1
+
\title{Product category}
2
+
\author{liamoc}
3
+
\taxon{Definition}
4
+
\p{
5
+
For two [categories](dt-002A) #{\textbf{A}} and #{\textbf{B}}, the \em{product category} #{\textbf{A} \times \textbf{B}} is the category whose objects are pairs consisting of an object of #{\textbf{A}} and an object of #{\textbf{B}}, and whose morphisms are similarly pairs of morphisms from #{\textbf{A}} and #{\textbf{B}}. Composition of morphisms is defined componentwise on the pairs using the composition from #{\textbf{A}} and #{\textbf{B}}.
6
+
}
+10
trees/dm-000O.tree
+10
trees/dm-000O.tree
···
1
+
\taxon{Definition}
2
+
\author{liamoc}
3
+
\title{Monoid}
4
+
\p{A \em{monoid} #{(S, \iota, \bullet)} consists of a set #{S}, an \em{identity} element #{\iota \in S}, and a binary operator #{(\bullet) : S \times S \rightarrow S} which satisfies, for all #{x,y,z \in S}:
5
+
\ul{
6
+
\li{ [associativity](dm-000F): #{x \bullet (y \bullet z) = (x \bullet y) \bullet z} }
7
+
\li{ left identity: #{\iota \bullet x = x}}
8
+
\li{ right identity: #{x \bullet \iota = x}}
9
+
}
10
+
}
+5
trees/dm-000P.tree
+5
trees/dm-000P.tree
+4
-4
trees/dt-001W.tree
+4
-4
trees/dt-001W.tree
···
4
4
\p{Show that if a function #{f : A \rightarrow B} on [cpos](dt-001D) #{A} and #{B} is [monotonic](dt-000J) and #{A} is finite, then #{f} is [continuous](dt-001J). }
5
5
\p{\em{Hint}: Finite [directed](dt-0010) sets contain their [lub](dt-0017)}
6
6
\scope{
7
-
\put\transclude/toc{false}
8
-
\put\transclude/numbered{false}
9
-
\put\transclude/expanded{false}
10
-
\subtree{\taxon{Solution}
7
+
\put\transclude/toc{false}
8
+
\put\transclude/numbered{false}
9
+
\put\transclude/expanded{false}
10
+
\subtree{\taxon{Solution}
11
11
\p{Because of \ref{dt-001O}, it suffices to show the second condition of [continuity](dt-001J), as #{f} is [monotonic](dt-000J). }
12
12
\p{Because #{A} is finite, any directed subset #{X \subseteq A} is also finite, and therefore #{\bigsqcup X \in X}. Because #{f} is [monotone](dt-000J), #{f(x) \sqsubseteq f (\bigsqcup X)} for all #{x \in X}. }
13
13
\p{The solution to \ref{dt-001N} shows that #{\Set{f(x) \mid x \in X}} is [directed](dt-0010) and therefore contains its upper bound #{c}. Because #{f} is monotone, #{f(\bigsqcup X)} must be #{c} (else it would contradict the above).}
+8
-23
trees/dt-001Z.tree
+8
-23
trees/dt-001Z.tree
···
4
4
\title{Constructions on [cpos](dt-001D) and PCF}
5
5
\author{liamoc}
6
6
\p{This lecture is based on material from [[haskellhutt]], [[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
7
+
\transclude{dt-002K}
7
8
\subtree{
8
-
\title{Products}
9
-
\p{Recall \ref{dt-000E}, which showed that the [product](dm-0005) of two [pointed posets](dt-000G) is itself a [pointed poset](dt-000G).
10
-
11
-
In \ref{dt-001X} you may also have shown that #{A \times B} is also a [cpo](dt-001D) if #{A} and #{B} are [cpos](dt-001D), with this definition for [lubs](dt-0017):
12
-
##{
13
-
\bigsqcup X \; = \; \left(\bigsqcup \{ x \mid \exists y.\ (x,y) \in X \}, \bigsqcup \{ y \mid \exists x.\ (x,y) \in X \}\right)
9
+
\title{Functions}
14
10
}
15
-
This definition can be made a little more comprehensible by defining it in terms of the two projection operators for pairs:
11
+
\subtree{
12
+
\title{Sums}
16
13
}
17
-
\transclude{dt-0020}
18
-
\transclude{dt-0021}
19
-
\transclude{dt-0022}
20
-
\transclude{dt-0023}
21
-
\transclude{dt-0024}
22
-
\p{These building blocks can be used to make many functions on [products](dt-0021) (thereby ensuring [continuity](dt-001J)):
14
+
\subtree{
15
+
\title{Strict Constructions}
23
16
}
24
-
\transclude{dt-0025}
25
-
\transclude{dt-0026}
26
-
\transclude{dt-0027}
27
-
\transclude{dt-0028}
28
-
\transclude{dt-0029}
29
-
\transclude{dt-002A}
30
-
\transclude{dt-002C}
17
+
\subtree{
18
+
\title{PCF}
31
19
}
32
-
33
-
34
-
+1
trees/dt-0022.tree
+1
trees/dt-0022.tree
+3
-5
trees/dt-0024.tree
+3
-5
trees/dt-0024.tree
···
1
1
\import{dt-macros}
2
2
\import{table-macros}
3
3
\taxon{Theorem}
4
+
\title{Continuity of split}
4
5
\author{liamoc}
5
6
\p{For [continuous functions](dt-001J) #{f} and #{g}, the [split function](dt-0023) #{\langle f, g \rangle} is [continuous](dt-001J).}
6
-
\scope{
7
-
\put\transclude/toc{false}
8
-
\put\transclude/numbered{false}
9
-
\subtree{\taxon{Proof}
7
+
\proofblock{
10
8
\ul{
11
9
\li{ \em{#{\langle f, g \rangle} is [monotonic](dt-000J)}. Let #{x \sqsubseteq y \in A}. Then: ##{\begin{array}{lclr}
12
10
\langle f , g \rangle\ x & = & (f(x), g(x)) & \text{(def)}\\
···
20
18
& = & \bigsqcup \{ \langle f , g \rangle\ x \mid x \in X \} & \text{(def)}
21
19
\end{array}}
22
20
}
23
-
}}
21
+
}
+2
-2
trees/dt-0025.tree
+2
-2
trees/dt-0025.tree
···
14
14
\node[dot] at (ZZ.west.1) {};
15
15
\node[dot] at (ZZ.west.2) {};
16
16
\node at (-6.3cm,0) {\Large $=$};
17
-
\end{tikzpicture} }
17
+
\end{tikzpicture} }}
18
18
\td{
19
19
\tex{\usepackage{string-diagrams}}{
20
20
\begin{tikzpicture}
···
37
37
\draw[thick,-|] (f.west.1) -- ([xshift=0.4cm]f.west.1);
38
38
\draw[thick] (g.west.1) -- (g.east.1);
39
39
\draw[thick,-|] (g.west.2) -- ([xshift=0.4cm]g.west.2);
40
-
\end{tikzpicture}}}
40
+
\end{tikzpicture}}
41
41
}\td{#{\begin{array}{l}\mathit{swap} : A \times B \rightarrow B \times A \\ \mathit{swap} = \langle \pi_1 , \pi_0 \rangle \end{array}}}
42
42
}}
+2
-1
trees/dt-002C.tree
+2
-1
trees/dt-002C.tree
···
1
1
\title{Derived properties of [cpo products](dt-0021)}
2
+
\taxon{Corollary}
2
3
\author{liamoc}
3
4
\p{
4
5
The [universal property](dt-0029) is called such because \em{all} the familiar properties of [products](dt-0021) follow from it – thinking in pictures helps to see how (Indeed, the [universal property](dt-0029) \em{characterises} products up to isomorphism):}
···
11
12
\li{ #{(f \circ g) \times (h \circ i) = (f \circ h) \times (g \circ i) \quad (**)}}
12
13
}
13
14
\p{
14
-
These last two statements #{(*)} and #{(**)} show that #{\times} is a \em{bifunctor} on the [category #{\textbf{Cpo}}](dt-002B), i.e., a [functor](dm-000J) #{\textbf{Cpo} \times \textbf{Cpo} \rightarrow \textbf{Cpo}}.
15
+
These last two statements #{(*)} and #{(**)} show that #{\times} is a [bifunctor](dm-000M) on the [category #{\textbf{Cpo}}](dt-002B), i.e., a [functor](dm-000J) #{\textbf{Cpo} \times \textbf{Cpo} \rightarrow \textbf{Cpo}}.
15
16
}
+8
trees/dt-002D.tree
+8
trees/dt-002D.tree
+7
trees/dt-002E.tree
+7
trees/dt-002E.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{[Cpo](dt-001D) isomorphism}
5
+
\p{An \em{isomorphism} between two [cpos](dt-001D) #{A} and #{B} is a [bijection](dm-000A) #{f} between #{A} and #{B} such that #{f} preserves the [cpo](dt-001D) structure, i.e., that #{f} and #{f^{-1}} are [continuous](dt-001J).
6
+
}
7
+
\p{We say two [cpos](dt-001D) #{A} and #{B} are \em{isomorphic}, written #{A \simeq B}, iff an \em{isomorphism} exists between them.}
+8
trees/dt-002F.tree
+8
trees/dt-002F.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Definition}
3
+
\author{liamoc}
4
+
\title{The set of continuous functions}
5
+
\p{
6
+
Let #{A \contto B} denote just the [continuous functions](dt-001J) from [cpo](dt-001D) #{A} to [cpo](dt-001D) #{B}:
7
+
##{A \contto B\; \triangleq\; \Set{ f : A \rightarrow B \mid f\ \text{is continuous} }}
8
+
}
+11
trees/dt-002G.tree
+11
trees/dt-002G.tree
···
1
+
\taxon{Exercise}
2
+
\author{liamoc}
3
+
\p{Express the function #{\mathit{juggle} (a, (b,c)) = ((a,b),c)} using just our primitive combinators for [projection](dt-0020) and [split](dt-0023).}
4
+
\scope{
5
+
\put\transclude/toc{false}
6
+
\put\transclude/numbered{false}
7
+
\put\transclude/expanded{false}
8
+
\subtree{\taxon{Solution}
9
+
\p{##{\mathit{juggle} \triangleq \langle \langle \pi_0 , \pi_0 \circ \pi_1 \rangle , \pi_1 \circ \pi_1 \rangle}}
10
+
}
11
+
}
+13
trees/dt-002H.tree
+13
trees/dt-002H.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Theorem}
3
+
\author{liamoc}
4
+
\title{Commutative monoid structure for [cpos](dt-001D)}
5
+
\p{[Cpos](dt-001D) form a [commutative monoid](dm-000P) "up to [isomorphism](dt-002E)" under #{\times} and #{\mathbf{1}} (the [cpo](dt-001D) consisting of only one element #{\bot}). That is, for all [cpos](dt-001D) #{A, B} and #{C}:
6
+
\ol{
7
+
\li{#{A \times \mathbf{1} \simeq A}}
8
+
\li{#{A \times (B \times C) \simeq (A \times B) \times C}}
9
+
\li{#{A \times B \simeq B \times A}}
10
+
}
11
+
\proofblock{
12
+
\p{The [isomorphisms](dt-002E) required are the [projection](dt-0020) #{\pi_0}, the #{\mathit{juggle}} function from \ref{dt-002G}, and [the swap function](dt-0025).}
13
+
}}
+15
trees/dt-002I.tree
+15
trees/dt-002I.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Exercise}
3
+
\author{liamoc}
4
+
\p{Show using the [universal property](dt-0029) that #{\langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle}}
5
+
\solnblock{
6
+
Instantiating the [universal property](dt-0029) where #{h := \langle f, g \rangle \circ h}, #{f := f \circ h}, and #{g := g \circ h}:
7
+
##{\pi_0 \circ \langle f, g \rangle \circ h = f \circ h \land
8
+
\pi_1 \circ \langle f, g \rangle \circ h = g \circ h\ \text{iff}\ \langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle}
9
+
Simplifying using the pictorial properties in \ref{dt-0027} (shown equivalent to the [universal property](dt-0029) in \ref{dt-0028}):
10
+
##{f \circ h = f \circ h \land
11
+
g \circ h = g \circ h\ \text{iff}\ \langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle}
12
+
By logical simplifications, we arrive at
13
+
##{\langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle}
14
+
as required.
15
+
}
+8
trees/dt-002J.tree
+8
trees/dt-002J.tree
···
1
+
\import{dt-macros}
2
+
\taxon{Theorem}
3
+
\author{liamoc}
4
+
\p{There is an [isomorphism](dt-002E) between [pairs](dt-0021) of [continuous functions](dt-002F) and continuous functions that output pairs: ##{(A \contto B) \times (A \contto C)\; \simeq\; (A \contto (B \times C))}
5
+
\proofblock{
6
+
Proof follows from the [universal property](dt-0029) after setting up the [isomorphism](dt-002E) with functions #{f(g_0,g_1) = \langle g_0 , g_1 \rangle} and #{f^{-1}(h) = (\pi_0 \circ h, \pi_1 \circ h)}.}
7
+
}
8
+
%Because we have the \gls{functor} $\times$ on cpos that satisfies the properties of products described above, the \gls{category} \textbf{Cpo} therefore has binary products.
+38
trees/dt-002K.tree
+38
trees/dt-002K.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Products}
4
+
\p{Recall \ref{dt-000E}, which showed that the [product](dm-0005) of two [pointed posets](dt-000G) is itself a [pointed poset](dt-000G).
5
+
6
+
In \ref{dt-001X} you may also have shown that #{A \times B} is also a [cpo](dt-001D) if #{A} and #{B} are [cpos](dt-001D), with this definition for [lubs](dt-0017):
7
+
##{
8
+
\bigsqcup X \; = \; \left(\bigsqcup \{ x \mid \exists y.\ (x,y) \in X \}, \bigsqcup \{ y \mid \exists x.\ (x,y) \in X \}\right)
9
+
}
10
+
This definition can be made a little more comprehensible by defining it in terms of the two projection operators for pairs:
11
+
}
12
+
\transclude{dt-0020}
13
+
\transclude{dt-0021}
14
+
\transclude{dt-0022}
15
+
\transclude{dt-0023}
16
+
\transclude{dt-0024}
17
+
\p{These building blocks can be used to make many functions on [products](dt-0021) (thereby ensuring [continuity](dt-001J)):
18
+
}
19
+
\transclude{dt-0025}
20
+
\transclude{dt-0026}
21
+
\transclude{dt-002G}
22
+
\transclude{dt-0027}
23
+
\transclude{dt-0028}
24
+
\transclude{dt-0029}
25
+
\transclude{dt-002A}
26
+
\transclude{dt-002C}
27
+
\transclude{dt-002I}
28
+
\transclude{dt-002D}
29
+
\scope{
30
+
\put\transclude/toc{false}
31
+
\put\transclude/numbered{false}
32
+
\subtree{
33
+
\taxon{Upshot}
34
+
\p{
35
+
Because we have the [functor](dm-000J) #{\times} on #{\textbf{Cpo}} that satisfies the properties of products described above, the [category #{\textbf{Cpo}}](dt-002B) therefore has \em{binary products}.}
36
+
37
+
}
38
+
}
+15
-1
trees/dt-macros.tree
+15
-1
trees/dt-macros.tree
···
1
1
\def\cal[body]{#{\mathcal{\body}}}
2
2
\def\syn[body]{#{\mathsf{\body}}}
3
+
\def\proofblock[body]{\scope{
4
+
\put\transclude/toc{false}
5
+
\put\transclude/numbered{false}
6
+
\subtree{\taxon{Proof}
7
+
\body
8
+
}}}
9
+
\def\solnblock[body]{\scope{
10
+
\put\transclude/toc{false}
11
+
\put\transclude/numbered{false}
12
+
\put\transclude/expanded{false}
13
+
\subtree{\taxon{Solution}
14
+
\body
15
+
}}}
3
16
\def\pow[body]{#{\mathcal{P}(\body)}}
4
17
\def\sems[body]{#{\llbracket \body \rrbracket}}
5
18
\def\nat{#{\mathbb{N}}}
···
11
24
\def\acr[distance]{\\[\distance]}
12
25
\def\lsquare{\startverb[\stopverb}
13
26
\def\rparen{\startverb)\stopverb}
14
-
\def\op-cl-int[x][y]{\lsquare\x,\y\rparen}
27
+
\def\op-cl-int[x][y]{\lsquare\x,\y\rparen}
28
+
\def\contto{\twoheadrightarrow}