From cb38aab26395a8afbd6a002815cf3c22b2bf1a9f Mon Sep 17 00:00:00 2001 From: Sergey Goncharov Date: Thu, 21 May 2026 10:08:28 +0100 Subject: [PATCH] 2pp --- ACV-abstract-2026/sym-sim.tex | 99 +++++++++++++++++++---------------- 1 file changed, 53 insertions(+), 46 deletions(-) diff --git a/ACV-abstract-2026/sym-sim.tex b/ACV-abstract-2026/sym-sim.tex index 6febb70..b937b17 100644 --- a/ACV-abstract-2026/sym-sim.tex +++ b/ACV-abstract-2026/sym-sim.tex @@ -14,6 +14,7 @@ \usepackage{microtype} \usepackage{stackengine} \usepackage{tikz-cd} +\usepackage{subcaption} \usetikzlibrary{arrows.meta} \usetikzlibrary{decorations} % Required for all decorations \usetikzlibrary{decorations.pathmorphing} % Specifically for 'zigzag' @@ -206,8 +207,7 @@ These settings can be varied in at least two ways: 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 -\emph{relator}. +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$ @@ -222,8 +222,9 @@ $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}. +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}) @@ -262,8 +263,8 @@ 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\}$. +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$, @@ -272,7 +273,7 @@ the symmetrization of any lax relator is the Barr relator. It is not clear thoug 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 +If $\relar^\leftrightarrow\subseteq\bar F$ then a symmetric $\relar$-simulation $R\subseteq X\times X$ is a $\bar F$\dash bisimulation. \end{proposition} % @@ -296,50 +297,56 @@ the premise ($\relar^\leftrightarrow\subseteq\bar F$) need not be true in genera 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{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 (\textsf{\bfseries\ref{it:ll-barr}--\textsf{\bfseries\ref{it:rl-barr}}} give rise to further variants): +\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} % -\begin{equation}\label{eq:diag-lax-sim} - \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", 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} -\end{equation} +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$. @@ -353,7 +360,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*} -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\}$. +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