Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation
This commit is contained in:
partowp
+1
-1
Submodule TexCommons updated: 348823b83c...6f6862db5e
+73
-37
@@ -388,8 +388,14 @@ Pouya Partow\inst{1}\orcidID{0009-0003-9652-9469}}
|
||||
%
|
||||
|
||||
\section{Coalgebraic Bisimulation}%\label{sec:}
|
||||
In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that at least has products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, and by relation we are referring to a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ such that the morphism $\brks{p_1,p_2}$ is a mono. We show morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$.
|
||||
A morphism $f\c R\rto S$ ($f\c R\spto S$) is a morphism in $\rel(\BC)$ ($\spa(\BC)$), whenever $f$, $g_1$ and $g_2$ are morphisms in $\BC$ for which the following diagram commutes in $\BC$:
|
||||
In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has
|
||||
products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\
|
||||
such spans $(X \stackrel{p_1}{\leftarrow} R
|
||||
\stackrel{p_2}{\to}Y)$ that the morphism $\brks{p_1,p_2}$ is a mono.
|
||||
We denote morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$.
|
||||
A morphism $R\rto S$ ($R\spto S$) in $\rel(\BC)$
|
||||
($\spa(\BC)$) is such a triple of morphisms $(f\c R\to S, g_1\c X_1\to Y_1, g_2\c X_2\to Y_2)$
|
||||
in $\BC$ that the following diagram commutes:
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
{X_1} \& R \& {X_2} \\
|
||||
@@ -417,8 +423,9 @@ A morphism $f\c R\rto S$ ($f\c R\spto S$) is a morphism in $\rel(\BC)$ ($\spa(\B
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
\end{definition}
|
||||
|
||||
We have notions of bisimulation that may involve relation lifting. An example of a relation lifting is to use the image factorization provided 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.}
|
||||
%
|
||||
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=\&]
|
||||
@@ -450,13 +457,33 @@ So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC
|
||||
\arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2]
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
|
||||
Also, there exist a well-known notion named relator, instead of relation lifting. A relator does not need to be a functor, but it should be a map of a specific type format that is monotone with respect to inclusion. Also, relators are defined only on $\Set$ unlike relation liftings. %We discuss relators more in depth in the later chapters.
|
||||
%
|
||||
%There exists a well-known notion named relator, instead of relation lifting. A relator does not need to be a functor, but it should be a map of a specific type format that is monotone with respect to inclusion. Also, relators are defined only on $\Set$ unlike relation liftings. %We discuss relators more in depth in the later chapters.
|
||||
For the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ and $\spa$ we mean $\rel(\Set)$ and $\spa(\Set)$, accordingly.
|
||||
|
||||
In $\Set$, there is another way to define the morphisms that is to say that $f\c R\rto S$ ($f\c R\spto S$) is a morphism in $\rel$ ($\spa$), whenever there are functions $g_1$ and $g_2$ that $x\mathrel{R}y\Rightarrow g_1(x)\mathrel{(FR)}g_2(y)$.
|
||||
We can define morphisms in $\rel$ differently by only requesting such functions $g_1$ and $g_2$ that $x\mathrel{R}y$ entails $g_1(x)\mathrel{S}g_2(y)$. Let us
|
||||
call such morphisms \emph{anonymous} (because they omit the witnessing part $f$, which is unique for relations but not for general spans). This however yields
|
||||
an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.}
|
||||
|
||||
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}
|
||||
|
||||
Now, considering the two types of morphisms that we can define for $\rel$, and having lifting over the relation or not, we give four notions of bisimulation:
|
||||
%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$.
|
||||
@@ -484,6 +511,9 @@ Now, considering the two types of morphisms that we can define for $\rel$, and h
|
||||
% \end{equation*}
|
||||
%\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=\&]
|
||||
@@ -499,8 +529,10 @@ Now, considering the two types of morphisms that we can define for $\rel$, and h
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
\end{definition}
|
||||
Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$ instead of $\Set$. Worth noting that with this definition,if $R$ is a bisimulation, it does not necassirily mean that $FR$ is a relation as well, for example $FR$ can have elements that are not pairs.
|
||||
|
||||
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*}
|
||||
@@ -536,7 +568,7 @@ A more general version of witnessless bisimulation is given by Hughes and Jacobs
|
||||
\end{definition}
|
||||
Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary category $\BC$.
|
||||
|
||||
\begin{definition}[Vanilla Bisimulation]
|
||||
\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=\&]
|
||||
@@ -554,6 +586,7 @@ Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary categ
|
||||
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.
|
||||
@@ -574,13 +607,12 @@ We do not know if this definition exists anywhere.
|
||||
|
||||
(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}
|
||||
\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.
|
||||
|
||||
To have a Hermida-Jacobs bisimulation to be a witnessless bisimulation we need to have $(FR)^\dagger\subseteq FX\times FY$ that is more common, for example it is true for the powerset functor, although we still can not prove it for the general case. Perhaps a condition is needed to be able to have a general statement.
|
||||
\end{rem}
|
||||
\todo{Discuss 4 versions of bisimulation (with witness/without witness, for relations/for spans). Which are equivalent? Which do not make sense?}
|
||||
|
||||
@@ -2005,7 +2037,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
|
||||
%\end{proof}
|
||||
\subsection{The concrete proof}
|
||||
\begin{lemma}\label{lem:sim-opsim-inc}
|
||||
Assuming that $\sigma\c R\to\powf R$ is witness for the 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*)]
|
||||
\item $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$\label{item:sim-opsim-inc:I}
|
||||
\item $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$\label{item:sim-opsim-inc:II}
|
||||
@@ -2013,25 +2045,28 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
|
||||
\begin{gather*}
|
||||
\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2),\\
|
||||
\powf p_2\comp\sigma(x_1,x_2)\subseteq\alpha(x_2).
|
||||
\end{gather*}
|
||||
Since $R$ is symmetric $(x_2,x_1)\in R$, so from $\powf p_2\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$, where
|
||||
\begin{align}
|
||||
\alpha(x_1)\subseteq&\;\powf p_1\comp\sigma(x_1,x_2),\label{eq:alpha_x_1}\\
|
||||
\powf p_2\comp\sigma(x_1,x_2)\subseteq&\;\alpha(x_2).\label{eq:alpha_x_2}
|
||||
\end{align}
|
||||
(I): Since $R$ is symmetric $(x_2,x_1)\in R$, so from \eqref{eq:alpha_x_2} we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$.
|
||||
Therefore:
|
||||
\begin{align*}
|
||||
\powf p_2\comp\sigma(x_2,x_1)&\\
|
||||
&=\powf p_2\comp\sigma\comp s(x_1,x_2)\\
|
||||
&=\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2).
|
||||
\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)=&\; \powf p_2\comp\sigma\comp s(x_1,x_2)\\
|
||||
=&\; \powf p_2\comp\sigma (x_2,x_1)\\
|
||||
\subseteq&\;\alpha(x_1)\\
|
||||
\subseteq&\; \powf p_1\comp\sigma(x_1,x_2) & \by{\eqref{eq:alpha_x_1}}
|
||||
\end{align*}
|
||||
So, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ we have $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$.
|
||||
|
||||
Furthermore, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$, where
|
||||
%
|
||||
(II): Analogously, from~\eqref{eq:alpha_x_1} by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$.
|
||||
Therefore:
|
||||
\begin{align*}
|
||||
\powf p_1\comp\sigma(x_2,x_1)&\\
|
||||
&=\powf p_1\comp\sigma\comp s(x_1,x_2)\\
|
||||
&=\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2).
|
||||
\powf p_2\comp\sigma(x_1,x_2)\subseteq&\; \alpha(x_2) &\by{\eqref{eq:alpha_x_2}}\\
|
||||
\subseteq&\; \powf p_1\comp\sigma(x_2,x_1) \\
|
||||
=&\; \powf p_1\comp\sigma\comp s(x_1,x_2) \\
|
||||
=&\;\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2).&
|
||||
\end{align*}
|
||||
So, from $\powf p_2\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$.\qed
|
||||
\qed
|
||||
\end{proof}
|
||||
We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
|
||||
\begin{gather*}
|
||||
@@ -2073,12 +2108,12 @@ We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
|
||||
% Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\meet\sigma_2$ is not necessarily a witness that $R$ is an Aczel-Mendler simulation.
|
||||
%\end{rem}
|
||||
Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. An abstract version of the following lemma is given by Dubut.
|
||||
\begin{lemma}\label{lem:alph-prod}
|
||||
Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, where $\powf p_1\comp\sigma'=\alpha\comp p_1$.
|
||||
\end{lemma}
|
||||
\begin{prop}\label{lem:alph-prod}
|
||||
Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then there exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, such that $\powf p_1\comp\sigma'=\alpha\comp p_1$.
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
We define $\sigma'(x_1,x_2)=\{(x'_1,x'_2)\mid x'_1\in\alpha\comp p_1(x_1,x_2)\;,\;(x'_1,x'_2)\in\sigma(x_1,x_2)\}$. We have $\sigma'\subseteq\sigma$ that gives $\powf p_2\comp\sigma'\subseteq\powf p_2\comp\sigma$. Additionally, we have $\powf p_1\comp\sigma'\subseteq\alpha\comp p_1$.
|
||||
Furthermore, if $x'_1\in\alpha\comp p_1(x_1,x_2)$, since $\alpha\comp p_1\subseteq \powf p_1\comp\sigma$ then $x'_1\in\powf p_1\comp\sigma(x_1,x_2)$, which means that exists $x'_2$ that $(x'_1,x'_2)\in\sigma(x_1,x_2)$. So, by definition of $\sigma'$, we have $(x'_1,x'_2)\in\sigma'(x_1,x_2)$, so $x'_1\in\powf p_1\comp\sigma'(x_1,x_2)$ that means $\alpha\comp p_1\subseteq \powf p_1\comp\sigma'$ as well. So, $\sigma'$ is another witness for $R$ to be an AM simulation, and we have $\alpha\comp p_1=\powf p_1\comp\sigma'$.
|
||||
Furthermore, if $x'_1\in\alpha\comp p_1(x_1,x_2)$, since $\alpha\comp p_1\subseteq \powf p_1\comp\sigma$ then $x'_1\in\powf p_1\comp\sigma(x_1,x_2)$. Let $(x'_1,x'_2)\in\sigma(x_1,x_2)$. By definition of $\sigma'$, we have $(x'_1,x'_2)\in\sigma'(x_1,x_2)$, so $x'_1\in\powf p_1\comp\sigma'(x_1,x_2)$ that means $\alpha\comp p_1\subseteq \powf p_1\comp\sigma'$ as well. So, $\sigma'$ is another witness for $R$ to be an AM simulation, and we have $\alpha\comp p_1=\powf p_1\comp\sigma'$.
|
||||
\qed
|
||||
\end{proof}
|
||||
\begin{prop}\label{prop:sym-rel-bisim}
|
||||
@@ -2088,12 +2123,13 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the
|
||||
\end{gather*}
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:I} we have
|
||||
For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:I} we have
|
||||
\begin{gather*}
|
||||
\powf p_1\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
|
||||
\powf p_1\comp\sigma(x_1,x_2),
|
||||
\powf p_1\comp\sigma(x_1,x_2).
|
||||
\end{gather*}
|
||||
and by~\autoref{lem:alph-prod}, $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. Furthermore, by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:II} we have
|
||||
% and by~\autoref{lem:alph-prod},
|
||||
Recall that $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:II} we have
|
||||
\begin{gather*}
|
||||
\powf p_2\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
|
||||
\powf p_2\comp(\powf s\comp\sigma\comp s)(x_1,x_2).
|
||||
|
||||
Reference in New Issue
Block a user