diff --git a/ACV-abstract-2026/references.bib b/ACV-abstract-2026/references.bib index 8f8d93c..97f5375 100644 --- a/ACV-abstract-2026/references.bib +++ b/ACV-abstract-2026/references.bib @@ -9,6 +9,14 @@ @STRING{lnm = "LNM" } @STRING{springer= "Springer" } +@Article{ Staton11, + author = {Sam Staton}, + title = {Relating coalgebraic notions of bisimulation}, + journal = {Log.\ Methods Comput.\ Sci.}, + year = {2011}, + volume = {7} +} + @Proceedings{ 2015IEEE, title = {2015 {IEEE} Symposium on Security and Privacy, {SP} 2015, San Jose, CA, USA, May 17-21, 2015}, diff --git a/ACV-abstract-2026/sym-sim.tex b/ACV-abstract-2026/sym-sim.tex index 0679ee7..5e62246 100644 --- a/ACV-abstract-2026/sym-sim.tex +++ b/ACV-abstract-2026/sym-sim.tex @@ -3,7 +3,7 @@ \PassOptionsToPackage{nosumlimits,nonamelimits}{amsmath} \PassOptionsToPackage{colorlinks,linkcolor={blue},citecolor={blue},urlcolor={red},breaklinks=true,final}{hyperref} -\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate, numberwithinsect,final]{lipics-v2021} +\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate, final]{lipics-v2021} \bibliographystyle{plainurl} % the mandatory bibstyle \sloppy @@ -72,21 +72,20 @@ \newcommand{\klstar}{\sharp} %% Kleisli star \newcommand{\relar}{\mathbf{R}} -\title{Soundness and Completeness of Symmetric Relators} %TODO Please add +\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} +%\titlerunning{From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly} -\author{Sergey Goncharov}{University of Birmingham, UK}{s.goncharov@bham.ac.uk}{https://orcid.org/0000-0001-6924-8766}{} \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.' +%\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} +%\keywords{Operational semantics, Higher-order GSOS, Extended combinatory logic} \category{} %optional, e.g. invited paper @@ -123,6 +122,8 @@ \def\subjclassHeading{} \makeatletter \def\@ccsdescString{\erule\vspace{-5ex}} +\def\keywordsHeading{} +\def\@keywords{\relax} \makeatother @@ -133,12 +134,6 @@ \maketitle -%TODO mandatory: add short abstract of the document -\begin{abstract} - -%One remarkable aspect of our approach is its potential for implementation in functional programming languages and proof assistants, -%to atomate SOS specification transformations and reasoning about them. -\end{abstract} @@ -179,6 +174,59 @@ %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 + +Notions of simulation and bisimulation play a central role in the theory of transition +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}). +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. +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$). + +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$. + +Thus, $r$ is a bisimulation iff both $r$ and its inverse $r^\circ$ are simulations. +\end{example} +% +These setting 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.) + \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} +% +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}$. + +A relation $r\subseteq X\times Y$ is an \emph{$\relar$-simulation} from an +$F$-coalgebra $(X,\alpha)$ to $(Y,\beta)$ if +\[ + r \;\subseteq\; \beta^\op\comp\relar r\comp\alpha, +\] +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 +is called \emph{$\relar$-bisimilarity}. +\end{definition} + 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} @@ -210,9 +258,10 @@ In this scenario, $\sigma$ is a witness for $r$ to be a simulation, but it is no 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 + \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: +% +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} @@ -223,8 +272,9 @@ Inspired by Hermida-Jacobs bisimulation\cite{HermidaJacobs98} we modify the defi $\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 +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. + + \bibliography{references} diff --git a/draft/draft.pdf b/draft/draft.pdf index ed20ef9..1ad9f3f 100644 Binary files a/draft/draft.pdf and b/draft/draft.pdf differ