Algebra of Programming - A Rival Summary

Note that this quite an opionated summary, using different notation and skipping over a lot of preliminaries.
See also An (exhaustive enough) Algebra of Programming Summary

A foray into domain theory

A ω-complete partial order (cpo) is a partial order \((X, \leq)\) with

  • minimal element (denoted as \(\bot\))
  • every ω-chain \(x_1 \leq x_2\leq\dots\) has a least upper bound (denoted as \(\bigvee_{i\in \mathbb{N}}x_i\))

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)\))

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\).

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 ω-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\).

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:
f-algebra.svg

F-algebras and F-algebra homomorphisms form a category \(\mathsf{Alg}(F)\)

The initial object in \(\mathsf{Alg}(F)\) is called the initial F-algebra.

Identity law

Let \((I,i)\) be the initial F-algebra. Then \(\mathrm{Hom}_{\mathsf{Alg}(F)}(I,I) = \{\mathrm{id}_I\}\)

Fusion law

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:
fusion.svg

Lambeks Lemma

Let \((I,i)\) be the initial F-algebra. Then \(i\) is an isomorphism in \(\mathcal{C}\)

In the diagram
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}\)

Closedness under limits

Let \(F : \mathcal{C} \to \mathcal{C}\).
Then \(\mathsf{Alg}(F)\) is closed under limits in \(\mathcal{C}\).

Closedness under preserved colimits

Let \(F : \mathcal{C} \to \mathcal{C}\).
Then \(\mathsf{Alg}(F)\) is closed under limits in \(\mathcal{C}\) preserved by \(F\).

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)\).

\(\mathsf{Coalg}(F) = (\mathsf{Alg}(F)^{\mathrm{op}})^{\mathrm{op}}\)

Co-Lambeks Lemma

Let \((T,t)\) be the terminal coalgebra. Then \(t\) is an isomorphism in \(\mathcal{C}\)

Dual to the proof of Lambeks lemma.

Closedness under colimits

Let \(F : \mathcal{C} \to \mathcal{C}\).
Then \(\mathsf{Coalg}(F)\) is closed under colimits in \(\mathcal{C}\).

Closedness under preserved limits

Let \(F : \mathcal{C} \to \mathcal{C}\).
Then \(\mathsf{Coalg}(F)\) is closed under colimits in \(\mathcal{C}\) preserved by \(F\).

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 ω-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 ω-chain in \(\mathsf{Set}\). The direct limit of that chain \(\bigcup_{i \in \mathbb{N}} A_i\).

Let \(F : (\mathbb{N}, \leq) \to \mathsf{Set}\) be an ω-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)\]

ω-cocontinuity
A functor is called ω-cocontinuous if it preserves colimits of ω-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))\).

Let \(F\) be a functor. If \(F\) is finitary, then it is also ω-cocontinuous.

Finitary functors are closed under

  • composition
  • finite products
  • arbitrary coproducts

Let \(F : \mathcal{C} \to \mathcal{C}\) be ω-cocontinuous. Then \(F\) has the initial algebra \(\mu F = \mathrm{colim}_{n \in \mathbb{N}}F^n \bot\).

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:

init-limit.svg
Since \(F\) preservers colimits we get another initial cocone by applying \(F\):
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:
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)\).

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

\(F\) finitary \(\nRightarrow\) \(F\) \(\omega^{\mathrm{op}}\)-continuous

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\).

Dual to the proof for the initial algebra construction.

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.

Corecursion and coinduction

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)\).

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) \]

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:
bisim.svg

\(x,y\) bisimilar \(\implies x\sim y\)

Let \(R \subseteq C \times D\) be a bisimulation. We form the pushout of \(\pi_0, \pi_1\) in \(\mathsf{Coalg}(F)\):
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)\).

If \(R \subseteq \nu F \times \nu F\) and \(x,y \in \nu F\) bisimilar, then \(x = y\).