diff --git a/ACV 2026/slides.tex b/ACV 2026/slides.tex index 7acb946..538056a 100644 --- a/ACV 2026/slides.tex +++ b/ACV 2026/slides.tex @@ -166,9 +166,9 @@ \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 - \item Motivation! Howe's method for categorical operational semantics \end{itemize} \end{frame} @@ -200,10 +200,9 @@ %\end{frame} \begin{frame}{From ``System'' to Mathematics} - The word ``system'' needs to be made precise. % \vspace{-0.6cm} \begin{block}{} - We model systems as mathematical notions like \textbf{labeled transition systems}: a set of states, together with a transition relation between them. + 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} @@ -266,7 +265,8 @@ 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 tea} (idle); + \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} @@ -317,28 +317,43 @@ A relation $R\subseteq X\times Y$ is a simulation from $(X,A,T)$ to $(Y,A,S)$ whenever \[ - x\mathrel{R}y,\; - x\xrightarrow{a}x' - \Rightarrow - \exists\,y'.\; - y\xrightarrow{a}y' - \;\land\; - x'Ry'. - \] - 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'. + \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} @@ -349,17 +364,18 @@ xRy, \] where $R$ is a simulation.\\ - 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. + 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. +% \vspace{-0.2cm} +% Ultimately, people care about similarity and bisimilarity, but simulation and bisimulation should be defined first. \end{columns} \end{frame} @@ -421,6 +437,27 @@ \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 @@ -621,27 +658,6 @@ \end{columns} \end{frame} -\begin{frame}{Motivation!} - \footnotesize - We have a coalgbera $(\mS,\gamma)$ in an arbitrary category $\mathbb{C}$. - \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} - \bibliographystyle{apalike} \bibliography{references} \addtocounter{framenumber}{-1}