From 4f9fc5a687b67354470e1c887038f819ddfb9ddc Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 24 Jul 2026 16:42:07 +0100 Subject: [PATCH] more! --- ACV 2026/slides.tex | 219 ++++++++++++++++++++++++++++++-------------- 1 file changed, 152 insertions(+), 67 deletions(-) diff --git a/ACV 2026/slides.tex b/ACV 2026/slides.tex index 158db8b..3057f6c 100644 --- a/ACV 2026/slides.tex +++ b/ACV 2026/slides.tex @@ -312,9 +312,9 @@ \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=\&] x \& y \\ @@ -363,7 +363,7 @@ xRy, \] 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} % \[ % x\sim y @@ -450,14 +450,14 @@ \end{gather*} \end{alertblock}\vspace{-0.5cm} -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.\\ -The closure preserves symmetry, and symmetric simulation is a bisimulation in traditional definitions.\\ -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. \end{frame} -\begin{frame}{Relators, Simulations and Bisimulations} +\begin{frame}{Relators and Simulations} \footnotesize @@ -465,7 +465,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \column{.47\textwidth} - + To define coalgebraic simulation, relators are invented. \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$. \end{alertblock} @@ -473,62 +473,101 @@ \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}$. \end{block} - \vspace{-0.3cm} - - \begin{alertblock}{Symmetrization of a Relator} - Symmetrization of a relator $\relar$ is defined as: - \begin{gather*} - \hat{\relar}=\relar r\cap (\relar r^{-1})^{-1} - \end{gather*} - \end{alertblock} - - +% \vspace{-0.3cm} +% +% \begin{alertblock}{Symmetrization of a Relator} +% Symmetrization of a relator $\relar$ is defined as: +% \begin{gather*} +% \hat{\relar}=\relar r\cap (\relar r^{-1})^{-1} +% \end{gather*} +% \end{alertblock} +\begin{block}{R-Similarity} + $\relar$-similarity is the greatest $\relar$-simulation. +\end{block} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \column{.47\textwidth} - \begin{alertblock}{Symmetric Relator} - A relator $\relar$ is symmetric if $\relar=\hat{\relar}$ - \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. + \begin{alertblock}{Example: Trivial Relator} + For an arbitrary set endofunctor $F$, the relator $\mathbf{K}$ takes every relation $r:X\rto Y$ to $FX\times FY$. + \end{alertblock}\vspace{-0.2cm} +% \begin{alertblock}{Symmetric Relator} +% A relator $\relar$ is symmetric if $\relar=\hat{\relar}$ +% \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} - \vspace{-0.2cm} - \begin{block}{R-Similarity} - $\relar$-similarity is the greatest $\relar$-simulation. + \begin{alertblock}{Example: Egli-Milner Relator} + The relator $\emre$ is a $\powf$-relator defined as:\vspace{-0.2cm} + \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} - \vspace{-0.3cm} - \begin{block}{R-Bisimilarity} - $\relar$-bisimilarity is the greatest $\relar$-bisimulation. - \end{block} - \end{columns} \end{frame} -\begin{frame}{Some Examples of Relators} - \footnotesize - \begin{columns}[T,onlytextwidth] +\begin{frame}{Symmetric 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! +% \column{.47\textwidth} + \begin{block}{$R$-bisimulation ($R$-bisimularity)} + An $\relar$-simulation (similarity) is a bisimulation (bisimilarity), if $\relar$ is \emph{symmetric}. \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} + \begin{alertblock}{Symmetrization of a Relator} + Symmetrization of a relator $\relar$ is defined as: + \begin{gather*} + \hat{\relar}=\relar r\cap (\relar r^{-1})^{-1} + \end{gather*} + \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} - We give a family of examples: +% \column{.47\textwidth} \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 $\bar{F}r=\bar{F}\pi_2\comp(\bar{F}\pi_1)^{-1}$. @@ -538,10 +577,13 @@ \begin{gather*} \hat{\emre}=\bar{\powf} \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} - Barr relators are nicely behaved relators.\\ - A trivial relator is a not a Barr relator. -\end{columns} +%\end{columns} \end{frame} \begin{frame}{Lax Barr relators} @@ -571,34 +613,55 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \column{.47\textwidth} \begin{block}{} - There are multiple of them: \begin{itemize} \item Left-lax: $\appr\comp\bar{F}r$ \item Right-lax: $\bar{F}\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}$ \end{itemize} - \end{block} + \end{block}\vspace{-0.2cm} \begin{alertblock}{Liftability} An ordering on a set endofunctor $F$ is called \emph{liftable}, if\vspace{-0.3cm} \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. \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{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} 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 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}. - \end{itemize} + \end{enumerate} \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} \begin{frame}{Span-based definitions} @@ -630,9 +693,8 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \column{.47\textwidth} - \vspace{0.1cm} - Assuming the axiom of choice, every HJ-bisimulation is an AM-bisimulation. - \begin{block}{} + \vspace{-0.2cm} + \begin{alertblock}{AM-Simulation} We have \emph{AM-simulation}, if we lax the diagram:\vspace{-0.4cm} \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] @@ -649,14 +711,37 @@ \arrow["{{Fp_2}}"', from=2-2, to=2-3] \end{tikzcd} \end{equation*} - \end{block}\vspace{-0.3cm} - We have found a symmetric AM-simulation that is not a bisimulation! - \begin{alertblock}{Proposition} - 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)$. - \end{alertblock} + \end{alertblock}\vspace{-0.2cm} + \begin{block}{} + \begin{itemize} + \item Every AM-(bi)simulation is an HJ-(bi)simulation. + \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{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} \bibliography{references} \addtocounter{framenumber}{-1}