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

more!

Browse Source
This commit is contained in:
partowp
2026-07-24 16:42:07 +01:00
parent 539b5fec3d
commit 4f9fc5a687
1 changed files with 152 additions and 67 deletions
Download Patch File Download Diff File Expand all files Collapse all files
ACV 2026/slides.tex
+152 -67
View File
@@ -312,9 +312,9 @@
\vspace{2mm} \vspace{2mm}
\begin{block}{Simulation and Bisimulation} \begin{block}{Simulation}
A relation $R\subseteq X\times Y$ is a simulation from $(X,A,T)$ to $(Y,A,S)$ whenever A relation $R\subseteq X\times Y$ is a simulation from $(X,A,T)$ to $(Y,A,S)$ whenever:
\[ \[
\begin{tikzcd}[ampersand replacement=\&] \begin{tikzcd}[ampersand replacement=\&]
x \& y \\ x \& y \\
@@ -363,7 +363,7 @@
xRy, xRy,
\] \]
where $R$ is a simulation.\\ where $R$ is a simulation.\\
Similarity is defined similarly, where $R$ is a simulation, and it is shown with $\precsim$. Bisimilarity is defined similarly, where $R$ is a bisimulation, and it is shown with $\sim$.
% Similarly, the \emph{bisimilarity relation} $\sim\subseteq X\times Y$ is the greatest bisimulation relation. Equivalently\vspace{-0.3cm} % Similarly, the \emph{bisimilarity relation} $\sim\subseteq X\times Y$ is the greatest bisimulation relation. Equivalently\vspace{-0.3cm}
% \[ % \[
% x\sim y % x\sim y
@@ -450,14 +450,14 @@
\end{gather*} \end{gather*}
\end{alertblock}\vspace{-0.5cm} \end{alertblock}\vspace{-0.5cm}
-In the literature, this is often proved using \emph{Howe's method}. \\ -In the literature, this is often proved using \emph{Howe's method}. \\
-The method, applies a closure on the bisimilarity relation on $\mS$.\\ -The method, applies a closure on the bisimilarity relation on $T$.\\
-Then one should prove that the result is a simulation.\\ -Then one should prove that the result is a simulation.\\
-The closure preserves symmetry, and symmetric simulation is a bisimulation in traditional definitions.\\ -The closure preserves symmetry, and symmetric simulation is a bisimulation in traditional definitions.\\
-We have found out that it is not always the case.\\ -We have found out that it is not always the case.\\
-That is why we want to know when exactly a symmetric simulation is a bisimulation. -That is why we want to know when exactly a symmetric simulation is a bisimulation.
\end{frame} \end{frame}
\begin{frame}{Relators, Simulations and Bisimulations} \begin{frame}{Relators and Simulations}
\footnotesize \footnotesize
@@ -465,7 +465,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth} \column{.47\textwidth}
To define coalgebraic simulation, relators are invented.
\begin{alertblock}{Relator} \begin{alertblock}{Relator}
Assuming $F:\Set\to\Set$ is a functor, an $F$-relator a monotone map that sends a morphism of $\rel$ that is a relation $X\rto Y$ to a relation $FX\rto FY$. Assuming $F:\Set\to\Set$ is a functor, an $F$-relator a monotone map that sends a morphism of $\rel$ that is a relation $X\rto Y$ to a relation $FX\rto FY$.
\end{alertblock} \end{alertblock}
@@ -473,62 +473,101 @@
\begin{block}{R-Simulation} \begin{block}{R-Simulation}
For an $F$-relator $\relar$, a relation $r:X\rto Y$ is a $\relar$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if $r\subseteq \beta\comp\relar r\comp\alpha^{-1}$. For an $F$-relator $\relar$, a relation $r:X\rto Y$ is a $\relar$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if $r\subseteq \beta\comp\relar r\comp\alpha^{-1}$.
\end{block} \end{block}
\vspace{-0.3cm} % \vspace{-0.3cm}
%
\begin{alertblock}{Symmetrization of a Relator} % \begin{alertblock}{Symmetrization of a Relator}
Symmetrization of a relator $\relar$ is defined as: % Symmetrization of a relator $\relar$ is defined as:
\begin{gather*} % \begin{gather*}
\hat{\relar}=\relar r\cap (\relar r^{-1})^{-1} % \hat{\relar}=\relar r\cap (\relar r^{-1})^{-1}
\end{gather*} % \end{gather*}
\end{alertblock} % \end{alertblock}
\begin{block}{R-Similarity}
$\relar$-similarity is the greatest $\relar$-simulation.
\end{block}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth} \column{.47\textwidth}
\begin{alertblock}{Symmetric Relator} \begin{alertblock}{Example: Trivial Relator}
A relator $\relar$ is symmetric if $\relar=\hat{\relar}$ For an arbitrary set endofunctor $F$, the relator $\mathbf{K}$ takes every relation $r:X\rto Y$ to $FX\times FY$.
\end{alertblock} \end{alertblock}\vspace{-0.2cm}
\vspace{-0.2cm} % \begin{alertblock}{Symmetric Relator}
\begin{block}{R-Bisimulation} % A relator $\relar$ is symmetric if $\relar=\hat{\relar}$
For an $F$-relator $\relar$, a relation $r:X\rto Y$ is a $\relar$-bisimulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is an $R$-simulation, and $R$ is a symmetric relator. % \end{alertblock}
% \vspace{-0.2cm}
% \begin{block}{R-Bisimulation}
% For an $F$-relator $\relar$, a relation $r:X\rto Y$ is a $\relar$-bisimulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is an $R$-simulation, and $R$ is a symmetric relator.
% \end{block}
% \vspace{-0.2cm}
% \begin{block}{R-Similarity}
% $\relar$-similarity is the greatest $\relar$-simulation.
% \end{block}
% \vspace{-0.3cm}
% \begin{block}{R-Bisimilarity}
% $\relar$-bisimilarity is the greatest $\relar$-bisimulation.
% \end{block}
\begin{block}{}
But it is a bad relator because every relation is a $\mathbf{K}$-bisimulation!
\end{block} \end{block}
\vspace{-0.2cm} \begin{alertblock}{Example: Egli-Milner Relator}
\begin{block}{R-Similarity} The relator $\emre$ is a $\powf$-relator defined as:\vspace{-0.2cm}
$\relar$-similarity is the greatest $\relar$-simulation. \begin{gather*}
\emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}
\end{gather*}
\end{alertblock}\vspace{-0.2cm}
\begin{block}{}
It gives us the traditional definition for simulation on Kripke frames.
\end{block} \end{block}
\vspace{-0.3cm}
\begin{block}{R-Bisimilarity}
$\relar$-bisimilarity is the greatest $\relar$-bisimulation.
\end{block}
\end{columns} \end{columns}
\end{frame} \end{frame}
\begin{frame}{Some Examples of Relators} \begin{frame}{Symmetric Relators}
\footnotesize % \footnotesize
\begin{columns}[T,onlytextwidth]
% \begin{columns}[T,onlytextwidth]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth} % \column{.47\textwidth}
\begin{alertblock}{Example: Trivial Relator} \begin{block}{$R$-bisimulation ($R$-bisimularity)}
For an arbitrary set endofunctor $F$, the relator $\mathbf{Q}$ takes every relation $r:X\rto Y$ to $FX\times FY$. An $\relar$-simulation (similarity) is a bisimulation (bisimilarity), if $\relar$ is \emph{symmetric}.
\end{alertblock}
It is a symmetric relator.
\begin{block}{}
But it is a bad relator because every relation is a $\mathbf{Q}$-bisimulation!
\end{block} \end{block}
\begin{alertblock}{Example: Egli-Milner Relator} \begin{alertblock}{Symmetrization of a Relator}
The relator $\emre$ is a $\powf$-relator defined as: Symmetrization of a relator $\relar$ is defined as:
\begin{gather*} \begin{gather*}
\emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\} \hat{\relar}=\relar r\cap (\relar r^{-1})^{-1}
\end{gather*} \end{gather*}
\end{alertblock} \end{alertblock}
\begin{block}{Symmetric Relators}
A relator $\relar$ is symmetric if $\relar=\hat{\relar}$
\end{block}\vspace{-0.5cm}
Egli-Milner is not symmetric.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \column{.47\textwidth}
% \end{columns}
\end{frame}
\begin{frame}{Barr Relators}
% \footnotesize
% \begin{columns}[T,onlytextwidth]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \column{.47\textwidth}
% \begin{alertblock}{Example: Trivial Relator}
% For an arbitrary set endofunctor $F$, the relator $\mathbf{Q}$ takes every relation $r:X\rto Y$ to $FX\times FY$.
% \end{alertblock}
% It is a symmetric relator.
% \begin{block}{}
% But it is a bad relator because every relation is a $\mathbf{Q}$-bisimulation!
% \end{block}
% \begin{alertblock}{Example: Egli-Milner Relator}
% The relator $\emre$ is a $\powf$-relator defined as:
% \begin{gather*}
% \emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}
% \end{gather*}
% \end{alertblock}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth} % \column{.47\textwidth}
We give a family of examples:
\begin{alertblock}{Example: Barr Relators} \begin{alertblock}{Example: Barr Relators}
Given a set endofunctor $F$, and $r$ is a relation that $r=\pi_2\comp\pi_1^{-1}$ ($\pi_1$ and $\pi_2$ are functions) the Barr relator $\bar{F}$ is defined as Given a set endofunctor $F$, and $r$ is a relation that $r=\pi_2\comp\pi_1^{-1}$ ($\pi_1$ and $\pi_2$ are functions) the Barr relator $\bar{F}$ is defined as
$\bar{F}r=\bar{F}\pi_2\comp(\bar{F}\pi_1)^{-1}$. $\bar{F}r=\bar{F}\pi_2\comp(\bar{F}\pi_1)^{-1}$.
@@ -538,10 +577,13 @@
\begin{gather*} \begin{gather*}
\hat{\emre}=\bar{\powf} \hat{\emre}=\bar{\powf}
\end{gather*} \end{gather*}
\end{block}\vspace{-0.5cm}
Barr relators are nicely behaved relators.
% A trivial relator is a not a Barr relator.
\begin{block}{}
So, we always have bisimulations with Barr relators.
\end{block} \end{block}
Barr relators are nicely behaved relators.\\ %\end{columns}
A trivial relator is a not a Barr relator.
\end{columns}
\end{frame} \end{frame}
\begin{frame}{Lax Barr relators} \begin{frame}{Lax Barr relators}
@@ -571,34 +613,55 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth} \column{.47\textwidth}
\begin{block}{} \begin{block}{}
There are multiple of them:
\begin{itemize} \begin{itemize}
\item Left-lax: $\appr\comp\bar{F}r$ \item Left-lax: $\appr\comp\bar{F}r$
\item Right-lax: $\bar{F}\comp\appr$ \item Right-lax: $\bar{F}\comp\appr$
\item Bi-lax: $\appr\comp\bar{F}r\comp\appr$ \item Bi-lax: $\appr\comp\bar{F}r\comp\appr$
\item Mid-lax: $F\pi_1\comp\appr\comp(F\pi_2)^{-1}$ \item Mid-lax: $F\pi_1\comp\appr\comp(F\pi_2)^{-1}$
\end{itemize} \end{itemize}
\end{block} \end{block}\vspace{-0.2cm}
\begin{alertblock}{Liftability} \begin{alertblock}{Liftability}
An ordering on a set endofunctor $F$ is called \emph{liftable}, if\vspace{-0.3cm} An ordering on a set endofunctor $F$ is called \emph{liftable}, if\vspace{-0.3cm}
\begin{gather*} \begin{gather*}
\alpha\appr\beta\Rightarrow\alpha\comp f\appr \beta\comp f,\\
\alpha\appr\beta\Rightarrow Ff'\comp\alpha\appr Ff'\comp \beta,\\
h\appr Fg\comp k\Rightarrow \exists k', h=Fg\comp k\;\&\;k'\appr k. h\appr Fg\comp k\Rightarrow \exists k', h=Fg\comp k\;\&\;k'\appr k.
\end{gather*} \end{gather*}
\end{alertblock} \end{alertblock}\vspace{-0.2cm}
An ordering and liftablity can be defined for an arbitrary category as well.
\end{columns} \end{columns}
\end{frame} \end{frame}
\begin{frame}{Lax Barr relators (2)} \begin{frame}{Symmetrization of Lax Barr relators}
\footnotesize
Having liftability allows us for an arbitrary function $g$ to have:\vspace{-0.2cm}
\begin{equation*}
\begin{tikzcd}[ampersand replacement=\&]
FX \& FX \\
FY \& FY
\arrow["{\appr_X}"{inner sep=.8ex}, "\shortmid"{marking}, tail, from=1-1, to=1-2]
\arrow["Fg"', from=1-1, to=2-1]
\arrow["Fg", from=1-2, to=2-2]
\arrow["{\appr_Y}"'{inner sep=.8ex}, "\shortmid"{marking}, tail, from=2-1, to=2-2]
\end{tikzcd}
\end{equation*}\vspace{-0.3cm}
% \begin{gather*}
% Fg\comp\appr=\appr\comp Fg\\
% (Fg)^{-1}\comp\sappr=\sappr\comp(Fg)^{-1}
% \end{gather*}
\begin{alertblock}{Proposition} \begin{alertblock}{Proposition}
Given a set endofunctor $F$, with a liftable ordering Given a set endofunctor $F$, with a liftable ordering
\begin{itemize} \begin{enumerate}
\item mid-lax and left-lax relators of $F$ are equal, \item mid-lax and left-lax relators of $F$ are equal,
\item Assuming the axiom of choice, righ-lax and left-lax relators of $F$ are equal, \item Assuming the axiom of choice, righ-lax and left-lax relators of $F$ are equal,
\item the symmetrizaion of the left-lax relator is \emph{sound} and \emph{complete} with respect to \emph{behavioural equivalence}. \item the symmetrizaion of the left-lax relator is \emph{sound} and \emph{complete} with respect to \emph{behavioural equivalence}.
\end{itemize} \end{enumerate}
\end{alertblock} \end{alertblock}
\vspace{-0.1cm}
\begin{block}{}
\begin{itemize}
\item Although, not every sound and complete relator is a Barr relator.\\
\item We do not know when the symmetrizaion of a Barr relator is a Barr relator.
\end{itemize}
\end{block}
\end{frame} \end{frame}
\begin{frame}{Span-based definitions} \begin{frame}{Span-based definitions}
@@ -630,9 +693,8 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth} \column{.47\textwidth}
\vspace{0.1cm} \vspace{-0.2cm}
Assuming the axiom of choice, every HJ-bisimulation is an AM-bisimulation. \begin{alertblock}{AM-Simulation}
\begin{block}{}
We have \emph{AM-simulation}, if we lax the diagram:\vspace{-0.4cm} We have \emph{AM-simulation}, if we lax the diagram:\vspace{-0.4cm}
\begin{equation*} \begin{equation*}
\begin{tikzcd}[ampersand replacement=\&] \begin{tikzcd}[ampersand replacement=\&]
@@ -649,14 +711,37 @@
\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{block}\vspace{-0.3cm} \end{alertblock}\vspace{-0.2cm}
We have found a symmetric AM-simulation that is not a bisimulation! \begin{block}{}
\begin{alertblock}{Proposition} \begin{itemize}
Given a symmetric span $(R,X)$, with the symmetry evidence $s:R\to R$, assuming $R$ is an AM-simulation on a coalgebra $(X,\alpha)$ with evidence $\sigma$, then $R$ is an AM-bisimulation iff $s$ is a coalgebra endomorphism on $(R,\sigma)$. \item Every AM-(bi)simulation is an HJ-(bi)simulation.
\end{alertblock} \item Assuming AoC every HJ-bisimulation is an AM-bisimulation.
\item Every HJ-bisimulation for a functor of form $\powf F$ in a topos is an AM-bisimulation.
\end{itemize}
\end{block}
\end{columns} \end{columns}
\end{frame} \end{frame}
\begin{frame}{Symmetric Simulation for Span-based Definitions}
\footnotesize
So far we have:
\begin{block}{}
\begin{itemize}
\item An example of an AM(HJ)-simulation that is not an AM(HJ)-bisimulation.
\item An example of an AM(HJ)-simulation that the witness for AM(HJ)-simulation does not serve as a witness for AM(HJ)-bisimulation for a $\powf$-coalgebra in $\Set$.
\end{itemize}
\end{block}
\begin{alertblock}{Proposition}
Given a symmetric span $(R,X)$, with the symmetry witness $s:R\to R$, assuming $R$ is an HJ-simulation on a coalgebra $(X,\alpha)$ with witness $\sigma$, then $R$ is an AM-bisimulation iff $s$ is a coalgebra endomorphism on $(R,\sigma)$.
\end{alertblock}
\begin{block}{}
\begin{itemize}
\item We have a proof that symmetric AM-simulations for coalgebras of $\powf$ and the maybe fucntor on $\Set$ are AM-bisimulation.
\item We want to know when exactly this proposition holds (perhaps liftability matters).
\end{itemize}
\end{block}
\end{frame}
\bibliographystyle{apalike} \bibliographystyle{apalike}
\bibliography{references} \bibliography{references}
\addtocounter{framenumber}{-1} \addtocounter{framenumber}{-1}