2pp
This commit is contained in:
parent
31e7040e60
commit
cb38aab263
@ -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,12 +297,11 @@ 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{figure}[t]
|
||||
\begin{subfigure}[t]{0.48\textwidth}
|
||||
\centering
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \& R \& Y \\
|
||||
FX \& FR \& FY
|
||||
@ -313,16 +313,12 @@ the diagram
|
||||
\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{equation}\label{eq:diag-lax-sim}
|
||||
\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
|
||||
@ -330,16 +326,27 @@ commuting one (\textsf{\bfseries\ref{it:ll-barr}--\textsf{\bfseries\ref{it:rl-ba
|
||||
\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["\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}
|
||||
\end{equation}
|
||||
\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$.
|
||||
@ -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
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user