#+title: Algebra of Programming - A Rival Summary #+author: Florian Guthmann #+email: florian.guthmann@fau.de #+options: num:nil \n:t html-style:nil html5-fancy:t html-postamble:nil toc:nil #+html_doctype: xhtml5 #+html_head: #+html_head: #+html_mathjax: path:/~oc45ujef/mathjax/es5/tex-mml-chtml.js #+macro: abbr @@html:$1@@ Note that this quite an opionated summary, using different notation and skipping over a lot of preliminaries. See also [[https://wwwcip.cs.fau.de/~oj14ozun/src+etc/algprog-summary.pdf][An (exhaustive enough) /Algebra of Programming/ Summary]] * A foray into domain theory #+begin_definition A *\omega-complete partial order* (cpo) is a partial order $(X, \leq)$ with - minimal element (denoted as $\bot$) - every \omega-chain $x_1 \leq x_2\leq\dots$ has a least upper bound (denoted as $\bigvee_{i\in \mathbb{N}}x_i$) #+end_definition #+begin_definition A function $f : (X, \leq_X) \to (Y, \leq_Y)$ is called *continuous* if - it is monotone (i.e. $\forall x, y \in X.\ x \leq_X y \implies f(x) \leq_Y f(y) $) - it preserves least upper bounds (i.e. $\forall (x_i)_{i \in \mathbb{N}}.\ f(\bigvee x_i) = \bigvee f(x_i)$) #+end_definition #+begin_theorem Let $(X,\leq)$ be a cpo, $f : X \to X$ be continuous. Then $\mu f = \bigvee_{n \in \mathbb{N}}f^i(\bot)$ is the least fixpoint of $f$. #+end_theorem #+begin_proof By minimality we get $\bot \leq f(\bot)$. Since $f$ is monotone it also holds that $\bot \leq f(\bot) \leq f(f(\bot)) \leq \dots$. Therefore $f^i(\bot)$ forms an \omega-chain, which has a least upper bound $\mu f$. To show that $\mu f$ is a fixpoint of $f$: \[ f(\mu f) = f\left(\bigvee_{i \in \mathbb{N}}f^i(\bot)\right) \overset{f~\text{continuous}}{=} \bigvee_{i \in \mathbb{N}} f^{i+1}(\bot) = \bigvee_{i \in \mathbb{N}} f^{i}(\bot) = \mu f \] Let $x \in X$ be a prefixpoint of $f$ (i.e. $f(x) \leq x$). By induction over $n$, we show that $f^n(\bot) \leq x$ for all $n$: - if $n=0$, the $f^0(\bot) = \bot \leq x$ holds by minimality - Suppose that $f^n(\bot) \leq x$. By monotonicity we get $f^{n+1}(\bot) \leq f(x)$, and by transitivity we conclude $f^{n+1}(\bot) \leq x$. So $\mu f$ is a fixpoint and the least prefixpoint (and therefore the least fixpoint) of $f$. #+end_proof * F-algebras Let $\mathcal{C}$ be a category and $F : \mathcal{C} \to \mathcal{C}$. A *F-algebra* is a pair $(A \in \mathrm{Ob}~\mathcal{C}, a : F A \to A)$. A $f \in \mathrm{Hom}_{\mathcal{C}}(A,B)$ is a *F-algebra homomorphism* between F-algebras $(A,a), (B,b)$ if the following diagram commutes: [[file:res/f-algebra.svg]] #+begin_lemma F-algebras and F-algebra homomorphisms form a category $\mathsf{Alg}(F)$ #+end_lemma The initial object in $\mathsf{Alg}(F)$ is called the *initial F-algebra*. - Identity law :: #+begin_theorem Let $(I,i)$ be the initial F-algebra. Then $\mathrm{Hom}_{\mathsf{Alg}(F)}(I,I) = \{\mathrm{id}_I\}$ #+end_theorem - Fusion law :: #+begin_theorem Let $f : (A,a) \to (B,b)$ be a F-algebra homomorphism, $(I,i)$ the initial F-algebra. Then the following diagram (known colloquially as "the Apollo 11 command module") commutes: [[file:res/fusion.svg]] #+end_theorem - Lambeks Lemma :: #+begin_lemma Let $(I,i)$ be the initial F-algebra. Then $i$ is an isomorphism in $\mathcal{C}$ #+end_lemma #+begin_proof In the diagram [[file:res/lambek.svg]] The lower square commutes obviously, the upper square by initiality of $(I,i)$. Then $i \circ h = \mathrm{id}_I$ follows again by initiality. Lastly we get $h \circ i = Fi \circ Fh = F (i \circ h) = F \mathrm{id}_{I} = \mathrm{id}_{FI}$ #+end_proof - Closedness under limits :: #+begin_theorem Let $F : \mathcal{C} \to \mathcal{C}$. Then $\mathsf{Alg}(F)$ is closed under limits in $\mathcal{C}$. #+end_theorem - Closedness under preserved colimits :: #+begin_theorem Let $F : \mathcal{C} \to \mathcal{C}$. Then $\mathsf{Alg}(F)$ is closed under limits in $\mathcal{C}$ preserved by $F$. #+end_theorem * F-coalgebras Dually, a *F-coalgebra* is a pair $(A \in \mathrm{Ob}~\mathcal{C}, a : F A \to A, a : A \to F A)$. F-coalgebras with F-coalgebra homomorphisms (defined in the obvious way) form the category $\mathsf{Coalg}(F)$. #+begin_remark $\mathsf{Coalg}(F) = (\mathsf{Alg}(F)^{\mathrm{op}})^{\mathrm{op}}$ #+end_remark - Co-Lambeks Lemma :: #+begin_lemma Let $(T,t)$ be the terminal coalgebra. Then $t$ is an isomorphism in $\mathcal{C}$ #+end_lemma #+begin_proof Dual to the proof of Lambeks lemma. #+end_proof - Closedness under colimits :: #+begin_theorem Let $F : \mathcal{C} \to \mathcal{C}$. Then $\mathsf{Coalg}(F)$ is closed under colimits in $\mathcal{C}$. #+end_theorem - Closedness under preserved limits :: #+begin_theorem Let $F : \mathcal{C} \to \mathcal{C}$. Then $\mathsf{Coalg}(F)$ is closed under colimits in $\mathcal{C}$ preserved by $F$. #+end_theorem * Initial algebra construction Let $\mathcal{C}$ be a cocomplete category, $\bot$ the initial object in $\mathcal{C}$. - direct limit :: Let $\mathcal{J}$ be the poset category $(\mathbb{N}, \leq)$. The colimit of a Functor $F : \mathcal{J} \to \mathcal{C}$ is called the *direct limit* of $F$. $F(0) \to F(1) \to \dots$ is called an *\omega-chain*. For $n,m \in \mathbb{N}$ let $f_{n,m}$ denote the unique morphism from $F n$ to $F m$. - direct limit in $\mathsf{Set}$ :: Let $A_0 \subseteq A_1 \subseteq \dots$ be an \omega-chain in $\mathsf{Set}$. The direct limit of that chain $\bigcup_{i \in \mathbb{N}} A_i$. #+begin_lemma Let $F : (\mathbb{N}, \leq) \to \mathsf{Set}$ be an \omega-chain. Then the direct limit of $F$ is given by \[ \coprod_{i \in \mathbb{N}} F(i)/_\sim \] where $\sim$ is the equivalence relation given by \[(a,n) \sim (b,m) :\Leftrightarrow \exists k \geq m,n .\ f_{n,k}(a) = f_{m,k}(b)\] #+end_lemma - \omega-cocontinuity :: A functor is called *\omega-cocontinuous* if it preserves colimits of \omega-chains - finitary functor :: A functor $F : \mathsf{Set} \to \mathsf{Set}$ is called *finitary* if for any set $X$ and $x \in F(X)$ there exists a finite set $Y$ together with an injection $m : Y \hookrightarrow X$ and $y \in F(Y)$ such that $x = F(m(y))$. #+begin_lemma Let $F$ be a functor. If $F$ is finitary, then it is also \omega-cocontinuous. #+end_lemma #+begin_lemma Finitary functors are closed under - composition - finite products - arbitrary coproducts #+end_lemma #+begin_theorem Let $F : \mathcal{C} \to \mathcal{C}$ be \omega-cocontinuous. Then $F$ has the initial algebra $\mu F = \mathrm{colim}_{n \in \mathbb{N}}F^n \bot$. #+end_theorem #+begin_proof Let $D : (\mathbb{N}, \leq) \to \mathcal{C}$ be the functor defined by $D n = F^n\bot$. Since $\mathcal{C}$ is cocomplete the limit of $D$ must exist and is given by $I$ and cocone $\iota : FD \Rightarrow \Delta(I)$ such that the following diagram commutes: [[file:res/init-limit.svg]] Since $F$ preservers colimits we get another initial cocone by applying $F$: [[file:res/finit-limit.svg]] The structure morphism $s : FI \to I$ is given by initiality of the cocone $(FI, F\iota)$. It follows that $(I, s)$ is a $F$-algebra. Let $(A, a)$ be an F-algebra. Then let $a_n$ be defined as follows: [[file:res/an.svg]] where $a_0$ is given by initiality and \[ a_{n+1} = a \circ Fa_n \] By induction over $n$ we get that $(A, a_n)$ form a cocone over $D$. By initiality of $(I, \iota)$ in $\mathsf{cocone}(D)$ we get a morphism $h : I \to A$. What is left is to show that $h$ is an $F$-algebra homomorphism, and unique in $\mathsf{Alg}(F)$. #+end_proof * Terminal coalgebra construction Let $D$ be a functor $(\mathbb{N}, \leq)^{\mathrm{op}} \to \mathcal{C}$. Then $D0 \leftarrow D1 \leftarrow \dots$ is called $\omega^{\mathrm{op}}$ -chain in $\mathcal{C}$. - $\omega^{\mathrm{op}}$-continuous :: A Functor is called *$\omega^{\mathrm{op}}$-continuous* if it preserves limits of $\omega^{\mathrm{op}}$-chains For every set $A$ the constant functor $\Delta(A) : \mathsf{Set} \to \mathsf{Set}$ is $\omega^{\mathrm{op}}$-continuous. The class of functors $F : \mathsf{Set} \to \mathsf{Set}$ is closed under - composition - products - coproducts #+begin_remark $F$ finitary $\nRightarrow$ $F$ $\omega^{\mathrm{op}}$-continuous #+end_remark #+begin_theorem Let $\mathcal{C}$ be complete, $F: \mathcal{C} \to \mathcal{C}$ a functor that is $\omega^{\mathrm{op}}$-continuous. Let $\top$ denote the terminal object in $\mathcal{C}$ Then $\mathrm{lim}_{n<\omega}F^n\top$ is the terminal coalgebra of $F$. #+end_theorem #+begin_proof Dual to the proof for the initial algebra construction. #+end_proof #+begin_theorem Let $F : \mathsf{Set} \to \mathsf{Set}$ be finitary. Let $\top$ denote the terminal object in $\mathsf{Set}$. Then $F^{\omega+\omega}\top$ is the teriminal $F$-coalgebra. #+end_theorem * Corecursion and coinduction #+begin_definition Let $F : \mathsf{Set} \to \mathsf{Set}$, $(C, c), (D,d)$ be coalgebras on $F$, $x\in C$ and $y \in D$. Then $x$ and $y$ are *behaviourly equivalent* (denoted $x \sim y$) iff there exists a coalgebra $(E,e)$ with coalgebra homomorphisms $h : C \to E$ and $k : D \to E$ such that $h(x) = k(y)$. #+end_definition #+begin_theorem If the terminal coalgebra $\nu F$ exists with $h_C : C \to \nu F, h_D : D \to \nu F$ being the unique coalgebra homomorphisms then \[ x \sim y \Leftrightarrow h_C(x) = h_D(x) \] #+end_theorem #+begin_definition Let $F : \mathsf{Set} \to \mathsf{Set}$ and $(C,c), (D,d)$ be coalgebras on $F$. A *bisimulation* is a relation $R \subseteq C \times D$ such that there exists an $r : R \to FR$ with: [[file:res/bisim.svg]] #+end_definition #+begin_theorem $x,y$ bisimilar $\implies x\sim y$ #+end_theorem #+begin_proof Let $R \subseteq C \times D$ be a bisimulation. We form the pushout of $\pi_0, \pi_1$ in $\mathsf{Coalg}(F)$: [[file:res/bisim-pushout2.svg]] Which commutes by the universal property of the pushout $(P,h_C,h_D)$. We get $h_C\circ \pi_0 = h_D\circ \pi_1$, and therefore $h_C(x) = h_D(y)$. #+end_proof #+begin_remark If $R \subseteq \nu F \times \nu F$ and $x,y \in \nu F$ bisimilar, then $x = y$. #+end_remark