\RequirePackage[l2tabu, orthodox]{nag}
\PassOptionsToPackage{final}{graphicx}
\PassOptionsToPackage{nosumlimits,nonamelimits}{amsmath}
\PassOptionsToPackage{colorlinks,linkcolor={blue},citecolor={blue},urlcolor={red},breaklinks=true,final}{hyperref}

\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate, final]{lipics-v2021}
\bibliographystyle{plainurl} % the mandatory bibstyle

\sloppy

\usepackage{proof}
\usepackage{xspace}
\usepackage{mdframed, ebproof}
\usepackage{microtype}
\usepackage{stackengine}
\usepackage{tikz-cd}
\usepackage{subcaption}
\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}}

\renewcommand{\paragraph}[1]{\medskip\noindent{\bfseries\sffamily #1.}}

\usepackage{ifdraft}
\ifdraft{
%  \usepackage{showframe}
  \usepackage{showlabels}
  \renewcommand{\showlabelfont}{\ttfamily\scriptsize}
  \usepackage[layout=footnote,draft]{fixme}

%  \usepackage[notcite,notref]{showkeys}
%  \renewcommand*\showkeyslabelformat[1]{%
%  \raisebox{1ex}{\raggedleft{\textit{\tiny #1}}}
}{
 \usepackage[layout=footnote,final]{fixme}
}

\FXRegisterAuthor{sg}{asg}{SG}  % Sergey
\FXRegisterAuthor{fg}{afg}{FG}  % Florian

\newcommand{\xCL}{\textbf{xCL}\xspace}  

\usepackage{todos}

\renewcommand{\xto}[1]{\mathrel{\raisebox{-.15pt}{$\xrightarrow{\;\smash{\raisebox{-.5pt}{\makebox(3,0)[b]{\scriptsize $#1$}}\;}}$}}}

\newcommand{\val}{\mathsf{v}}
\newcommand{\com}{\mathsf{c}}

\newcommand{\dl}{\chi}

\newcommand{\Fst}{\Pi_1} %{\oname{Fst}} 
\newcommand{\Snd}{\Pi_2} %{\oname{Snd}} 

\newcommand{\Sigmas}{\Sigma^\star}

\newcommand{\mS}{\mu\Sigma}
\newcommand{\mSv}{\mS_\val}
\newcommand{\mSc}{\mS_\com}

\renewcommand{\comp}{\cdot}
\newcommand{\klstar}{\sharp}  			%% Kleisli star
\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
%\titlerunning{From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly}

\author{Pouya Partow}{University of Birmingham, UK}{p.partow@bham.ac.uk}{https://orcid.org/0009-0003-9652-9469}{}
\author{Sergey Goncharov}{University of Birmingham, UK}{s.goncharov@bham.ac.uk}{https://orcid.org/0000-0001-6924-8766}{}

%\authorrunning{J. Open Access and J.\,R. Public} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'

\Copyright{Jane Open Access and Joan R. Public} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/

%\ccsdesc[100]{\textcolor{red}{Replace ccsdesc macro with valid one}} %TODO mandatory: Please choose ACM 2012 classifications from https://dl.acm.org/ccs/ccs_flat.cfm 

%\keywords{Operational semantics, Higher-order GSOS, Extended combinatory logic}

\category{} %optional, e.g. invited paper

\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
%\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional

%\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
%\supplementdetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93, subcategory={Description, Subcategory}, swhid={Software Heritage Identifier}]{General Classification (e.g. Software, Dataset, Model, ...)}{URL to related version} %linktext, cite, and subcategory are optional

%\funding{(Optional) general funding statement \dots}%optional, to capture a funding statement, which applies to all authors. Please enter author specific funding statements as fifth argument of the \author macro.

%\acknowledgements{I want to thank \dots}%optional

\nolinenumbers %uncomment to disable line numbering



%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\EventEditors{John Q. Open and Joan R. Access}
%\EventNoEds{2}
%\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
%\EventShortTitle{CVIT 2016}
%\EventAcronym{CVIT}
%\EventYear{2016}
%\EventDate{December 24--27, 2016}
%\EventLocation{Little Whinging, United Kingdom}
%\EventLogo{}
%\SeriesVolume{42}
%\ArticleNo{23}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\hideLIPIcs

\def\subjclassHeading{}
\makeatletter
\def\@ccsdescString{\erule\vspace{-5ex}}
\def\keywordsHeading{}
\def\@keywords{\relax}
\makeatother


\begin{document}
\allowdisplaybreaks
\let\cedilla\c
\renewcommand{\c}{\colon}

\maketitle




%

%
%\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{Coalgebraic Bisimulation}
%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*}
%	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}

%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.


\bigskip

Simulation and bisimulation play a central role in coalgebra 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}).
Contrastingly, \emph{simulation} is a non-canonical notion of program in-equivalence 
(or approximation), subject to the same issue, but much less explored. 

\paragraph{Simulation, Bisimulation, Relators}
%
Consider the following baseline example. 
%
\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$.
A \emph{simulation} on $(X, c)$ is such $R$ that $(x,y)\in R$ entails: for all $x'\in c(x)$
there is $y'\in c(y)$ with $(x',y')\in R$. A \emph{bisimulation} additionally requires the
symmetric back condition: for all $y'\in c(y)$ there is $x'\in c(x)$ with $(x',y')\in R$.
\end{example}
%
These settings can be varied in at least 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.) 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 --- but we stick to $\BC=\Set$ in the sequel). 
\end{itemize}
%
A convenient framing for simulations and bisimulations is the notion of \emph{relator}. 

\begin{definition}[Relators, Simulation, Bisimulation]
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, c)$ to $(Y, d)$ if
$R \;\subseteq\;  d^\op\comp\relar R\comp c$.
%
%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}

\paragraph{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 the relators 
\textsf{\bfseries\ref{it:ll-barr}}--\textsf{\bfseries\ref{it:ml-barr}} take the form $\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 a symmetric $\relar$-simulation
$R\subseteq X\times X$ is a $\bar F$\dash bisimulation.
\end{proposition}
%
The conclusion here 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}


\paragraph{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.
%
%
\begin{figure}[t]
\begin{subfigure}[t]{0.48\textwidth}
\centering
\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}
\caption{Aczel-Mendler bisimulation}
\label{fig:diag-sim}
\end{subfigure}
\hfill
\begin{subfigure}[t]{0.48\textwidth}
\centering
\begin{tikzcd}[ampersand replacement=\&]
	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", dashed, from=1-2, to=2-2]
	\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}
\caption{Aczel-Mendler simulation}
\label{fig:diag-lax-sim}
\end{subfigure}
\end{figure}
%
In $\Set$, with the axiom of choice, Hermida-Jacobs bisimulation coincides with
the \emph{Aczel-Mendler bisimulation}~\cite{Staton11}: $R\subseteq X\times Y$
for which \autoref{fig:diag-sim} commutes for some witness $\sigma\c R\to FR$.
\emph{Aczel-Mendler simulation}~\cite{Dubut25} replaces \autoref{fig:diag-sim} with
the laxly commuting \autoref{fig:diag-lax-sim}
(\textsf{\bfseries\ref{it:ll-barr}}--\textsf{\bfseries\ref{it:rl-barr}} give rise to further variants).
%
%(\textsf{\bfseries\ref{it:ll-barr}}--\textsf{\bfseries\ref{it:rl-barr}} give rise to 
%further variants, obtained in the obvious way).
%

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)
	\end{cases}
\end{gather*}
Then $\sigma$ is a witnesses of simulation but not a bisimulation: $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, 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.



%\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}


\end{document}

%%% Local Variables:
%%% mode: LaTeX
%%% TeX-master: t
%%% End:
