mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
561 lines
No EOL
36 KiB
TeX
561 lines
No EOL
36 KiB
TeX
\chapter{Partiality Monads}\label{chp:partiality}
|
|
Moggi's categorical semantics~\cite{moggi} describe a way to interpret an effectful programming language in a category. For this one needs a (strong) monad $T$ capturing the desired effects, then we can take the elements of $TA$ as denotations for programs of type $A$. The Kleisli category of $T$ can be viewed as the category of programs, which gives us a way of composing programs (Kleisli composition).
|
|
|
|
For this thesis we will restrict ourselves to monads for modelling partiality, the goal of this chapter is to capture what it means to be a partiality monad and look at two common examples.
|
|
|
|
\section{Properties of Partiality Monads}
|
|
We will now look at how to express the following non-controversial properties of a minimal partiality monad categorically:
|
|
|
|
|
|
\begin{itemize}
|
|
\item Irrelevance of execution order
|
|
\item Partiality of programs
|
|
\item No other effect besides some form of non-termination
|
|
\end{itemize}
|
|
|
|
The first property of course holds for any commutative monad, the other two are more interesting.
|
|
|
|
To ensure that programs are partial, we recall the following notion by Cockett and Lack~\cite{restriction}, that axiomatizes the notion of partiality in a category:
|
|
|
|
\newcommand{\tdom}{\text{dom}\;}
|
|
\begin{definition}[Restriction Structure]
|
|
A restriction structure on a category $\mathcal{C}$ is a mapping $dom : \mathcal{C}(X, Y) \rightarrow \mathcal{C}(X , X)$ with the following properties:
|
|
\begin{alignat*}{1}
|
|
f \circ (\tdom f) & = f\tag*{(R1)}\label{R1} \\
|
|
(\tdom f) \circ (\tdom g) & = (\tdom g) \circ (\tdom f)\tag*{(R2)}\label{R2} \\
|
|
\tdom(g \circ (\tdom f)) & = (\tdom g) \circ (\tdom f)\tag*{(R3)}\label{R3} \\
|
|
(\tdom h) \circ f & = f \circ \tdom (h \circ f)\tag*{(R4)}\label{R4}
|
|
\end{alignat*}
|
|
for any $X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z$.
|
|
\end{definition}
|
|
|
|
\begin{lemma}
|
|
For any $f : X \rightarrow Y$ the restriction morphism $\tdom f$ is idempotent.
|
|
\end{lemma}
|
|
\begin{proof}
|
|
This follows by \ref{R3} and \ref{R1}:
|
|
\[\tdom f \circ \tdom f = \tdom (f \circ \tdom f) = \tdom f\]
|
|
\end{proof}
|
|
|
|
The idempotent morphism $\tdom f : X \rightarrow X$ represents the domain of definiteness of $f : X \rightarrow Y$. In the category of partial functions this takes the following form:
|
|
|
|
\[
|
|
(\tdom f)(x) = \begin{cases}
|
|
x & \text{if } f(x) \text{ is defined} \\
|
|
\text{undefined} & \text{else}
|
|
\end{cases}
|
|
\]
|
|
|
|
That is, $\tdom f$ is only defined on values where $f$ is defined and for those values it behaves like the identity function.
|
|
|
|
\begin{definition}[Restriction Category]
|
|
Every category has a trivial restriction structure by taking $dom (f : X \rightarrow Y) = id_X$.
|
|
We call categories with a non-trivial restriction structure \textit{restriction categories}.
|
|
\end{definition}
|
|
|
|
For a suitable defined partiality monad $T$ the Kleisli category $\C^T$ should be a restriction category.
|
|
|
|
Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides some sort of non-termination:
|
|
|
|
\begin{definition}[Equational Lifting Monad]
|
|
\label{def:eqlm}
|
|
A commutative monad $T$ is called an \textit{equational lifting monad} if the following diagram commutes:
|
|
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJUWCJdLFsyLDAsIlRYIFxcdGltZXMgVFgiXSxbMiwyLCJUKFRYIFxcdGltZXMgWCkiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiXFx0YXUiXSxbMCwyLCJUIFxcbGFuZ2xlIFxcZXRhICwgaWQgXFxyYW5nbGUiLDJdXQ==
|
|
\[\begin{tikzcd}
|
|
TX && {TX \times TX} \\
|
|
\\
|
|
&& {T(TX \times X)}
|
|
\arrow["\Delta", from=1-1, to=1-3]
|
|
\arrow["\tau", from=1-3, to=3-3]
|
|
\arrow["{T \langle \eta , id \rangle}"', from=1-1, to=3-3]
|
|
\end{tikzcd}\]
|
|
where $\Delta : X \rightarrow X \times X$ is the diagonal morphism.
|
|
\end{definition}
|
|
|
|
To make the equational lifting property more comprehensible we can alternatively state it using do-notation. The equational lifting property states that the following programs must be equal:
|
|
|
|
\begin{multicols}{2}
|
|
\begin{minted}{haskell}
|
|
do x <- p
|
|
return (x , p)
|
|
\end{minted}
|
|
|
|
\begin{minted}{haskell}
|
|
do x <- p
|
|
return (x , return x)
|
|
\end{minted}
|
|
\end{multicols}
|
|
|
|
That is, if some computation $p : TX$ terminates with the result $x : X$, then $p = return\;x$ must hold. This of course implies that running $p$ multiple times yields the same result as running $p$ once.
|
|
|
|
\begin{theorem}[\cite{eqlm}]
|
|
If $T$ is an equational lifting monad the Kleisli category $\mathcal{C}^T$ is a restriction category.
|
|
\end{theorem}
|
|
|
|
Definition~\ref{def:eqlm} combines all three properties stated above, so when studying partiality monads in this thesis, we ideally expect them to be equational lifting monads. For the rest of this chapter we will use these definitions to compare two monads that are commonly used to model partiality.
|
|
|
|
\section{The Maybe Monad}
|
|
The endofunctor $MX = X + 1$ extends to a monad by taking $\eta_X = i_1 : X \rightarrow X + 1$ and $\mu_X = [ id , i_2 ] : (X + 1) + 1 \rightarrow X + 1$. The monad laws follow easily. This is generally known as the maybe monad and can be viewed as the canonical example of an equational lifting monad:
|
|
|
|
\begin{theorem} M is an equational lifting monad.
|
|
\end{theorem}
|
|
\begin{proof}
|
|
We define strength as:
|
|
\[ \tau_{X,Y} := X \times (Y + 1) \overset{dstl}{\longrightarrow} (X \times Y) + (X \times 1) \overset{id+!}{\longrightarrow} (X \times Y) + 1 \]
|
|
|
|
Naturality of $\tau$ follows by naturality of $dstl$:
|
|
|
|
\begin{alignat*}{1}
|
|
& (id + !) \circ dstl \circ (id \times (f + id)) \\
|
|
= \; & (id + !) \circ ((id \times f) + (id \times id)) \circ dstl \\
|
|
= \; & ((id \times f) + !) \circ dstl \\
|
|
= \; & ((id \times f) + id) \circ (id + !) \circ dstl
|
|
\end{alignat*}
|
|
|
|
The other strength laws and commutativity can be proven by using simple properties of distributive categories, we added these proofs to the formalization for completeness.
|
|
|
|
We are left to check the equational lifting law:
|
|
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYKzEiXSxbMywwLCIoWCsxKVxcdGltZXMoWCsxKSJdLFszLDIsIigoWCsxKVxcdGltZXMgWCkgKygoWCsxKVxcdGltZXMgMSkiXSxbMyw0LCIoKFgrMSlcXHRpbWVzIFgpKzEiXSxbMCwxLCJcXERlbHRhIl0sWzEsMiwiZHN0bCJdLFsyLDMsImlkK1xcOyEiXSxbMCwzLCJcXGxhbmdsZSBpXzEsaWRcXHJhbmdsZSArIFxcOyEiLDJdXQ==
|
|
\[\begin{tikzcd}
|
|
{X+1} &&& {(X+1)\times(X+1)} \\
|
|
\\
|
|
&&& {((X+1)\times X) +((X+1)\times 1)} \\
|
|
\\
|
|
&&& {((X+1)\times X)+1}
|
|
\arrow["\Delta", from=1-1, to=1-4]
|
|
\arrow["dstl", from=1-4, to=3-4]
|
|
\arrow["{id+\;!}", from=3-4, to=5-4]
|
|
\arrow["{\langle i_1,id\rangle + \;!}"', from=1-1, to=5-4]
|
|
\end{tikzcd}\]
|
|
|
|
This is easily proven by pre-composing with $i_1$ and $i_2$:
|
|
\begin{alignat*}{1}
|
|
&(id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle
|
|
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_1) \circ \langle i_1 , id \rangle
|
|
\\=\;&(id\;+\;!) \circ i_1 \circ \langle i_1 , id \rangle
|
|
\\=\;&i_1 \circ \langle i_1 , id \rangle
|
|
\end{alignat*}
|
|
|
|
\begin{alignat*}{1}
|
|
&(id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle
|
|
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_2) \circ \langle i_2 , id \rangle
|
|
\\=\;&(id\;+\;!) \circ i_2 \circ \langle i_2 , id \rangle
|
|
\\=\;&i_2 \;\circ\; ! \circ \langle i_2 , id \rangle
|
|
\\=\;&i_2 \;\circ\; !
|
|
\end{alignat*}
|
|
\end{proof}
|
|
|
|
In the setting of classical mathematics this monad is therefore sufficient for modelling partiality, but in general it will not be useful for modelling non-termination as a side effect, since one would need to know beforehand whether a program terminates or not. For the purpose of modelling possibly non-terminating computations another monad has been developed by Capretta~\cite{delay}.
|
|
|
|
\section{The Delay Monad}
|
|
\todo[inline]{Take introduction from setoids chapter and put it here!}
|
|
Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
|
|
This monad is usually defined by the two coinductive constructors $now$ and $later$, where $now$ is for lifting a value to a computation and $later$ intuitively delays a computation by one time unit:
|
|
|
|
\todo[inline]{Explain convention of double lines vs single lines ==> remove double lines here!!}
|
|
|
|
\[\mprset{fraction={===}}
|
|
\inferrule {x : X} {now\; x : DX}\hskip 2cm
|
|
\inferrule {c : DX} {later\; c : DX}\]
|
|
|
|
Categorically we obtain this monad by the final coalgebras $DX = \nu A. X + A$, which we assume to exist. In this section we will show that $\mathbf{D}$ is a strong and commutative monad.
|
|
|
|
Since $DX$ is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By Lambek's lemma the coalgebra structure $out : DX \rightarrow X + DX$ is an isomorphism, whose inverse can be decomposed into the two constructors mentioned before: $out^{-1} = [ now , later ] : X + DX \rightarrow DX$.
|
|
|
|
\begin{lemma}~\label{lem:delay}
|
|
The following conditions hold:
|
|
\begin{itemize}
|
|
\item $now : X \rightarrow DX$ and $later : DX \rightarrow DX$ satisfy:
|
|
\begin{equation*}
|
|
out \circ now = i_1 \qquad\qquad\qquad out \circ later = i_2 \tag*{(D1)}\label{D1}
|
|
\end{equation*}
|
|
\item For any $f : X \rightarrow DY$ there exists a unique morphism $f^* : DX \rightarrow DY$ satisfying:
|
|
\begin{equation*}
|
|
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJEWCJdLFszLDAsIlggKyBEWCJdLFswLDEsIkRZIl0sWzMsMSwiWSArIERZIl0sWzAsMSwib3V0Il0sWzAsMiwiZl4qIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywib3V0Il0sWzEsMywiWyBvdXQgXFxjaXJjIGYgLCBpXzIgXFxjaXJjIGZeKiBdIl1d
|
|
\begin{tikzcd}
|
|
DX &&& {X + DX} \\
|
|
DY &&& {Y + DY}
|
|
\arrow["out", from=1-1, to=1-4]
|
|
\arrow["{f^*}", dashed, from=1-1, to=2-1]
|
|
\arrow["out", from=2-1, to=2-4]
|
|
\arrow["{[ out \circ f , i_2 \circ f^* ]}", from=1-4, to=2-4]
|
|
\end{tikzcd}\tag*{(D2)}\label{D2}
|
|
\end{equation*}
|
|
\item There exists a unique morphism $\tau : X \times DY \rightarrow D(X \times Y)$ satisfying:
|
|
\begin{equation*}
|
|
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFsyLDAsIlggXFx0aW1lcyAoWSArIERZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgKyBEKFggXFx0aW1lcyBZKSJdLFswLDEsIlxcdGF1IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzMsNCwiaWQgK1xcdGF1IiwyXSxbMSw0LCJvdXQiXV0=
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{X \times DY} \&\& {X \times (Y + DY)} \&\& {X \times Y + X \times DY} \\
|
|
{D(X \times Y)} \&\&\&\& {X \times Y + D(X \times Y)}
|
|
\arrow["\tau", dashed, from=1-1, to=2-1]
|
|
\arrow["{id \times out}", from=1-1, to=1-3]
|
|
\arrow["dstl", from=1-3, to=1-5]
|
|
\arrow["{id +\tau}"', from=1-5, to=2-5]
|
|
\arrow["out", from=2-1, to=2-5]
|
|
\end{tikzcd}\tag*{(D3)}\label{D3}
|
|
\end{equation*}
|
|
\end{itemize}
|
|
\end{lemma}
|
|
\begin{proof}
|
|
We will make use of the fact that every $DX$ is a final coalgebra:
|
|
\begin{itemize}
|
|
\item[\ref{D1}] These follow by definition:
|
|
\begin{alignat*}{3}
|
|
&out \circ now &&= out \circ out^{-1} \circ i_1 &= i_1
|
|
\\&out \circ later &&= out \circ out^{-1} \circ i_2 &= i_2
|
|
\end{alignat*}
|
|
\item[\ref{D2}] We define $f^* = \;\coalg{\alpha} \circ i_1$, where $\coalg{\alpha}$ is the unique coalgebra morphism in this diagram:
|
|
|
|
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWCArIERZIl0sWzcsMSwiWSArIChEWCArIERZKSJdLFswLDAsIkRYIl0sWzAsMiwiRFkiXSxbNywyLCJZICsgRFkiXSxbMCwxLCJcXGFscGhhIDo9IFsgWyBbIGlfMSAsIGlfMiBcXGNpcmMgaV8yIF0gXFxjaXJjIChvdXQgXFxjaXJjIGYpICwgaV8yIFxcY2lyYyBpXzEgXSBcXGNpcmMgb3V0ICwgKGlkICsgaV8yKSBcXGNpcmMgb3V0IF0iXSxbMiwwLCJpXzEiXSxbMCwzLCJcXGNvYWxne1xcYWxwaGF9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzMsNCwib3V0Il0sWzEsNCwiaWQgKyBcXGNvYWxne1xcYWxwaGF9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
|
|
\[\begin{tikzcd}[ampersand replacement=\&]
|
|
DX \\
|
|
{DX + DY} \&\&\&\&\&\&\& {Y + (DX + DY)} \\
|
|
DY \&\&\&\&\&\&\& {Y + DY}
|
|
\arrow["{\alpha := [ [ [ i_1 , i_2 \circ i_2 ] \circ (out \circ f) , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ]}", from=2-1, to=2-8]
|
|
\arrow["{i_1}", from=1-1, to=2-1]
|
|
\arrow["{\coalg{\alpha}}", dashed, from=2-1, to=3-1]
|
|
\arrow["out", from=3-1, to=3-8]
|
|
\arrow["{id + \coalg{\alpha}}", dashed, from=2-8, to=3-8]
|
|
\end{tikzcd}\]
|
|
|
|
Note that $\coalg{\alpha} \circ i_2 = id : (DY, out) \rightarrow (DY, out)$, by uniqueness of the identity morphism and the fact that $\coalg{\alpha} \circ i_2$ is a coalgebra morphism:
|
|
\begin{alignat*}{1}
|
|
&out \circ \coalg{\alpha} \circ i_2
|
|
\\=\;&(id+\coalg{\alpha}) \circ \alpha \circ i_2
|
|
\\=\;&(id + \coalg{\alpha}) \circ (id + i_2) \circ out
|
|
\\=\;&(id + \coalg{\alpha} \circ i_2) \circ out
|
|
\end{alignat*}
|
|
Let us verify that $f^*$ indeed satisfies the requisite property:
|
|
|
|
\begin{alignat*}{1}
|
|
&out \circ \coalg{\alpha} \circ i_1
|
|
\\=\;&(id + \coalg{\alpha}) \circ \alpha \circ i_1
|
|
\\=\;&(id + \coalg{\alpha}) \circ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out
|
|
\\=\;&[ [ (id + \coalg{\alpha}) \circ i_1 , (id + \coalg{\alpha}) \circ i_2 \circ i_2 ] \circ out \circ f , (id + \coalg{\alpha}) \circ i_2 \circ i_1 ] \circ out
|
|
\\=\;&[ [ i_1 , i_2 \circ \coalg{\alpha} \circ i_2 ] \circ out \circ f , i_2 \circ \coalg{\alpha} \circ i_1 ] \circ out
|
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out
|
|
\end{alignat*}
|
|
|
|
We are left to check uniqueness of $f^*$. Let $g : DX \rightarrow DY$ and $out \circ g = [ out \circ f , i_2 \circ g ] \circ out$.
|
|
Note that $[ g , id ] : DX + DY \rightarrow DY$ is a coalgebra morphism:
|
|
\begin{alignat*}{1}
|
|
&out \circ [ g , id ]
|
|
\\=\;&[ out \circ g , out ]
|
|
\\=\;&[ [ out \circ f , i_2 \circ g ] \circ out , out]
|
|
\\=\;&[ [ [ i_1 , i_2 ] \circ out \circ f , i_2 \circ g ] \circ out , (id + id) \circ out ]
|
|
\\=\;&[ [ [ i_1 , i_2 \circ [g , id] \circ i_2 ] \circ out \circ f , i_2 \circ [g , id] \circ i_1 ] \circ out , (id + [g , id] \circ i_2) \circ out ]
|
|
\\=\;&[ [ [ (id + [g , id]) \circ i_1 , (id + [g , id]) \circ i_2 \circ i_2 ] \circ out \circ f , (id + [g , id]) \circ i_2 \circ i_1 ] \circ out
|
|
\\\;&, (id + [g , id]) \circ (id + i_2) \circ out ]
|
|
\\=\;&(id + [g , id]) \circ [ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ]
|
|
\end{alignat*}
|
|
|
|
Thus, $[ g , id ] = \coalg{\alpha}$ by uniqueness of $\coalg{\alpha}$.
|
|
It follows: \[g = [ g , id ] \circ i_1 =\;\coalg{\alpha} \circ i_1 = f^*\]
|
|
\item[\ref{D3}] This follows immediately since $\tau$ is the unique coalgebra morphism from $(X \times DY, dstl \circ (id \times out))$ into the terminal coalgebra $(D(X \times Y) , out)$.
|
|
\end{itemize}
|
|
\end{proof}
|
|
|
|
\begin{lemma}
|
|
The following properties follow from \autoref{lem:delay}:
|
|
\begin{enumerate}
|
|
\item $out \circ Df = (f + Df) \circ out$
|
|
\item $f^* = [ f , {(later \circ f)}^* ] \circ out$
|
|
\item $later \circ f^* = {(later \circ f)}^* = f^* \circ later$
|
|
\end{enumerate}
|
|
\end{lemma}
|
|
\begin{proof}
|
|
\begin{itemize}
|
|
\item[1.] Note that definitionally: $Df = {(now \circ f)}^*$ for any $f : X \rightarrow TY$. The statement is then simply a consequence of~\ref{D1} and~\ref{D2}:
|
|
\begin{alignat*}{1}
|
|
&out \circ Df
|
|
\\=\;&out \circ {(now \circ f)}^*
|
|
\\=\;&[ out \circ now \circ f , i_2 \circ {(now \circ f)}^* ] \circ out\tag*{\ref{D2}}
|
|
\\=\;&(f + Df) \circ out\tag*{\ref{D1}}
|
|
\end{alignat*}
|
|
\item[2.] By uniqueness of $f^*$ it suffices to show:
|
|
\begin{alignat*}{1}
|
|
&out \circ [ f , {(later \circ f)}^* ] \circ out
|
|
\\=\;&[ out \circ f , out \circ {(later \circ f)}^* ] \circ out
|
|
\\=\;&[out \circ f , [ out \circ later \circ f , i_2 \circ {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D2}}
|
|
\\=\;&[out \circ f , i_2 \circ [ f , {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D1}}
|
|
\end{alignat*}
|
|
\item[3.]
|
|
These equations follow by monicity of $out$:
|
|
\begin{alignat*}{1}
|
|
&out \circ {(later \circ f)}^*
|
|
\\=\;&[ out \circ later \circ f , i_2 \circ {(later \circ f)}^*] \circ out\tag*{\ref{D2}}
|
|
\\=\;&i_2 \circ [ f , {(later \circ f)}^*] \circ out\tag*{\ref{D1}}
|
|
\\=\;&i_2 \circ f^*
|
|
\\=\;&out \circ later \circ f^*\tag*{\ref{D1}}
|
|
\\=\;&i_2 \circ f^*\tag*{\ref{D1}}
|
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_2
|
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ later\tag*{\ref{D1}}
|
|
\\=\;&out \circ f^* \circ later \tag*{\ref{D2}}
|
|
\end{alignat*}
|
|
\end{itemize}
|
|
\end{proof}
|
|
|
|
\begin{theorem}
|
|
$\mathbf{D} = (D, now, (-)^*)$ is a Kleisli triple.
|
|
\end{theorem}
|
|
\begin{proof}
|
|
We will now use the properties proven in Corollary~\ref{lem:delay} to prove the Kleisli triple laws:
|
|
\begin{itemize}
|
|
\item[\ref{K1}]
|
|
By uniqueness of $now^*$ it suffices to show that $out \circ id = [ out \circ now , i_2 \circ id ] \circ out$ which instantly follows by \ref{D1}.
|
|
\item[\ref{K2}] Let $f : X \rightarrow DY$. We proceed by monicity of $out$:
|
|
\begin{alignat*}{1}
|
|
&out \circ f^* \circ now
|
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ now\tag*{\ref{D2}}
|
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_1\tag*{\ref{D1}}
|
|
\\=\;&out \circ f
|
|
\end{alignat*}
|
|
\item[\ref{K3}] Let $f : Y \rightarrow Z, g : X \rightarrow Z$ to show $f^* \circ g^* = (f^* \circ g)^*$ by uniqueness of $(f^* \circ g)^*$ it suffices to show:
|
|
\begin{alignat*}{1}
|
|
&out \circ f^* \circ g^*
|
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ g^*\tag*{\ref{D2}}
|
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ [ out \circ g , i_2 \circ g^* ] \circ out\tag*{\ref{D2}}
|
|
\\=\;&[ [ out \circ f , i_2 \circ f^* ] \circ out \circ g , i_2 \circ f^* \circ g^* ] \circ out
|
|
\\=\;&[ out \circ f^* \circ g , i_2 \circ f^* \circ g^* ] \circ out\tag*{\ref{D2}}
|
|
\end{alignat*}
|
|
\end{itemize}
|
|
\end{proof}
|
|
|
|
Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$ yields the following proof principle:
|
|
\begin{remark}[Proof by coinduction]~\label{rem:coinduction}
|
|
Given two morphisms $f, g : X \rightarrow DY$. To show that $f = g$ it suffices to show that there exists a coalgebra structure $\alpha : X \rightarrow Y + X$ such that the following diagrams commute:
|
|
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJYIl0sWzAsMSwiRFkiXSxbMiwxLCJZICsgRFkiXSxbMiwwLCJZICsgWCJdLFs0LDAsIlgiXSxbNCwxLCJEWSJdLFs2LDAsIlkgKyBYIl0sWzYsMSwiWSArIERZIl0sWzEsMiwib3V0Il0sWzAsMywiXFxhbHBoYSJdLFswLDEsImYiXSxbMywyLCJpZCArIGYiXSxbNCw2LCJcXGFscGhhIl0sWzQsNSwiZyJdLFs2LDcsImlkICsgZyJdLFs1LDcsIm91dCJdXQ==
|
|
\[\begin{tikzcd}[ampersand replacement=\&]
|
|
X \&\& {Y + X} \&\& X \&\& {Y + X} \\
|
|
DY \&\& {Y + DY} \&\& DY \&\& {Y + DY}
|
|
\arrow["out", from=2-1, to=2-3]
|
|
\arrow["\alpha", from=1-1, to=1-3]
|
|
\arrow["f", from=1-1, to=2-1]
|
|
\arrow["{id + f}", from=1-3, to=2-3]
|
|
\arrow["\alpha", from=1-5, to=1-7]
|
|
\arrow["g", from=1-5, to=2-5]
|
|
\arrow["{id + g}", from=1-7, to=2-7]
|
|
\arrow["out", from=2-5, to=2-7]
|
|
\end{tikzcd}\]
|
|
Uniqueness of the coalgebra morphism $\coalg{\alpha} : (X, \alpha) \rightarrow (DY, out)$ then results in $f = g$.
|
|
\end{remark}
|
|
|
|
\begin{theorem}
|
|
$\mathbf{D}$ is a strong monad.
|
|
\end{theorem}
|
|
\begin{proof}
|
|
Most of the following proofs are done via coinduction (Remark~\ref{rem:coinduction}). We will only give the requisite coalgebra structure. The proofs that the diagrams commute can be looked up in the Agda formalization.
|
|
|
|
First we need to show naturality of $\tau$, i.e. we need to show that
|
|
\[\tau \circ (f \times (now \circ g)^*) = (now \circ (f \times g))^* \circ \tau\]
|
|
The coalgebra for coinduction is:
|
|
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwyLCJEKEFcXHRpbWVzIEIpIl0sWzQsMiwiQVxcdGltZXMgQiArIEQoQSBcXHRpbWVzIEIpIl0sWzEsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzIsMCwiWCBcXHRpbWVzIFkgKyBYIFxcdGltZXMgRFkiXSxbNCwwLCJBIFxcdGltZXMgQiArIFggXFx0aW1lcyBEWSJdLFsxLDIsIm91dCJdLFswLDMsImlkIFxcdGltZXMgb3V0Il0sWzMsNCwiZHN0bCJdLFswLDEsIlxcY29hbGd7LX0iLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNCw1LCJmIFxcdGltZXMgZyArIGlkIl0sWzUsMiwiaWQgKyBcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
|
|
\[\begin{tikzcd}[ampersand replacement=\&]
|
|
{X \times DY} \& {X \times (Y + DY)} \& {X \times Y + X \times DY} \&\& {A \times B + X \times DY} \\
|
|
\\
|
|
{D(A\times B)} \&\&\&\& {A\times B + D(A \times B)}
|
|
\arrow["out", from=3-1, to=3-5]
|
|
\arrow["{id \times out}", from=1-1, to=1-2]
|
|
\arrow["dstl", from=1-2, to=1-3]
|
|
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1]
|
|
\arrow["{f \times g + id}", from=1-3, to=1-5]
|
|
\arrow["{id + \coalg{\text{-}}}", dashed, from=1-5, to=3-5]
|
|
\end{tikzcd}\]
|
|
We write $\coalg{\text{-}}$ to abbreviate the used coalgebra, i.e.\ in the previous diagram
|
|
\[\coalg{\text{-}} = \coalg{(f\times g + id) \circ dstl \circ (id \times out)}.\]
|
|
|
|
Next we check the strength laws:
|
|
\begin{itemize}
|
|
\item[\ref{S1}] To show that $(now \circ \pi_2)^* \circ \tau = \pi_2$ we do coinduction using the following coalgebra:
|
|
% https://q.uiver.app/#q=WzAsNixbMCwwLCIxIFxcdGltZXMgRFgiXSxbMCwxLCJEWCJdLFszLDAsIlggKyAxIFxcdGltZXMgRFgiXSxbMywxLCJYICsgRFgiXSxbMSwwLCIxIFxcdGltZXMgWCArIERYIl0sWzIsMCwiMSBcXHRpbWVzIFggKyAxIFxcdGltZXMgRFgiXSxbMSwzLCJvdXQiXSxbMCwxLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywiaWQgKyBcXGNvYWxney19Il0sWzAsNCwiaWQgXFx0aW1lcyBvdXQiXSxbNCw1LCJkc3RsIl0sWzUsMiwiXFxwaV8yICsgaWQiXV0=
|
|
\[\begin{tikzcd}[ampersand replacement=\&]
|
|
{1 \times DX} \& {1 \times X + DX} \& {1 \times X + 1 \times DX} \& {X + 1 \times DX} \\
|
|
DX \&\&\& {X + DX}
|
|
\arrow["out", from=2-1, to=2-4]
|
|
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=2-1]
|
|
\arrow["{id + \coalg{\text{-}}}", from=1-4, to=2-4]
|
|
\arrow["{id \times out}", from=1-1, to=1-2]
|
|
\arrow["dstl", from=1-2, to=1-3]
|
|
\arrow["{\pi_2 + id}", from=1-3, to=1-4]
|
|
\end{tikzcd}\]
|
|
\item[\ref{S2}] We don't need coinduction to show $\tau \circ (id \times now) = now$, but we need a small helper lemma:
|
|
\begin{equation*}
|
|
\tau \circ (id \times out^{-1}) = out^{-1} \circ (id + \tau) \circ dstl \tag*{($\ast$)}\label{helper}
|
|
\end{equation*}
|
|
which is a direct consequence of \ref{D3}.
|
|
With this the proof is straightforward:
|
|
\begin{alignat*}{1}
|
|
& \tau \circ (id \times now) \\
|
|
=\; & \tau \circ (id \times out^{-1}) \circ (id \times i_1) \\
|
|
=\; & out^{-1} \circ (id + \tau) \circ dstl \circ (id \times i_1)\tag*{\ref*{helper}} \\
|
|
=\; & now
|
|
\end{alignat*}
|
|
where the last step follows by $dstl \circ (id \times i_1) = i_1$.
|
|
\item[\ref{S3}] We need to check $\tau^* \circ \tau = \tau \circ (id \times id^*)$, the coalgebra for coinduction is:
|
|
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRERZIl0sWzAsMiwiRChYXFx0aW1lcyBZKSJdLFsxLDAsIlggXFx0aW1lcyAoRFkgKyBERFkpIl0sWzIsMCwiWCBcXHRpbWVzIERZICsgWCBcXHRpbWVzIEREWSJdLFsyLDIsIlggXFx0aW1lcyBZICsgRChYIFxcdGltZXMgWSkiXSxbMiwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBERFkiXSxbMCwxLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzEsNCwib3V0Il0sWzUsNCwiaWQgKyBcXGNvYWxney19IiwyXSxbMyw1LCJbIChpZCArIChpZCBcXHRpbWVzIG5vdykpIFxcY2lyYyBkc3RsIFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpICwgaV8yIF0iLDJdXQ==
|
|
\[\begin{tikzcd}[ampersand replacement=\&]
|
|
{X \times DDY} \& {X \times (DY + DDY)} \& {X \times DY + X \times DDY} \\
|
|
\&\& {X \times Y + X \times DDY} \\
|
|
{D(X\times Y)} \&\& {X \times Y + D(X \times Y)}
|
|
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1]
|
|
\arrow["{id \times out}", from=1-1, to=1-2]
|
|
\arrow["dstl", from=1-2, to=1-3]
|
|
\arrow["out", from=3-1, to=3-3]
|
|
\arrow["{id + \coalg{\text{-}}}"', from=2-3, to=3-3]
|
|
\arrow["{[ (id + (id \times now)) \circ dstl \circ (id \times out) , i_2 ]}"', from=1-3, to=2-3]
|
|
\end{tikzcd}\]
|
|
\item[\ref{S4}] To show $D\alpha \circ \tau = \tau \circ (id \times \tau) \circ \alpha$ by coinduction we take the coalgebra:
|
|
% https://q.uiver.app/#q=WzAsNixbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgRFoiXSxbMCwyLCJEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIFogKyBEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwxLCJYIFxcdGltZXMgWSAgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzEsMCwiKFggXFx0aW1lcyBZKSBcXHRpbWVzIChaKyBEWikiXSxbMiwwLCIoWFxcdGltZXMgWSkgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzAsMSwiXFxjb2FsZ3stfSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsIm91dCJdLFszLDIsImlkICtcXGNvYWxney19IiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDUsImRzdGwiXSxbNSwzLCJcXGxhbmdsZSBcXHBpXzEgXFxjaXJjIFxccGlfMSAsIFxcbGFuZ2xlIFxccGlfMiBcXGNpcmMgXFxwaV8xICwgXFxwaV8yIFxccmFuZ2xlIFxccmFuZ2xlICsgaWQiLDJdXQ==
|
|
\[\begin{tikzcd}[ampersand replacement=\&]
|
|
{(X \times Y) \times DZ} \& {(X \times Y) \times (Z+ DZ)} \& {(X\times Y) \times Z + (X \times Y) \times DZ} \\
|
|
\&\& {X \times Y \times Z + (X \times Y) \times DZ} \\
|
|
{D(X \times Y \times Z)} \&\& {X \times Y \times Z + D(X \times Y \times Z)}
|
|
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1]
|
|
\arrow["out", from=3-1, to=3-3]
|
|
\arrow["{id +\coalg{\text{-}}}"', from=2-3, to=3-3]
|
|
\arrow["{id \times out}", from=1-1, to=1-2]
|
|
\arrow["dstl", from=1-2, to=1-3]
|
|
\arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-3, to=2-3]
|
|
\end{tikzcd}\]
|
|
\end{itemize}
|
|
\end{proof}
|
|
|
|
To prove that $\mathbf{D}$ is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} or \textit{Parametric Corecursion}~\cite{param-corec}. In our setting this takes the following form:
|
|
|
|
\begin{definition}
|
|
We call a morphism $g : X \rightarrow D (Y + X)$ \textit{guarded} if there exists an $h : X \rightarrow Y + D(Y+X)$ such that the following diagram commutes:
|
|
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzMsMCwiRCAoWSArWCkiXSxbMywxLCIoWSArIFgpICsgRChZICsgWCkiXSxbMCwxLCJZICsgRChZK1gpIl0sWzAsMSwiZyJdLFsxLDIsIm91dCJdLFszLDIsImlfMSArIGlkIiwyXSxbMCwzLCJoIiwyXV0=
|
|
\[\begin{tikzcd}[ampersand replacement=\&]
|
|
X \&\&\& {D (Y +X)} \\
|
|
{Y + D(Y+X)} \&\&\& {(Y + X) + D(Y + X)}
|
|
\arrow["g", from=1-1, to=1-4]
|
|
\arrow["out", from=1-4, to=2-4]
|
|
\arrow["{i_1 + id}"', from=2-1, to=2-4]
|
|
\arrow["h"', from=1-1, to=2-1]
|
|
\end{tikzcd}\]
|
|
\end{definition}
|
|
|
|
\begin{corollary}[Solution Theorem]
|
|
\label{cor:solution}
|
|
Let $g : X \rightarrow D(Y + X)$ be guarded. \textit{Solutions} of g are unique, i.e. given two morphisms $f, i : X \rightarrow DY$ then
|
|
$f = [ now , f ]^* \circ g$ and $i = [ now , i ]^* \circ g$ already implies $f = i$.
|
|
\end{corollary}
|
|
\begin{proof}
|
|
Let $g : X \rightarrow D(Y + X)$ be guarded by $h : X \rightarrow Y + D(Y+X)$ and $f, i : X \rightarrow DY$ be solutions of g.
|
|
It suffices to show $[ now , f ]^* = [ now , i ]^*$, because then follows:
|
|
\[f = [ now , f ]^* \circ g = [ now , i ]^* \circ g = i\]
|
|
We prove this by coinduction using:
|
|
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcY29hbGd7LX0iXSxbMiwwLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
|
|
\[\begin{tikzcd}[ampersand replacement=\&]
|
|
{D(Y + X)} \& {(Y + X) + D(Y+X)} \&\& {Y + D(Y+X)} \\
|
|
DY \&\&\& {Y + DY}
|
|
\arrow["out", from=2-1, to=2-4]
|
|
\arrow["out", from=1-1, to=1-2]
|
|
\arrow["{[ [ i_1 , h ] , i_2 ]}", from=1-2, to=1-4]
|
|
\arrow["{id + \coalg{\text{-}}}", from=1-4, to=2-4]
|
|
\arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=2-1]
|
|
\end{tikzcd}\]
|
|
\end{proof}
|
|
|
|
Let us record some facts that we will use to prove commutativity of $\mathbf{D}$:
|
|
|
|
\begin{corollary}
|
|
These properties of $\tau$ and $\sigma$ hold:
|
|
\begin{alignat*}{2}
|
|
& out \circ \tau & & = (id + \tau) \circ dstl \circ (id \times out)\tag*{($\tau_1$)}\label{tau1}
|
|
\\&out \circ \sigma &&= (id + \sigma) \circ dstr \circ (out \times id)\tag*{($\sigma_1$)}\label{sigma1}
|
|
\\&\tau \circ (id \times out^{-1}) &&= out^{-1} \circ (id + \tau) \circ dstl\tag*{($\tau_2$)}\label{tau2}
|
|
\\& \sigma \circ (out^{-1} \times id) &&= out^{-1} \circ (id + \sigma) \circ dstr\tag*{($\sigma_2$)}\label{sigma2}
|
|
\end{alignat*}
|
|
\end{corollary}
|
|
|
|
\begin{proof}
|
|
\begin{itemize}
|
|
\item[\ref{tau1}] This is just~\ref{D3} restated.
|
|
\item[\ref{sigma1}]
|
|
\begin{alignat*}{1}
|
|
&out \circ \sigma
|
|
\\=\;&out \circ Dswap \circ \tau \circ swap
|
|
\\=\;&(swap + Dswap) \circ out \circ \tau \circ swap
|
|
\\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ (id \times out) \circ swap \tag*{\ref{tau1}}
|
|
\\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ swap \circ (out \times id)
|
|
\\=\;&(swap + Dswap) \circ (id + \tau) \circ (swap + swap) \circ dstr \circ (out \times id)
|
|
\\=\;&(id + \sigma) \circ dstr \circ (out \times id)
|
|
\end{alignat*}
|
|
\item[\ref{tau2}] By monicity of $out$:
|
|
\begin{alignat*}{1}
|
|
&out \circ \tau \circ (id \times out^{-1})
|
|
\\=\;&(id + \tau) \circ dstl \circ (id \times out) \circ (id \times out^{-1})\tag*{\ref{tau1}}
|
|
\\=\;&(id + \tau) \circ dstl
|
|
\end{alignat*}
|
|
\item[\ref{sigma2}] By monicity of $out$:
|
|
\begin{alignat*}{1}
|
|
&out \circ \sigma \circ (out^{-1} \times id)
|
|
\\=\;&(id + \sigma) \circ dstr \circ (out \times id) \circ (out^{-1} \times id)\tag*{\ref{sigma1}}
|
|
\\=\;&(id + \sigma) \circ dstr
|
|
\end{alignat*}
|
|
\end{itemize}
|
|
\end{proof}
|
|
|
|
\begin{theorem}
|
|
$\mathbf{D}$ is commutative.
|
|
\end{theorem}
|
|
\begin{proof}
|
|
Using \autoref{cor:solution} it suffices to show that both $\tau^* \circ \sigma$ and $\sigma^* \circ \tau$ are solutions of some guarded morphism $g$.
|
|
|
|
Let $w = (dstr + dstr) \circ dstl \circ (out \times out)$ and take
|
|
\[g = out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\]
|
|
$g$ is trivially guarded by $[ id + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w$.
|
|
|
|
We are left to show that both $\tau^* \circ \sigma$ and $\sigma^* \circ \tau$ are solutions of $g$. Consider:
|
|
|
|
\[\tau^* \circ \sigma = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \tau^* \circ \sigma ] ] \circ w = [ now , \tau^* \circ \sigma]^* \circ g \]
|
|
\[\sigma^* \circ \tau = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \sigma^* \circ \tau ] ] \circ w = [ now , \sigma^* \circ \tau]^* \circ g \]
|
|
|
|
The last step in both equations can be proven generally for any $f : DX \times DY \rightarrow D(X \times Y)$ using monicity of $out$:
|
|
\begin{alignat*}{1}
|
|
& out \circ {[ now , f ]}^* \circ out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w
|
|
\\=\; & [ out \circ [ now , f ] , i_2 \circ {[ now , f ]}^* ] \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D2}}
|
|
\\=\; & [ id + \sigma , i_2 \circ {[ now , f]}^* \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D1}}
|
|
\\=\; & [ id + \sigma , i_2 \circ [ \tau , {[ now , f]}^* \circ later \circ now \circ i_2 ] ] \circ w
|
|
\\=\; & [ id + \sigma , i_2 \circ [ \tau , {[ later \circ now , later \circ f]}^* \circ now \circ i_2 ] ] \circ w
|
|
\\=\; & [ id + \sigma , i_2 \circ [ \tau , later \circ f ] ] \circ w
|
|
\end{alignat*}
|
|
|
|
Let us now check the first step in the equation for $\sigma^* \circ \tau$, the same step for $\tau^* \circ \sigma$ is then symmetric.
|
|
|
|
Again we proceed by monicity of $out$:
|
|
\begin{alignat*}{1}
|
|
& out \circ \sigma^* \circ \tau
|
|
\\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ out \circ \tau\tag*{\ref{D2}}
|
|
\\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ (id + \tau) \circ dstl \circ (id \times out)\tag*{\ref{D3}}
|
|
\\=\;&[ (id + \sigma) \circ dstr \circ (out \times id) , i_2 \circ \sigma^* \circ \tau ] \circ dstl \circ (id \times out)\tag*{\ref{sigma1}}
|
|
\\=\;&[ (id + \sigma) \circ dstr \circ (out \times id) , i_2 \circ \sigma^* \circ \tau ] \circ ((out^{-1} \times id) + (out^{-1} \times id)) \circ dstl \circ (out \times out)
|
|
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ \sigma^* \circ \tau \circ (out^{-1} \times id)] \circ dstl \circ (out \times out)
|
|
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ \sigma^* \circ D(out^{-1} \times id) \circ \tau] \circ dstl \circ (out \times out)
|
|
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (\sigma \times (out^{-1} \times id))^* \circ \tau] \circ dstl \circ (out \times out)
|
|
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (out^{-1} \circ (id + \sigma) \circ dstr)^* \circ \tau] \circ dstl \circ (out \times out)\tag*{\ref{sigma2}}
|
|
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (out^{-1} \circ (id + \sigma))^* \circ Ddstr \circ \tau] \circ dstl \circ (out \times out)
|
|
\\=\;&[ (id + \sigma) \circ dstr, i_2 \circ (out^{-1} \circ (id + \sigma))^* \circ [D i_1 \circ \tau , D i_2 \circ \tau] \circ dstr] \circ dstl \circ (out \times out)\tag*{\ref{Dcomm-helper}}
|
|
\\=\;&[ (id + \sigma), i_2 \circ (out^{-1} \circ (id + \sigma))^* \circ [D i_1 \circ \tau , D i_2 \circ \tau]] \circ (dstr + dstr) \circ dstl \circ (out \times out)
|
|
\\=\;&[ (id + \sigma), i_2 \circ [(out^{-1} \circ i_1)^* \circ \tau , (out^{-1} \circ i_2 \circ \sigma)^* \circ \tau]] \circ w
|
|
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , (later \circ \sigma)^* \circ \tau]] \circ w \tag*{\ref{K1}}
|
|
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , later \circ \sigma^* \circ \tau]] \circ w
|
|
\end{alignat*}
|
|
|
|
where
|
|
\[Ddstr \circ \tau = [ Di_1 \circ \tau , Di_2 \circ \tau ] \circ dstr \tag*{(*)}\label{Dcomm-helper}\]
|
|
is proven using epicness of $dstr^{-1}$:
|
|
|
|
\begin{alignat*}{1}
|
|
& Ddstr \circ \tau \circ dstr^{-1}
|
|
\\=\;&[ Ddstr \circ \tau \circ (i_1 \times id) , Ddstr \circ \tau \circ (i_2 \times id) ]
|
|
\\=\;&[ Ddstr \circ D(i_1 \times id) \circ \tau , Ddstr \circ D(i_2 \times id) \circ \tau ]
|
|
\\=\;&[ Di_1 \circ \tau , Di_2 \circ \tau ]
|
|
\end{alignat*}
|
|
\end{proof}
|
|
|
|
\improvement[inline]{Elaborate more?}
|
|
We have now seen that $\mathbf{D}$ is strong and commutative, however it is not an equational lifting monad, since besides modelling non-termination, the delay monad also counts the execution time of a computation. This is a result of the too intensional notion of equality that this monad comes with.
|
|
|
|
In chapter~\ref{chp:setoids} we will see a way to remedy this: taking the quotient of the delay monad where execution time is ignored. This will then yield an equational lifting monad on the category of setoids. However, in a general setting it is generally believed to be impossible to define a monad structure on this quotient. Chapman et al. have identified the axiom of countable choice (which crucially holds in the category of setoids) as a sufficient requirement for defining a monad structure on the quotient of $\mathbf{D}$. |