diff --git a/ACV 2026/slides.tex b/ACV 2026/slides.tex index 3057f6c..50d3f02 100644 --- a/ACV 2026/slides.tex +++ b/ACV 2026/slides.tex @@ -165,7 +165,7 @@ 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 Reviewing definitions of coalgebra and (bi)simulation \item Our motivation: To ease proving program equivalence \item Relator-based notions \item Span-based notions @@ -177,14 +177,14 @@ 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} + This question is everywhere, for example:\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[\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 catch} + \begin{block}{The point} ``Behaving the same'' is intuitive, but making it \emph{precise} and \emph{checkable} is surprisingly subtle. \end{block} \end{frame} @@ -453,8 +453,8 @@ -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 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. + -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} @@ -465,7 +465,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \column{.47\textwidth} - To define coalgebraic simulation, relators are invented. + 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} @@ -533,7 +533,7 @@ \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} + \hat{\relar}r=\relar r\cap (\relar r^{-1})^{-1} \end{gather*} \end{alertblock} \begin{block}{Symmetric Relators} @@ -658,8 +658,8 @@ \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 the symmetrizaion of a Barr relator is a Barr relator. + \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}