mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Proof that D is commutative
This commit is contained in:
parent
d6c13a88e4
commit
54588e48e9
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 149 additions and 24 deletions
|
|
@ -123,6 +123,21 @@
|
|||
numpages = {38}
|
||||
}
|
||||
|
||||
@article{param-corec,
|
||||
title = {Parametric corecursion},
|
||||
journal = {Theoretical Computer Science},
|
||||
volume = {260},
|
||||
number = {1},
|
||||
pages = {139-163},
|
||||
year = {2001},
|
||||
note = {Coalgebraic Methods in Computer Science 1998},
|
||||
issn = {0304-3975},
|
||||
doi = {https://doi.org/10.1016/S0304-3975(00)00126-2},
|
||||
url = {https://www.sciencedirect.com/science/article/pii/S0304397500001262},
|
||||
author = {Lawrence S. Moss},
|
||||
abstract = {This paper gives a treatment of substitution for “parametric” objects in final coalgebras, and also presents principles of definition by corecursion for such objects. The substitution results are coalgebraic versions of well-known consequences of initiality, and the work on corecursion is a general formulation which allows one to specify elements of final coalgebras using systems of equations. One source of our results is the theory of hypersets, and at the end of this paper we sketch a development of that theory which calls upon the general work of this paper to a very large extent and particular facts of elementary set theory to a much smaller extent.}
|
||||
}
|
||||
|
||||
@inproceedings{quotienting,
|
||||
author = {Chapman, James and Uustalu, Tarmo and Veltri, Niccol\`{o}},
|
||||
title = {Quotienting the Delay Monad by Weak Bisimilarity},
|
||||
|
|
@ -157,6 +172,26 @@
|
|||
numpages = {37}
|
||||
}
|
||||
|
||||
@article{sol-thm,
|
||||
author = {Aczel, Peter and Ad\'{a}mek, Jir\'{\i} and Milius, Stefan and Velebil, Jir\'{\i}},
|
||||
title = {Infinite trees and completely iterative theories: a coalgebraic view},
|
||||
year = {2003},
|
||||
issue_date = {07 May 2003},
|
||||
publisher = {Elsevier Science Publishers Ltd.},
|
||||
address = {GBR},
|
||||
volume = {300},
|
||||
number = {1–3},
|
||||
issn = {0304-3975},
|
||||
url = {https://doi.org/10.1016/S0304-3975(02)00728-4},
|
||||
doi = {10.1016/S0304-3975(02)00728-4},
|
||||
abstract = {Infinite trees form a free completely iterative theory over any given signature--this fact, proved by Elgot, Bloom and Tindell, turns out to be a special case of a much more general categorical result exhibited in the present paper. We prove that whenever an endofunctor H of a category has final coalgebras for all functors H(-) + X, then those coalgebras, TX, form a monad. This monad is completely iterative, i.e., every guarded system of recursive equations has a unique solution. And it is a free completely iterative monad on H. The special case of polynomial endofunctors of the category Set is the above mentioned theory, or monad, of infinite trees.This procedure can be generalized to monoidal categories satisfying a mild side condition: if, for an object H, the endofunctor H ⊗ _ + I has a final coalgebra, T, then T is a monoid. This specializes to the above case for the monoidal category of all endofunctors.},
|
||||
journal = {Theor. Comput. Sci.},
|
||||
month = {may},
|
||||
pages = {1–45},
|
||||
numpages = {45},
|
||||
keywords = {coalgebra, completely iterative theory, monad, monoidal category, solution theorem}
|
||||
}
|
||||
|
||||
@article{uniformelgot,
|
||||
author = {Sergey Goncharov},
|
||||
title = {Uniform Elgot Iteration in Foundations},
|
||||
|
|
|
|||
|
|
@ -119,13 +119,13 @@ Since $DX$ is defined as a final coalgebra, we can define morphisms via corecurs
|
|||
\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=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFsyLDAsIlggXFx0aW1lcyAoWSArIERZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgKyBEKFggXFx0aW1lcyBZKSJdLFswLDEsIlxcdGF1IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiLDJdLFsyLDMsImRzdGwiLDJdLFszLDQsImlkICtcXHRhdSIsMl0sWzEsNCwib3V0Il1d
|
||||
% 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 \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}
|
||||
|
|
@ -218,31 +218,121 @@ Since $DX$ is a final coalgebra we get the following proof principle:
|
|||
Next we check the strength laws:
|
||||
\begin{itemize}
|
||||
\item[\ref{S1}] To show that $(now \circ \pi_2)^* \circ \tau = \pi_2$ we take the following coalgebra:
|
||||
% https://q.uiver.app/#q=WzAsNixbMCwwLCIxIFxcdGltZXMgRFgiXSxbMCwxLCJEWCJdLFs1LDAsIlggKyAxIFxcdGltZXMgRFgiXSxbNSwxLCJYICsgRFgiXSxbMiwwLCIxIFxcdGltZXMgWCArIERYIl0sWzMsMCwiMSBcXHRpbWVzIFggKyAxIFxcdGltZXMgRFgiXSxbMSwzLCJvdXQiXSxbMCwxLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywiaWQgKyAhIl0sWzAsNCwiaWQgXFx0aW1lcyBvdXQiXSxbNCw1LCJkc3RsIl0sWzUsMiwiXFxwaV8yICsgaWQiXV0=
|
||||
% https://q.uiver.app/#q=WzAsNixbMCwwLCIxIFxcdGltZXMgRFgiXSxbMCwxLCJEWCJdLFszLDAsIlggKyAxIFxcdGltZXMgRFgiXSxbMywxLCJYICsgRFgiXSxbMSwwLCIxIFxcdGltZXMgWCArIERYIl0sWzIsMCwiMSBcXHRpbWVzIFggKyAxIFxcdGltZXMgRFgiXSxbMSwzLCJvdXQiXSxbMCwxLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywiaWQgKyAhIl0sWzAsNCwiaWQgXFx0aW1lcyBvdXQiXSxbNCw1LCJkc3RsIl0sWzUsMiwiXFxwaV8yICsgaWQiXV0=
|
||||
\[\begin{tikzcd}
|
||||
{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-6]
|
||||
{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["{!}", dashed, from=1-1, to=2-1]
|
||||
\arrow["{id + !}", from=1-6, to=2-6]
|
||||
\arrow["{id + !}", 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 since $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=WzAsNixbMCwwLCJYIFxcdGltZXMgRERZIl0sWzAsMiwiRChYXFx0aW1lcyBZKSJdLFsxLDAsIlggXFx0aW1lcyAoRFkgKyBERFkpIl0sWzIsMCwiWCBcXHRpbWVzIERZICsgWCBcXHRpbWVzIEREWSJdLFsyLDIsIlggXFx0aW1lcyBZICsgRChYIFxcdGltZXMgWSkiXSxbMiwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBERFkiXSxbMCwxLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzEsNCwib3V0Il0sWzUsNCwiaWQgKyBcXDshIiwyXSxbMyw1LCJbIChpZCArIChpZCBcXHRpbWVzIG5vdykpIFxcY2lyYyBkc3RsIFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpICwgaV8yIF0iLDJdXQ==
|
||||
\[\begin{tikzcd}
|
||||
{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["{!}", 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 + \;!}"', 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 that $D\alpha \circ \tau = \tau \circ (id \times \tau) \circ \alpha$ we take the following coalgebra:
|
||||
% https://q.uiver.app/#q=WzAsNixbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgRFoiXSxbMCwyLCJEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMywyLCJYIFxcdGltZXMgWSBcXHRpbWVzIFogKyBEKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMywxLCJYIFxcdGltZXMgWSAgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzIsMCwiKFggXFx0aW1lcyBZKSBcXHRpbWVzIChaKyBEWikiXSxbMywwLCIoWFxcdGltZXMgWSkgXFx0aW1lcyBaICsgKFggXFx0aW1lcyBZKSBcXHRpbWVzIERaIl0sWzAsMSwiISIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsxLDIsIm91dCJdLFszLDIsImlkICtcXDshIiwyXSxbMCw0LCJpZCBcXHRpbWVzIG91dCJdLFs0LDUsImRzdGwiXSxbNSwzLCJcXGxhbmdsZSBcXHBpXzEgXFxjaXJjIFxccGlfMSAsIFxcbGFuZ2xlIFxccGlfMiBcXGNpcmMgXFxwaV8xICwgXFxwaV8yIFxccmFuZ2xlIFxccmFuZ2xlICsgaWQiLDJdXQ==
|
||||
\[\begin{tikzcd}
|
||||
{(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["{!}", dashed, from=1-1, to=3-1]
|
||||
\arrow["out", from=3-1, to=3-4]
|
||||
\arrow["{id +\;!}"', from=2-4, to=3-4]
|
||||
\arrow["{id \times out}", from=1-1, to=1-3]
|
||||
\arrow["dstl", from=1-3, to=1-4]
|
||||
\arrow["{\pi_2 + id}", from=1-4, to=1-6]
|
||||
\arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-4, to=2-4]
|
||||
\end{tikzcd}\]
|
||||
\item[\ref{S2}] To show that $\tau \circ (id \times now) = now$ we don't need coinduction, 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 since $dstl \circ (id \times i_1) = i_1$.
|
||||
\item[\ref{S3}]
|
||||
\item[\ref{S4}]
|
||||
\end{itemize}
|
||||
\end{proof}
|
||||
|
||||
To show that $\mathbf{D}$ is commutative we will use another proof principle previously called the \textit{Solution Theorem}~\cite{sol-thm} and \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=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcOyEiXSxbMiwwLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
|
||||
\[\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 + \;!}", from=1-4, to=2-4]
|
||||
\arrow["{!}", dashed, from=1-1, to=2-1]
|
||||
\end{tikzcd}\]
|
||||
\end{proof}
|
||||
|
||||
\begin{theorem}
|
||||
$\mathbf{D}$ is commutative.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
Using corollary~\ref{cor:solution} it suffices to show that both $\tau^* \circ \hat{\tau}$ and $\hat{\tau}^* \circ \tau$ are solutions of some guarded morphism $g$.
|
||||
|
||||
Let $w = (dstr + dstr) ∘ dstl ∘ (out \times out)$ and
|
||||
\[g = out^{-1} \circ [ i_1 + D i_1 \circ \hat{\tau} , 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 \hat{\tau} , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w$.
|
||||
|
||||
We are left to show that $\tau^* \circ \hat{\tau}$ and $\hat{\tau}^* \circ \tau$ are solutions of $g$, i.e.:
|
||||
|
||||
\[\tau^* \circ \hat{\tau} = out^{-1} \circ [ id + \hat{\tau} , i_2 \circ [ \tau , later \circ \tau^* \circ \hat{\tau} ] ] \circ w = [ now , \tau^* \circ \hat{\tau}]^* \circ g \]
|
||||
\[\hat{\tau}^* \circ \tau = out^{-1} \circ [ id + \hat{\tau} , i_2 \circ [ \tau , later \circ \hat{\tau}^* \circ \tau ] ] \circ w = [ now , \hat{\tau}^* \circ \tau]^* \circ g \]
|
||||
|
||||
The first step in both equations can be proven by monicity of $out$ and then using \ref{D3} and the dual diagram for $\hat{\tau}$ which is a direct consequence of \ref{D3}:
|
||||
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJYIFxcdGltZXMgRFkiXSxbMCwxLCJEKFggXFx0aW1lcyBZKSJdLFs0LDAsIlggXFx0aW1lcyBZICsgWCBcXHRpbWVzIERZIl0sWzQsMSwiWCBcXHRpbWVzIFkgK0QoWCBcXHRpbWVzIFkpIl0sWzIsMCwiWCBcXHRpbWVzIChZICsgRFkpIl0sWzAsMSwiXFxoYXR7XFx0YXV9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMywib3V0Il0sWzIsMywiaWQgKyBcXGhhdHtcXHRhdX0iLDJdLFswLDQsImlkIFxcdGltZXMgb3V0Il0sWzQsMiwiZHN0bCJdXQ==
|
||||
\[\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["{\hat{\tau}}", dashed, from=1-1, to=2-1]
|
||||
\arrow["out", from=2-1, to=2-5]
|
||||
\arrow["{id + \hat{\tau}}"', from=1-5, to=2-5]
|
||||
\arrow["{id \times out}", from=1-1, to=1-3]
|
||||
\arrow["dstl", from=1-3, to=1-5]
|
||||
\end{tikzcd}\]
|
||||
the last step holds generally for any $f : DX \times DY \rightarrow D(X \times Y)$.
|
||||
\end{proof}
|
||||
Loading…
Reference in a new issue