pouya/coalgebraic-simulation
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

draft

Browse Source
This commit is contained in:
partowp
2026-06-19 16:32:57 +01:00
parent 3193f636aa
commit d424aa48a6
1 changed files with 21 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+21 -15
View File
@@ -418,7 +418,7 @@ A morphism $f\c R\rto S$ ($f\c R\spto S$) is a morphism in $\rel(\BC)$ ($\spa(\B
\end{equation*} \end{equation*}
\end{definition} \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. 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.}
% %
%\begin{equation*} %\begin{equation*}
% \begin{tikzcd}[ampersand replacement=\&] % \begin{tikzcd}[ampersand replacement=\&]
@@ -499,7 +499,7 @@ Now, considering the two types of morphisms that we can define for $\rel$, and h
\end{tikzcd} \end{tikzcd}
\end{equation*} \end{equation*}
\end{definition} \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$. 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.
\begin{definition}[Witnessless Bisimulation] \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)$. 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)$.
@@ -516,6 +516,7 @@ Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$ instea
% \end{tikzcd} % \end{tikzcd}
% \end{equation*} % \end{equation*}
\end{definition} \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.
\begin{definition}[Hermida-Jacobs Bisimulation] \begin{definition}[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: 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:
@@ -533,7 +534,7 @@ Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$ instea
\end{tikzcd} \end{tikzcd}
\end{equation*} \end{equation*}
\end{definition} \end{definition}
Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary category $\BC$.
\begin{definition}[Vanilla Bisimulation] \begin{definition}[Vanilla Bisimulation]
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)$. 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)$.
@@ -550,32 +551,37 @@ Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$ instea
% \end{tikzcd} % \end{tikzcd}
% \end{equation*} % \end{equation*}
\end{definition} \end{definition}
We do not know if this definition exists anywhere.
\begin{prop} \begin{prop}
The following propositions hold: The following propositions hold in $\Set$:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)] \begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item Every Aczel-Mendler bisimulation is a vanilla bisimulation. %\item Every Aczel-Mendler bisimulation is a vanilla bisimulation.
\item Every vanilla bisimulation is an Aczel-Mendler bisimulation. \item Every vanilla bisimulation is an Aczel-Mendler bisimulation.
\item Every Aczel-Mendler bisimulation is a Hermida-Jacobs 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 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 witnessless bisimulation is a Hermida-Jacobs bisimulation.
\item Assuming the axiom of choice, every witnessless bisimulation is a Hermida-Jacobs bisimulation. %\item Every Hermida-Jacobs bisimulation is a witnessless bisimulation.
\item Every vanilla bisimulation is a witnessless bisimulation.
\item Every witnessless bisimulation is a vanilla bisimulation.
\end{enumerate} \end{enumerate}
\end{prop} \end{prop}
\begin{proof} \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): ???%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)$.
(II): 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}. (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}.
(III): It is trivial. (II):\autoref{lem:norm-simp}, and given by Staton.
(IV): Given by Staton. (III): Given by Staton, and similar to \autoref{lem:norm-simp}.
(V): Similar to (I) we can define $\gamma(x,y)=(\alpha(x),\beta(y))$ as the witness for $R$ to be a 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.
(VI):
\end{proof} \end{proof}
\begin{rem}
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}
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?} \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.} \todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}