Work on coalgebras

tex/.vscode/ltex.dictionary.en-US.txt

@@ -43,3 +43,8 @@ Corecursion
 Coinduction
 Colimits
 Colimit
+F-coalgebra
+coalgebras
+F-coalgebras
+coalgebra
+corecursion

tex/catprog.sty

@@ -47,6 +47,7 @@
 \def\Mon{\ensuremath{\catname{Mon}}}
 \def\Gra{\ensuremath{\catname{Gra}}}
 \providecommand{\Alg}[1]{\ensuremath{\catname{Alg}(#1)}}
+\providecommand{\Coalg}[1]{\ensuremath{\catname{Coalg}(#1)}}
 %% Objects of category
 \providecommand{\obj}[1]{\ensuremath{\vert #1 \vert}}
 %% Dual category
@@ -58,6 +59,8 @@
 %% Banana brackets for catamorphisms
 \RequirePackage{stmaryrd}
 \providecommand{\cata}[1]{\llparenthesis #1 \rrparenthesis}
+% Lens brackets for anamorphisms https://unicodeplus.com/U+3016
+\providecommand{\ana}[1]{〖 #1 〗}
 
 
 \providecommand{\eps}{{\operatorname\epsilon}}
@@ -77,7 +80,7 @@
 \providecommand{\ass}{\mathrel{\coloneqq}}
 \providecommand{\bnf}{\mathrel{\Coloneqq}}
 
-%% Some standard functors
+%% Some standard functorsw
 \providecommand{\PSet}{{\mathcal P}}				% Powerset
 \providecommand{\FSet}{{\mathcal P}_{\omega}}			% Finite powerset
 \providecommand{\CSet}{{\mathcal P}_{\omega_1}}			% Countable powerset
@@ -92,7 +95,8 @@
 \providecommand{\iso}{\mathbin{\cong}}
 \providecommand{\tensor}{\mathbin{\otimes}}
 \providecommand{\unit}{\star}
-\providecommand{\bang}{\operatorname!}				% Initial/final map
+\providecommand{\bang}{\operatorname!}				% Terminal map
+\providecommand{\cobang}{\operatorname¡}				% Initial map
 
 %% Various arrows
 \providecommand{\from}{\leftarrow}

tex/main.tex

@@ -70,7 +70,7 @@
 \usepackage{tikz}
 \usetikzlibrary{cd, babel, quotes}
 \usepackage{quiver}
-\declaretheorem[name=Definition,style=definition,numberwithin=chapter]{definition}
+\declaretheorem[name=Definition,style=definition,numberwithin=section]{definition}
 \declaretheorem[name=Example,style=definition,sibling=definition]{example}
 \declaretheorem[style=definition,numbered=no]{exercise}
 \declaretheorem[name=Remark,style=definition,sibling=definition]{remark}

tex/sections/02_categories.tex

@@ -640,9 +640,9 @@ These are examples of special \emph{F-algebras} in $\Set$. In this section we wi
     \arrow["a"', from=3-1, to=3-3]
   \end{tikzcd}
 \]
-commutes.
+commutes. We sometimes denote that initial F-algebra as $\mu F$.
 
-The dual notion of \emph{terminal F-algebra} is usually not of interested, since it is just inherited from $\CC$:
+The dual notion of \emph{terminal F-algebra} is usually not of interest, since it is just inherited from $\CC$:
 % https://q.uiver.app/#q=WzAsNCxbMCwwLCJGQSJdLFsyLDAsIkEiXSxbMCwyLCJGMSJdLFsyLDIsIjEiXSxbMiwzLCIhIl0sWzAsMSwiYSJdLFswLDIsIkYhIiwyXSxbMSwzLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
 \[
   \begin{tikzcd}
@@ -717,7 +717,7 @@ We can now abstract the fusion and identity laws that we defined for each data t
   \end{enumerate}
 \end{proof}
 
-\begin{proposition}[Lambeks Lemma]
+\begin{proposition}[Lambeks Lemma]\label{prop:lambek}
   Let $(I,i)$ be an initial F-algebra. The F-algebra structure $i$ is an isomorphism.
 \end{proposition}
 \begin{proof}
@@ -745,16 +745,183 @@ We can now abstract the fusion and identity laws that we defined for each data t
   \[\cata{Fi} \comp i = Fi \comp F\cata{Fi} = F(i \comp \cata{Fi}) = F {id}_I = {id}_{FI}.\]
 \end{proof}
 
+\begin{example}
+  Using \autoref{prop:lambek}, we can prove that not every functor $F$ has an initial F-algebra.
+  Consider the power set functor $\PSet : Set \rightarrow Set$.
+  If there was an initial algebra $i : \PSet X \rightarrow X$, then $\PSet X \iso X$, which does not hold, because of Cantor's Theorem.
+\end{example}
+
 \subsection{Term Algebras}
-% TODO
+% TODO term algebras
 
 \subsection{Parametric Data Types}
-% TODO
+% TODO parametric data types
 
 \section{Functor Coalgebras}
-% TODO coalgebras
+Coalgebras describe state based system by observations.
+Formally they are dual (we soon see in what sense) to F-algebras:
+\begin{definition}[F-Coalgebra]
+  Let $F : \CC \to \CC$ be an endofunctor.
+  An F-coalgebra is a pair $(C, c : C \to FC)$ and a homomorphism between coalgebras $h : (B,b) \rightarrow (C,c)$ is a morphism $B \to C$ such that
+  % https://q.uiver.app/#q=WzAsNCxbMCwwLCJCIl0sWzIsMCwiRkIiXSxbMCwyLCJDIl0sWzIsMiwiRkMiXSxbMCwxLCJiIl0sWzIsMywiYyJdLFswLDIsImgiLDJdLFsxLDMsIkZoIl1d
+  \[
+    \begin{tikzcd}
+      B && FB \\
+      \\
+      C && FC
+      \arrow["b", from=1-1, to=1-3]
+      \arrow["c", from=3-1, to=3-3]
+      \arrow["h"', from=1-1, to=3-1]
+      \arrow["Fh", from=1-3, to=3-3]
+    \end{tikzcd}
+  \]
+  commutes.
+\end{definition}
+Coalgebras together with their homomorphisms form a category that we call $\Coalg{F}$.
+F-coalgebras and F-algebras are dual in the sense that $\Coalg{F} = \dual{\Alg{\dual{F}}} \not= \dual{\Alg{F}}$, where $\dual{F} : \dual{\CC} \to \dual{\CC}$.
+
+This time we are interested in \emph{terminal F-coalgebras} $(T,t)$, which are characterized by the fact that for any coalgebra $(C,c)$ there exists a unique homomorphism such that
+% https://q.uiver.app/#q=WzAsNCxbMCwwLCJDIl0sWzIsMCwiRkMiXSxbMCwyLCJUIl0sWzIsMiwiRlQiXSxbMCwxLCJjIl0sWzIsMywidCJdLFswLDIsIlxcYW5he2N9IiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMywiRlxcYW5he2N9Il1d
+\[\begin{tikzcd}
+    C && FC \\
+    \\
+    T && FT
+    \arrow["c", from=1-1, to=1-3]
+    \arrow["t", from=3-1, to=3-3]
+    \arrow["{\ana{c}}"', dashed, from=1-1, to=3-1]
+    \arrow["{F\ana{c}}", from=1-3, to=3-3]
+  \end{tikzcd}\]
+commutes. We sometimes denote the terminal F-algebra as $\nu F$.
+
+Dual to F-algebras the \emph{initial F-coalgebra} is trivial:
+% https://q.uiver.app/#q=WzAsNCxbMCwwLCIwIl0sWzIsMCwiRjAiXSxbMCwyLCJDIl0sWzIsMiwiRkMiXSxbMCwyLCJcXGNvYmFuZyIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFswLDEsIlxcY29iYW5nIl0sWzIsMywiYyJdLFsxLDMsIkZcXGNvYmFuZyJdXQ==
+\[\begin{tikzcd}
+    0 && F0 \\
+    \\
+    C && FC
+    \arrow["\cobang"', dashed, from=1-1, to=3-1]
+    \arrow["\cobang", from=1-1, to=1-3]
+    \arrow["c", from=3-1, to=3-3]
+    \arrow["F\cobang", from=1-3, to=3-3]
+  \end{tikzcd}\]
+
+\begin{example}
+  Let us now consider some examples of (terminal) F-coalgebras. They describe state systems, thus we will describe the corresponding automaton.
+  \begin{enumerate}
+    \item Let $FX = X + 1 : \Set \to \Set$. Let $Q$ be the state space,
+          then state transitions of this system have the form $Q \overset{d}{\to} Q + 1$,
+          i.e.\ an element $q \in Q$ either has a next state $d\;q \in Q$ or terminates, $d\;q \in 1$.
+
+          Homomorphisms are morphisms between state spaces that respect the state transitions $d$:
+          \begin{itemize}
+            \item $h\;d\;q = d'\;h\;q$,
+            \item $q$ terminates $\iff$ $h\;q$ terminates,
+          \end{itemize}
+          which is expressed by the usual diagram:
+          % https://q.uiver.app/#q=WzAsNCxbMCwwLCJRIl0sWzIsMCwiUSArIDEiXSxbMCwyLCJRJyJdLFsyLDIsIlEnICsgMSJdLFswLDIsImgiLDJdLFsxLDMsImggKyBcXGJhbmciXSxbMCwxLCJkIl0sWzIsMywiZCciXV0=
+          \[\begin{tikzcd}
+              Q && {Q + 1} \\
+              \\
+              {Q'} && {Q' + 1}
+              \arrow["h"', from=1-1, to=3-1]
+              \arrow["{h + \bang}", from=1-3, to=3-3]
+              \arrow["d", from=1-1, to=1-3]
+              \arrow["{d'}", from=3-1, to=3-3]
+            \end{tikzcd}\]
+
+          The terminal F-coalgebra is $\mathbb{N}_\infty = \mathbb{N}\cup\{\infty\}$, with $t : \mathbb{N}_\infty \to 1 + \mathbb{N}_\infty$ defined by
+          \[t\;x := \begin{cases}
+              \infty     & \text{if } x = \infty \\
+              \ast \in 1 & \text{if } x = 0      \\
+              n          & \text{if } x = n + 1
+            \end{cases}\]
+          and the unique homomorphism $h : (Q,d) \to (\mathbb{N}_\infty, t)$ returns the number of steps an element $q \in Q$ has to take until it terminates.
+          % \item Let $FX = A + X : \Set \to \Set$ for some set $A$. A coalgebra $Q \overset{d}{\to} A + Q$ sends every state $q \in Q$ to a next state or terminates with a result $d\;q \in A$.
+    \item Let $FX = A \times X : \Set \to \Set$ for some set $A$. A coalgebra $Q \overset{\langle o,t \rangle}{\longrightarrow} A \times Q$ returns for every $q \in Q$ an output $o\;q \in A$ and the next state $t\;q \in Q$.
+
+          Homomorphisms $h : (Q, \langle o,t\rangle) \to (Q', \langle o', t'\rangle)$ are mappings $h : Q \to Q'$ such that
+          \begin{itemize}
+            \item $o\;q = o'\;h\;q$,
+            \item $h\;t\;q = t\;h\;q$.
+          \end{itemize}
+          The terminal F-coalgebra is $A^\omega$, i.e.\ the set of \emph{streams} over $A$ with \[A^\omega \overset{\langle hd,tl \rangle}{\longrightarrow} A \times A^\omega\] defined by
+          \[(a_0, a_1, a_2, \ldots) \mapsto (a_0, (a_1, a_2, \ldots)).\]
+          The unique homomorphism $h : (Q, \langle o , t\rangle) \rightarrow (A^\omega, \langle hd, tl \rangle)$ maps a state $q \in Q$ to the stream \[(o\;q,  o(t\;q), o(t(t\;q)),\ldots).\]
+    \item Recall that deterministic finite automata (DFA) are tuples $A = (Q, \Sigma, \delta, q_0, E)$ where
+          \begin{itemize}
+            \item $Q$ is a state space,
+            \item $\Sigma$ is a finite alphabet,
+            \item $\delta : Q \times \Sigma \to Q$ is a state transition function,
+            \item $q_0 \in Q$ is the initial state,
+            \item $E \subseteq Q$ is the set of accepting states.
+          \end{itemize}
+          By changing the type of $\delta$ via currying to $\delta : Q \to Q^\Sigma$ and representing $E$ as a map $f : Q \to 2$, we can represent a DFA (without the initial state) as a map
+          \[Q \overset{\langle f,\delta \rangle}{\longrightarrow} 2 \times Q^\Sigma.\]
+
+          Thus, we can represent DFA as coalgebras for $FX = 2 \times X^\Sigma : \Set \to \Set$. A homomorphism between automata \[h : (Q \overset{\langle f, \delta\rangle}{\longrightarrow} 2 \times Q^\Sigma) \to Q' \overset{\langle f', \delta' \rangle}{\longrightarrow} 2 \times {Q'}^{\Sigma'}\] is then a mapping $h : Q \to Q'$ such that
+          \[h(\delta\;(a,q)) = {\delta'}(a, h\;q).\]
+
+          The terminal F-coalgebra is $2^{\Sigma^*} \iso \PSet(\Sigma^*)$, i.e.\ the set of formal languages over $\Sigma$ with the structure $\langle \varepsilon? , \partial \rangle : \PSet(\Sigma^*) \rightarrow 2 \times \PSet(\Sigma^*)$ defined by
+          \[\varepsilon?(L) = \begin{cases}
+              1 & \varepsilon \in L \\
+              0 & \text{else}
+            \end{cases}\]
+          and
+          \[\partial(L)(a) = a^\mone L = \{w \;\vert\; aw \in L\}.\]
+
+          Finally, the unique homomorphism $h : Q \rightarrow \PSet(\Sigma^*)$ returns for any $q \in Q$ the formal language that is accepted by $q$.
+  \end{enumerate}
+\end{example}
+
+\begin{proposition}
+  Let $T \overset{t}{\longrightarrow} FT$ be a terminal F-coalgebra, then $t$ is an isomorphism.
+\end{proposition}
+\begin{proof}
+  Follows by duality from \autoref{prop:lambek}.
+\end{proof}
 
-\subsection{Terminal F-Coalgebras}
 \subsection{Corecursion and Coinduction}
+\emph{Corecursion} is a proof principle: each F-coalgebra $(C,c)$ induces a unique homomorphism $h : (C,C) \to (\nu F, t)$.
+\begin{example} Let us consider some functions defined by corecursion:
+  \begin{enumerate}
+    \item Recall $A^\omega \overset{\langle hd , tl \rangle}{\longrightarrow} A \times A^\omega$, we can define a function $zip : A^\omega \times A^\omega \to A^\omega$ by
+          \[hd(zip\;\sigma\;\tau) = hd\;\sigma; \qquad tl(zip\;\sigma\;\tau) = zip\;\tau\;(tl\;\sigma).\]
+          This definition corresponds to the following coalgebra structure:
+          % https://q.uiver.app/#q=WzAsNCxbMCwwLCJBXlxcb21lZ2EgXFx0aW1lcyBBXlxcb21lZ2EiXSxbMywwLCJBIFxcdGltZXMgKEFeXFxvbWVnYSBcXHRpbWVzIEFeXFxvbWVnYSkiXSxbMCwyLCJBXlxcb21lZ2EiXSxbMywyLCJBIFxcdGltZXMgQV5cXG9tZWdhIl0sWzAsMiwiemlwIiwyXSxbMiwzLCJcXGxhbmdsZSBoZCAsIHRsIFxccmFuZ2xlIiwyXSxbMSwzLCJpZCBcXHRpbWVzIHppcCJdLFswLDEsIlxcbGFuZ2xlIGhkIFxcY29tcCBcXHBpXzEgLCBcXGxhbmdsZSBcXHBpXzIgLCB0bCBcXGNvbXAgXFxwaV8xIFxccmFuZ2xlIFxccmFuZ2xlIl1d
+          \[\begin{tikzcd}
+              {A^\omega \times A^\omega} &&& {A \times (A^\omega \times A^\omega)} \\
+              \\
+              {A^\omega} &&& {A \times A^\omega}
+              \arrow["zip"', from=1-1, to=3-1]
+              \arrow["{\langle hd , tl \rangle}"', from=3-1, to=3-4]
+              \arrow["{id \times zip}", from=1-4, to=3-4]
+              \arrow["{\langle hd \comp \pi_1 , \langle \pi_2 , tl \comp \pi_1 \rangle \rangle}", from=1-1, to=1-4]
+            \end{tikzcd}\]
+    \item Similarly, for $f : A \rightarrow B$ we can define $map\;f : A^\omega \to B^\omega$ by
+          \[hd(map\;f\;as) = f(hd\;as); \qquad tl(map\;f\;as) = map\;f\;(tl\;as),\]
+          which corresponds to the coalgebra structure:
+          % https://q.uiver.app/#q=WzAsNCxbMCwwLCJBXlxcb21lZ2EiXSxbMiwwLCJBIFxcdGltZXMgQV5cXG9tZWdhIl0sWzAsMiwiQl5cXG9tZWdhIl0sWzIsMiwiQiBcXHRpbWVzIEJeXFxvbWVnYSJdLFswLDIsIm1hcFxcO2YiLDJdLFswLDEsIlxcbGFuZ2xlIGhkLCB0bCBcXHJhbmdsZSJdLFsyLDMsIlxcbGFuZ2xlIGhkICwgdGwgXFxyYW5nbGUiXSxbMSwzLCJpZCBcXHRpbWVzIG1hcFxcO2YiXV0=
+          \[\begin{tikzcd}
+              {A^\omega} && {A \times A^\omega} \\
+              \\
+              {B^\omega} && {B \times B^\omega}
+              \arrow["{map\;f}"', from=1-1, to=3-1]
+              \arrow["{\langle hd, tl \rangle}", from=1-1, to=1-3]
+              \arrow["{\langle hd , tl \rangle}", from=3-1, to=3-3]
+              \arrow["{id \times map\;f}", from=1-3, to=3-3]
+            \end{tikzcd}\]
+  \end{enumerate}
+\end{example}
+
+\emph{Coinduction} is a proof principle for showing \emph{behavioral equivalence}.
+\begin{definition}[Behavioral equivalence]
+  Let $F : \Set \to \Set$. Two elements of coalgebras $x \in (C,c), y \in (D,d)$ are called behavioral equivalent ``$x \sim y$'' if there exist
+  \[(C,c) \overset{h}{\longrightarrow} (E,e) \overset{k}{\longleftarrow} (D,d),\]
+  such that $h\;x = k\;y$.
+\end{definition}
+% TODO if \nu F exists, ...
+% TODO bisimilarity
+% TODO proof bisimilar \to \sim, etc
+% TODO examples of bisimilarity
 \section{Limits}
 \section{Colimits}