work on iteration chapter

thesis/src/04_iteration.tex

@@ -1,4 +1,98 @@
 \chapter{Iteration Algebras and Monads}
+In this chapter we will draw on the inherent connection between recursion and iteration to establish a partiality monad in a general setting without axioms that comes from previous results in the research on iteration theories. 
 \section{Elgot Algebras}
+
+% TODO check everything here more thoroughly
+
+\begin{definition}[Elgot Algebra]
+  A (unguarded) Elgot Algebra~\cite{uniformelgot} consists of:
+  \begin{itemize}
+    \item An object X
+    \item for every $f : S \rightarrow X + S$ the iteration $f^\# : S \rightarrow X$, satisfying:
+    \begin{itemize}
+      \item \textbf{Fixpoint}: $f^\# = [ id , f ^\# ] \circ f$
+      \item \textbf{Uniformity}: $(id + h) \circ f = g \circ h \Rightarrow f ^\# = g^\# \circ h$
+      \\ for $f : S \rightarrow X + S,\; g : R \rightarrow A + R,\; h : S \rightarrow R$
+      \item \textbf{Folding}: $((f^\# + id) \circ h)^\# = [ (id + inl) \circ f , inr \circ h ] ^\#$
+      \\ for $f : S \rightarrow A + S,\; h : R \rightarrow S + R$
+    \end{itemize}
+  \end{itemize}
+\end{definition}
+
+A morphism between Elgot algebras $h : (A, (-)^{\#_a}) \rightarrow (B, (-)^{\#_a})$ is an iteration preserving morphism $h : A \rightarrow B$ i.e. a morphism satisfying: $h \circ f^{\#_a} = ((h + id) \circ f)^{\#_b}$
+
+\begin{theorem}
+  Elgot algebras on a category $\mathcal{C}$ and the morphisms between them form a category that we call $\mathit{Elgot}(\mathcal{C})$.
+\end{theorem}
+\begin{proof}
+  The identity morphism $id : (A, (-)^\#) \rightarrow (A, (-)^\#)$ is the identity morphism of $\mathcal{C}$ that is trivially iteration preserving.
+
+  Composition of two morphisms $f : (B , (-)^{\#_b}) \rightarrow (C, (-)^{\#_c})$ and $g : (A , (-)^{\#_a}) \rightarrow (B , (-)^{\#_b})$ is the composition of the underlying morphisms, we are left to check that it is iteration preserving, i.e. let $X \in \obj{C}$ and $h : X \rightarrow A + X$:
+  \begin{alignat*}{1}
+    &f \circ g \circ h^{\#_a}\\
+    =\;& f \circ ((g + id) \circ h)^{\#_b}\tag*{g iteration preserving}\\
+    =\;&((f \circ g) \circ h)^{\#_c}\tag*{f iteration preserving}
+  \end{alignat*}
+
+  The laws concerning $id$ and composition follow directly since they hold in $\mathcal{C}$.
+\end{proof}
+
 \section{Pre-Elgot Monads}
-\section{The initial Pre-Elgot Monad}
+
+\begin{definition}[Pre-Elgot Monad]
+  A monad $\mathbf{T}$ is called pre-Elgot if every $TX$ extends to an Elgot algebra such that Kleisli lifting is iteration preversing, i.e.
+  \[h^* \circ f^\# = ((h^* + id) \circ f)^\#\qquad \text{for}\; f : Z \rightarrow TX + Z, h : X \rightarrow TY\]
+\end{definition}
+\section{The Initial Pre-Elgot Monad}
+In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial pre-Elgot monad.
+
+\begin{lemma}
+  If every $X \in \obj{C}$ extends to a free Elgot algebra $KX$ we get a monad $\mathbf{K}$.
+\end{lemma}
+\begin{proof}
+  Existence of all free objects in $\mathit{Elgot}(\mathcal{C})$ yields an adjunction between $\mathcal{C}$ and $\mathit{Elgot}(\mathcal{C})$ that in turn gives us a monad on $\mathcal{C}$.
+\end{proof}
+
+To show that $\mathbf{K}$ is strong we will need a notion of stability:
+
+\begin{definition}[Right-Stable Free Elgot Algebra]\label{def:rightstablefreeelgot}
+  Let $KY$ be a free Elgot algebra on $Y \in \obj{C}$. We call $KY$ \textit{right-stable} if for every $A \in \mathit{Elgot}(\mathcal{C})$ and $f : X \times Y \rightarrow A$ there exists a unique $f^\sharp_r : X \times KY \rightarrow A$ satisfying:
+  \begin{alignat*}{1}
+    &f = f^\sharp_r \circ (id \times \eta)\tag*{($\sharp_r 1$)}\label{sharpr1}\\
+    &f^\sharp_r \circ (id \times h^\#) = ((f + id) \circ dstl \circ (id \times h))^\#\tag*{($\sharp_r 2$)}\label{sharpr2}
+  \end{alignat*}
+  We also call the property that \ref{sharpr2} establishes \textit{right iteration preserving}.
+\end{definition}
+
+We get the following dual definition:
+
+\begin{definition}[Left-Stable Free Elgot Algebra]\label{def:leftstablefreeelgot}
+  Let $KY$ be a free Elgot algebra on $Y \in \obj{C}$. We call $KY$ \textit{left-stable} if for every $A \in \mathit{Elgot}(\mathcal{C})$ and $f : Y \times X \rightarrow A$ there exists a unique $f^\sharp_l : KY \times X \rightarrow A$ satisfying:
+  \begin{alignat*}{1}
+    &f = f^\sharp_l \circ (\eta \times id)\tag*{($\sharp_l 1$)}\label{sharpl1}\\
+    &f^\sharp_l \circ (h^\# \times id) = ((f + id) \circ dstr \circ (h \times id))^\#\tag*{($\sharp_l 2$)}\label{sharpl2}
+  \end{alignat*}
+  We also call the property that \ref{sharpl2} establishes \textit{left iteration preserving}.
+\end{definition}
+
+\begin{lemma}
+  Definitions \ref{def:rightstablefreeelgot} and \ref{def:leftstablefreeelgot} are equivalent in the sense that they imply each other.
+\end{lemma}
+\begin{proof} We show that we can derive both operators from each other, the full proof that the laws are satisfied is not very insightful and as such we just refer to the formalization.
+
+  \begin{itemize}
+    \item[$"\Rightarrow"$]\;\\
+    Given a left-stable free Elgot algebra $KY$ with an iteration operator $(-)^{\sharp_l}$, then $KY$ is also right-stable with the iteration operator $f^{\sharp_r} := (f \circ swap)^{\sharp_l} \circ swap$.
+    \item[$"\Leftarrow"$]\;\\
+    Dually given a right-stable free Elgot Algebra $KY$ with an iteration operator $(-)^{\sharp_r}$, then $KY$ is also left-stable with the iteration operator $f^{\sharp_l} := (f \circ swap)^{\sharp_r} \circ swap$.
+  \end{itemize}
+\end{proof}
+
+We will usually refer to right-stable free Elgot algebras as just stable Elgot algebras.
+
+\begin{theorem}
+  In a cartesian closed category every free Elgot algebra is stable.
+\end{theorem}
+\begin{proof}
+  asd
+\end{proof}