The first draft for the first two sections
This commit is contained in:
partowp
+195
-188
@@ -741,210 +741,197 @@ From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and re
|
|||||||
|
|
||||||
\subsection{Categories of Spans and Relations as Double Categories}
|
\subsection{Categories of Spans and Relations as Double Categories}
|
||||||
As mentioned in the previous section, there is a way to define morphisms in $\spa$ and $\rel$ that can not be captured if an abstract category $\BC$ is replacing $\Set$. We show that $\spa(\BC)$, $\spa_a$, $\rel(\BC)$, and $\rel_a$ are all double categories to give an abstract notion that does capture all the different notions together. Also, double categories show us a way to have $\spa_a(\BC)$ and $\rel_a(\BC)$, i.e., category of spans and category of relations over an arbitrary category $\BC$ with anonymous morphisms[really?!].
|
As mentioned in the previous section, there is a way to define morphisms in $\spa$ and $\rel$ that can not be captured if an abstract category $\BC$ is replacing $\Set$. We show that $\spa(\BC)$, $\spa_a$, $\rel(\BC)$, and $\rel_a$ are all double categories to give an abstract notion that does capture all the different notions together. Also, double categories show us a way to have $\spa_a(\BC)$ and $\rel_a(\BC)$, i.e., category of spans and category of relations over an arbitrary category $\BC$ with anonymous morphisms[really?!].
|
||||||
\todo{Finish at last. "at last" means after finishing the section for bisimulation without talking about double categories.}
|
\todo{Finish at last. "at last" means after finishing the section for simulation without talking about double categories.}
|
||||||
\section{Coalgebraic Bisimulation}%\label{sec:}
|
\section{Coalgebraic Bisimulation}%\label{sec:}
|
||||||
|
|
||||||
\begin{definition}[Relation Lifting]
|
|
||||||
Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, where the following diagram commutes:
|
|
||||||
\begin{equation*}
|
|
||||||
\begin{tikzcd}[ampersand replacement=\&]
|
|
||||||
\rel(\BC) \&\& \rel(\BC) \\
|
|
||||||
{\BC\times\BC} \&\& {\BC\times\BC}
|
|
||||||
\arrow["{\rel(F)}", from=1-1, to=1-3]
|
|
||||||
\arrow[from=1-1, to=2-1]
|
|
||||||
\arrow[from=1-3, to=2-3]
|
|
||||||
\arrow["{F\times F}"', from=2-1, to=2-3]
|
|
||||||
\end{tikzcd}
|
|
||||||
\end{equation*}
|
|
||||||
\end{definition}
|
|
||||||
%
|
%
|
||||||
We have notions of bisimulation that may involve relation lifting. An example of a relation lifting is obtained
|
%\begin{definition}[Relation Lifting]
|
||||||
by the image factorization in regular categories. \ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.}
|
% Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, where the following diagram commutes:
|
||||||
|
% \begin{equation*}
|
||||||
|
% \begin{tikzcd}[ampersand replacement=\&]
|
||||||
|
% \rel(\BC) \&\& \rel(\BC) \\
|
||||||
|
% {\BC\times\BC} \&\& {\BC\times\BC}
|
||||||
|
% \arrow["{\rel(F)}", from=1-1, to=1-3]
|
||||||
|
% \arrow[from=1-1, to=2-1]
|
||||||
|
% \arrow[from=1-3, to=2-3]
|
||||||
|
% \arrow["{F\times F}"', from=2-1, to=2-3]
|
||||||
|
% \end{tikzcd}
|
||||||
|
% \end{equation*}
|
||||||
|
%\end{definition}
|
||||||
|
%%
|
||||||
|
%We have notions of bisimulation that may involve relation lifting. An example of a relation lifting is obtained
|
||||||
|
%by the image factorization in regular categories. \ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.}
|
||||||
|
%%
|
||||||
|
%%\begin{equation*}
|
||||||
|
%% \begin{tikzcd}[ampersand replacement=\&]
|
||||||
|
% % R \& {R^\dagger} \&\& {X\times X}
|
||||||
|
% % \arrow["{e_R}"', two heads, from=1-1, to=1-2]
|
||||||
|
% % \arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
|
||||||
|
% % \arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
|
||||||
|
% % \end{tikzcd}
|
||||||
|
%%\end{equation*}
|
||||||
|
%We define a functor of type $(-)^\dagger\c\spa(\BC)\to\rel(\BC)$. It takes every span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the image of its legs:
|
||||||
%
|
%
|
||||||
%\begin{equation*}
|
%\begin{equation*}
|
||||||
% \begin{tikzcd}[ampersand replacement=\&]
|
% \begin{tikzcd}[ampersand replacement=\&]
|
||||||
% R \& {R^\dagger} \&\& {X\times X}
|
% R \& {R^\dagger} \&\& {X\times Y}
|
||||||
% \arrow["{e_R}"', two heads, from=1-1, to=1-2]
|
% \arrow["{e_R}"', two heads, from=1-1, to=1-2]
|
||||||
% \arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
|
% \arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
|
||||||
% \arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
|
% \arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
|
||||||
% \end{tikzcd}
|
% \end{tikzcd}
|
||||||
%\end{equation*}
|
%\end{equation*}
|
||||||
We define a functor of type $(-)^\dagger\c\spa(\BC)\to\rel(\BC)$. It takes every span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the image of its legs:
|
|
||||||
|
|
||||||
\begin{equation*}
|
|
||||||
\begin{tikzcd}[ampersand replacement=\&]
|
|
||||||
R \& {R^\dagger} \&\& {X\times Y}
|
|
||||||
\arrow["{e_R}"', two heads, from=1-1, to=1-2]
|
|
||||||
\arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
|
|
||||||
\arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
|
|
||||||
\end{tikzcd}
|
|
||||||
\end{equation*}
|
|
||||||
|
|
||||||
So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ that takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation:
|
|
||||||
\begin{equation*}
|
|
||||||
\begin{tikzcd}[ampersand replacement=\&]
|
|
||||||
\& {(FR)^\dagger} \& \\
|
|
||||||
FX \&\& FY \\
|
|
||||||
\& {FX\times FY}
|
|
||||||
\arrow["{{{(Fp_1)^\dagger}}}"', from=1-2, to=2-1]
|
|
||||||
\arrow["{{{(Fp_2)^\dagger}}}", from=1-2, to=2-3]
|
|
||||||
\arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2]
|
|
||||||
\end{tikzcd}
|
|
||||||
\end{equation*}
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
||||||
By varying from anonymous to non-anonymous morphisms and from $\rel$ to $\spa$ we
|
|
||||||
can obtain for flavors of bisimulation (\autoref{eq:acz-mend-diag}--\autoref{def:vanila}) --
|
|
||||||
\autoref{fig:anonymous_onymous} contains a comprehensible summary.
|
|
||||||
|
|
||||||
\begin{figure}[t]
|
|
||||||
\centering
|
|
||||||
\begin{tabular}{|l|c|c|}
|
|
||||||
\hline
|
|
||||||
& \textbf{Anonymous} & \textbf{Onymous} \\
|
|
||||||
\hline
|
|
||||||
\textbf{Relations} & Witnessless & Hermida-Jacobs \\
|
|
||||||
\hline
|
|
||||||
\textbf{Spans} & Vanilla & Aczel-Mendler \\
|
|
||||||
\hline
|
|
||||||
\end{tabular}
|
|
||||||
\caption{Comparison of anonymous and onymous settings for relations and spans.}
|
|
||||||
\label{fig:anonymous_onymous}
|
|
||||||
\end{figure}
|
|
||||||
|
|
||||||
%We take $\rel(F)\c\rel(\BC)\to\rel(\BC)$ to be the functor that for an arbitrary functor $F\c\BC\to\BC$ takes a relation $R$, where $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and gives the relation that is the image of the function $\brks{Fp_1,Fp_2}\c FR\to FX\times FY$.
|
|
||||||
%\begin{definition}[Bisimulation]
|
|
||||||
% For a functor $F\c\BC\to\BC$, a bisimulation is a $\rel(F)$-coalgebra in $\rel$.
|
|
||||||
%\end{definition}
|
|
||||||
|
|
||||||
%\begin{definition}[$F$-Relator]
|
|
||||||
% For a set functor $F$, and for sets $X$ and $Y$, an $F$-relator $\relar$ is a map that takes every relation on $X\times Y$ to a relation on $FX\times FY$, and it is monotone with respect to inclusion.
|
|
||||||
%\end{definition}
|
|
||||||
%Also, for the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ we mean $\rel(\BC)$.
|
|
||||||
%
|
%
|
||||||
%\begin{prop}
|
%So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ that takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation:
|
||||||
% Assuming that $(R,\alpha)$ is a $\rel(F)$-coalgebra, where $\alpha=\beta_1\times\beta_2$ in $\BC\times\BC$, then the following diagram commutes, and vice-versa:
|
%\begin{equation*}
|
||||||
% \begin{equation*}
|
% \begin{tikzcd}[ampersand replacement=\&]
|
||||||
% \begin{tikzcd}[ampersand replacement=\&]
|
% \& {(FR)^\dagger} \& \\
|
||||||
% {X_1} \& R \& {X_2} \\
|
% FX \&\& FY \\
|
||||||
% {FX_1} \& FR \& {FX_2}
|
% \& {FX\times FY}
|
||||||
% \arrow["{\beta_1}"', from=1-1, to=2-1]
|
% \arrow["{{{(Fp_1)^\dagger}}}"', from=1-2, to=2-1]
|
||||||
% \arrow["{p_1}"', from=1-2, to=1-1]
|
% \arrow["{{{(Fp_2)^\dagger}}}", from=1-2, to=2-3]
|
||||||
% \arrow["{p_2}", from=1-2, to=1-3]
|
% \arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2]
|
||||||
% \arrow["\beta", from=1-2, to=2-2]
|
% \end{tikzcd}
|
||||||
% \arrow["{\beta_2}", from=1-3, to=2-3]
|
%\end{equation*}
|
||||||
% \arrow["{Fp_1}", from=2-2, to=2-1]
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% \arrow["{Fp_2}"', from=2-2, to=2-3]
|
%By varying from anonymous to non-anonymous morphisms and from $\rel$ to $\spa$ we
|
||||||
% \end{tikzcd}
|
%can obtain for flavors of bisimulation (\autoref{eq:acz-mend-diag}--\autoref{def:vanila}) --
|
||||||
% \end{equation*}
|
%\autoref{fig:anonymous_onymous} contains a comprehensible summary.
|
||||||
%\end{prop}
|
|
||||||
\begin{definition}[Aczel-Mendler Bisimulation]
|
|
||||||
\todo{Explain in terms of span morphisms}.
|
|
||||||
|
|
||||||
|
|
||||||
A relation $R\subseteq X\times Y$ is an \emph{Aczel-Mendler bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to FR$ called witness that commutes in the following diagram:
|
|
||||||
\begin{equation*}\label{eq:acz-mend-diag}
|
|
||||||
\begin{tikzcd}[ampersand replacement=\&]
|
|
||||||
{X} \& R \& {Y} \\
|
|
||||||
{FX} \& FR \& {FY}
|
|
||||||
\arrow["{\alpha}"', from=1-1, to=2-1]
|
|
||||||
\arrow["{p_1}"', from=1-2, to=1-1]
|
|
||||||
\arrow["{p_2}", from=1-2, to=1-3]
|
|
||||||
\arrow["\gamma", from=1-2, to=2-2]
|
|
||||||
\arrow["{\beta}", from=1-3, to=2-3]
|
|
||||||
\arrow["{Fp_1}", from=2-2, to=2-1]
|
|
||||||
\arrow["{Fp_2}"', from=2-2, to=2-3]
|
|
||||||
\end{tikzcd}
|
|
||||||
\end{equation*}
|
|
||||||
\end{definition}
|
|
||||||
Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$
|
|
||||||
instead of $\Set$. It is worth noting that with this definition, if $R$ is a
|
|
||||||
relation, it does not necassirily mean that $FR$ is a relation as well.
|
|
||||||
%
|
%
|
||||||
\begin{definition}[Witnessless Bisimulation]
|
%
|
||||||
A relation $R\subseteq X\times Y$ is a \emph{witnessless bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)^\dagger}\beta(y)$.
|
%
|
||||||
% \begin{equation*}
|
%%We take $\rel(F)\c\rel(\BC)\to\rel(\BC)$ to be the functor that for an arbitrary functor $F\c\BC\to\BC$ takes a relation $R$, where $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and gives the relation that is the image of the function $\brks{Fp_1,Fp_2}\c FR\to FX\times FY$.
|
||||||
% \begin{tikzcd}[ampersand replacement=\&]
|
%%\begin{definition}[Bisimulation]
|
||||||
% {X} \& R \& {Y} \\
|
%% For a functor $F\c\BC\to\BC$, a bisimulation is a $\rel(F)$-coalgebra in $\rel$.
|
||||||
% {FX} \& \rel(F)R \& {FY}
|
%%\end{definition}
|
||||||
% \arrow["{\alpha}"', from=1-1, to=2-1]
|
%
|
||||||
% \arrow["{p_1}"', from=1-2, to=1-1]
|
%%\begin{definition}[$F$-Relator]
|
||||||
% \arrow["{p_2}", from=1-2, to=1-3]
|
%% For a set functor $F$, and for sets $X$ and $Y$, an $F$-relator $\relar$ is a map that takes every relation on $X\times Y$ to a relation on $FX\times FY$, and it is monotone with respect to inclusion.
|
||||||
% \arrow["{\beta}", from=1-3, to=2-3]
|
%%\end{definition}
|
||||||
% \arrow["{q_1}", from=2-2, to=2-1]
|
%%Also, for the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ we mean $\rel(\BC)$.
|
||||||
% \arrow["{q_2}"', from=2-2, to=2-3]
|
%%
|
||||||
% \end{tikzcd}
|
%%\begin{prop}
|
||||||
% \end{equation*}
|
%% Assuming that $(R,\alpha)$ is a $\rel(F)$-coalgebra, where $\alpha=\beta_1\times\beta_2$ in $\BC\times\BC$, then the following diagram commutes, and vice-versa:
|
||||||
\end{definition}
|
%% \begin{equation*}
|
||||||
A more general version of witnessless bisimulation is given by Hughes and Jacobs, where the lifting is an arbitrary lifting not necessarily the one with image factorization that we mentioned here.
|
%% \begin{tikzcd}[ampersand replacement=\&]
|
||||||
|
%% {X_1} \& R \& {X_2} \\
|
||||||
\begin{definition}[Hermida-Jacobs Bisimulation]
|
%% {FX_1} \& FR \& {FX_2}
|
||||||
A relation $R\subseteq X\times Y$ is a \emph{Hermida-Jacobs bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to (FR)^\dagger$ called witness that commutes in the following diagram:
|
%% \arrow["{\beta_1}"', from=1-1, to=2-1]
|
||||||
\begin{equation*}
|
%% \arrow["{p_1}"', from=1-2, to=1-1]
|
||||||
\begin{tikzcd}[ampersand replacement=\&]
|
%% \arrow["{p_2}", from=1-2, to=1-3]
|
||||||
{X} \& R \& {Y} \\
|
%% \arrow["\beta", from=1-2, to=2-2]
|
||||||
{FX} \& (FR)^\dagger \& {FY}
|
%% \arrow["{\beta_2}", from=1-3, to=2-3]
|
||||||
\arrow["{\alpha}"', from=1-1, to=2-1]
|
%% \arrow["{Fp_1}", from=2-2, to=2-1]
|
||||||
\arrow["{p_1}"', from=1-2, to=1-1]
|
%% \arrow["{Fp_2}"', from=2-2, to=2-3]
|
||||||
\arrow["{p_2}", from=1-2, to=1-3]
|
%% \end{tikzcd}
|
||||||
\arrow["\gamma", from=1-2, to=2-2]
|
%% \end{equation*}
|
||||||
\arrow["{\beta}", from=1-3, to=2-3]
|
%%\end{prop}
|
||||||
\arrow["{(Fp_1)^\dagger}", from=2-2, to=2-1]
|
%\begin{definition}[Aczel-Mendler Bisimulation]
|
||||||
\arrow["{(Fp_2)^\dagger}"', from=2-2, to=2-3]
|
%\todo{Explain in terms of span morphisms}.
|
||||||
\end{tikzcd}
|
%
|
||||||
\end{equation*}
|
%
|
||||||
\end{definition}
|
% A relation $R\subseteq X\times Y$ is an \emph{Aczel-Mendler bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to FR$ called witness that commutes in the following diagram:
|
||||||
Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary category $\BC$.
|
% \begin{equation*}\label{eq:acz-mend-diag}
|
||||||
|
|
||||||
\begin{definition}[Vanilla Bisimulation]\label{def:vanila}
|
|
||||||
A relation $R\subseteq X\times Y$ is a \emph{vanilla bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)}\beta(y)$.
|
|
||||||
% \begin{equation*}
|
|
||||||
% \begin{tikzcd}[ampersand replacement=\&]
|
% \begin{tikzcd}[ampersand replacement=\&]
|
||||||
% {X} \& R \& {Y} \\
|
% {X} \& R \& {Y} \\
|
||||||
% {FX} \& FR \& {FY}
|
% {FX} \& FR \& {FY}
|
||||||
% \arrow["{\alpha}"', from=1-1, to=2-1]
|
% \arrow["{\alpha}"', from=1-1, to=2-1]
|
||||||
% \arrow["{p_1}"', from=1-2, to=1-1]
|
% \arrow["{p_1}"', from=1-2, to=1-1]
|
||||||
% \arrow["{p_2}", from=1-2, to=1-3]
|
% \arrow["{p_2}", from=1-2, to=1-3]
|
||||||
|
% \arrow["\gamma", from=1-2, to=2-2]
|
||||||
% \arrow["{\beta}", from=1-3, to=2-3]
|
% \arrow["{\beta}", from=1-3, to=2-3]
|
||||||
% \arrow["{Fp_1}", from=2-2, to=2-1]
|
% \arrow["{Fp_1}", from=2-2, to=2-1]
|
||||||
% \arrow["{Fp_2}"', from=2-2, to=2-3]
|
% \arrow["{Fp_2}"', from=2-2, to=2-3]
|
||||||
% \end{tikzcd}
|
% \end{tikzcd}
|
||||||
% \end{equation*}
|
% \end{equation*}
|
||||||
\end{definition}
|
%\end{definition}
|
||||||
We do not know if this definition exists anywhere.
|
%Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$
|
||||||
\begin{prop}
|
%instead of $\Set$. It is worth noting that with this definition, if $R$ is a
|
||||||
The following propositions hold in $\Set$:
|
%relation, it does not necassirily mean that $FR$ is a relation as well.
|
||||||
\todo{How about proving that 1.3,1.4,1.5 are equivalent to each other, and all together to 1.2 under axiom of choice? }
|
%%
|
||||||
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
%\begin{definition}[Witnessless Bisimulation]
|
||||||
%\item Every Aczel-Mendler bisimulation is a vanilla bisimulation.
|
% A relation $R\subseteq X\times Y$ is a \emph{witnessless bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)^\dagger}\beta(y)$.
|
||||||
\item Every vanilla bisimulation is an Aczel-Mendler bisimulation.
|
%% \begin{equation*}
|
||||||
\item Every Aczel-Mendler bisimulation is a Hermida-Jacobs bisimulation.
|
%% \begin{tikzcd}[ampersand replacement=\&]
|
||||||
\item Assuming the axiom of choice, every Hermida-Jacobs bisimulation is an Aczel-Mendler bisimulation.
|
%% {X} \& R \& {Y} \\
|
||||||
\item Every witnessless bisimulation is a Hermida-Jacobs bisimulation.
|
%% {FX} \& \rel(F)R \& {FY}
|
||||||
%\item Every Hermida-Jacobs bisimulation is a witnessless bisimulation.
|
%% \arrow["{\alpha}"', from=1-1, to=2-1]
|
||||||
\end{enumerate}
|
%% \arrow["{p_1}"', from=1-2, to=1-1]
|
||||||
\end{prop}
|
%% \arrow["{p_2}", from=1-2, to=1-3]
|
||||||
\begin{proof}
|
%% \arrow["{\beta}", from=1-3, to=2-3]
|
||||||
%(I): ???%Assuming $x\mathrel{R}y$, then given by~\eqref{eq:acz-mend-diag} we have $\gamma(x,y)\in FR$, $Fp_1\comp\gamma(x,y)=\alpha(x)$, and $Fp_2\comp\gamma(x,y)=\beta(y)$ that means $\alpha(x)\mathrel{(FR)}\beta(y)$.
|
%% \arrow["{q_1}", from=2-2, to=2-1]
|
||||||
|
%% \arrow["{q_2}"', from=2-2, to=2-3]
|
||||||
(I): Since $R$ is a vanilla bisimulation, for every $(x,y)\in R$ we have $\alpha(x)\mathrel{(FR)}\beta(y)$, so we can define $\gamma\c R\to FR$ as $\gamma(x,y)=(\alpha(x),\beta(y))$, and then $\gamma$ commutes in~\eqref{eq:acz-mend-diag}.
|
%% \end{tikzcd}
|
||||||
|
%% \end{equation*}
|
||||||
(II):\autoref{lem:norm-simp}, and given by Staton.
|
%\end{definition}
|
||||||
|
%A more general version of witnessless bisimulation is given by Hughes and Jacobs, where the lifting is an arbitrary lifting not necessarily the one with image factorization that we mentioned here.
|
||||||
(III): Given by Staton, and similar to \autoref{lem:norm-simp}.
|
%
|
||||||
|
%\begin{definition}[Hermida-Jacobs Bisimulation]
|
||||||
(IV): Similar to (I) we can define $\gamma(x,y)=(\alpha(x),\beta(y))$ as the witness for $R$ to be a Hermida-Jacobs bisimulation.
|
% A relation $R\subseteq X\times Y$ is a \emph{Hermida-Jacobs bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to (FR)^\dagger$ called witness that commutes in the following diagram:
|
||||||
\end{proof}
|
% \begin{equation*}
|
||||||
\begin{rem}\todo{No, these definitions are just equivalent.}
|
% \begin{tikzcd}[ampersand replacement=\&]
|
||||||
For vanilla bisimulation to be a witnessless bisimulation (or vice-versa) for a relation $R$ we need to have $FR\subseteq (FR)^\dagger$ (or $(FR)^\dagger\subseteq FR$), which is rarely true. The condition may not even be true for other relation liftings for these functors.
|
% {X} \& R \& {Y} \\
|
||||||
\end{rem}
|
% {FX} \& (FR)^\dagger \& {FY}
|
||||||
\begin{rem}
|
% \arrow["{\alpha}"', from=1-1, to=2-1]
|
||||||
\todo{No, this does not follow from anythying.}
|
% \arrow["{p_1}"', from=1-2, to=1-1]
|
||||||
To have an Aczel-Mendler bisimulation to be a vanilla bisimulation we need to have $FR\subseteq FX\times FY$ that is a rare condition. It does not hold for powerset functor or maybe functor.
|
% \arrow["{p_2}", from=1-2, to=1-3]
|
||||||
\end{rem}
|
% \arrow["\gamma", from=1-2, to=2-2]
|
||||||
\todo{Discuss 4 versions of bisimulation (with witness/without witness, for relations/for spans). Which are equivalent? Which do not make sense?}
|
% \arrow["{\beta}", from=1-3, to=2-3]
|
||||||
|
% \arrow["{(Fp_1)^\dagger}", from=2-2, to=2-1]
|
||||||
\todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}\\
|
% \arrow["{(Fp_2)^\dagger}"', from=2-2, to=2-3]
|
||||||
--------------------------------------------------------------
|
% \end{tikzcd}
|
||||||
|
% \end{equation*}
|
||||||
|
%\end{definition}
|
||||||
|
%Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary category $\BC$.
|
||||||
|
%
|
||||||
|
%\begin{definition}[Vanilla Bisimulation]\label{def:vanila}
|
||||||
|
% A relation $R\subseteq X\times Y$ is a \emph{vanilla bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)}\beta(y)$.
|
||||||
|
%% \begin{equation*}
|
||||||
|
%% \begin{tikzcd}[ampersand replacement=\&]
|
||||||
|
%% {X} \& R \& {Y} \\
|
||||||
|
%% {FX} \& FR \& {FY}
|
||||||
|
%% \arrow["{\alpha}"', from=1-1, to=2-1]
|
||||||
|
%% \arrow["{p_1}"', from=1-2, to=1-1]
|
||||||
|
%% \arrow["{p_2}", from=1-2, to=1-3]
|
||||||
|
%% \arrow["{\beta}", from=1-3, to=2-3]
|
||||||
|
%% \arrow["{Fp_1}", from=2-2, to=2-1]
|
||||||
|
%% \arrow["{Fp_2}"', from=2-2, to=2-3]
|
||||||
|
%% \end{tikzcd}
|
||||||
|
%% \end{equation*}
|
||||||
|
%\end{definition}
|
||||||
|
%We do not know if this definition exists anywhere.
|
||||||
|
%\begin{prop}
|
||||||
|
% The following propositions hold in $\Set$:
|
||||||
|
% \todo{How about proving that 1.3,1.4,1.5 are equivalent to each other, and all together to 1.2 under axiom of choice? }
|
||||||
|
% \begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
||||||
|
% %\item Every Aczel-Mendler bisimulation is a vanilla bisimulation.
|
||||||
|
% \item Every vanilla bisimulation is an Aczel-Mendler bisimulation.
|
||||||
|
% \item Every Aczel-Mendler bisimulation is a Hermida-Jacobs bisimulation.
|
||||||
|
% \item Assuming the axiom of choice, every Hermida-Jacobs bisimulation is an Aczel-Mendler bisimulation.
|
||||||
|
% \item Every witnessless bisimulation is a Hermida-Jacobs bisimulation.
|
||||||
|
% %\item Every Hermida-Jacobs bisimulation is a witnessless bisimulation.
|
||||||
|
% \end{enumerate}
|
||||||
|
%\end{prop}
|
||||||
|
%\begin{proof}
|
||||||
|
% %(I): ???%Assuming $x\mathrel{R}y$, then given by~\eqref{eq:acz-mend-diag} we have $\gamma(x,y)\in FR$, $Fp_1\comp\gamma(x,y)=\alpha(x)$, and $Fp_2\comp\gamma(x,y)=\beta(y)$ that means $\alpha(x)\mathrel{(FR)}\beta(y)$.
|
||||||
|
%
|
||||||
|
% (I): Since $R$ is a vanilla bisimulation, for every $(x,y)\in R$ we have $\alpha(x)\mathrel{(FR)}\beta(y)$, so we can define $\gamma\c R\to FR$ as $\gamma(x,y)=(\alpha(x),\beta(y))$, and then $\gamma$ commutes in~\eqref{eq:acz-mend-diag}.
|
||||||
|
%
|
||||||
|
% (II):\autoref{lem:norm-simp}, and given by Staton.
|
||||||
|
%
|
||||||
|
% (III): Given by Staton, and similar to \autoref{lem:norm-simp}.
|
||||||
|
%
|
||||||
|
% (IV): Similar to (I) we can define $\gamma(x,y)=(\alpha(x),\beta(y))$ as the witness for $R$ to be a Hermida-Jacobs bisimulation.
|
||||||
|
%\end{proof}
|
||||||
|
%\begin{rem}\todo{No, these definitions are just equivalent.}
|
||||||
|
% For vanilla bisimulation to be a witnessless bisimulation (or vice-versa) for a relation $R$ we need to have $FR\subseteq (FR)^\dagger$ (or $(FR)^\dagger\subseteq FR$), which is rarely true. The condition may not even be true for other relation liftings for these functors.
|
||||||
|
%\end{rem}
|
||||||
|
%\begin{rem}
|
||||||
|
%\todo{No, this does not follow from anythying.}
|
||||||
|
% To have an Aczel-Mendler bisimulation to be a vanilla bisimulation we need to have $FR\subseteq FX\times FY$ that is a rare condition. It does not hold for powerset functor or maybe functor.
|
||||||
|
%\end{rem}
|
||||||
|
%\todo{Discuss 4 versions of bisimulation (with witness/without witness, for relations/for spans). Which are equivalent? Which do not make sense?}
|
||||||
|
%
|
||||||
|
%\todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}\\
|
||||||
|
%--------------------------------------------------------------
|
||||||
\begin{definition}[Aczel-Mendler Bisimulation]
|
\begin{definition}[Aczel-Mendler Bisimulation]
|
||||||
In an arbitrary category $\BC$, a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{Aczel-Mendler bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\spa(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$.
|
In an arbitrary category $\BC$, a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{Aczel-Mendler bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\spa(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
@@ -1004,7 +991,7 @@ The given definition is highly abstract. There is a relation lifting that abstra
|
|||||||
In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a \emph{Hermida-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.
|
In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a \emph{Hermida-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
%
|
%
|
||||||
\begin{prop}
|
\begin{prop}\label{prop:HeJ-AM}
|
||||||
In a regular category $\BC$ with the axiom of choice, every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is an Aczel-Mendler bisimulation.
|
In a regular category $\BC$ with the axiom of choice, every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is an Aczel-Mendler bisimulation.
|
||||||
\end{prop}
|
\end{prop}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
@@ -1035,8 +1022,28 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
|
|||||||
|
|
||||||
(2): Follows from~\autoref{prop:rel-rela}.
|
(2): Follows from~\autoref{prop:rel-rela}.
|
||||||
|
|
||||||
(3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$.
|
(3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. Assuming $(x,y)\in R$ there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\qed
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
\begin{cor}
|
||||||
|
Recalling~\autoref{prop:HeJ-AM}, all the four introduced definitions for bisimulation (\autoref{fig:anonymous_onymous}) are equivalent under the axiom of choice.
|
||||||
|
\end{cor}
|
||||||
|
\begin{figure}[t]
|
||||||
|
\centering
|
||||||
|
\begin{tabular}{|l|c|c|}
|
||||||
|
\hline
|
||||||
|
& \textbf{Anonymous} & \textbf{Onymous} \\
|
||||||
|
\hline
|
||||||
|
\textbf{Relations} & Hughes-Jacobs & Hermida-Jacobs \\
|
||||||
|
\hline
|
||||||
|
\textbf{Spans} & Span-based & Aczel-Mendler \\
|
||||||
|
\hline
|
||||||
|
\end{tabular}
|
||||||
|
\caption{Comparison of anonymous and onymous settings for relations and spans in $\Set$.}
|
||||||
|
\label{fig:anonymous_onymous}
|
||||||
|
\end{figure}
|
||||||
|
%
|
||||||
|
\subsection{Bisimulation in Double Categories}
|
||||||
|
\todo{Start writing this after the section for double categories in the previous section. You should first introduce your definition, and then give all the definitions as examples of your "double coalgebra".}
|
||||||
%
|
%
|
||||||
\section{Coalgebraic Simulation}
|
\section{Coalgebraic Simulation}
|
||||||
We show the category of preorders with monotone functions between them with $\preord$. In the diagrams, any arrow that shows a functor, but does not have a label is showing a forgetful functor. Also, we use $\rel$ to refer to the category of binary relations. Assuming $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and $S\in\obj(\rel)$ and $S\subseteq Y_1\times Y_2$, then a morphism $f\c R\to S$ in this category is the pair $(f_1,f_2)$ of morhpisms in $\Set$, where, $f_1\c X_1\to Y_1$ and $f_2\c X_2\to Y_2$, and for each $(x_1,x_2)\in R$ we have $(f_1(x_1),f_2(x_2))\in S$. Also, we show projections of $R\in\obj(\rel)$ with $p_1$ and $p_2$ that are morphisms in $\Set$.
|
We show the category of preorders with monotone functions between them with $\preord$. In the diagrams, any arrow that shows a functor, but does not have a label is showing a forgetful functor. Also, we use $\rel$ to refer to the category of binary relations. Assuming $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and $S\in\obj(\rel)$ and $S\subseteq Y_1\times Y_2$, then a morphism $f\c R\to S$ in this category is the pair $(f_1,f_2)$ of morhpisms in $\Set$, where, $f_1\c X_1\to Y_1$ and $f_2\c X_2\to Y_2$, and for each $(x_1,x_2)\in R$ we have $(f_1(x_1),f_2(x_2))\in S$. Also, we show projections of $R\in\obj(\rel)$ with $p_1$ and $p_2$ that are morphisms in $\Set$.
|
||||||
@@ -2536,7 +2543,7 @@ Indeed, $\sigma^\dagger$ is a witness for $R$ to be an HJ-simulation, but it is
|
|||||||
\end{gather*}
|
\end{gather*}
|
||||||
\end{example}
|
\end{example}
|
||||||
|
|
||||||
\subsection{From Symmetric Simulation To Bisimulation (Span-based)}
|
\subsection{From Symmetric Simulation To Bisimulation (Aczel-Mendler)}
|
||||||
%\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}
|
%\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}
|
||||||
% Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
|
% Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
|
||||||
% \begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
% \begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
||||||
|
|||||||
Reference in New Issue
Block a user