\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 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, for example:\vspace{-0.4cm} \begin{itemize} \setlength{\itemsep}{6pt} \item[\faServer] \textbf{Hardware redesign.} A chip redesigned for a cheaper price 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 point} ``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 drink} (idle); \draw[->] (brewing tea) -- node[above] {take drink} (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 drink} (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) -- node[above,font=\tiny] {take drink} (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 drink} (idle); \draw[->] (brewing tea) -- node[above] {take drink} (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} 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.\\ Bisimilarity is defined similarly, where $R$ is a bisimulation, and it is shown with $\sim$. % 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 Motivation} 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 $T$.\\ -Then one should prove that the result is a simulation.\\ -The closure preserves symmetry, and symmetric simulation is a bisimulation in traditional definitions.\\ -We need to know how to generally derive bisimulation from simulation.\\ -And what is the impact of choosing specific notion of simulation (span-based, relation-based)? \end{frame} \begin{frame}{Relators and Simulations} \footnotesize \begin{columns}[T,onlytextwidth] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \column{.47\textwidth} Relators unify simulation and bisimulation. \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} \begin{block}{R-Similarity} $\relar$-similarity is the greatest $\relar$-simulation. \end{block} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \column{.47\textwidth} \begin{alertblock}{Example: Trivial Relator} For an arbitrary set endofunctor $F$, the relator $\mathbf{K}$ takes every relation $r:X\rto Y$ to $FX\times FY$. \end{alertblock}\vspace{-0.2cm} % \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} \begin{block}{} But it is a bad relator because every relation is a $\mathbf{K}$-bisimulation! \end{block} \begin{alertblock}{Example: Egli-Milner Relator} The relator $\emre$ is a $\powf$-relator defined as:\vspace{-0.2cm} \begin{gather*} \emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\} \end{gather*} \end{alertblock}\vspace{-0.2cm} \begin{block}{} It gives us the traditional definition for simulation on Kripke frames. \end{block} \end{columns} \end{frame} \begin{frame}{Symmetric Relators} % \footnotesize % \begin{columns}[T,onlytextwidth] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % \column{.47\textwidth} \begin{block}{$R$-bisimulation ($R$-bisimularity)} An $\relar$-simulation (similarity) is a bisimulation (bisimilarity), if $\relar$ is \emph{symmetric}. \end{block} \begin{alertblock}{Symmetrization of a Relator} Symmetrization of a relator $\relar$ is defined as: \begin{gather*} \hat{\relar}r=\relar r\cap (\relar r^{-1})^{-1} \end{gather*} \end{alertblock} \begin{block}{Symmetric Relators} A relator $\relar$ is symmetric if $\relar=\hat{\relar}$ \end{block}\vspace{-0.5cm} Egli-Milner is not symmetric. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % \column{.47\textwidth} % \end{columns} \end{frame} \begin{frame}{Barr 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} \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}\vspace{-0.5cm} Barr relators are nicely behaved relators. % A trivial relator is a not a Barr relator. \begin{block}{} So, we always have bisimulations with Barr relators. \end{block} %\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}{} \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}\vspace{-0.2cm} \begin{alertblock}{Liftability} An ordering on a set endofunctor $F$ is called \emph{liftable}, if\vspace{-0.3cm} \begin{gather*} h\appr Fg\comp k\Rightarrow \exists k', h=Fg\comp k\;\&\;k'\appr k. \end{gather*} \end{alertblock}\vspace{-0.2cm} An ordering and liftablity can be defined for an arbitrary category as well. \end{columns} \end{frame} \begin{frame}{Symmetrization of Lax Barr relators} \footnotesize Having liftability allows us for an arbitrary function $g$ to have:\vspace{-0.2cm} \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] FX \& FX \\ FY \& FY \arrow["{\appr_X}"{inner sep=.8ex}, "\shortmid"{marking}, tail, from=1-1, to=1-2] \arrow["Fg"', from=1-1, to=2-1] \arrow["Fg", from=1-2, to=2-2] \arrow["{\appr_Y}"'{inner sep=.8ex}, "\shortmid"{marking}, tail, from=2-1, to=2-2] \end{tikzcd} \end{equation*}\vspace{-0.3cm} % \begin{gather*} % Fg\comp\appr=\appr\comp Fg\\ % (Fg)^{-1}\comp\sappr=\sappr\comp(Fg)^{-1} % \end{gather*} \begin{alertblock}{Proposition} Given a set endofunctor $F$, with a liftable ordering \begin{enumerate} \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{enumerate} \end{alertblock} \vspace{-0.1cm} \begin{block}{} \begin{itemize} \item Although, not every sound and complete relator is a Barr relator!\\ \item We do not know when Clause 3 does not produce a Barr relator. \end{itemize} \end{block} \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 $$, 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.2cm} \begin{alertblock}{AM-Simulation} 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{alertblock}\vspace{-0.2cm} \begin{block}{} \begin{itemize} \item Every AM-(bi)simulation is an HJ-(bi)simulation. \item Assuming AoC every HJ-bisimulation is an AM-bisimulation. \item Every HJ-bisimulation for a functor of form $\powf F$ in a topos is an AM-bisimulation. \end{itemize} \end{block} \end{columns} \end{frame} \begin{frame}{Symmetric Simulation for Span-based Definitions} \footnotesize So far we have: \begin{block}{} \begin{itemize} \item An example of an AM(HJ)-simulation that is not an AM(HJ)-bisimulation. \item An example of an AM(HJ)-simulation that the witness for AM(HJ)-simulation does not serve as a witness for AM(HJ)-bisimulation for a $\powf$-coalgebra in $\Set$. \end{itemize} \end{block} \begin{alertblock}{Proposition} Given a symmetric span $(R,X)$, with the symmetry witness $s:R\to R$, assuming $R$ is an HJ-simulation on a coalgebra $(X,\alpha)$ with witness $\sigma$, then $R$ is an AM-bisimulation iff $s$ is a coalgebra endomorphism on $(R,\sigma)$. \end{alertblock} \begin{block}{} \begin{itemize} \item We have a proof that symmetric AM-simulations for coalgebras of $\powf$ and the maybe fucntor on $\Set$ are AM-bisimulation. \item We want to know when exactly this proposition holds (perhaps liftability matters). \end{itemize} \end{block} \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}