diff --git a/ACV-abstract-2026/references.bib b/ACV-abstract-2026/references.bib index 3cdd10d..8f8d93c 100644 --- a/ACV-abstract-2026/references.bib +++ b/ACV-abstract-2026/references.bib @@ -6232,3 +6232,13 @@ doi = {10.4230/LIPIcs.ITP.2019.30}, timestamp = {Sat, 05 Sep 2020 18:04:33 +0200} } + +@article{Dubut25, + title={Aczel-mendler bisimulations in a regular category}, + author={Dubut, J{\'e}r{\'e}my}, + journal={Logical Methods in Computer Science}, + volume={21}, + year={2025}, + publisher={Episciences. org} +} + diff --git a/ACV-abstract-2026/sym-sim.pdf b/ACV-abstract-2026/sym-sim.pdf index 5616ea5..cae3d3f 100644 Binary files a/ACV-abstract-2026/sym-sim.pdf and b/ACV-abstract-2026/sym-sim.pdf differ diff --git a/ACV-abstract-2026/sym-sim.tex b/ACV-abstract-2026/sym-sim.tex index ffe07c9..0679ee7 100644 --- a/ACV-abstract-2026/sym-sim.tex +++ b/ACV-abstract-2026/sym-sim.tex @@ -13,7 +13,18 @@ \usepackage{mdframed, ebproof} \usepackage{microtype} \usepackage{stackengine} +\usepackage{tikz-cd} +\usetikzlibrary{arrows.meta} +\usetikzlibrary{decorations} % Required for all decorations +\usetikzlibrary{decorations.pathmorphing} % Specifically for 'zigzag' +\tikzset{ + commutative diagrams/.cd, + arrow style = tikz, + diagrams = {>=stealth}, + row sep = large, + column sep = huge +} \input{catprog} \renewcommand{\by}[1]{\text{/$\mspace{-2mu}$/~#1}} @@ -59,6 +70,7 @@ \renewcommand{\comp}{\cdot} \newcommand{\klstar}{\sharp} %% Kleisli star +\newcommand{\relar}{\mathbf{R}} \title{Soundness and Completeness of Symmetric Relators} %TODO Please add %Or: It is expected from a symmetric simulation to be a bisimulation @@ -136,37 +148,82 @@ %\section{Mathematical Preliminaries}%\label{sec:} -\paragraph{Compositionality} -Given a labeled transition systems $(S,L,\to)$, where $S$ is a set of states, $L$ is a set of labels, and $\to\subseteq S\times L\times S$ is a set of labeled transitions, a \emph{simulation} is a relation $r\subseteq S\times S$ such that the following sentence holds: -\begin{gather*} - (x,y)\in r, x\xto{l} x' \Rightarrow \exists y', y\xto{l} y' \;\text{ and } (x',y')\in r -\end{gather*} -The greatest simulation relation over $S$ is called \emph{similarity} and shown with $\leq$. A simulation relation $r$ on $S$ is a \emph{bisimulation} iff the following sentence holds: -\begin{gather*} - (x,y)\in r, y\xto{l} y' \Rightarrow \exists x', x\xto{l} x' \;\text{ and } (x',y')\in r -\end{gather*} -The greatest bisimulation relation over $S$ is called \emph{bisimilarity} and shown with $\sim$. This is the traditional definition of bisimilarity. There are many different notions. For this definition, we can say that the symmetric similarity is the bisimilarity. But it is not always true for different notions. +%\paragraph{Compositionality} +%Given a labeled transition systems $(S,L,\to)$, where $S$ is a set of states, $L$ is a set of labels, and $\to\subseteq S\times L\times S$ is a set of labeled transitions, a \emph{simulation} is a relation $r\subseteq S\times S$ such that the following sentence holds: +%\begin{gather*} +% (x,y)\in r, x\xto{l} x' \Rightarrow \exists y', y\xto{l} y' \;\text{ and } (x',y')\in r +%\end{gather*} +%The greatest simulation relation over $S$ is called \emph{similarity} and shown with $\leq$. A simulation relation $r$ on $S$ is a \emph{bisimulation} iff the following sentence holds: +%\begin{gather*} +% (x,y)\in r, y\xto{l} y' \Rightarrow \exists x', x\xto{l} x' \;\text{ and } (x',y')\in r +%\end{gather*} +%The greatest bisimulation relation over $S$ is called \emph{bisimilarity} and shown with $\sim$. This is the traditional definition of bisimilarity. There are many different notions. For this definition, we can say that the symmetric similarity is the bisimilarity. But it is not always true for different notions. +% +%\paragraph{Coalgebraic Bisimulation} +%For an endofunctor $F$ over a category $\BC$, a coalgebra, is a pair $(X,\alpha)$, where $X$ is an object of $\BC$ and $\alpha\c X\to FX$ is a morphism in $\BC$. Coalgebras serve as an abstraction of variant transition systems. For example, a labeled transition system $(S,L,\to)$ is a coalgebra $(S,\gamma)$, where $\gamma\c S\to\mathcal{P}(L\times S)$ and $\mathcal{P}$ is the powerset functor. +% +%$S$ can be the set of the terms of a programming language given by a signature $\Sigma$, and $\to$ can be the set of labeled inductions of the language, given by an operational semantics. Following that, a context $C$ is defined as: +%\begin{gather*} +% C\Coloneqq\Box\mid f(C,\bar{t})\mid f(\bar{t},C)\mid f(\bar{u},C,\bar{s}) +%\end{gather*} +%$f\in\Sigma$ and by $\bar{t}$, $\bar{s}$ and $\bar{u}$ we mean vectors of terms in $S$. $\Box$ is a placeholder. Assuming $t\in S$, then $C[t]\in S$. We call a relation $r$ congruence iff for terms $t$ and $s$, and a context $C$, $t\mathrel{r}s$ gives $C[t]\mathrel{r}C[s]$. A language with its operational semantics is compositional iff the bisimilarity relation over the terms of the language is a congruence. +% +%\paragraph{Howe's method} +%Howe's method has been traditionally used for compositionality results. \emph{Howe closure} of a relation $r$ is shown by $\hat{r}$ and is defined with the following inference rule: +%\begin{gather*} +% \infer{f(\bar{t})\mathrel{\hat{r}} s}{\bar{t}\mathrel{\hat{r}} \bar{s} & f(\bar{s})\mathrel{r} s} +%\end{gather*} +%Assuming that $r$ is reflexive, then $r\subseteq\hat{r}$, and $\hat{r}$ is a congruence. Additionally, if $r$ is reflexive and symmetric, then $\hat{r}^\star$, the transitive closure of $\hat{r}$ is symmetric (the transitive closure trick). So, to prove that bisimilarity is a congruence it is sufficient to prove that $\hat{\sim}$ is a bisimulation. Given the non-symmetric nature of the closure, it is more common to prove that $\hat{\sim}$ is a simulation. It is usually expected from a symmetric simulation to be a bisimulation. But it has not always been the case. +% +%\paragraph{Relators} -\paragraph{Coalgebraic Bisimulation} -For an endofunctor $F$ over a category $\BC$, a coalgebra, is a pair $(X,\alpha)$, where $X$ is an object of $\BC$ and $\alpha\c X\to FX$ is a morphism in $\BC$. Coalgebras serve as an abstraction of variant transition systems. For example, a labeled transition system $(S,L,\to)$ is a coalgebra $(S,\gamma)$, where $\gamma\c S\to\mathcal{P}(L\times S)$ and $\mathcal{P}$ is the powerset functor. +%There exist various notions of (bi)simulation in the literature. For some of them, it is expected from a symmetric simulation to be a bisimulation. It is true for the most traditionally known notion. A more advanced example is in Howe's method. Howe's method is used to prove that applicative bisimilarity is a congruence. It is done by applying Howe closure on bisimilarity, and then proving that the given relation is a bisimulation. Howe closure of bisimilarity includes it and preserves its symmetry. More importantly, Howe closure of bisimilarity is a congruence. Given the non-symmetric nature of Howe closure, it is more common to prove that applying Howe closure on the bisimilarity, gives a simulation, and then we have the rest. But getting to bisimulation from having a symmetric simulation is a step that we believe needs to be taken with care, and we discuss here. -$S$ can be the set of the terms of a programming language given by a signature $\Sigma$, and $\to$ can be the set of labeled inductions of the language, given by an operational semantics. Following that, a context $C$ is defined as: +There exist various notions of (bi)simulation in the literature. It is usually expected from a symmetric simulation to be a bisimulation. It is true for the most traditionally known notion, but such conclusion must be made with care. We describe a scenario, in which we have a proof that a symmetric relation is a simulation, but the proof does not serve as a proof for the relation to be a bisimulation. +We take the Aczel-Mendler simulation\cite{Dubut25}. Given a partial order over a functor $F\c\BC\to\BC$, a relation $r$ on $X$ is a simulation on a coalgebra $(X,\alpha)$ iff there exists a coalgebra $(R,\sigma)$ called \emph{witness} that laxly commutes in the following diagram: +\begin{equation}\label{eq:diag-lax-sim} + \begin{tikzcd}[ampersand replacement=\&] + X \& r \& X \\ + FX \& Fr \& FX + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2] + \arrow["{p_1}"', from=1-2, to=1-1] + \arrow["{p_2}", from=1-2, to=1-3] + \arrow["\sigma", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3] + \arrow["{{Fp_1}}", from=2-2, to=2-1] + \arrow["{{Fp_2}}"', from=2-2, to=2-3] + \end{tikzcd} +\end{equation} +If~\eqref{eq:diag-lax-sim} commutes fully, then $\sigma$ is a witness for $r$ to be an \emph{Aczel-Mendler bisimulation}. + +Assuming that $F=\mathcal{P}$ is the powerset functor on $\Set$, we take $r=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$, and $\alpha(x)=X$ for every $x\in X$, and $\sigma$ is defined as below: \begin{gather*} - C\Coloneqq\Box\mid f(C,\bar{t})\mid f(\bar{t},C)\mid f(\bar{u},C,\bar{s}) + \sigma(w)= + \begin{cases} + r & w\neq (1,3) \\ + r\setminus\{(1,2)\} & w=(1,3) + \end{cases} \end{gather*} -$f\in\Sigma$ and by $\bar{t}$, $\bar{s}$ and $\bar{u}$ we mean vectors of terms in $S$. $\Box$ is a placeholder. Assuming $t\in S$, then $C[t]\in S$. We call a relation $r$ congruence iff for terms $t$ and $s$, and a context $C$, $t\mathrel{r}s$ gives $C[t]\mathrel{r}C[s]$. A language with its operational semantics is compositional iff the bisimilarity relation over the terms of the language is a congruence. - -\paragraph{Howe's method} -Howe's method has been traditionally used for compositionality results. \emph{Howe closure} of a relation $r$ is shown by $\hat{r}$ and is defined with the following inference rule: -\begin{gather*} - \infer{f(\bar{t})\mathrel{\hat{r}} s}{\bar{t}\mathrel{\hat{r}} \bar{s} & f(\bar{s})\mathrel{r} s} -\end{gather*} -Assuming that $r$ is reflexive, then $r\subseteq\hat{r}$, and $\hat{r}$ is a congruence. Additionally, if $r$ is reflexive and symmetric, then $\hat{r}^\star$, the transitive closure of $\hat{r}$ is symmetric (the transitive closure trick). So, to prove that bisimilarity is a congruence it is sufficient to prove that $\hat{\sim}$ is a bisimulation. Given the non-symmetric nature of the closure, it is more common to prove that $\hat{\sim}$ is a simulation. It is usually expected from a symmetric simulation to be a bisimulation. But it has not always been the case. - -\paragraph{Relators} - +In this scenario, $\sigma$ is a witness for $r$ to be a simulation, but it is not a witness for $r$ to be a bisimulation, since for every $w\in r$ we have $\alpha(p_1(w))\subseteq\mathcal{P}p_1(\sigma(w))=X$. Also, for every $w\in r$, $\mathcal{P}p_2(\sigma(w))\subseteq\alpha(p_2(w))=X$. But it is not a bisimulation, since $\alpha(p_2(1,3))=\alpha(3)=X\neq\mathcal{P}p_2(\sigma(1,3))=X\setminus\{2\}$. +Inspired by Hermida-Jacobs bisimulation\cite{HermidaJacobs98} we modify the definition by setting $\BC$ to be a regular category, and changing the span $(FR,Fp_1,Fp_2)$ in~\eqref{eq:diag-lax-sim} with the span $((Fr)^\dagger,(Fp_1)^\dagger,(Fp_2)^\dagger)$, where $(Fr)^\dagger$ is the image of $\brks{Fp_1,Fp_2}$, and $\brks{(Fp_1)^\dagger,(Fp_2)^\dagger}\c(FR)^\dagger\to FX\times FX$ is monic, so $(Fr)^\dagger$ is a relation. By the symmetry of $r$ there exists $s\c r\to r$ that we call \emph{swap}, where $p_1\comp s=p_2$ and $p_2\comp s=p_1$. The necessary and sufficient condition for $\sigma$ to be a witness for $r$ to be a bisimulation is that +\begin{gather}\label{eq:nec-suf-sim} + \sigma\comp s=(Fs)^\dagger\comp\sigma +\end{gather} + , i.e., $s$ is a $F$-coalgebra morphism from $\sigma$ to itself. Nevertheless, still we have the following example of the $\sigma\c r\to(Fr)^\dagger$ that is a witness for $r$ to be a simulation over $(X,\alpha)$, but it is not a witness for $r$ to be a bisimulation. Keeping the setting of the previous example, we modify $\sigma$ as follows: + \begin{gather*} + \sigma(w)= + \begin{cases} + (X,X) & w\neq (1,3) \\ + (X,X\setminus\{2\}) & w=(1,3) + \end{cases} + \end{gather*} + $\sigma$ is a witness for $r$ to be a simulation since for every $w\in r$ we have $\alpha(p_1(w))\subseteq((\mathcal{P}p_1)^\dagger(\sigma(w)))=X$. Also, for every $w\in r$, $((\mathcal{P}p_2)^\dagger(\sigma(w)))\subseteq\alpha(p_2(w))=X$. But it is not a bisimulation, since $\alpha(p_2(1,3))=\alpha(3)=X\neq(\mathcal{P}p_2)^\dagger(\sigma(1,3))=X\setminus\{2\}$. +It worth mentioning that $\sigma$ does not satisfy~\eqref{eq:nec-suf-sim}. But still we do not know if having such $\sigma$ can give us a witness that satisfies~\eqref{eq:nec-suf-sim} or guarantees the existence of such witness. +There is a solution for this problem, if we change the context. If we take our category to be $\Set$, we can talk about a kind of well-studied maps named \emph{relator}. For a set functor $F$, a relator $\relar$ takes a relation $r\subseteq X\times Y$ to another relation $\relar r\subseteq FX\times FY$. A relator is monotone with respect to inclusion. For example, in our alternative for Aczel-Mendler simulation, for every set functor $F$, the map that takes a relation $r$ to $(Fr)^\dagger$ is a relator. We show the reverse of a relation $r$ with $r^\op$, and composition of $r$ with another relation $t$ with $t\comp r$. A relation $r\subseteq X\times Y$ is called $\relar$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ iff $r\subseteq \beta\comp\relar r\comp\alpha^\op$. Additionally, a relator is called symmetric iff $\relar (r^\op)=(\relar r)^\op$, and a $\relar$-simulation for a symmetric $\relar$ is called a $\relar$-bisimulation that resembles~\eqref{eq:nec-suf-sim}. $\relar$-similarity and $\relar$-bisimilarity are the greatest $\relar$-simulation and $\relar$-bisimulation, respectively. We call a relator $\relar$ sound iff $\relar$-similarity from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ is included in the behavioural equivalence from $(X,\alpha)$ to $(Y,\beta)$, and we call it complete iff the behavioural equivalence is included in the $\relar$-similarity. \newpage \bibliography{references} diff --git a/ACV-abstract-2026/sym-sim.vtc b/ACV-abstract-2026/sym-sim.vtc index df25928..3722f55 100644 --- a/ACV-abstract-2026/sym-sim.vtc +++ b/ACV-abstract-2026/sym-sim.vtc @@ -1 +1 @@ -\contitem\title{Soundness and Completeness of Symmetric Relators}\author{Sergey Goncharov and Pouya Partow}\page{:1--:2} +\contitem\title{Soundness and Completeness of Symmetric Relators}\author{Sergey Goncharov and Pouya Partow}\page{:1--:3}