diff --git a/thesis/.vscode/ltex.hiddenFalsePositives.en-US.txt b/thesis/.vscode/ltex.hiddenFalsePositives.en-US.txt index 84ad58c..107d87d 100644 --- a/thesis/.vscode/ltex.hiddenFalsePositives.en-US.txt +++ b/thesis/.vscode/ltex.hiddenFalsePositives.en-US.txt @@ -20,3 +20,8 @@ {"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q test: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"} {"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"} {"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:diamond Diamond\\E$"} +{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object X for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"} +{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"} +{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"} +{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QA (unguarded) Elgot Algebra \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q consists of: An object A for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q the iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying: law:fixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:uniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:folding Folding: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"} +{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Qlaw:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q law:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"} diff --git a/thesis/src/04_iteration.tex b/thesis/src/04_iteration.tex index df71e64..a83f251 100644 --- a/thesis/src/04_iteration.tex +++ b/thesis/src/04_iteration.tex @@ -5,24 +5,43 @@ In this chapter we will draw on the inherent connection between partiality and i \improvement{Add some text} \unsure[inline]{Check types etc.} +\begin{definition}[Unguarded Elgot Algebra] + \todo[inline]{Definition unguarded Elgot algebra} +\end{definition} \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: + \item An object A + \item for every $f : X \rightarrow A + X$ the iteration $f^\# : X \rightarrow A$, satisfying: \begin{itemize} \item \customlabel{law:fixpoint}{\textbf{Fixpoint}}: $f^\# = [ id , f ^\# ] \circ f$ + \\ for $f : X \rightarrow A + X$ \item \customlabel{law:uniformity}{\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$ + \\ for $f : X \rightarrow A + X,\; g : Y \rightarrow A + Y,\; h : X \rightarrow Y$ \item \customlabel{law:folding}{\textbf{Folding}}: $((f^\# + id) \circ h)^\# = [ (id + inl) \circ f , inr \circ h ] ^\#$ - \\ for $f : S \rightarrow A + S,\; h : R \rightarrow S + R$ + \\ for $f : X \rightarrow A + X,\; h : Y \rightarrow X + Y$ \end{itemize} \end{itemize} \end{definition} -\todo[inline]{Diamond and stutter laws} -\customlabel{law:diamond}{\textbf{Diamond}} +\begin{lemma} + Every Elgot algebra $(A , (-)^\#)$ satisfies the following additional laws + + \begin{itemize} + \item \customlabel{law:stutter}{\textbf{Stutter}}: $(([ h , h ] + id) \circ f)^\# = (i_1 \circ h , [ h + i_1 , i_2 \circ i_2 ] )^\# \circ inr$ + \\ for $f : X \rightarrow (Y + Y) + X, h : Y \rightarrow A$ + \item \customlabel{law:diamond}{\textbf{Diamond}}: $((id + \Delta) \circ f)^\# = ([ i_1 , ((id + \Delta) \circ f)^\# + id] \circ f)^\#$ + \\ for $f : X \rightarrow A + (X + X)$ + \item \customlabel{law:compositionality}{\textbf{Compositionality}}: $((f^\# + id) \circ h)^\# = ([ (id + i_1) \circ f , i_2 \circ i_2 ] \circ [ i_1 , h ])^\# \circ i_2$ + \\ for $f : X \rightarrow A + X, h : Y \rightarrow X + Y$ + \end{itemize} +\end{lemma} +\begin{proof} + \todo[inline]{Prove diamond and stutter laws} +\end{proof} + +\todo[inline]{Mention here that previous lemma implies that unguarded Elgot are id guarded Elgot and diamond gives alternate way of classifying Elgot algebras citing Sergey} Morphisms between Elgot algebras that are coherent with respect to the iteration operator are of special interest to us, the following definition classifies them. @@ -707,7 +726,7 @@ The following Lemma is central to the proof of commutativity. \\=\;&(\pi_1 + (\pi_1 \circ \pi_1 \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id) \\=\;&(\pi_1 + \pi_1) \circ dstr \circ (\hat{f} \times id) \\=\;&\pi_1 \circ (\hat{f} \times id) - \\=\;&\hat{f} \circ \pi_1 + \\=\;&\hat{f} \circ \pi_1 . \end{alignat*} This concludes the proof. @@ -716,8 +735,8 @@ The following Lemma is central to the proof of commutativity. \begin{theorem} $\mathbf{K}$ is a commutative monad. \end{theorem} -\begin{proof} - We use remark~\ref{rem:proofbystability} again: +\begin{proof} We need to show that $\tau^* \circ \sigma = \sigma^* \circ \tau : KX \times KY \rightarrow K(X \times Y)$. + Let us proceed by right stability, consider the following diagram. % https://q.uiver.app/#q=WzAsNSxbMSwwLCJLWCBcXHRpbWVzIEtZIl0sWzMsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzEsMiwiSyhYIFxcdGltZXMgS1kpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMCwzLCJLWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdSJdLFswLDIsIlxcaGF0e1xcdGF1fSIsMl0sWzEsMywiXFxoYXR7XFx0YXV9XioiXSxbMiwzLCJcXHRhdV4qIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMywiXFxoYXR7XFx0YXV9IiwyLHsiY3VydmUiOjJ9XV0= \[\begin{tikzcd} & {KX \times KY} && {K(KX \times Y)} \\ @@ -731,11 +750,16 @@ The following Lemma is central to the proof of commutativity. \arrow["{id \times \eta}", curve={height=-12pt}, from=4-1, to=1-2] \arrow["{\sigma}"', curve={height=12pt}, from=4-1, to=3-4] \end{tikzcd}\] - \todo[inline]{Maybe don't omit proofs, give them point by point?} - The proofs for \ref{sharpr1} and the proof that $\sigma^* \circ \tau$ is right iteration preserving are straightforward and can be looked up in the formalization. - The proof that $\tau^* \circ \sigma$ is right iteration preserving is non-trivial, so we will look at it in more detail: - Let $Z \in \obj{\C}, h : Z \rightarrow KY + Z$ and let us introduce a definition for brevity: $\psi = \tau^* \circ \sigma$. We now use remark~\ref{rem:proofbyleftstability} to show that $\psi$ is right iteration preserving: + The diagram commutes since + \[\sigma^* \circ \tau \circ (id \times \eta) = \sigma^* \circ \eta = \sigma\] + and + \[\tau^* \circ \sigma \circ (id \times \eta) = \tau^* \circ K(id \times \eta) \circ \sigma = (\tau \circ (id \times \eta))^* \circ \sigma = \sigma.\] + + We are left to show that both $\sigma^* \circ \tau$ and $\tau^* \circ \sigma$ are right iteration preserving. Let $h : Z \rightarrow KY + Z$, indeed + \[\sigma^* \circ \tau \circ (id \times h^\#) = \sigma^* ((\tau + id) \circ dstl \circ (id \times h))^\# = (((\sigma^* \circ \tau) + id) \circ dstl \circ (id \times h))^\#. \] + + Let $\psi := \tau^* \circ \sigma$ and let us proceed by left stability to show that $\psi$ is right iteration preserving, consider the following diagram % https://q.uiver.app/#q=WzAsNCxbNCwwLCJLWCBcXHRpbWVzIEtZIl0sWzQsMSwiSyhYIFxcdGltZXMgWSkiXSxbMCwxLCJLWCBcXHRpbWVzIFoiXSxbMCwzLCJYIFxcdGltZXMgWiJdLFswLDEsIlxccHNpIl0sWzIsMCwiaWQgXFx0aW1lcyBoXlxcIyJdLFsyLDEsIigoXFxwc2kgKyBpZCkgXFxjaXJjIGRzdGwgXFxjaXJjIChpZCBcXHRpbWVzIGgpKV5cXCMiLDJdLFszLDIsIlxcZXRhIFxcdGltZXMgaWQiXSxbMywxLCJcXHRhdSBcXGNpcmMgKGlkIFxcdGltZXMgaF5cXCMpIiwyXV0= \[\begin{tikzcd} &&&& {KX \times KY} \\ @@ -748,8 +772,61 @@ The following Lemma is central to the proof of commutativity. \arrow["{\eta \times id}", from=4-1, to=2-1] \arrow["{\tau \circ (id \times h^\#)}"', from=4-1, to=2-5] \end{tikzcd}\] -\change[inline]{Be more specific} -\todo[inline]{Introduce Diamond and Stutter laws} + which commutes, since + \begin{alignat*}{1} + &\psi \circ (id \times h^\#) \circ (\eta \times id) + \\=\;&\psi \circ (\eta \times id) \circ (id \times h^\#) + \\=\;&\tau^* \circ \eta \circ (id \times h^\#) + \\=\;&\tau \circ (id \times h^\#) + \\=\;&((\tau + id) \circ dstl \circ (id \times h))^\# + \\=\;&((\psi + id) \circ dstl \circ (id \times h))^\# \circ (\eta \times id).\tag{\ref{law:uniformity}} + \end{alignat*} + + We are left to show that both $\psi \circ (id \times h^\#)$ and $((\psi + id) \circ dstl \circ (id \times h))^\#$ are left iteration preserving. Let $g : A \rightarrow KX + A$, then $\psi \circ (id \times h^\#)$ is left iteration preserving, since + \begin{alignat*}{1} + &\psi \circ (id \times h^\#) \circ (g^\# \times id) + \\=\;&\psi \circ (g^\# \times id) \circ (id \times h^\#) + \\=\;&\tau^* \circ ((\sigma + id) \circ dstr \circ (g \times id))^\# \circ (id \times h^\#) + \\=\;&((\psi + id) \circ dstr \circ (g \times id))^\# \circ (id \times h^\#) + \\=\;&(((\psi \circ (id \times h^\#)) + id) \circ dstr \circ (g \times id))^\#.\tag{\ref{law:uniformity}} + \end{alignat*} + + Lastly, we need to show that + \[((\psi + id) \circ dstl \circ (id \times h))^\# \circ (g^\# \times id) = ((((\psi + id) \circ dstl \circ (id \times h))^\# + id) \circ dstr \circ (g \times id))^\#.\] + Note that by \ref{law:uniformity} the left-hand side can be rewritten as + \[((((\psi + id) \circ dstr \circ (g \times id))^\# + id) \circ dstl \circ (id \times h))^\#.\] + + Consider now, that + \begin{alignat*}{1} + &((((\psi + id) \circ dstl \circ (id \times h))^\# + id) \circ dstr \circ (g \times id))^\# + \\=\;&(((((\psi + id) \circ dstl \circ (id \times h))^\#)^* + id) \circ (\eta + id) \circ dstr \circ (g \times id))^\# + \\=\;&(((\psi + id) \circ dstl \circ (id \times h))^\#)^* \circ ((\eta + id) \circ dstr \circ (g \times id))^\# + \\=\;&(((\psi + id) \circ dstl \circ (id \times h))^\#)^* \circ (((\sigma \circ (\eta \times id)) + id) \circ dstr \circ (g \times id))^\# + \\=\;&(((\psi + id) \circ dstl \circ (id \times h))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id) + \\=\;&(((\psi^* + id) \circ (\eta + id) \circ dstl \circ (id \times h))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id) + \\=\;&\psi^* \circ (((\eta + id) \circ dstl \circ (id \times h))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id) + \\=\;&\psi^* \circ (((\eta + id) \circ dstl \circ (id \times h))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id) + \\=\;&\psi^* \circ ((((\tau \circ (id \times \eta)) + id) \circ dstl \circ (id \times h))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id) + \\=\;&\psi^* \circ (((\tau + id) \circ dstl \circ (id \times ((\eta + id) \circ h)))^\#)^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id) + \\=\;&\psi^* \circ (\tau \circ (id \times ((\eta + id) \circ h)^\#))^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times id) + \\=\;&\psi^* \circ \tau^* \circ K(id \times ((\eta + id) \circ h)^\#) \circ \sigma \circ (((\eta + id) \circ g)^\# \times id) + \\=\;&\psi^* \circ \tau^* \circ \sigma \circ (id \times ((\eta + id) \circ h)^\#) \circ (((\eta + id) \circ g)^\# \times id) + \\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#), + \end{alignat*} + and by a symmetric argument + \begin{alignat*}{1} + &((((\psi + id) \circ dstr \circ (g \times id))^\# + id) \circ dstl \circ (id \times h))^\# + \\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#). + \end{alignat*} + + We are thus done by + \begin{alignat*}{1} + &((\psi + id) \circ dstl \circ (id \times h))^\# \circ (g^\# \times id) + \\=\;&((((\psi + id) \circ dstr \circ (g \times id))^\# + id) \circ dstl \circ (id \times h))^\#\tag{\ref{law:uniformity}} + \\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#) + \\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\# \times ((\eta + id) \circ h)^\#)\tag{\ref{lem:KCommKey}} + \\=\;&((((\psi + id) \circ dstl \circ (id \times h))^\# + id) \circ dstr \circ (g \times id))^\#. + \end{alignat*} \end{proof} \begin{theorem}\label{thm:Klifting}