diff --git a/TexCommons b/TexCommons index 348823b..6f6862d 160000 --- a/TexCommons +++ b/TexCommons @@ -1 +1 @@ -Subproject commit 348823b83c5e4f661b721e6c44cbd1957fed0efb +Subproject commit 6f6862db5e3789c8da7e61e393bffbfda2d8f897 diff --git a/draft/draft.tex b/draft/draft.tex index 5f1e595..f88b358 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -388,8 +388,14 @@ 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 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$: +In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has +products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\ +such spans $(X \stackrel{p_1}{\leftarrow} R +\stackrel{p_2}{\to}Y)$ that the morphism $\brks{p_1,p_2}$ is a mono. +We denote morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$. +A morphism $R\rto S$ ($R\spto S$) in $\rel(\BC)$ +($\spa(\BC)$) is such a triple of morphisms $(f\c R\to S, g_1\c X_1\to Y_1, g_2\c X_2\to Y_2)$ +in $\BC$ that the following diagram commutes: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] {X_1} \& R \& {X_2} \\ @@ -417,8 +423,9 @@ A morphism $f\c R\rto S$ ($f\c R\spto S$) is a morphism in $\rel(\BC)$ ($\spa(\B \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. \ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.} +% +We have notions of bisimulation that may involve relation lifting. An example of a relation lifting is obtained +by the image factorization in regular categories. \ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.} % %\begin{equation*} % \begin{tikzcd}[ampersand replacement=\&] @@ -450,13 +457,33 @@ So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC \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. +% +%There exists 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)$. +We can define morphisms in $\rel$ differently by only requesting such functions $g_1$ and $g_2$ that $x\mathrel{R}y$ entails $g_1(x)\mathrel{S}g_2(y)$. Let us +call such morphisms \emph{anonymous} (because they omit the witnessing part $f$, which is unique for relations but not for general spans). This however yields +an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.} + +By varying from anonymous to non-anonymous morphisms and from $\rel$ to $\spa$ we +can obtain for flavors of bisimulation (\autoref{eq:acz-mend-diag}--\autoref{def:vanila}) -- +\autoref{fig:anonymous_onymous} contains a comprehensible summary. + +\begin{figure}[t] +\centering +\begin{tabular}{|l|c|c|} +\hline + & \textbf{Anonymous} & \textbf{Onymous} \\ +\hline +\textbf{Relations} & Witnessless & Hermida-Jacobs \\ +\hline +\textbf{Spans} & Vanilla & Aczel-Mendler \\ +\hline +\end{tabular} +\caption{Comparison of anonymous and onymous settings for relations and spans.} +\label{fig:anonymous_onymous} +\end{figure} -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$. @@ -484,6 +511,9 @@ Now, considering the two types of morphisms that we can define for $\rel$, and h % \end{equation*} %\end{prop} \begin{definition}[Aczel-Mendler Bisimulation] +\todo{Explain in terms of span morphisms}. + + 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} \begin{tikzcd}[ampersand replacement=\&] @@ -499,8 +529,10 @@ Now, considering the two types of morphisms that we can define for $\rel$, and h \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. - +Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$ +instead of $\Set$. It is worth noting that with this definition, if $R$ is a +relation, it does not necassirily mean that $FR$ is a relation as well. +% \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*} @@ -536,7 +568,7 @@ A more general version of witnessless bisimulation is given by Hughes and Jacobs \end{definition} Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary category $\BC$. -\begin{definition}[Vanilla Bisimulation] +\begin{definition}[Vanilla Bisimulation]\label{def:vanila} 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*} % \begin{tikzcd}[ampersand replacement=\&] @@ -554,6 +586,7 @@ Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary categ We do not know if this definition exists anywhere. \begin{prop} The following propositions hold in $\Set$: + \todo{How about proving that 1.3,1.4,1.5 are equivalent to each other, and all together to 1.2 under axiom of choice? } \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] %\item Every Aczel-Mendler bisimulation is a vanilla bisimulation. \item Every vanilla bisimulation is an Aczel-Mendler bisimulation. @@ -574,13 +607,12 @@ We do not know if this definition exists anywhere. (IV): Similar to (I) we can define $\gamma(x,y)=(\alpha(x),\beta(y))$ as the witness for $R$ to be a Hermida-Jacobs bisimulation. \end{proof} -\begin{rem} +\begin{rem}\todo{No, these definitions are just equivalent.} For vanilla bisimulation to be a witnessless bisimulation (or vice-versa) for a relation $R$ we need to have $FR\subseteq (FR)^\dagger$ (or $(FR)^\dagger\subseteq FR$), which is rarely true. The condition may not even be true for other relation liftings for these functors. \end{rem} \begin{rem} +\todo{No, this does not follow from anythying.} To have an Aczel-Mendler bisimulation to be a vanilla bisimulation we need to have $FR\subseteq FX\times FY$ that is a rare condition. It does not hold for powerset functor or maybe functor. - - To have a Hermida-Jacobs bisimulation to be a witnessless bisimulation we need to have $(FR)^\dagger\subseteq FX\times FY$ that is more common, for example it is true for the powerset functor, although we still can not prove it for the general case. Perhaps a condition is needed to be able to have a general statement. \end{rem} \todo{Discuss 4 versions of bisimulation (with witness/without witness, for relations/for spans). Which are equivalent? Which do not make sense?} @@ -2005,33 +2037,36 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a %\end{proof} \subsection{The concrete proof} \begin{lemma}\label{lem:sim-opsim-inc} - Assuming that $\sigma\c R\to\powf R$ is witness for the symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have: + Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have: \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] \item $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$\label{item:sim-opsim-inc:I} \item $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$\label{item:sim-opsim-inc:II} \end{enumerate} \end{lemma} \begin{proof} - By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have - \begin{gather*} - \alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2),\\ - \powf p_2\comp\sigma(x_1,x_2)\subseteq\alpha(x_2). - \end{gather*} - Since $R$ is symmetric $(x_2,x_1)\in R$, so from $\powf p_2\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$, where + By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have + \begin{align} + \alpha(x_1)\subseteq&\;\powf p_1\comp\sigma(x_1,x_2),\label{eq:alpha_x_1}\\ + \powf p_2\comp\sigma(x_1,x_2)\subseteq&\;\alpha(x_2).\label{eq:alpha_x_2} + \end{align} + (I): Since $R$ is symmetric $(x_2,x_1)\in R$, so from \eqref{eq:alpha_x_2} we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$. + Therefore: \begin{align*} - \powf p_2\comp\sigma(x_2,x_1)&\\ - &=\powf p_2\comp\sigma\comp s(x_1,x_2)\\ - &=\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2). + \powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)=&\; \powf p_2\comp\sigma\comp s(x_1,x_2)\\ + =&\; \powf p_2\comp\sigma (x_2,x_1)\\ + \subseteq&\;\alpha(x_1)\\ + \subseteq&\; \powf p_1\comp\sigma(x_1,x_2) & \by{\eqref{eq:alpha_x_1}} \end{align*} - So, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ we have $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$. - - Furthermore, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$, where + % + (II): Analogously, from~\eqref{eq:alpha_x_1} by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$. + Therefore: \begin{align*} - \powf p_1\comp\sigma(x_2,x_1)&\\ - &=\powf p_1\comp\sigma\comp s(x_1,x_2)\\ - &=\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2). + \powf p_2\comp\sigma(x_1,x_2)\subseteq&\; \alpha(x_2) &\by{\eqref{eq:alpha_x_2}}\\ + \subseteq&\; \powf p_1\comp\sigma(x_2,x_1) \\ + =&\; \powf p_1\comp\sigma\comp s(x_1,x_2) \\ + =&\;\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2).& \end{align*} - So, from $\powf p_2\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$.\qed + \qed \end{proof} We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$: \begin{gather*} @@ -2073,12 +2108,12 @@ We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$: % Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\meet\sigma_2$ is not necessarily a witness that $R$ is an Aczel-Mendler simulation. %\end{rem} Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. An abstract version of the following lemma is given by Dubut. -\begin{lemma}\label{lem:alph-prod} - Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, where $\powf p_1\comp\sigma'=\alpha\comp p_1$. -\end{lemma} +\begin{prop}\label{lem:alph-prod} + Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then there exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, such that $\powf p_1\comp\sigma'=\alpha\comp p_1$. +\end{prop} \begin{proof} We define $\sigma'(x_1,x_2)=\{(x'_1,x'_2)\mid x'_1\in\alpha\comp p_1(x_1,x_2)\;,\;(x'_1,x'_2)\in\sigma(x_1,x_2)\}$. We have $\sigma'\subseteq\sigma$ that gives $\powf p_2\comp\sigma'\subseteq\powf p_2\comp\sigma$. Additionally, we have $\powf p_1\comp\sigma'\subseteq\alpha\comp p_1$. - Furthermore, if $x'_1\in\alpha\comp p_1(x_1,x_2)$, since $\alpha\comp p_1\subseteq \powf p_1\comp\sigma$ then $x'_1\in\powf p_1\comp\sigma(x_1,x_2)$, which means that exists $x'_2$ that $(x'_1,x'_2)\in\sigma(x_1,x_2)$. So, by definition of $\sigma'$, we have $(x'_1,x'_2)\in\sigma'(x_1,x_2)$, so $x'_1\in\powf p_1\comp\sigma'(x_1,x_2)$ that means $\alpha\comp p_1\subseteq \powf p_1\comp\sigma'$ as well. So, $\sigma'$ is another witness for $R$ to be an AM simulation, and we have $\alpha\comp p_1=\powf p_1\comp\sigma'$. + Furthermore, if $x'_1\in\alpha\comp p_1(x_1,x_2)$, since $\alpha\comp p_1\subseteq \powf p_1\comp\sigma$ then $x'_1\in\powf p_1\comp\sigma(x_1,x_2)$. Let $(x'_1,x'_2)\in\sigma(x_1,x_2)$. By definition of $\sigma'$, we have $(x'_1,x'_2)\in\sigma'(x_1,x_2)$, so $x'_1\in\powf p_1\comp\sigma'(x_1,x_2)$ that means $\alpha\comp p_1\subseteq \powf p_1\comp\sigma'$ as well. So, $\sigma'$ is another witness for $R$ to be an AM simulation, and we have $\alpha\comp p_1=\powf p_1\comp\sigma'$. \qed \end{proof} \begin{prop}\label{prop:sym-rel-bisim} @@ -2088,12 +2123,13 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the \end{gather*} \end{prop} \begin{proof} - For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:I} we have + For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:I} we have \begin{gather*} \powf p_1\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)= - \powf p_1\comp\sigma(x_1,x_2), + \powf p_1\comp\sigma(x_1,x_2). \end{gather*} - and by~\autoref{lem:alph-prod}, $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. Furthermore, by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:II} we have +% and by~\autoref{lem:alph-prod}, + Recall that $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:II} we have \begin{gather*} \powf p_2\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)= \powf p_2\comp(\powf s\comp\sigma\comp s)(x_1,x_2).