diff --git a/ACV-abstract-2026/references.bib b/ACV-abstract-2026/references.bib index 97f5375..4dd8acb 100644 --- a/ACV-abstract-2026/references.bib +++ b/ACV-abstract-2026/references.bib @@ -6242,7 +6242,7 @@ } @article{Dubut25, - title={Aczel-mendler bisimulations in a regular category}, + title={{Aczel-Mendler} bisimulations in a regular category}, author={Dubut, J{\'e}r{\'e}my}, journal={Logical Methods in Computer Science}, volume={21}, @@ -6250,3 +6250,28 @@ publisher={Episciences. org} } +@Article{HJ04, + author = {Hughes, Jesse and Jacobs, Bart}, + title = {Simulations in coalgebra}, + journal = {Theoretical Computer Science}, + year = 2004, + volume = 327, + number = 1, + pages = {71--108}, + month = oct, + abstract = {A new approach to simulations is proposed within the theory of coalgebras by taking a notion of order on a functor as primitive. Such an order forms a basic building block for a + “lax relation lifting”, or “relator” as used by other authors. Simulations appear as coalgebras of this lifted functor, and similarity as greatest simulation. Two-way similarity is then simi +larity in both directions. In general, it is different from bisimilarity (in the usual coalgebraic sense), but a sufficient condition is formulated (and illustrated) to ensure that bisimilari +ty and two-way similarity coincide. Also, suitable conditions are identified which ensures that similarity on a final coalgebra forms an (algebraic) dcpo structure. This involves a close inve +stigation of the iterated applications Fn(∅) and Fn(1) of a functor F with an order to the initial algebras and final objects.}, + doi = {10.1016/j.tcs.2004.07.022}, + file = {Full Text PDF:HJ04_Simulations_in_coalgebra.pdf:PDF}, + issn = {0304-3975}, + keywords = {Coalgebra, Relation lifting, Simulation}, + series = {Selected {Papers} of {CMCS} '03}, + url = {http://www.sciencedirect.com/science/article/pii/S030439750400444X}, + urldate = {2017-11-13}, +} + + + diff --git a/ACV-abstract-2026/sym-sim.tex b/ACV-abstract-2026/sym-sim.tex index 5e62246..ef13055 100644 --- a/ACV-abstract-2026/sym-sim.tex +++ b/ACV-abstract-2026/sym-sim.tex @@ -70,7 +70,8 @@ \renewcommand{\comp}{\cdot} \newcommand{\klstar}{\sharp} %% Kleisli star -\newcommand{\relar}{\mathbf{R}} +\newcommand{\relar}{\wave F} +\newcommand{\sappr}{\sqsupseteq} \title{Coalgebraic Notions of Simulation, Bisimulation and Relators} %TODO Please add %Or: It is expected from a symmetric simulation to be a bisimulation @@ -155,7 +156,7 @@ %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. +%For an endofunctor $F$ over a category $\BC$, a coalgebra, is a pair $(X, c)$, where $X$ is an object of $\BC$ and $ c\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*} @@ -181,27 +182,32 @@ Notions of simulation and bisimulation play a central role in the theory of tran systems and in program semantics. Bisimulation is a certain canonical notion of program (or system) equivalence, which can be formulated in different equivalent ways in base cases, while these ways need not remain equivalent under further generalizations. -This is acknowledged and investigated in the literature (see e.g.\ \cite{Staton11}). +This is acknowledged and investigated in the literature (see e.g.~\cite{Staton11}). Contrastingly, \emph{simulation} is a non-canonical notion of program in-equivalence -(or approximation), subject to the same issue, but much less explored in this case. +(or approximation), subject to the same issue, but much less explored. + +\section{Simulation, Bisimulation, Relators} + + Consider the following baseline example. % -\begin{example}[Kripke Frame, Simulation, Bisimulation] A Kripke frame consists -of a set $W$ and a function $c\c W\to\PSet W$ (equivalently: relation $r\subseteq W\times W$). +\begin{example}[Kripke Frame, Simulation, Bisimulation]\label{exa:pset} A Kripke frame consists +of a set $X$ and a function $c\c X\to\PSet X$ (equivalently: relation $R\subseteq X\times X$). -Simulation on $(W, C)$ is such a relation $r\subseteq W\times W$ that $(x,y)\in r$ -entails: for all $x'\in c(x)$ there is $y'\in c(y)$, such that $(x',y')\in r$. -Such a relation is a bisimulation if additionally $(x,y)\in r$ -entails: for all $y'\in c(y)$ there is $x'\in c(x)$, such that $(x',y')\in r$. +Simulation on $(X, c)$ is such a relation $R\subseteq X\times X$ that $(x,y)\in R$ +entails: for all $x'\in c(x)$ there is $y'\in c(y)$, such that $(x',y')\in R$. +Such a relation is a bisimulation if additionally $(x,y)\in R$ +entails: for all $y'\in c(y)$ there is $x'\in c(x)$, such that $(x',y')\in R$. -Thus, $r$ is a bisimulation iff both $r$ and its inverse $r^\circ$ are simulations. +Thus, $R$ is a bisimulation iff both $R$ and its inverse $R^\op$ are simulations. \end{example} % -These setting can be varied at least in two ways: +These settings can be varied at least in two ways: % \begin{itemize} \item The powerset functor $\PSet$ can be replaced by another endofunctor $F\c\Set\to\Set$ - (to model systems with input, output, probability, nontermination, etc.) + (to model systems with input, output, probability, nontermination, etc.) Kripke frames + $(X,c\c X\to\PSet X)$ are thus replaced by arbitrary \emph{coalgebras} $(X,c\c X\to FX)$. \item A different underlying category $\BC$ can be used in place of $\Set$ (e.g.\ nominal sets, to model systems with name management). \end{itemize} @@ -210,69 +216,177 @@ A convenient way to work with simulations and bisimulations is via the notion of \emph{relator}. \begin{definition}[Relators, Simulation, Bisimulation] -Given a set functor $F\c\Set\to\Set$, an \emph{$F$-relator} is a monotone map $\relar$ -sending a relation $r\subseteq X\times Y$ to a relation $\relar r\subseteq FX\times FY$. -A relator $\relar$ is \emph{symmetric} if $\relar(r^\op)=(\relar r)^\op$, and -\emph{normal} if $\relar 1_X=1_{FX}$. +Given a functor $F\c\Set\to\Set$, an \emph{$F$-relator} is a monotone map $\relar$ +sending a relation $R\subseteq X\times Y$ to a relation $\relar R\subseteq FX\times FY$. +A relator $\relar$ is \emph{symmetric} if $\relar(R^\op)=(\relar R)^\op$. +%, and +%\emph{normal} if $\relar 1_X=1_{FX}$. -A relation $r\subseteq X\times Y$ is an \emph{$\relar$-simulation} from an -$F$-coalgebra $(X,\alpha)$ to $(Y,\beta)$ if +A relation $R\subseteq X\times Y$ is an \emph{$\relar$-simulation} from an +$F$-coalgebra $(X, c)$ to $(Y, d)$ if \[ - r \;\subseteq\; \beta^\op\comp\relar r\comp\alpha, + R \;\subseteq\; d^\op\comp\relar R\comp c, \] -i.e.\ $x\mathrel{r}y$ implies $\alpha(x)\mathrel{\relar r}\beta(y)$. -The greatest $\relar$-simulation from $(X,\alpha)$ to $(Y,\beta)$ (which exists by -Knaster-Tarski) is \emph{$\relar$-similarity}. When $\relar$ is symmetric, -$\relar$-simulations are called \emph{$\relar$-bisimulations} and $\relar$-similarity +i.e.\ $x\mathrel{R}y$ implies $ c(x)\mathrel{\relar R} d(y)$. +%The greatest $\relar$-simulation from $(X, c)$ to $(Y, d)$ (which exists by +%Knaster-Tarski) is \emph{$\relar$-similarity}. +When $\relar$ is symmetric, $\relar$-simulations are called \emph{$\relar$-bisimulations} and $\relar$-similarity is called \emph{$\relar$-bisimilarity}. \end{definition} +% +The canonical relator (usually) capturing bisimulation (like in \autoref{exa:pset}) +is the Barr relator:\par +% +\begin{definition}[Barr Relator] +The \emph{Barr relator} $\bar{F}$ of $F$ sends a relation $R\subseteq X\times Y$, +viewed as a span via projections $\pi_1\c R\to X$, $\pi_2\c R\to Y$, to +\[ + \bar{F} R = F\pi_2\comp(F\pi_1)^\op \;\subseteq\; FX\times FY. +\] +\end{definition} +% +We ask: +% +\begin{enumerate} + \item How to construct relators for established notions of simulation? + \item How to generally prove that ensuing symmetric simulations are bisimulations? + \item How alternative notions of simulations align with the relator-based one? +\end{enumerate} -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: +\section{Relaxing Barr Relators}%\label{sec:} + +Fixing a functor $F\c\Set\to\Set$, and assuming that every $FX$ is naturally ordered, +we consider four ways of relaxing Barr relators, to model simulation: +% +\begin{enumerate} + \item\label{it:ll-barr} left-lax Barr relator $\appr\comp\bar{F}$ + \item\label{it:rl-barr} right-lax Barr relator $\bar{F}\comp\appr$ + \item\label{it:bl-barr} bi-lax Barr relator $\appr\comp\bar{F}\comp\appr$ + \item\label{it:ml-barr} mid-lax Barr relator $R\mapsto F\pi_2\comp\sappr\comp(F\pi_1)^\op$, by + viewing $R$ as a span via projections $\pi_1\c R\to X$, $\pi_2\c R\to Y$. +\end{enumerate} +% +Bi-lax Barr relators are used by Hughes and Jacobs in their definition of coalgebraic +simulation~\cite{HJ04}, and right-lax Barr relator figures in the construction of +abstract Howe's closure, for proving congruence of applicative bisimilarity +in higher-oder mathematical semantics~\cite{UrbatTsampasEtAl23}. +% +\begin{example} +For $F=\PSet$, let $\appr$ be the subset inclusion relation. Then, all relators +\textsf{\bfseries\ref{it:ll-barr}}--\textsf{\bfseries\ref{it:ml-barr}} coincide and yield $\relar R = \{(U,V)\in\PSet X\times\PSet Y\mid \forall x\in U.\,\exists y\in V.\, (x,y)\in R\}$. +\end{example} +% +For any relator $\relar$, we can consider its \emph{symmetrization} $\relar^\leftrightarrow$, +which is a relator sending $R$ to $\relar R\cap (\relar R^\op)^\op$. For $F=\PSet$, +the symmetrization of any lax relator is the Barr relator. It is not clear though, +when this is true in general. The following is easy to verify: +% +\begin{proposition} +If $\relar^\leftrightarrow\subseteq\bar F$ then any symmetric $\relar$-simulation +$R\subseteq X\times X$ is a $\bar F$\dash bisimulation. +\end{proposition} +% +The conclusion of this proposition is a desirable property of simulation, however +the premise ($\relar^\leftrightarrow\subseteq\bar F$) need not be true in general +(a trivial counterexample is $\relar R = FX\times FY$ for every $R\subseteq X\times Y$). + +%It is easy to +%prove that +%% +%\begin{proposition} +%The Barr relator is the symmetrization of both the left-lax and the right-lax Barr +%relator, where the symmetrization of a relator $\relar$ sends $R$ to +%$\relar(R)\cap (\relar(R^\op))^\op$. +%\end{proposition} + + +\section{Aczel-Mendler Simulation vs.\ Hermida-Jacobs Simulation}%\label{sec:} + +\emph{Hermida-Jacobs bisimulation} is the $\bar{F}$-simulation \cite{HermidaJacobs98}, +which is indeed a bisimulation, as $\bar{F}$ is a symmetric relator. It is thus appropriate +to regard $\bar{F}$-simulation as a generalization of Hermida and Jacobs' notion +to arbitrary relators. + +In $\Set$, with the axiom of choice, Hermida-Jacobs bisimulation coincides with +the \emph{Aczel-Mendler bisimulation}~\cite{Staton11}, i.e.\ such a relation $R\subseteq X\times Y$ that +the diagram +% +\begin{equation}\label{eq:diag-sim} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& Y \\ + FX \& FR \& FY + \arrow[" c"', from=1-1, to=2-1] + \arrow["{p_1}"', from=1-2, to=1-1] + \arrow["{p_2}", from=1-2, to=1-3] + \arrow["\sigma", dashed,from=1-2, to=2-2] + \arrow["d", from=1-3, to=2-3] + \arrow["{{Fp_1}}", from=2-2, to=2-1] + \arrow["{{Fp_2}}"', from=2-2, to=2-3] + \end{tikzcd} +\end{equation} +% +commutes for some $\sigma$, where $(X,c)$ and $(Y,d)$ are given coalgebras. The +fact that $R$ is an $\bar F$-simulation thus comes with a \emph{wittness} $\sigma\c R\to FR$. + +\emph{Aczel-Mendler simulation}~\cite{Dubut25} adapts Aczel-Mendler bisimulation +by replacing the strictly commuting diagram~\eqref{eq:diag-sim} with a laxly +commuting one: +% \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] + X \& R \& X \\ + FX \& FR \& FX + \arrow[" c"', 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[" c", 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}. +% +(\textsf{\bfseries\ref{it:ll-barr}}--\textsf{\bfseries\ref{it:rl-barr}} give rise to +further variants, obtained in the obvious way). -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: +Curiously, if we switch to this notion of simulation, it is no longer granted +that symmetric simulation is a bisimulation even for $F=\PSet$. +% +\begin{example} +Take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$, and $ c(x)=X$ for every $x\in X$, and $\sigma$ is defined as below: \begin{gather*} \sigma(w)= \begin{cases} - r & w\neq (1,3) \\ - r\setminus\{(1,2)\} & w=(1,3) + R & w\neq (1,3) \\ + R\setminus\{(1,2)\} & w=(1,3) \end{cases} \end{gather*} -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\}$. +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 $ c(p_1(w))\subseteq\mathcal{P}p_1(\sigma(w))=X$. Also, for every $w\in R$, $\mathcal{P}p_2(\sigma(w))\subseteq c(p_2(w))=X$. But it is not a bisimulation, since $ c(p_2(1,3))= c(3)=X\neq\mathcal{P}p_2(\sigma(1,3))=X\setminus\{2\}$. +\end{example} -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. +%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, c)$, 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 $ c(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 c(p_2(w))=X$. But it is not a bisimulation, since $ c(p_2(1,3))= c(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^\op\comp\relar r\comp\alpha$. 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. + + +%\todo{Rewrite.} + +%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 inverse 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, c)$ to a coalgebra $(Y, d)$ iff $R\subseteq d^\op\comp\relar R\comp c$. 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, c)$ to a coalgebra $(Y, d)$ is included in the behavioural equivalence from $(X, c)$ to $(Y, d)$, and we call it complete iff the behavioural equivalence is included in the $\relar$-similarity. \bibliography{references}