mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
work on thesis
This commit is contained in:
parent
7986abb134
commit
58d47f7b41
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
6 changed files with 210 additions and 69 deletions
1
.gitignore
vendored
1
.gitignore
vendored
|
|
@ -56,3 +56,4 @@ thesis/main.bbl-SAVE-ERROR
|
|||
thesis/main.bcf-SAVE-ERROR
|
||||
thesis/main.tdo
|
||||
main.synctex(busy)
|
||||
thesis/main.pyg
|
||||
|
|
|
|||
1
thesis/.vscode/ltex.dictionary.en-US.txt
vendored
1
thesis/.vscode/ltex.dictionary.en-US.txt
vendored
|
|
@ -62,3 +62,4 @@ Corecursion
|
|||
subobject
|
||||
isomorphisms
|
||||
epicness
|
||||
fixpoint
|
||||
|
|
|
|||
|
|
@ -16,3 +16,6 @@
|
|||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QIt suffices to show \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, because then follows: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q We prove this by coinduction using: &&& &&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\Q[inline]Move this remark to the beginning of proof The first step in both equations can be proven by monicity of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and then using \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and the dual diagram for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which is a direct consequence of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q: &&&& &&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||
{"rule":"ENGLISH_WORD_REPEAT_RULE","sentence":"^\\QTo show that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q it suffices to show that there exists a coalgebra structure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q such that the following diagrams commute: &&&&&& &&&&&& \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Uniqueness of the coalgebra morphism \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q then results in \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\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 Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q 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]+\\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]+$"}
|
||||
|
|
|
|||
|
|
@ -114,8 +114,10 @@
|
|||
\newcommand*{\elgotalgs}[1]{\ensuremath{\mathit{ElgotAlgs}(#1)}}
|
||||
% category of monads on #1
|
||||
\newcommand*{\monads}[1]{\ensuremath{\mathit{Monads}(#1)}}
|
||||
\newcommand*{\strongmonads}[1]{\ensuremath{\mathit{StrongMonads}(#1)}}
|
||||
% category of pre-Elgot monads on #1
|
||||
\newcommand*{\preelgot}[1]{\ensuremath{\mathit{PreElgot}(#1)}}
|
||||
\newcommand*{\strongpreelgot}[1]{\ensuremath{\mathit{StrongPreElgot}(#1)}}
|
||||
\newcommand*{\setoids}{\ensuremath{\mathit{Setoids}}}
|
||||
% free objects
|
||||
\newcommand*{\freee}[1]{\ensuremath{#1^\bigstar}}
|
||||
|
|
@ -151,6 +153,14 @@ Erlangen, \today{} \rule{7cm}{1pt}\\
|
|||
\newcommandx{\info}[2][1=]{\todo[inline,linecolor=OliveGreen,backgroundcolor=OliveGreen!25,bordercolor=OliveGreen,#1]{#2}}
|
||||
\newcommandx{\improvement}[2][1=]{\todo[inline,linecolor=Plum,backgroundcolor=Plum!25,bordercolor=Plum,#1]{#2}}
|
||||
|
||||
% for creating custom labels like (Fixpoint)
|
||||
\makeatletter
|
||||
\newcommand{\customlabel}[2]{%
|
||||
\protected@write \@auxout {}{\string \newlabel {#1}{{#2}{\thepage}{#2}{#1}{}} }%
|
||||
\hypertarget{#1}{#2}%
|
||||
}
|
||||
\makeatother
|
||||
|
||||
|
||||
% \include{src/examples}
|
||||
\include{src/00_introduction}
|
||||
|
|
|
|||
|
|
@ -294,30 +294,27 @@ Monads are widely known among programmers as a way of modelling effects in pure
|
|||
\end{tikzcd}\]
|
||||
\end{definition}
|
||||
|
||||
% Morphisms between monads are natural transformations that respect the monad operations:
|
||||
As with many categorical concepts we may consider the category of monads:
|
||||
|
||||
% \begin{definition}[Monad Morphism]
|
||||
% A morphism between monads $(S, \eta^S, \mu^S)$ and $(T, \eta^T, \mu^T)$ is a natural transformation $\alpha : S \rightarrow T$ between the underlying functors satisfying:
|
||||
% % https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzIsMCwiU1giXSxbMiwxLCJUWCJdLFszLDAsIlNTWCJdLFs1LDAsIlNUWCJdLFszLDEsIlNYIl0sWzcsMCwiVFRYIl0sWzcsMSwiVFgiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl1d
|
||||
% \[\begin{tikzcd}[ampersand replacement=\&]
|
||||
% X \&\& SX \& SSX \&\& STX \&\& TTX \\
|
||||
% \&\& TX \& SX \&\&\&\& TX
|
||||
% \arrow["{\eta^S}", from=1-1, to=1-3]
|
||||
% \arrow["\alpha", from=1-3, to=2-3]
|
||||
% \arrow["{\eta^T}"', from=1-1, to=2-3]
|
||||
% \arrow["S\alpha", from=1-4, to=1-6]
|
||||
% \arrow["{\mu^S}"', from=1-4, to=2-4]
|
||||
% \arrow["\alpha", from=1-6, to=1-8]
|
||||
% \arrow["\alpha"', from=2-4, to=2-8]
|
||||
% \arrow["{\mu^T}", from=1-8, to=2-8]
|
||||
% \end{tikzcd}\]
|
||||
% \end{definition}
|
||||
|
||||
% \begin{definition}[The Category of Monads]
|
||||
% Monads on a category $\C$ together with monad morphisms form a category that we call $\monads{\C}$. The identity morphism is the identity natural transformation that trivially respects the monad operations and composition of morphisms is composition of natural transformations.
|
||||
% \end{definition}
|
||||
\begin{definition}[The Category of Monads]~\label{def:monads}
|
||||
Let $\C$ be a category.
|
||||
A morphism between monads $(S : \C \rightarrow \C, \eta^S, \mu^S)$ and $(T : \C \rightarrow \C, \eta^T, \mu^T)$ is a natural transformation $\alpha : S \rightarrow T$ between the underlying functors satisfying:
|
||||
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzIsMCwiU1giXSxbMiwxLCJUWCJdLFszLDAsIlNTWCJdLFs1LDAsIlNUWCJdLFszLDEsIlNYIl0sWzcsMCwiVFRYIl0sWzcsMSwiVFgiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl1d
|
||||
\[\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \&\& SX \& SSX \&\& STX \&\& TTX \\
|
||||
\&\& TX \& SX \&\&\&\& TX
|
||||
\arrow["{\eta^S}", from=1-1, to=1-3]
|
||||
\arrow["\alpha", from=1-3, to=2-3]
|
||||
\arrow["{\eta^T}"', from=1-1, to=2-3]
|
||||
\arrow["S\alpha", from=1-4, to=1-6]
|
||||
\arrow["{\mu^S}"', from=1-4, to=2-4]
|
||||
\arrow["\alpha", from=1-6, to=1-8]
|
||||
\arrow["\alpha"', from=2-4, to=2-8]
|
||||
\arrow["{\mu^T}", from=1-8, to=2-8]
|
||||
\end{tikzcd}\]
|
||||
|
||||
% \improvement[inline]{Explain benefits of initial monad}
|
||||
This yields the category of monads on $\C$ which we call $\monads{\C}$. The identity morphism of $\monads{\C}$ is the identity natural transformation $Id : F \rightarrow F$ which trivially respects the monad unit and multiplication. Composition of monad morphisms is composition of the underlying natural transformation, the diagrams then also follow easily.
|
||||
\end{definition}
|
||||
|
||||
Monads can also be specified in a second equivalent way that is better suited to describe computation.
|
||||
|
||||
|
|
@ -330,8 +327,6 @@ Monads can also be specified in a second equivalent way that is better suited to
|
|||
\end{alignat*}
|
||||
\end{definition}
|
||||
|
||||
% In functional programming languages like Haskell the Kleisli lifting $(-)^*$ is usually called \textit{bind} or written infix as \mintinline{haskell}{>>=} and $\eta$ is called $return$. Given two programs $f : X \rightarrow MY, g : Y \rightarrow MZ$, where $M$ is a Kleisli triple the composition $g^* \circ f$ can then be (in a pointful manner) written as \mintinline{haskell}{f x >>= g} or using Haskell's do-notation:
|
||||
|
||||
Let $f : X \rightarrow TY, g : Y \rightarrow TZ$ be two programs, where $T$ is a Kleisli triple. These programs can be composed by taking: $f^* \circ g : X \rightarrow TZ$, which is called Kleisli composition. Haskell's do-notation is a useful tool for writing Kleisli composition in a legible way. $f^* \circ g$ can equivalently be expressed as:
|
||||
\begin{minted}{haskell}
|
||||
do y <- f x
|
||||
|
|
@ -387,7 +382,9 @@ When modelling partiality with a monad, one would expect the following two progr
|
|||
\end{multicols}
|
||||
where p and q are (partial) computations. This condition can be expressed categorically, but first we need another definition:
|
||||
|
||||
\begin{definition}[Strong Monad] A monad $(T, \eta, \mu)$ on a cartesian category $\C$ is called strong if there exists a natural transformation $\tau_{X,Y} : X \times TY \rightarrow T(X \times Y)$, satisfying the following conditions:
|
||||
\change[inline]{Find Motivation for strong monads}
|
||||
|
||||
\begin{definition}[Strong Monad] A monad $(T, \eta, \mu)$ on a cartesian category $\C$ is called strong if there exists a natural transformation $\tau_{X,Y} : X \times TY \rightarrow T(X \times Y)$ that satisfies the following conditions:
|
||||
\begin{alignat*}{2}
|
||||
&T\pi_2 \circ \tau_{1,X} &&= \pi_2 \tag*{(S1)}\label{S1}\\
|
||||
&\tau_{X,Y} \circ (id_X \times \eta_Y) &&= \eta_{X\times Y} \tag*{(S2)}\label{S2}\\
|
||||
|
|
@ -397,9 +394,27 @@ where p and q are (partial) computations. This condition can be expressed catego
|
|||
where $\alpha_{X,Y,Z} = \langle \langle \pi_1 , \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2 \rangle : X \times (Y \times Z) \rightarrow (X \times Y) \times Z$ is the associativity morphism on products.
|
||||
\end{definition}
|
||||
|
||||
As with monads we can now consider the category of strong monads:
|
||||
\begin{definition}[The Category of Strong Monads]\label{def:strongmonads}
|
||||
Let $\C$ be a category. A morphism between two strong monads $(S : \C \rightarrow \C, \eta^S, \mu^S, \tau^S)$ and $(T : \C \rightarrow \C, \eta^T, \mu^T, \tau^T)$ is a morphism between monads as in \autoref{def:monads} that additionally satisfies:
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgU1kiXSxbMCwyLCJTKFggXFx0aW1lcyBZKSJdLFsyLDIsIlQoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIFRZIl0sWzAsMSwiXFx0YXVeUyJdLFsxLDIsIlxcYWxwaGEiXSxbMCwzLCJpZCBcXHRpbWVzIFxcYWxwaGEiXSxbMywyLCJcXHRhdV5UIiwyXV0=
|
||||
\[\begin{tikzcd}[ampersand replacement=\&]
|
||||
{X \times SY} \&\& {X \times TY} \\
|
||||
\\
|
||||
{S(X \times Y)} \&\& {T(X \times Y)}
|
||||
\arrow["{\tau^S}", from=1-1, to=3-1]
|
||||
\arrow["\alpha", from=3-1, to=3-3]
|
||||
\arrow["{id \times \alpha}", from=1-1, to=1-3]
|
||||
\arrow["{\tau^T}"', from=1-3, to=3-3]
|
||||
\end{tikzcd}\]
|
||||
This yields the category $\strongmonads{\C}$ of strong monads over $\C$.
|
||||
\end{definition}
|
||||
|
||||
Now we can express the above condition:
|
||||
\begin{definition}[Commutative Monad]
|
||||
A strong monad $\mathbf{T}$ is called commutative if the (right) strength $\tau$ commutes with the induced (left) strength $\sigma_{X,Y} = Mswap \circ \tau_{Y,X} \circ swap$. Concretely if the following equation holds:
|
||||
A strong monad $\mathbf{T}$ is called commutative if the (right) strength $\tau$ commutes with the induced (left) strength:
|
||||
\[\sigma_{X,Y} = Mswap \circ \tau_{Y,X} \circ swap : TX \times Y \rightarrow T(X \times Y)\]
|
||||
Concretely, $\mathbf{T}$ is called strong if the following diagram commutes:
|
||||
% https://q.uiver.app/#q=WzAsNCxbMCwyLCJUKFggXFx0aW1lcyBUWSkiXSxbMiwwLCJUKFRYIFxcdGltZXMgWSkiXSxbMiwyLCJUKFggXFx0aW1lcyBZKSJdLFswLDAsIlRYIFxcdGltZXMgVFkiXSxbMywxLCJcXHRhdSJdLFszLDAsIlxcc2lnbWEiLDJdLFswLDIsIlxcdGF1XioiLDJdLFsxLDIsIlxcc2lnbWFeKiJdXQ==
|
||||
\[\begin{tikzcd}
|
||||
{TX \times TY} && {T(TX \times Y)} \\
|
||||
|
|
|
|||
|
|
@ -12,10 +12,10 @@ In this chapter we will draw on the inherent connection between partiality and i
|
|||
\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$
|
||||
\item \customlabel{law:fixpoint}{\textbf{Fixpoint}}: $f^\# = [ id , f ^\# ] \circ f$
|
||||
\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$
|
||||
\item \textbf{Folding}: $((f^\# + id) \circ h)^\# = [ (id + inl) \circ f , inr \circ h ] ^\#$
|
||||
\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$
|
||||
\end{itemize}
|
||||
\end{itemize}
|
||||
|
|
@ -23,7 +23,8 @@ In this chapter we will draw on the inherent connection between partiality and i
|
|||
|
||||
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}$ for any $f : X \rightarrow A + X$.
|
||||
|
||||
\begin{theorem}
|
||||
\change[inline]{This should not be a theorem}
|
||||
\begin{theorem}~\label{def:elgotalgebras}
|
||||
Elgot algebras on a category $\C$ and the morphisms between them form a category that we call $\elgotalgs{\C}$.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
|
|
@ -50,70 +51,180 @@ We can form products and exponentials of Elgot algebras in a canonical way, for
|
|||
|
||||
Let $(A, (-)^{\#_a}) , (B, (-)^{\#_b}) \in \vert\elgotalgs{\C}\vert$ and $A \times B$ be the product of $A$ and $B$ in $\C$. Given $f : X \rightarrow (A \times B) + X$ we define the iteration as:
|
||||
\[f^\# = \langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle : X \rightarrow A \times B\]
|
||||
We show that $(A \times B, (-)^\#)$ is indeed an Elgot algebra:
|
||||
\todo[inline]{Show Elgot laws for product}
|
||||
Next we show that $(A \times B, (-)^\#)$ is indeed an Elgot algebra:
|
||||
\begin{itemize}
|
||||
\item \textbf{Fixpoint}:
|
||||
\item \textbf{Uniformity}:
|
||||
\item \textbf{Folding}:
|
||||
\item \textbf{Fixpoint}: Let $f : X \rightarrow (A \times B) + X$. \change{rewrite} The fixpoint law for $f^\#$ follows by the fixpoint law of $((\pi_1 + id) \circ f)^{\#_a}$ and $((\pi_2 + id) \circ f)^{\#_b}$:
|
||||
\begin{alignat*}{1}
|
||||
&\langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle
|
||||
\\=\;&\langle [ id , ((\pi_1 + id) \circ f)^{\#_a} ] \circ (\pi_1 + id) \circ f
|
||||
\\ &, [ id , ((\pi_2 + id) \circ f)^{\#_b} ] \circ (\pi_2 + id) \circ f \rangle \tag{\ref{law:fixpoint}}
|
||||
\\=\;&\langle [ \pi_1 , ((\pi_1 + id) \circ f)^{\#_a} ] \circ f , [ \pi_2 , ((\pi_2 + id) \circ f)^{\#_b} ] \circ f \rangle
|
||||
\\=\;&\langle [ \pi_1 , ((\pi_1 + id) \circ f)^{\#_a} ] , [ \pi_2 , ((\pi_2 + id) \circ f)^{\#_b} ] \rangle \circ f
|
||||
\\=\;&[ \langle \pi_1 , \pi_2 \rangle , \langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle ] \circ f
|
||||
\\=\;&[ id , \langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle ] \circ f
|
||||
\end{alignat*}
|
||||
\item \textbf{Uniformity}: Let $f : X \rightarrow (A \times B) + X, g : Y \rightarrow (A \times B) + Y, h : X \rightarrow Y$ and $(id + h) \circ f = g \circ h$.
|
||||
Note that this implies:
|
||||
\begin{alignat*}{2}
|
||||
&(id + h) \circ (\pi_1 + id) \circ f &&= (\pi_1 + id) \circ g \circ h
|
||||
\\&(id + h) \circ (\pi_2 + id) \circ f &&= (\pi_2 + id) \circ g \circ h
|
||||
\end{alignat*}
|
||||
|
||||
\ref{law:uniformity} of $(-)^{\#_a}$ and $(-)^{\#_b}$ with the previous two equations yields:
|
||||
\begin{alignat*}{2}
|
||||
&\langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_1 + id) \circ f)^{\#_a} \rangle &&= ((\pi_1 + id) \circ g)^{\#_a} \circ h
|
||||
\\&\langle ((\pi_2 + id) \circ f)^{\#_b} , ((\pi_2 + id) \circ f)^{\#_b} \rangle &&= ((\pi_2 + id) \circ g)^{\#_b} \circ h
|
||||
\end{alignat*}
|
||||
|
||||
This concludes the proof of:
|
||||
\[ \langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle = \langle ((\pi_1 + id) \circ g)^{\#_a} , ((\pi_2 + id) \circ g)^{\#_b} \rangle \circ h \]
|
||||
\item \textbf{Folding}: Let $f : X \rightarrow (A \times B) + X, h : Y \rightarrow X + Y$. We need to show:
|
||||
\begin{alignat*}{1}
|
||||
&\langle ((\pi_1 + id) \circ (\langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle + h)))^{\#_a}
|
||||
\\&,((\pi_2 + id) \circ (\langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle + h)))^{\#_b} \rangle
|
||||
\\=\;&\langle (\pi_1 + id) \circ [ (id + i_1) \circ f , i_2 \circ h ]^{\#_a} , (\pi_2 + id) \circ [ (id + i_1) \circ f , i_2 \circ h ]^{\#_b} \rangle
|
||||
\end{alignat*}
|
||||
|
||||
Indeed, the folding laws for $(-)^{\#_a}$ and $(-)^{\#_b}$ imply
|
||||
\begin{alignat*}{1}
|
||||
&((\pi_1 + id) \circ (\langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle + h)))^{\#_a}
|
||||
\\=\;&(((\pi_1 + id) \circ f)^{\#_a} + h)^{\#_a}
|
||||
\\=\;&[ (id + i_1) \circ (\pi_1 + id) \circ f , i_2 \circ h ]^{\#_a}\tag{\ref{law:folding}}
|
||||
\\=\;&(\pi_1 + id) \circ [ (id + i_1) \circ f , i_2 \circ h ]^{\#_a}
|
||||
\end{alignat*}
|
||||
and
|
||||
\begin{alignat*}{1}
|
||||
&((\pi_2 + id) \circ (\langle ((\pi_1 + id) \circ f)^{\#_a} , ((\pi_2 + id) \circ f)^{\#_b} \rangle + h)))^{\#_b}
|
||||
\\=\;&(((\pi_2 + id) \circ f)^{\#_b} + h)^{\#_b}
|
||||
\\=\;&[ (id + i_1) \circ (\pi_2 + id) \circ f , i_2 \circ h ]^{\#_b}\tag{\ref{law:folding}}
|
||||
\\=\;&(\pi_2 + id) \circ [ (id + i_1) \circ f , i_2 \circ h ]^{\#_b}
|
||||
\end{alignat*}
|
||||
which concludes the proof of the folding law.
|
||||
\end{itemize}
|
||||
|
||||
\todo[inline]{More explicit}
|
||||
The product diagram of $A \times B$ in $\C$ then also holds in $\elgotalgs{\C}$, we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism $\langle f , g \rangle$ is iteration preserving for any $f : (Z, (-)^{\#_z}) \rightarrow (X, (-)^{\#_x}), g : (Z, (-)^{\#_z}) \rightarrow (Y, (-)^{\#_y})$, which follows since $f$ and $g$ are iteration preserving.
|
||||
The product diagram of $A \times B$ in $\C$ then also holds in $\elgotalgs{\C}$, we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism $\langle f , g \rangle$ is iteration preserving for any $f : (Z, (-)^{\#_z}) \rightarrow (X, (-)^{\#_x}), g : (Z, (-)^{\#_z}) \rightarrow (Y, (-)^{\#_y})$:
|
||||
|
||||
Let $h : X \rightarrow E + X$ where $E \in \obj{\elgotalgs{\C}}$. We use the fact that $f, g$ are iteration preserving to show:
|
||||
\begin{alignat*}{1}
|
||||
&\langle f , g \rangle \circ (h^{\#_e})
|
||||
\\=\;&\langle f \circ (h^{\#_e}) , g \circ (h^{\#_e}) \rangle
|
||||
\\=\;&\langle ((f + id) \circ h)^{\#_a} , ((g + id) \circ h)^{\#_b} \rangle
|
||||
\\=\;&\langle ((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)^{\#_a} , ((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)^{\#_b} \rangle
|
||||
\end{alignat*}
|
||||
Which confirms that $\langle f , g \rangle$ is indeed iteration preserving. Thus, we have shown that $\elgotalgs{\C}$ is cartesian if $\C$ is cartesian.
|
||||
\end{proof}
|
||||
|
||||
\begin{lemma}\label{lem:elgotexp}
|
||||
Given $X \in \obj{\C}$ and $(A, (-)^{\#_a}) \in \vert\elgotalgs{\C}\vert$. The exponential $X^A$ (if it exists) can be equipped with an Elgot algebra structure.
|
||||
\end{lemma}
|
||||
\todo[inline]{Prove explicitly}
|
||||
\begin{proof}
|
||||
Take $f^\# = curry (((eval + id) \circ dstr \circ (f \times id))^{\#_a})$ for any $f : Z \rightarrow A^X + Z$.
|
||||
The \textbf{Fixpoint}, \textbf{Uniformity} and \textbf{Folding} laws for $(A^X, (-)^\#)$ follow by the laws of $(A, (-)^{\#_a})$ and some rewriting using properties of distributive categories.
|
||||
|
||||
\begin{itemize}
|
||||
\item \textbf{Fixpoint}: Let $f : Y \rightarrow X^A + Y$ with $Y \in \obj{C}$. By uniqueness of $f^\# = curry\;(((eval + id) \circ dstr \circ (f \times id))^{\#_a})$ it suffices to show:
|
||||
\begin{alignat*}{1}
|
||||
&eval \circ ([ id , curry (((eval + id) \circ dstr \circ (f \times id))^{\#_a}) ] \circ f] \times id)
|
||||
\\=\;&eval \circ [ id , curry (((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id ] \circ dstr \circ (f \times id)\tag*{\ref{hlp:elgot_exp_fixpoint}}
|
||||
\\=\;&[ eval , eval \circ curry (((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id ] \circ dstr \circ (f \times id)
|
||||
\\=\;&[ eval , ((eval + id) \circ dstr \circ (f \times id))^{\#_a} ] \circ dstr \circ (f \times id)
|
||||
\\=\;&[ id , ((eval + id) \circ dstr \circ (f \times id))^{\#_a} ] \circ (eval + id) \circ dstr \circ (f \times id)
|
||||
\\=\;&((eval + id) \circ dstr \circ (f \times id))^{\#_a}\tag{\ref{law:fixpoint}}
|
||||
\end{alignat*}
|
||||
Where
|
||||
\begin{alignat*}{1}
|
||||
&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) ] \times id
|
||||
\\= \;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id ] \circ dstr \tag*{(*)}\label{hlp:elgot_exp_fixpoint}
|
||||
\end{alignat*}
|
||||
follows by post-composing with $\pi_1$ and $\pi_2$:
|
||||
|
||||
\begin{alignat*}{1}
|
||||
&\pi_1 \circ [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id ] \circ dstr
|
||||
\\=\;&[ \pi_1 , \pi_1 \circ curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id ] \circ dstr
|
||||
\\=\;&[ \pi_1 , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \circ \pi_1 ] \circ dstr
|
||||
\\=\;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) ] \circ (\pi_1 + \pi_1) \circ dstr
|
||||
\\=\;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) ] \circ \pi_1
|
||||
\end{alignat*}
|
||||
|
||||
\begin{alignat*}{1}
|
||||
&\pi_2 \circ [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id ] \circ dstr
|
||||
\\=\;&[ \pi_2 , \pi_2 \circ curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id ] \circ dstr
|
||||
\\=\;&[ \pi_2 , \pi_2 ] \circ dstr
|
||||
\\=\;&\pi_2
|
||||
\end{alignat*}
|
||||
\item \textbf{Uniformity}: Let $Y, Z \in \obj{C}, f : Y \rightarrow X^A + Y, g : Z \rightarrow X^A + Z, h : Y \rightarrow Z$ and $(id + h) \circ f = g \circ h$. By uniqueness of $f^\# = curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a})$ it suffices to show:
|
||||
\begin{alignat*}{1}
|
||||
&((eval + id) \circ dstr \circ (f \times id))^{\#_a}
|
||||
\\=\;&((eval + id) \circ dstr \circ (g \times id))^{\#_a} \circ (h \times id)\tag{\ref{law:uniformity}}
|
||||
\\=\;&eval \circ (((eval + id) \circ dstr \circ (g \times id))^{\#_a} \times id) \circ (h \times id)
|
||||
\\=\;&eval \circ (((eval + id) \circ dstr \circ (g \times id))^{\#_a} \circ h \times id)
|
||||
\end{alignat*}
|
||||
Note that the application of \ref{law:uniformity} requires:
|
||||
\begin{alignat*}{1}
|
||||
&(id + (h \times id)) \circ (eval + id) \circ dstr \circ (f \times id)
|
||||
\\=\;&(eval + id) \circ (id + (h \times id)) \circ dstr \circ (f \times id)
|
||||
\\=\;&(eval + id) \circ dstr \circ (id \times h) \circ (id \times id) \circ (f \times id)
|
||||
\\=\;&(eval + id) \circ dstr \circ (g \times id) \circ (h \times id)
|
||||
\end{alignat*}
|
||||
\item \textbf{Folding}: Let $Y, Z \in \obj{C}, f : Y \rightarrow X^A + Y, h : Y \rightarrow Z$.
|
||||
\begin{alignat*}{1}
|
||||
&(f^\# + h)^\#
|
||||
\\=\;&curry(((eval + id) \circ dstr \circ ((curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) + h) \times id))^{\#_a})
|
||||
\\=\;&curry(((eval + id) \circ ((curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id) + (h \times id)) \circ dstr)^{\#_a})
|
||||
\\=\;&curry(((eval \circ (curry(((eval + id) \circ dstr \circ (f \times id))^{\#_a}) \times id) + (h \times id)) \circ dstr)^{\#_a})
|
||||
\\=\;&curry(((((eval + id) \circ dstr \circ (f \times id))^{\#_a} + (h \times id)) \circ dstr)^{\#_a})
|
||||
\\=\;&curry(((((eval + id) \circ dstr \circ (f \times id))^{\#_a} + dstr \circ (h \times id)))^{\#_a} \circ dstr)\tag{\ref{law:uniformity}}
|
||||
\\=\;&curry([ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr)\tag{\ref{law:folding}}
|
||||
\\=\;&curry(((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))^{\#_a})\tag{\ref{law:uniformity}}
|
||||
\\=\;&[ (id + i_1) \circ f , i_2 \circ h ]^\#
|
||||
\end{alignat*}
|
||||
Where the first application of \ref{law:uniformity} is justified by:
|
||||
\begin{alignat*}{1}
|
||||
&(id + dstr) \circ (((eval + id) \circ dstr \circ (f \times id))^{\#_a} + (h \times id)) \circ dstr
|
||||
\\=\;&(((eval + id) \circ dstr \circ (f \times id))^{\#_a} + (dstr \circ (h \times id))) \circ dstr
|
||||
\end{alignat*}
|
||||
which follows instantly, and the second application is justified by:
|
||||
\begin{alignat*}{1}
|
||||
&(id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ dstr^{-1}
|
||||
\\=\;&[ (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ (i_1 \times id)
|
||||
\\&, (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ (i_2 \times id) ]
|
||||
\\=\;&[ (id + dstr) \circ (eval + id) \circ dstr \circ (((id + i_1) \circ f) \times id)
|
||||
\\&, (id + dstr) \circ (eval + id) \circ dstr \circ ((i_2 \circ h) \times id) ]
|
||||
\\=\;&[ (id + dstr) \circ (eval + id) \circ dstr \circ ((id + i_1) \times id) \circ (f \times id)
|
||||
\\&, (id + dstr) \circ (eval + id) \circ dstr \circ (i_2 \times id) \circ (h \times id) ]
|
||||
\\=\;&[ (id + dstr) \circ (eval + id) \circ (id + (i_1 \times id)) \circ dstr \circ (f \times id)
|
||||
\\&, (id + dstr) \circ (eval + id) \circ i_2 \circ (h \times id) ]
|
||||
\\=\;&[ (eval + i_1) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ]
|
||||
\\=\;&[ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr \circ dstr^{-1}
|
||||
\end{alignat*}
|
||||
which uses epicness of $dstr^{-1}$.
|
||||
\end{itemize}
|
||||
\end{proof}
|
||||
|
||||
\section{Pre-Elgot Monads}
|
||||
|
||||
\improvement{Add some text, explain Elgot monads and while loops}
|
||||
|
||||
\begin{definition}[Pre-Elgot Monad]
|
||||
\begin{definition}[(Strong) 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 preserving, i.e.
|
||||
\[h^* \circ f^\# = ((h^* + id) \circ f)^\#\qquad \text{for}\; f : Z \rightarrow TX + Z, h : X \rightarrow TY\]
|
||||
\[h^* \circ f^\# = ((h^* + id) \circ f)^\#\qquad \text{for}\; Z \in \obj{\C}, f : Z \rightarrow TX + Z, h : X \rightarrow TY\]
|
||||
|
||||
If $\mathbf{T}$ is additionally strong and the strength $\tau$ is iteration preserving in the following sense:
|
||||
\[\tau \circ (id \times f^\#) = ((\tau + id) \circ dstl \circ (id \times f))^\# \qquad \text{for}\; Z \in \obj{\C}, f : Z \rightarrow TX + Z\]
|
||||
Then $\mathbf{T}$ is called strong pre-Elgot.
|
||||
\end{definition}
|
||||
|
||||
Let us briefly introduce the category of (strong) pre-Elgot monads because the initial object of this category will be of special interest to us.
|
||||
|
||||
\begin{remark}[Strong pre-Elgot Monad]
|
||||
A pre-Elgot monad $\mathbf{T}$ is strong if $\mathbf{T}$ is a strong monad and the strength $\tau$ is iteration preserving in the following sense:
|
||||
\[\tau \circ (id \times f^\#) = ((\tau + id) \circ dstl \circ (id \times f))^\#\]
|
||||
\change[inline]{be more concrete with types here}
|
||||
\end{remark}
|
||||
\begin{definition}[The Category of (Strong) Pre-Elgot Monads]
|
||||
Let $\C$ be a category. We define the category $\preelgot{\C}$ where objects are pre-Elgot monads and morphisms between pre-Elgot monads are morphisms between monads as in \autoref{def:monads} and additionally every $\alpha_X$ is a morphism between Elgot algebras as in \autoref{def:elgotalgebras}.
|
||||
|
||||
Pre-Elgot monads on $\C$ form a category that is a subcategory of $\monads{\C}$.
|
||||
|
||||
\begin{definition}[Category of pre-Elgot monads]
|
||||
Let $\C$ be a category. We define the category $\preelgot{\C}$ where objects are pre-Elgot monads and morphisms between two pre-Elgot monads $(S, \eta^S, \mu^S, (-)^{\#_S})$ and $(T, \eta^T, \mu^T, (-)^{\#_T})$ are natural transformations $\alpha : S \rightarrow T$ satisfying the following diagrams:
|
||||
% https://q.uiver.app/#q=WzAsMTEsWzAsMCwiWCJdLFsyLDAsIlNYIl0sWzIsMSwiVFgiXSxbMywwLCJTU1giXSxbNSwwLCJTVFgiXSxbMywxLCJTWCJdLFs1LDEsIlRUWCJdLFs0LDIsIlRYIl0sWzYsMCwiWCJdLFs4LDAsIlNBIl0sWzgsMSwiVEEiXSxbMCwxLCJcXGV0YV5TIl0sWzEsMiwiXFxhbHBoYSJdLFswLDIsIlxcZXRhXlQiLDJdLFszLDQsIlNcXGFscGhhIl0sWzMsNSwiXFxtdV5TIiwyXSxbNCw2LCJcXGFscGhhIl0sWzUsNywiXFxhbHBoYSIsMl0sWzYsNywiXFxtdV5UIl0sWzksMTAsIlxcYWxwaGEiXSxbOCw5LCJoXntcXCNfU30iXSxbOCwxMCwiKChcXGFscGhhICsgaWQpIFxcY2lyYyBmKV57XFwjX1R9IiwyXV0=
|
||||
\[\begin{tikzcd}
|
||||
X && SX & SSX && STX & X && SA \\
|
||||
&& TX & SX && TTX &&& TA \\
|
||||
&&&& TX
|
||||
\arrow["{\eta^S}", from=1-1, to=1-3]
|
||||
\arrow["\alpha", from=1-3, to=2-3]
|
||||
\arrow["{\eta^T}"', from=1-1, to=2-3]
|
||||
\arrow["S\alpha", from=1-4, to=1-6]
|
||||
\arrow["{\mu^S}"', from=1-4, to=2-4]
|
||||
\arrow["\alpha", from=1-6, to=2-6]
|
||||
\arrow["\alpha"', from=2-4, to=3-5]
|
||||
\arrow["{\mu^T}", from=2-6, to=3-5]
|
||||
\arrow["\alpha", from=1-9, to=2-9]
|
||||
\arrow["{h^{\#_S}}", from=1-7, to=1-9]
|
||||
\arrow["{((\alpha + id) \circ h)^{\#_T}}"', from=1-7, to=2-9]
|
||||
\end{tikzcd}\]
|
||||
Similarly, morphisms between strong pre-Elgot Monads are morphisms between strong monads as in \autoref{def:strongmonads} and every $\alpha_X$ is a morphism between Elgot algebras. This describes the category of strong pre-Elgot monads that we call $\strongpreelgot{\C}$.
|
||||
\end{definition}
|
||||
|
||||
\todo[inline]{Category of (strong) pre-Elgot monads, introduce category of monads in preliminaries}
|
||||
\todo[inline]{Initial pre-Elgot bridges gap to Elgot monads under countable choice\ldots}
|
||||
|
||||
\section{The Initial Strong 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.
|
||||
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 strong pre-Elgot monad.
|
||||
|
||||
\begin{proposition}
|
||||
Existence of all free Elgot algebras yields a monad that we call $\mathbf{K}$.
|
||||
|
|
|
|||
Loading…
Reference in a new issue