pouya/coalgebraic-simulation
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
Files
748b1b582ddc6347b7581920fd1ba2fdf1e5f99b
coalgebraic-simulation/ACV 2026/slides.tex
T
partowp 748b1b582d some editting
2026-07-24 10:32:29 +01:00

672 lines
23 KiB
TeX
Raw Blame History

\documentclass{beamer}
\usetheme{focus}
% Add option [numbering=none] to disable the footer progress bar
% Add option [numbering=fullbar] to show the footer progress bar as always full with a slide countx
\definecolor{main}{RGB}{29, 160, 196}
\definecolor{text}{RGB}{15, 40, 60}
\definecolor{background}{RGB}{255, 255, 255}
\definecolor{catchgreen}{RGB}{0, 166, 147}
\setbeamercolor{block title alerted}{fg=white, bg=catchgreen}
\setbeamercolor{block body alerted}{fg=text, bg=catchgreen!10}
\setbeamertemplate{block begin}
{
\par\vskip\medskipamount%
\IfStrEq{\insertblocktitle}{}{}{
\begin{beamercolorbox}[colsep*=.75ex]{block title}
\usebeamerfont*{block title}\insertblocktitle%
\end{beamercolorbox}%
}
{\parskip0pt\par}%
\ifbeamercolorempty[bg]{block title}
{}
{\ifbeamercolorempty[bg]{block body}{}{\nointerlineskip\vskip-0.5pt}}%
\usebeamerfont{block body}%
\begin{beamercolorbox}[colsep*=.75ex,vmode]{block body}%
\ifbeamercolorempty[bg]{block body}{\vskip-.25ex}{\vskip-.75ex}\vbox{}%
}
\setbeamercovered{invisible}
%------------------------------------------------
\usepackage{booktabs} % Required for better table rules
\usepackage{xstring}
%\usepackage{tikz}
\renewcommand{\baselinestretch}{1.3}
\usepackage[T1]{fontenc}
\usepackage[sfdefault]{AlegreyaSans}
\usepackage{bussproofs}
\EnableBpAbbreviations
\usepackage{multicol}
\usepackage{transparent}
\usepackage{lipsum}
\usepackage{graphicx}
\usepackage{eso-pic}
\usepackage{proof}
\usepackage{amsthm}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{hyperref}
\usepackage{amssymb}
\usepackage{mathtools}
\usepackage{minted}
\usepackage{wasysym}
\usepackage{fontawesome}
\usepackage{tikz-cd}
\usepackage{xcolor}
\usepackage{multicol}
\usepackage{abraces}
\usepackage{accsupp}
\usepackage{stmaryrd}
\usepackage{multicol}
\def\bs{{\;\Downarrow\;}}
\def\la#1{\stackrel{#1}{\rightarrow}}
\def\a{\rightarrow}
\def\as{\rightarrow^{\star}}
\def\sp{{\hspace{1cm}}}
\def\mp{{\hspace{0.66cm}}}
\newcommand{\Dar}{\Downarrow}
\newcommand{\val}{\mathsf{v}}
\newcommand{\com}{\mathsf{c}}
\newcommand{\comp}{\cdot}
\newcommand{\inl}{\mathsf{inl}}
\newcommand{\inr}{\mathsf{inr}}
\newcommand{\id}{\mathsf{id}}
\renewcommand{\prod}{\mathbin{\text{\rotatebox[origin=c]{180}{$\amalg$}}}}
\renewcommand{\coprod}{\mathbin{\text{{$\amalg$}}}}
\newcommand{\lcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\LEFTcircle$}}}}
\newcommand{\fcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\CIRCLE$}}}}
\newcommand{\tcomp}{\textsf{comp}}
\newcommand{\unt}{\mathsf{unit}}
\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}
\newcommand{\bool}{\mathsf{bool}}
\newcommand{\fpc}{\mathsf{fix}}
\newcommand{\casec}{\mathsf{if}}
\newcommand{\ndet}{\oplus} %{\pmb{\klplus}}
%\newcommand{\paral}{\parallel}
% {\ensuremath{\boldsymbol{\mid\mid}}}
\newcommand{\paralv}{\pmb{\parallel_\val}}
\newcommand{\hask}{\includegraphics[height=\fontcharht\font`\B]{res/haskell-logo.png}}
\newcommand{\mS}{\mu\Sigma}
\newcommand{\lbs}[1]{{\mathrel{\;\overset{\raisebox{4pt}{$\scriptstyle #1$\;}}{\smash{\xRightarrow{\hspace{.75em}}}}\;}}}
\newcommand{\ubs}{{\mathrel{\;\overset{\raisebox{4pt}{\;}}{\smash{\xRightarrow{\hspace{.75em}}}}\;}}}
\newcommand{\bba}{
\mathrel{%
\begin{tikzpicture}[baseline=-6pt]
\draw[double, double distance=.75pt, -{Stealth[inset=0pt, angle=75:4pt]}] (0,.02) -- (0,-.28);
\end{tikzpicture}%
}%
}
\newcommand{\relar}{\mathsf{R}}
\newcommand{\powf}{\mathcal{P}}
\newcommand{\eval}{\mathsf{eval}}
\newcommand{\refl}{\mathsf{refl}}
\newcommand{\trans}{\mathsf{trans}}
\newcommand{\preord}{\mathbf{PreOrd}}
\newcommand{\rel}{\mathbf{Rel}}
\newcommand{\spa}{\mathbf{Span}}
\newcommand{\gra}{\mathbf{Gra}}
\newcommand{\obj}{\mathbf{Obj}}
\newcommand{\emre}{\mathbf{L}}
\newcommand{\spto}{\mathrel{\tikz{\draw[-{Stealth}] (0.0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
\newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0.04,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);\draw (0.04,0) -- (0,-0.07);\draw (0.04,0) -- (0,0.07);}}}
\newcommand{\powfi}{\mathcal{P}_{\mathsf{inj}}}
\newcommand{\appr}{\sqsubseteq}
\newcommand{\sappr}{\sqsupseteq}
\newcommand{\Dom}{\mathsf{Dom}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\simeet}{%
\mathbin{%
\ooalign{%
$\sqcap$\cr
\hidewidth\raisebox{0.2ex}{\scalebox{0.44}{$\otimes$}}\hidewidth\cr
}%
}%
}
\title{\Large Coalgebraic Notions of Simulation, Bisimulation and Relators}
\author{\small Pouya Partow\\
\footnotesize Joint work with Sergey Goncharov}
%\titlegraphic{\transparent{0.1}\includegraphics[width=\textwidth,height=\textheight]{res/ut-logo.png}}
\titlegraphic{\transparent{1} \includegraphics[scale=0.1]{res/ut-logo.png}}
\institute{\small School of Computer Science\\ University of Birmingham}
\date{ACV 2026\\ July 25th 2026\\ Lisbon}
\begin{document}
\begin{frame}
\maketitle
\end{frame}
\setlength{\parskip}{2ex}
%
\begin{frame}{Overview}
The content of the talk:
\begin{itemize}
\item Intuitive introduction to coalgebra and (bi)simulation
\item Reviewing basic definitions of coalgebra and (bi)simulation
\item Our motivation: To ease proving program equivalence
\item Relator-based notions
\item Span-based notions
\end{itemize}
\end{frame}
\begin{frame}{Why Does Equivalence of Systems Matter?}
\begin{alertblock}{A basic but fundamental question}
When can we say that two systems \emph{behave the same}?
\end{alertblock}
\vspace{-0.4cm}
This question is everywhere, often silently assumed:\vspace{-0.4cm}
\begin{itemize}
\setlength{\itemsep}{6pt}
\item[\faServer] \textbf{Hardware redesign.} A chip redesigned for cheaper production must still compute exactly what the old one did.
\item[\faCode] \textbf{Software upgrades.} A bank replaces its backend --- from the customer's view (balances, transactions), nothing should change.
\end{itemize}
\vspace{0.2cm}
\begin{block}{The catch}
``Behaving the same'' is intuitive, but making it \emph{precise} and \emph{checkable} is surprisingly subtle.
\end{block}
\end{frame}
%\begin{frame}{From ``System'' to Mathematics}
% \begin{block}{The word ``system'' needs to be made precise}
% To reason formally about equivalence, we need a precise model of what a system \emph{is}.
% \end{block}
% \vspace{0.3cm}
% In this work, systems are modeled as \textbf{Kripke frames}.
% \begin{block}{Definition: Kripke frame}
% A pair $(W, R)$ where $W$ is a set of \emph{states}, and $R \subseteq W \times W$ is a \emph{transition relation}.
% \end{block}
%\end{frame}
\begin{frame}{From ``System'' to Mathematics}
% \vspace{-0.6cm}
\begin{block}{}
We model systems as mathematical notions like \textbf{labeled transition systems}: a set of states, together with a labeled transition relation between them.
\end{block}
\begin{alertblock}{Example: a vending machine}
% \begin{columns}
% \column{0.5\textwidth}
% After inserting a coin, the machine may nondeterministically dispense \emph{coffee} or \emph{tea} --- then return to its idle state.
% \column{0.5\textwidth}
\begin{center}
\begin{tikzpicture}[>=stealth, thick]
\node[circle, draw, minimum size=1cm] (brewing tea) at (0,1.8) {$\mathsf{brewing\;tea}$};
\node[circle, draw, minimum size=1cm] (idle) at (4,1.8) {$\mathsf{idle}$};
\node[circle, draw, minimum size=1cm] (active) at (4,0) {$\mathsf{active}$};
\node[circle, draw, minimum size=1cm] (brewing coffee) at (8,1.8) {$\mathsf{brewing\;coffee}$};
\draw[->] (idle) -- node[left] {insert coin} (active);
\draw[->] (active) to[bend right=20] node[below] {select coffee} (brewing coffee);
\draw[->] (active) to[bend left=20] node[below] {select tea} (brewing tea);
\draw[->] (brewing coffee) -- node[above] {take coffee} (idle);
\draw[->] (brewing tea) -- node[above] {take tea} (idle);
\end{tikzpicture}
\end{center}
% \end{columns}
\end{alertblock}
\end{frame}
\begin{frame}{Simulation and Bisimulation}
\begin{columns}[T]
\column{0.47\textwidth}
\begin{alertblock}{Similar to}
\centering
\begin{tikzpicture}[>=stealth, thick, scale=1, every node/.style={transform shape}]
\node[circle, draw, minimum size=.9cm] (tea) at (0,1.8) {\scriptsize brewing tea};
\node[circle, draw, minimum size=.9cm] (idle) at (4,1.8) {\scriptsize idle};
\node[circle, draw, minimum size=.9cm] (active) at (4,0) {\scriptsize active};
\draw[->] (idle) -- node[left,font=\tiny] {insert coin} (active);
\draw[->] (active) to[bend left=20]
node[below,font=\tiny] {select tea} (tea);
\draw[->] (tea) -- node[above,font=\tiny] {take tea} (idle);
\end{tikzpicture}
\end{alertblock}
\column{0.47\textwidth}
\begin{alertblock}{Bisimilar with}
\centering
\begin{tikzpicture}[>=stealth, thick, scale=.9, every node/.style={transform shape}]
\node[circle, draw, minimum size=1cm] (tea) at (0,1.8) {\scriptsize brewing tea/coffee};
\node[circle, draw, minimum size=1cm] (idle) at (4,1.8) {\scriptsize idle};
\node[circle, draw, minimum size=1cm] (active) at (4,0) {\scriptsize active};
\draw[->] (idle) -- node[left,font=\tiny] {insert coin} (active);
\draw[->] (active) to[bend left=20]
node[below,font=\tiny] {select tea} (tea);
\draw[->] (active) to[bend left=10] node[above,font=\tiny,yshift=2mm] {select coffee} (tea);
\draw[->] (tea) to[bend right=10] node[below,font=\tiny] {take tea} (idle);
\draw[->] (tea) to[bend left=10] node[above,font=\tiny] {take coffee} (idle);
\end{tikzpicture}
\end{alertblock}
\end{columns}
%
% \vspace{-2mm}
%
\begin{block}{}
\begin{center}
\begin{tikzpicture}[>=stealth, thick, scale=.7, every node/.style={transform shape}]
\node[circle, draw, minimum size=1cm] (brewing tea) at (0,1.8) {$\mathsf{brewing\;tea}$};
\node[circle, draw, minimum size=1cm] (idle) at (4,1.8) {$\mathsf{idle}$};
\node[circle, draw, minimum size=1cm] (active) at (4,0) {$\mathsf{active}$};
\node[circle, draw, minimum size=1cm] (brewing coffee) at (8,1.8) {$\mathsf{brewing\;coffee}$};
\draw[->] (idle) -- node[left] {insert coin} (active);
\draw[->] (active) to[bend right=20] node[below] {select coffee} (brewing coffee);
\draw[->] (active) to[bend left=20] node[below] {select tea} (brewing tea);
\draw[->] (brewing coffee) -- node[above] {take coffee} (idle);
\draw[->] (brewing tea) -- node[above] {take tea} (idle);
\end{tikzpicture}
\end{center}
% \end{columns}
\end{block}
\end{frame}
\begin{frame}{Mathematical Definitions}
\footnotesize
\begin{columns}[T,onlytextwidth]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.48\textwidth}
\begin{alertblock}{Labelled Transition Systems}
A \emph{labelled transition system} is a triple $(X,A,T)$, where $T\;\subseteq\;X\times A\times X$.
We write $x\xrightarrow{a}x'$
for $(x,a,x')\in T$.
\end{alertblock}
\vspace{2mm}
\begin{block}{Simulation and Bisimulation}
A relation $R\subseteq X\times Y$ is a simulation from $(X,A,T)$ to $(Y,A,S)$ whenever
\[
\begin{tikzcd}[ampersand replacement=\&]
x \& y \\
{x'} \& {y'}
\arrow["R"{description}, no head, from=1-1, to=1-2]
\arrow["a"', from=1-1, to=2-1]
\arrow["a", dashed, from=1-2, to=2-2]
\arrow["R"{description}, dashed, no head, from=2-1, to=2-2]
\end{tikzcd}
\]
% A simulation relation like $R$ is a bisimulation whenever
% \[
% x\mathrel{R}y,\;
% y\xrightarrow{a}y'
% \Rightarrow
% \exists\,x'.\;
% x\xrightarrow{a}x'
% \;\land\;
% x'Ry'.
% \]
\end{block}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.48\textwidth}
\begin{block}{Bisimulation}
A simulation relation like $R$ is a bisimulation whenever:\vspace{-0.5cm}
\[
\begin{tikzcd}[ampersand replacement=\&]
x \& y \\
{x'} \& {y'}
\arrow["R"{description}, no head, from=1-1, to=1-2]
\arrow["a", dashed, from=1-1, to=2-1]
\arrow["a"', from=1-2, to=2-2]
\arrow["R"{description}, dashed, no head, from=2-1, to=2-2]
\end{tikzcd}
\]
\end{block}
\vspace{-0.2cm}
\begin{alertblock}{Similarity and Bisimilaritiy}
The \emph{similarity relation} $\precsim\subseteq X\times Y$ is the greatest simulation relation. Equivalently
\vspace{-0.3cm}
\[
x\precsim y
\iff
\exists\,R.\;
xRy,
\]
where $R$ is a simulation.\\
Similarity is defined similarly, where $R$ is a simulation, and it is shown with $\precsim$.
% Similarly, the \emph{bisimilarity relation} $\sim\subseteq X\times Y$ is the greatest bisimulation relation. Equivalently\vspace{-0.3cm}
% \[
% x\sim y
% \iff
% \exists\,R.\;
% xRy,
% \]
% where $R$ is a bisimulation.
\end{alertblock}
% \vspace{-0.2cm}
% Ultimately, people care about similarity and bisimilarity, but simulation and bisimulation should be defined first.
\end{columns}
\end{frame}
\begin{frame}{Coalgebras: A Uniform View of Transition Systems}
\small
\begin{columns}[T]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{0.48\textwidth}
\begin{alertblock}{Coalgebras}
\vspace{-2mm}
Fix an endofunctor
\vspace{-2mm}
\[
F:\mathbf{C}\rightarrow\mathbf{C}.
\]
\vspace{-2mm}
An $F$-coalgebra is a pair $(X,\gamma)$, consisting of an object $X$, and a map
\vspace{-2mm}
\[
\gamma:X\rightarrow FX.
\]
\vspace{-2mm}
Different choices of $F$ describe
different transition systems.
\vspace{-1mm}
\end{alertblock}
\vspace{-1mm}
\begin{block}{Our Goal}
\centering
Develop
\textbf{simulation, bisimulation}
once, for all coalgebras.
\end{block}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{0.48\textwidth}
\begin{alertblock}{Different kinds of systems}
\vspace{-2mm}
\begin{itemize}
\setlength{\itemsep}{2pt}
\item Labeled Transition Systems ($FX=\powf(A\times X)$)
\item Kripke frames ($FX=\powf X$)
\item \textcolor{red}{Operational Semantics of Programming Languages (\emph{Abstract HO-GSOS, and Big-step SOS!})}
\item Markov Chains ($FX=(\mathcal{D}X)^A$)
\item Mealy Machines ($FX=(O\times X)^I$)
\item[$\vdots$]
\end{itemize}
\vspace{-1mm}
\end{alertblock}
\end{columns}
\end{frame}
\begin{frame}{Towards Program Equivalence}
\footnotesize
We have developed a coalgbera $(T,\gamma)$ that gives the big-step semantics for an arbitrary programming language in a specified family of them, called \emph{abstract HO-GSOS}.
% \begin{block}{}
% -$\mS$ is representing terms of a programming language,\\
% -and $\gamma$ is giving their big-step reduction.
% \end{block}
\begin{alertblock}{Main Goal}
We want to prove that for terms $t$ and $s$, and a context $C$:\vspace{-0.3cm}
\begin{gather*}
t\sim s\Rightarrow C[t]\sim C[s]
\end{gather*}
\end{alertblock}\vspace{-0.5cm}
-In the literature, this is often proved using \emph{Howe's method}. \\
-The method, applies a closure on the bisimilarity relation on $\mS$.\\
-Then one should prove that the result is a simulation.\\
-The closure preserves symmetry, and symmetric simulation is a bisimulation in traditional definitions.\\
-We have found out that it is not always the case.\\
-That is why we want to know when exactly a symmetric simulation is a bisimulation.
\end{frame}
\begin{frame}{Relators, Simulations and Bisimulations}
\footnotesize
\begin{columns}[T,onlytextwidth]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth}
\begin{alertblock}{Relator}
Assuming $F:\Set\to\Set$ is a functor, an $F$-relator a monotone map that sends a morphism of $\rel$ that is a relation $X\rto Y$ to a relation $FX\rto FY$.
\end{alertblock}
\vspace{-0.3cm}
\begin{block}{R-Simulation}
For an $F$-relator $\relar$, a relation $r:X\rto Y$ is a $\relar$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if $r\subseteq \beta\comp\relar r\comp\alpha^{-1}$.
\end{block}
\vspace{-0.3cm}
\begin{alertblock}{Symmetrization of a Relator}
Symmetrization of a relator $\relar$ is defined as:
\begin{gather*}
\hat{\relar}=\relar r\cap (\relar r^{-1})^{-1}
\end{gather*}
\end{alertblock}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth}
\begin{alertblock}{Symmetric Relator}
A relator $\relar$ is symmetric if $\relar=\hat{\relar}$
\end{alertblock}
\vspace{-0.2cm}
\begin{block}{R-Bisimulation}
For an $F$-relator $\relar$, a relation $r:X\rto Y$ is a $\relar$-bisimulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is an $R$-simulation, and $R$ is a symmetric relator.
\end{block}
\vspace{-0.2cm}
\begin{block}{R-Similarity}
$\relar$-similarity is the greatest $\relar$-simulation.
\end{block}
\vspace{-0.3cm}
\begin{block}{R-Bisimilarity}
$\relar$-bisimilarity is the greatest $\relar$-bisimulation.
\end{block}
\end{columns}
\end{frame}
\begin{frame}{Some Examples of Relators}
\footnotesize
\begin{columns}[T,onlytextwidth]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth}
\begin{alertblock}{Example: Trivial Relator}
For an arbitrary set endofunctor $F$, the relator $\mathbf{Q}$ takes every relation $r:X\rto Y$ to $FX\times FY$.
\end{alertblock}
It is a symmetric relator.
\begin{block}{}
But it is a bad relator because every relation is a $\mathbf{Q}$-bisimulation!
\end{block}
\begin{alertblock}{Example: Egli-Milner Relator}
The relator $\emre$ is a $\powf$-relator defined as:
\begin{gather*}
\emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}
\end{gather*}
\end{alertblock}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth}
We give a family of examples:
\begin{alertblock}{Example: Barr Relators}
Given a set endofunctor $F$, and $r$ is a relation that $r=\pi_2\comp\pi_1^{-1}$ ($\pi_1$ and $\pi_2$ are functions) the Barr relator $\bar{F}$ is defined as
$\bar{F}r=\bar{F}\pi_2\comp(\bar{F}\pi_1)^{-1}$.
\end{alertblock}
\begin{block}{}
The symmetrization of the Egli-Milner relator is a Barr relator, i.e.,
\begin{gather*}
\hat{\emre}=\bar{\powf}
\end{gather*}
\end{block}
Barr relators are nicely behaved relators.\\
A trivial relator is a not a Barr relator.
\end{columns}
\end{frame}
\begin{frame}{Lax Barr relators}
\footnotesize
\begin{columns}[T,onlytextwidth]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth}
An ordering of a set endofunctor $F$ is a functor $G$ that commutes in the following diagram:
\begin{equation*}
\begin{tikzcd}[ampersand replacement=\&]
\& \mathbf{PoSet} \& \\
\Set \&\& \Set
\arrow["U", from=1-2, to=2-3]
\arrow["G", from=2-1, to=1-2]
\arrow["F"', from=2-1, to=2-3]
\end{tikzcd}
\end{equation*}
Meaning that for every $X$, there is a poset $(FX,\appr)$.
\begin{block}{}
For example $(\powf X,\subseteq)$ for every set $X$.
\end{block}
With orderings we define \emph{lax Barr relators}.\\
Lax Barr relators are different abstractions of the Egli-Milner relator.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth}
\begin{block}{}
There are multiple of them:
\begin{itemize}
\item Left-lax: $\appr\comp\bar{F}r$
\item Right-lax: $\bar{F}\comp\appr$
\item Bi-lax: $\appr\comp\bar{F}r\comp\appr$
\item Mid-lax: $F\pi_1\comp\appr\comp(F\pi_2)^{-1}$
\end{itemize}
\end{block}
\begin{alertblock}{Liftability}
An ordering on a set endofunctor $F$ is called \emph{liftable}, if\vspace{-0.3cm}
\begin{gather*}
\alpha\appr\beta\Rightarrow\alpha\comp f\appr \beta\comp f,\\
\alpha\appr\beta\Rightarrow Ff'\comp\alpha\appr Ff'\comp \beta,\\
h\appr Fg\comp k\Rightarrow \exists k', h=Fg\comp k\;\&\;k'\appr k.
\end{gather*}
\end{alertblock}
\end{columns}
\end{frame}
\begin{frame}{Lax Barr relators (2)}
\begin{alertblock}{Proposition}
Given a set endofunctor $F$, with a liftable ordering
\begin{itemize}
\item mid-lax and left-lax relators of $F$ are equal,
\item Assuming the axiom of choice, righ-lax and left-lax relators of $F$ are equal,
\item the symmetrizaion of the left-lax relator is \emph{sound} and \emph{complete} with respect to \emph{behavioural equivalence}.
\end{itemize}
\end{alertblock}
\end{frame}
\begin{frame}{Span-based definitions}
\footnotesize
\begin{columns}[T,onlytextwidth]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth}
\begin{alertblock}{Aczel-Mendler Bisimulation}
For coalgebras $(X,\alpha)$, and $(Y,\beta)$ a span $(R,X,Y)$ is an \emph{AM-bisimulation}, if there is a \emph{witness} $\gamma$ that commutes in the following:
\begin{equation*}
\begin{tikzcd}[ampersand replacement=\&]
X \& R \& Y \\
FX \& FR \& FY
\arrow["\alpha"', 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["{{\gamma}}", from=1-2, to=2-2]
\arrow["\beta", 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*}
\end{alertblock}\vspace{-0.2cm}
In a \emph{regular category}, if we change $FR$ with $\bar{F}R$ that shows the image of $<Fp_1,Fp_2>$, and the legs of $\bar{F}$ (Barr relator in $\Set$), we have an \emph{Hermida-Jacobs} bisimulation.
\begin{block}{}\vspace{-0.2cm}
Every AM-bisimulation is an HJ-bisimulation.
\end{block}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\column{.47\textwidth}
\vspace{0.1cm}
Assuming the axiom of choice, every HJ-bisimulation is an AM-bisimulation.
\begin{block}{}
We have \emph{AM-simulation}, if we lax the diagram:\vspace{-0.4cm}
\begin{equation*}
\begin{tikzcd}[ampersand replacement=\&]
X \& R \& Y \\
FX \& FR \& FY
\arrow["\alpha"', from=1-1, to=2-1]
\arrow["\appr"{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["\beta", from=1-3, to=2-3]
\arrow["\appr"{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*}
\end{block}\vspace{-0.3cm}
We have found a symmetric AM-simulation that is not a bisimulation!
\begin{alertblock}{Proposition}
Given a symmetric span $(R,X)$, with the symmetry evidence $s:R\to R$, assuming $R$ is an AM-simulation on a coalgebra $(X,\alpha)$ with evidence $\sigma$, then $R$ is an AM-bisimulation iff $s$ is a coalgebra endomorphism on $(R,\sigma)$.
\end{alertblock}
\end{columns}
\end{frame}
\bibliographystyle{apalike}
\bibliography{references}
\addtocounter{framenumber}{-1}
\begin{frame}{\quad}
% \vspace{-1cm}
\begin{center}
\textcolor[rgb]{0.384, 0.384, 0}{\Huge Thank you for your attention! :-)}
\end{center}
\end{frame}
\end{document}
Reference in New Issue View Git Blame Copy Permalink