From 3193f636aa2f1d8a2e23d2602d240519e2715235 Mon Sep 17 00:00:00 2001 From: partowp Date: Thu, 18 Jun 2026 18:08:04 +0100 Subject: [PATCH] more --- draft/draft.tex | 132 +++++++++++++++++++++++++++++++++++------------- 1 file changed, 98 insertions(+), 34 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 4e67328..05b2acd 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -289,7 +289,8 @@ \newcommand{\obj}{\mathbf{Obj}} \newcommand{\relar}{\mathbf{R}} \newcommand{\emre}{\mathbf{L}} -\newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}} +\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{\powf}{\mathcal{P}} \newcommand{\sappr}{\sqsupseteq} @@ -387,30 +388,84 @@ Pouya Partow\inst{1}\orcidID{0009-0003-9652-9469}} % \section{Coalgebraic Bisimulation}%\label{sec:} -In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that at least has products, and by $\rel(\BC)$ we refer to the relatios in $\BC$, and by relation we are referring to a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ such that the morphism $\brks{p_1,p_2}$ is a mono. For the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ and $\spa$ we mean $\rel(\Set)$ and $\spa(\Set)$, accordingly. -%\begin{definition}[Relation Lifting] -% Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, where the following diagram commutes: -% \begin{equation*} -% \begin{tikzcd}[ampersand replacement=\&] -% \rel(\BC) \&\& \rel(\BC) \\ -% {\BC\times\BC} \&\& {\BC\times\BC} -% \arrow["{\rel(F)}", from=1-1, to=1-3] -% \arrow[from=1-1, to=2-1] -% \arrow[from=1-3, to=2-3] -% \arrow["{F\times F}"', from=2-1, to=2-3] -% \end{tikzcd} -% \end{equation*} -%\end{definition} -%We have notions of bisimulation that may involve relation lifting. An example of relation lifting is to use the image factorization provided in regular categories. -\begin{definition}[$F$-Relator] - For a set functor $F$, and for sets $X$ and $Y$, an $F$-relator $\relar$ is a map that takes every relation on $X\times Y$ to a relation on $FX\times FY$, and it is monotone with respect to inclusion. -\end{definition} -%Also, for the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ we mean $\rel(\BC)$. +In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that at least has products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, and by relation we are referring to a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ such that the morphism $\brks{p_1,p_2}$ is a mono. We show morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$. +A morphism $f\c R\rto S$ ($f\c R\spto S$) is a morphism in $\rel(\BC)$ ($\spa(\BC)$), whenever $f$, $g_1$ and $g_2$ are morphisms in $\BC$ for which the following diagram commutes in $\BC$: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + {X_1} \& R \& {X_2} \\ + {Y_1} \& S \& {Y_2} + \arrow["{g_1}"', 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["f", from=1-2, to=2-2] + \arrow["{g_2}", from=1-3, to=2-3] + \arrow["{q_1}", from=2-2, to=2-1] + \arrow["{q_2}"', from=2-2, to=2-3] + \end{tikzcd} + \end{equation*} + +\begin{definition}[Relation Lifting] + Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, where the following diagram commutes: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + \rel(\BC) \&\& \rel(\BC) \\ + {\BC\times\BC} \&\& {\BC\times\BC} + \arrow["{\rel(F)}", from=1-1, to=1-3] + \arrow[from=1-1, to=2-1] + \arrow[from=1-3, to=2-3] + \arrow["{F\times F}"', from=2-1, to=2-3] + \end{tikzcd} + \end{equation*} +\end{definition} + +We have notions of bisimulation that may involve relation lifting. An example of a relation lifting is to use the image factorization provided in regular categories. % -%We take $\rel(F)\c\rel(\BC)\to\rel(\BC)$ to be the functor that for an arbitrary functor $F$ takes a relation $R$, where $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and gives the relation that is the image of the function $\brks{Fp_1,Fp_2}\c FR\to FX\times FY$. +%\begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% R \& {R^\dagger} \&\& {X\times X} +% \arrow["{e_R}"', two heads, from=1-1, to=1-2] +% \arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4] +% \arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4] +% \end{tikzcd} +%\end{equation*} +We define a functor of type $(-)^\dagger\c\spa(\BC)\to\rel(\BC)$. It takes every span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the image of its legs: + +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + R \& {R^\dagger} \&\& {X\times Y} + \arrow["{e_R}"', two heads, from=1-1, to=1-2] + \arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4] + \arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4] + \end{tikzcd} +\end{equation*} + +So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ that takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + \& {(FR)^\dagger} \& \\ + FX \&\& FY \\ + \& {FX\times FY} + \arrow["{{{(Fp_1)^\dagger}}}"', from=1-2, to=2-1] + \arrow["{{{(Fp_2)^\dagger}}}", from=1-2, to=2-3] + \arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2] + \end{tikzcd} +\end{equation*} + +Also, there exist a well-known notion named relator, instead of relation lifting. A relator does not need to be a functor, but it should be a map of a specific type format that is monotone with respect to inclusion. Also, relators are defined only on $\Set$ unlike relation liftings. %We discuss relators more in depth in the later chapters. +For the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ and $\spa$ we mean $\rel(\Set)$ and $\spa(\Set)$, accordingly. + +In $\Set$, there is another way to define the morphisms that is to say that $f\c R\rto S$ ($f\c R\spto S$) is a morphism in $\rel$ ($\spa$), whenever there are functions $g_1$ and $g_2$ that $x\mathrel{R}y\Rightarrow g_1(x)\mathrel{(FR)}g_2(y)$. + +Now, considering the two types of morphisms that we can define for $\rel$, and having lifting over the relation or not, we give four notions of bisimulation: +%We take $\rel(F)\c\rel(\BC)\to\rel(\BC)$ to be the functor that for an arbitrary functor $F\c\BC\to\BC$ takes a relation $R$, where $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and gives the relation that is the image of the function $\brks{Fp_1,Fp_2}\c FR\to FX\times FY$. %\begin{definition}[Bisimulation] % For a functor $F\c\BC\to\BC$, a bisimulation is a $\rel(F)$-coalgebra in $\rel$. %\end{definition} + +%\begin{definition}[$F$-Relator] +% For a set functor $F$, and for sets $X$ and $Y$, an $F$-relator $\relar$ is a map that takes every relation on $X\times Y$ to a relation on $FX\times FY$, and it is monotone with respect to inclusion. +%\end{definition} +%Also, for the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ we mean $\rel(\BC)$. % %\begin{prop} % Assuming that $(R,\alpha)$ is a $\rel(F)$-coalgebra, where $\alpha=\beta_1\times\beta_2$ in $\BC\times\BC$, then the following diagram commutes, and vice-versa: @@ -428,7 +483,6 @@ In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that at le % \end{tikzcd} % \end{equation*} %\end{prop} - \begin{definition}[Aczel-Mendler Bisimulation] A relation $R\subseteq X\times Y$ is an \emph{Aczel-Mendler bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to FR$ called witness that commutes in the following diagram: \begin{equation*}\label{eq:acz-mend-diag} @@ -445,9 +499,10 @@ In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that at le \end{tikzcd} \end{equation*} \end{definition} +Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$ instead of $\Set$. Worth noting that with this definition,if $R$ is a bisimulation, it does not necassirily mean that $FR$ is a relation as well, for example $FR$ can have elements that are not pairs. -\begin{definition}[Witnessless $\relar$-Bisimulation] - For a relator $\relar$, a relation $R\subseteq X\times Y$ is a \emph{witnessless $\relar$-bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(\relar R)}\beta(y)$. +\begin{definition}[Witnessless Bisimulation] + A relation $R\subseteq X\times Y$ is a \emph{witnessless bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)^\dagger}\beta(y)$. % \begin{equation*} % \begin{tikzcd}[ampersand replacement=\&] % {X} \& R \& {Y} \\ @@ -462,23 +517,24 @@ In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that at le % \end{equation*} \end{definition} -\begin{definition}[Witnessful $\relar$-Bisimulation] - For a relator $\relar$, a relation $R\subseteq X\times Y$ is a \emph{witnessful $\relar$-bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to \relar R$ called witness that commutes in the following diagram: +\begin{definition}[Hermida-Jacobs Bisimulation] + A relation $R\subseteq X\times Y$ is a \emph{Hermida-Jacobs bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to (FR)^\dagger$ called witness that commutes in the following diagram: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] {X} \& R \& {Y} \\ - {FX} \& \relar R \& {FY} + {FX} \& (FR)^\dagger \& {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["{q_1}", from=2-2, to=2-1] - \arrow["{q_2}"', from=2-2, to=2-3] + \arrow["{(Fp_1)^\dagger}", from=2-2, to=2-1] + \arrow["{(Fp_2)^\dagger}"', from=2-2, to=2-3] \end{tikzcd} \end{equation*} \end{definition} + \begin{definition}[Vanilla Bisimulation] A relation $R\subseteq X\times Y$ is a \emph{vanilla bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)}\beta(y)$. % \begin{equation*} @@ -499,10 +555,12 @@ In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that at le \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] \item Every Aczel-Mendler bisimulation is a vanilla bisimulation. \item Every vanilla bisimulation is an Aczel-Mendler bisimulation. - \item Every Aczel-Mendler bisimulation is a witnessful bisimulation. - \item Assuming the axiom of choice, every witnessful bisimulation is an Aczel-Mendler bisimulation. - \item Every witnessless bisimulation is a witnessful bisimulation. - \item Assuming the axiom of choice, every witnessless bisimulation is a witnessful bisimulation. + \item Every Aczel-Mendler bisimulation is a Hermida-Jacobs bisimulation. + \item Assuming the axiom of choice, every Hermida-Jacobs bisimulation is an Aczel-Mendler bisimulation. + \item Every witnessless bisimulation is a Hermida-Jacobs bisimulation. + \item Assuming the axiom of choice, every witnessless bisimulation is a Hermida-Jacobs bisimulation. + \item Every vanilla bisimulation is a witnessless bisimulation. + \item Every witnessless bisimulation is a vanilla bisimulation. \end{enumerate} \end{prop} \begin{proof} @@ -510,7 +568,13 @@ In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that at le (II): Since $R$ is a vanilla bisimulation, for every $(x,y)\in R$ we have $\alpha(x)\mathrel{(FR)}\beta(y)$, so we can define $\gamma\c R\to FR$ as $\gamma(x,y)=(\alpha(x),\beta(y))$, and then $\gamma$ commutes in~\eqref{eq:acz-mend-diag}. - (III): + (III): It is trivial. + + (IV): Given by Staton. + + (V): Similar to (I) we can define $\gamma(x,y)=(\alpha(x),\beta(y))$ as the witness for $R$ to be a Hermida-Jacobs bisimulation. + + (VI): \end{proof} \todo{Discuss 4 versions of bisimulation (with witness/without witness, for relations/for spans). Which are equivalent? Which do not make sense?}