diff --git a/tex/.vscode/ltex.dictionary.en-US.txt b/tex/.vscode/ltex.dictionary.en-US.txt index a171c7f..e440aa4 100644 --- a/tex/.vscode/ltex.dictionary.en-US.txt +++ b/tex/.vscode/ltex.dictionary.en-US.txt @@ -43,3 +43,8 @@ Corecursion Coinduction Colimits Colimit +F-coalgebra +coalgebras +F-coalgebras +coalgebra +corecursion diff --git a/tex/catprog.sty b/tex/catprog.sty index ac3094d..5e495df 100644 --- a/tex/catprog.sty +++ b/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} diff --git a/tex/main.pdf b/tex/main.pdf index bcb2b27..bd02ec1 100644 Binary files a/tex/main.pdf and b/tex/main.pdf differ diff --git a/tex/main.tex b/tex/main.tex index f5ffd9d..7d337f9 100644 --- a/tex/main.tex +++ b/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} diff --git a/tex/sections/02_categories.tex b/tex/sections/02_categories.tex index b6f7de1..6d08326 100644 --- a/tex/sections/02_categories.tex +++ b/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} \ No newline at end of file