condencing

ACV-abstract-2026/sym-sim.tex

@@ -178,38 +178,32 @@
 
 \bigskip
 
-Notions of simulation and bisimulation play a central role in the theory of transition 
+Simulation and bisimulation play a central role in coalgebra and in program semantics. Bisimulation is a certain canonical notion of program 
-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. 
 
-\section{Simulation, Bisimulation, Relators}
+\paragraph{Simulation, Bisimulation, Relators}
-
+%
-
 Consider the following baseline example. 
 %
-\begin{example}[Kripke Frame, Simulation, Bisimulation]\label{exa:pset} A Kripke frame consists 
+\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$).
+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)$
-Simulation on $(X, c)$ is such a relation $R\subseteq X\times X$ that $(x,y)\in R$ 
+there is $y'\in c(y)$ with $(x',y')\in R$. A \emph{bisimulation} additionally requires the
-entails: for all $x'\in c(x)$ there is $y'\in c(y)$, such that $(x',y')\in R$.
+symmetric back condition: for all $y'\in c(y)$ there is $x'\in c(x)$ with $(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^\op$ are simulations.
 \end{example}
 %
-These settings can be varied at least in two ways: 
+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). 
+  nominal sets, to model systems with name management --- but we stick to $\BC=\Set$ in the sequel). 
 \end{itemize}
 %
 A convenient way to work with simulations and bisimulations is via the notion of 
@@ -224,10 +218,8 @@ A relator $\relar$ is \emph{symmetric} if $\relar(R^\op)=(\relar R)^\op$.
 
 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$.
-  R \;\subseteq\;  d^\op\comp\relar R\comp c,
+%
-\]
-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
@@ -240,9 +232,7 @@ 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$.
-  \bar{F} R = F\pi_2\comp(F\pi_1)^\op \;\subseteq\; FX\times FY.
-\]
 \end{definition}
 %
 We ask:
@@ -253,8 +243,8 @@ We ask:
   \item How alternative notions of simulations align with the relator-based one? 
 \end{enumerate}
 
-\section{Relaxing Barr Relators}%\label{sec:}
+\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:
 %
@@ -286,7 +276,7 @@ If $\relar^\leftrightarrow\subseteq\bar F$ then any symmetric $\relar$-simulatio
 $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 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$).
 
@@ -300,8 +290,8 @@ the premise ($\relar^\leftrightarrow\subseteq\bar F$) need not be true in genera
 %\end{proposition}
 
 
-\section{Aczel-Mendler Simulation vs.\ Hermida-Jacobs Simulation}%\label{sec:}
+\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 
@@ -326,11 +316,11 @@ the diagram
 \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$.
+fact that $R$ is an $\bar F$-simulation thus comes with a \emph{witness} $\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:
+commuting one (\textsf{\bfseries\ref{it:ll-barr}--\textsf{\bfseries\ref{it:rl-barr}}} give rise to further variants):
 %
 \begin{equation}\label{eq:diag-lax-sim}
 	\begin{tikzcd}[ampersand replacement=\&]
@@ -348,8 +338,8 @@ commuting one:
 	\end{tikzcd}
 \end{equation}
 %
-(\textsf{\bfseries\ref{it:ll-barr}}--\textsf{\bfseries\ref{it:rl-barr}} give rise to 
+%(\textsf{\bfseries\ref{it:ll-barr}}--\textsf{\bfseries\ref{it:rl-barr}} give rise to 
-further variants, obtained in the obvious way).
+%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$.
@@ -363,7 +353,7 @@ Take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$, and $ c(x)=X$ for every
 		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 $ 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\}$.
+Then $\sigma$ witnesses $R$ to be a 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