From 720a02a87fc206f82c7af61e917534ce8c1ca62a Mon Sep 17 00:00:00 2001 From: partowp Date: Sat, 13 Jun 2026 23:40:47 +0100 Subject: [PATCH] proof! --- draft/draft.tex | 438 +++++++++++++++++++++++++++++------------------- 1 file changed, 268 insertions(+), 170 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 3ea97a5..dda38ba 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1638,27 +1638,268 @@ Then we have \end{equation*} We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest are simulations. \todo{So, $\sigma_3$ is a unique witness of bisimulation. How can we characterize it among all witnesses of simulation.} -\begin{definition}\label{def:join-meet} -We define $\join$ and $\meet$ on morphisms as follows: +%\begin{definition}\label{def:join-meet} +%We define $\join$ and $\meet$ on morphisms as follows: +%\begin{gather*} +% \forall x_1,x_2\in X,\\ +% \sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2),\\ +% \sigma_1 \meet \sigma_2 (x_1,x_2)= (\powf p_1)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2)\times(\powf p_2)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2). +%\end{gather*} +%\end{definition} +%\begin{lemma}\label{lem:proj-dist-set} +% For relations $R_1$ and $R_2$ the following equation holds: +% \begin{gather*} +% %(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2) +% (\powf p_i)(R_1\cup R_2)=(\powf p_i)(R_1)\cup(\powf p_i)(R_2) +% \end{gather*} +%\end{lemma} +%\begin{proof} +% We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. +% Assuming $x_1\in(\powf p_1)^\dagger(R_1\cup R_2)$ then exists $x_2$ that $(x_1,x_2)\in R_1\cup R_2$, thus either $(x_1,x_2)\in R_1$ or $(x_1,x_2)\in R_2$, so we have $x_1\in(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$, respectively. So, we have $x_1\in (\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$. +% +% Now, assuming that $x_1\in(\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$ either $x_1\in(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$. Without loss of generality, we can assume $x_1\in(\powf p_1)^\dagger(R_j)$, where $j\in\{1,2\}$. +% Then there exists $x_2$ that $(x_1,x_2)\in R_j$, then we have $(x_1,x_2)\in R_1\cup R_2$ that gives $x_1\in(\powf p_1)^\dagger(R_1\cup R_2)$. +% % We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. +% % +% % First, we prove $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. +% % Assuming $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$ then exists $y_2$ that we have either $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $(y_1,y_2)\in\sigma(x_1,x_2)$. So, we have either $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. +% % +% % Now, we prove $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have: +% % \begin{itemize} +% % \item $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. +% % \item $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in\sigma(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. +% % \end{itemize} \qed +% % \todo{Rewrite the proof according to the statement!} +%\end{proof} +%\begin{lemma} +% Assuming that $\sigma_1$ and $\sigma_2$ are simulation structures of type $R\to(\powf R)^\dagger$, then $\sigma_1 \join \sigma_2$ and $\sigma_1 \meet \sigma_2$ are also simulation structures of the same type. +%\end{lemma} +%\begin{proof} +% Since $\sigma_1$ and $\sigma_2$ are simulation structures, for every $(x_1,x_2)\in R$, for $i\in\{1,2\}$ we have: +% \begin{gather} +% \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2),\\ +% (\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2). +% \end{gather} +% First, we prove the case for $\join$. Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$ we have the following: +% \begin{gather*} +% \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2) +% \end{gather*} +% So, by~\autoref{lem:proj-dist-set} we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))$. +% Similarly, we have $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$ that gives the following: +% \begin{gather*} +% (\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2) +% \end{gather*} +% So, by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))\subseteq\alpha(x_2)$. +% +% Now, we prove the case for $\meet$. For $\meet$ unlike $\join$ we need to prove that $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$. To achieve this, we need to show that assuming $\pi_1$, $\pi_2$ are projections of $\sigma_1\meet\sigma_2(x_1,x_2)$, then for $j\in\{1,2\}$ we have $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)\subseteq\powf p_j(R)$. Since $(\powf p_j)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\powf p_j(R)$, we have $\pi_j\comp(\sigma_1 \meet \sigma_2) (x_1,x_2)\subseteq\powf p_j(R)$, so we have $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$, meaning that $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)=(\powf p_j)^\dagger\comp(\sigma_1\meet\sigma_2)(x_1,x_2)$.\ppnote{The last part of the proof is necessary because the type of the codomain of the definition of $\meet$ is not $(\powf R)^\dagger$, but it is $\powf X\times\powf X$. Perhaps the epi-mono factorization must be used to cope with this in the abstract case.} +% +% For $j\in\{1,2\}$ we have +% \begin{gather}\label{eq:proj-meet} +% (\powf p_j)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))=(\powf p_j)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_j)^\dagger\comp\sigma_2(x_1,x_2). +% \end{gather} +% Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$, we have +% \begin{gather*} +% \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2), +% \end{gather*} +% so by~\eqref{eq:proj-meet} we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))$. Similarly, since $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$, we have +% \begin{gather*} +% (\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2), +% \end{gather*} +% so by~\eqref{eq:proj-meet} we have $(\powf p_2)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))\subseteq\alpha(x_2)$.\qed +%\end{proof} +%\begin{lemma}\label{lem:sim-opsim-inc} +% Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have: +% \begin{enumerate} +% \item $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ +% \item $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ +% \end{enumerate} +%\end{lemma} +%\begin{proof} +% We prove the second clause. +% 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)^\dagger\comp\sigma(x_1,x_2),\\ +% (\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2). +% \end{gather*} +% From $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ since $R$ is symmetric we get $\alpha(x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_2,x_1)$, where +% \begin{gather*} +% (\powf p_1)^\dagger\comp\sigma(x_2,x_1)=(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2). +% \end{gather*} +% So, from $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. Similarly, we can get the other inequation.\qed +%\end{proof} +%\begin{lemma}\label{lem:sim-bisim-inc} +% Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure, +% \begin{enumerate} +% \item if $\sigma\appr\beta$ then we have: +% \begin{gather*} +% \alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2), +% \end{gather*} +% and if $R$ is symmetric we have +% \begin{gather*} +% (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_2). +% \end{gather*} +% \item if $\beta\appr\sigma$ then we have: +% \begin{gather*} +% (\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2) +% \end{gather*} +% and if $R$ is symmetric we have +% \begin{gather*} +% \alpha(x_1)=(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2). +% \end{gather*} +% \end{enumerate} +%\end{lemma} +%\begin{proof} +% \begin{enumerate} +% \item Since $\sigma$ is a simulation structure for an arbitrary $(x_1,x_2)\in R$ we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Since $\sigma\appr\beta$ we have $(\powf p_1)\comp\sigma(x_1,x_2)\subseteq(\powf p_1)\comp\beta(x_1,x_2)$, while $(\powf p_1)\comp\beta(x_1,x_2)=\alpha(x_1)$ by definition of bisimulation. So we have $\alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Then because of the symmetry of $R$ the second clause is easily achievable by using the equations in~\eqref{eq:diag-sym-rel}. +% \item This clause can be proven similar to (1). +% \end{enumerate}\qed +%\end{proof} +%\begin{prop} +% Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure, +% \begin{enumerate} +% \item if $\sigma\appr\beta$ then we have: +% \begin{gather*} +% \beta=\sigma\join ((\powf s)^\dagger\comp\sigma\comp s) +% \end{gather*} +% \item if $\beta\appr\sigma$ then we have: +% \begin{gather*} +% \beta=\sigma\meet((\powf s)^\dagger\comp\sigma\comp s) +% \end{gather*} +% \end{enumerate} +%\end{prop} +%\begin{proof} +% 1. We need to prove that $\sigma\join((\powf s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. +% By~\autoref{lem:sim-opsim-inc}.(1), for every $(x_1,x_2)\in R$, we have $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(1), we have $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. So, we have $(\powf p_1)^\dagger\comp\sigma\join(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_1)$, then by~\autoref{lem:proj-dist-set} we have $(\powf p_1)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. +% +% Also, by~\autoref{lem:sim-bisim-inc}.(1) we have $(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$. So, since we already have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ then by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_2)$. +% +% 2. We need to prove that $\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. +% For $i\in\{1,2\}$, for every $(x_1,x_2)\in R$, we have: +% {\small +% \begin{align*} +% &(\powf p_i)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)\\ +% &=(\powf p_i)^\dagger\comp(((\powf p_1)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))\times((\powf p_2)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_2)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)))\\ +% &=(\powf p_i)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_i)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2) +% \end{align*} +% } +% +% By~\autoref{lem:sim-opsim-inc}.(1), $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)=\alpha(x_1)$, so we have $(\powf p_1)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. +% +% Also, by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$, so, since by~\autoref{lem:sim-opsim-inc}.(2), we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$, so we have $(\powf p_2)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))=\alpha(x_2)$.\qed +%\end{proof} +%\begin{cor} +% Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then if the bisimulation morphism exists, it is equal with the following morphism: +% \begin{gather*} +% (\bigjoin_{\sigma\in S}\sigma)\meet(\powf s)^\dagger\comp(\bigjoin_{\sigma\in S}\sigma)\comp s +% \end{gather*} +%\end{cor} +% +%\begin{lemma} +% For every $S\in \powf R$, +% \begin{gather*} +% ((\powf p_1)(S),(\powf p_2)(S))\in(\powf R)^\dagger\Leftrightarrow(\powf p_1)(S)\subseteq(\powf p_1)(R),(\powf p_2)(S)\subseteq(\powf p_2)(R) +% \end{gather*} +%\end{lemma} +%\begin{lemma}\label{lem:alph-prod} +% Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then there there exists a simulation structure $\sigma\in S$ that for every $(x_1,x_2)$, $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. +%\end{lemma} +%\begin{proof} +% Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ for every $(x_1,x_2)$ as the following: +% \begin{gather*} +% \sigma(x_1,x_2)=(\alpha(x_1), (\powf p_2)^\dagger\comp\delta(x_1,x_2)) +% \end{gather*} +% We have $\sigma(x_1,x_2)\in(\powf R)^\dagger$, as $\alpha(x_1)\subseteq\powf p_1(R)$ and $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\powf p_2(R)$ are inherited from $\delta$ being a simulation structure. +% Also, it obviously is a simulation as $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$. +%\end{proof} +%\begin{prop}\label{prop:sym-rel-bisim} +% Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then the following morphism is the bisimulation structure: +% \begin{gather*} +% (\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s +% \end{gather*} +%\end{prop} +%\begin{proof} +% For every $(x_1,x_2)\in R$ we have +% \begin{gather*} +% (\powf p_1)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)= +% (\powf p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2), +% \end{gather*} +% and +% \begin{gather*} +% (\powf p_2)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)= +% (\powf p_2)^\dagger\comp((\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2). +% \end{gather*} +% By~\autoref{lem:alph-prod} there exists a simulation $\delta\in S$ for which we have $(\powf p_1)^\dagger\comp\delta(x_1,x_2)=\alpha(x_1)$. So, $(\powf p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2)=\alpha(x_1)$. Then by the equations in~\eqref{eq:diag-sym-rel} we also get $(\powf p_2)^\dagger\comp((\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=\alpha(x_2)$.\qed +%\end{proof} +%\section{Symmetric Simulation in Quantaloids} +%We generalize~\autoref{prop:sym-rel-bisim} in regular quantaloids. A quantaloid is a category enriched with suplattices. +%Abstractly, first we define an operation that we need on morphisms that takes two simulation witnesses of type $R\to(FR)^\dagger$ to a morphism of type $R\to FX\times FX$: +%\begin{gather*} +% \sigma_1\simeet\sigma_2=(Fp_1)^\dagger\comp\sigma_1\meet(Fp_1)^\dagger\comp\sigma_2\times(Fp_2)^\dagger\comp\sigma_1\meet(Fp_2)^\dagger\comp\sigma_2 +%\end{gather*} +%\begin{lemma}\label{lem:alph-prod-abs} +% Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation witnesses of the type $R\to (FR)^\dagger$, then there exists a simulation witness $\sigma\in S$ that, $(Fp_1)^\dagger\comp\sigma=\alpha\comp p_1$. +%\end{lemma} +%\begin{proof} +% Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ as the following: +% \begin{gather*} +% \sigma=\brks{(\alpha\comp p_1), (Fp_2)^\dagger\comp\delta} +% \end{gather*} +% We have $(Fp_1)^\dagger\comp\sigma$. +%\end{proof} +\subsection{The concrete proof} +\begin{lemma}\label{lem:sim-opsim-inc} + Assuming that $\sigma\c R\to\powf R$ is a simulation structure, and $R$ is symmetric, 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 + \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). + \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)$ we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$, where + \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). + \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 +\end{proof} +First, we define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$: \begin{gather*} \forall x_1,x_2\in X,\\ - \sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2),\\ - \sigma_1 \meet \sigma_2 (x_1,x_2)= (\powf p_1)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2)\times(\powf p_2)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2). + \sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2). \end{gather*} -\end{definition} +%\begin{lemma} +% 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\join\sigma_2$ is also a witness that $R$ is an Aczel-Mendler simulation. +%\end{lemma} +%\begin{proof} +% \todo{Finish.} +%\end{proof} \begin{lemma}\label{lem:proj-dist-set} For relations $R_1$ and $R_2$ the following equation holds: \begin{gather*} %(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2) - (\powf p_i)(R_1\cup R_2)=(\powf p_i)(R_1)\cup(\powf p_i)(R_2) + \powf p_i(R_1\cup R_2)=\powf p_i(R_1)\cup(\powf p_i)(R_2) \end{gather*} \end{lemma} \begin{proof} We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. - Assuming $x_1\in(\powf p_1)^\dagger(R_1\cup R_2)$ then exists $x_2$ that $(x_1,x_2)\in R_1\cup R_2$, thus either $(x_1,x_2)\in R_1$ or $(x_1,x_2)\in R_2$, so we have $x_1\in(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$, respectively. So, we have $x_1\in (\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$. + Assuming $x_1\in\powf p_1(R_1\cup R_2)$ then exists $x_2$ that $(x_1,x_2)\in R_1\cup R_2$, thus either $(x_1,x_2)\in R_1$ or $(x_1,x_2)\in R_2$, so we have $x_1\in\powf p_1R_1$ or $x_1\in\powf p_1R_2$, respectively. So, we have $x_1\in \powf p_1R_1\cup\powf p_1R_2$. - Now, assuming that $x_1\in(\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$ either $x_1\in(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$. Without loss of generality, we can assume $x_1\in(\powf p_1)^\dagger(R_j)$, where $j\in\{1,2\}$. - Then there exists $x_2$ that $(x_1,x_2)\in R_j$, then we have $(x_1,x_2)\in R_1\cup R_2$ that gives $x_1\in(\powf p_1)^\dagger(R_1\cup R_2)$. + Now, assuming that $x_1\in\powf p_1R_1\cup\powf p_1R_2$ either $x_1\in\powf p_1R_1$ or $x_1\in\powf p_1R_2$. Without loss of generality, we can assume $x_1\in\powf p_1R_j$, where $j\in\{1,2\}$. + Then there exists $x_2$ that $(x_1,x_2)\in R_j$, then we have $(x_1,x_2)\in R_1\cup R_2$ that gives $x_1\in\powf p_1(R_1\cup R_2)$.\qed % We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. % % First, we prove $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. @@ -1671,181 +1912,38 @@ We define $\join$ and $\meet$ on morphisms as follows: % \end{itemize} \qed % \todo{Rewrite the proof according to the statement!} \end{proof} -\begin{lemma} - Assuming that $\sigma_1$ and $\sigma_2$ are simulation structures of type $R\to(\powf R)^\dagger$, then $\sigma_1 \join \sigma_2$ and $\sigma_1 \meet \sigma_2$ are also simulation structures of the same type. -\end{lemma} -\begin{proof} - Since $\sigma_1$ and $\sigma_2$ are simulation structures, for every $(x_1,x_2)\in R$, for $i\in\{1,2\}$ we have: - \begin{gather} - \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2),\\ - (\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2). - \end{gather} - First, we prove the case for $\join$. Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$ we have the following: - \begin{gather*} - \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2) - \end{gather*} - So, by~\autoref{lem:proj-dist-set} we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))$. - Similarly, we have $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$ that gives the following: - \begin{gather*} - (\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2) - \end{gather*} - So, by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))\subseteq\alpha(x_2)$. - - Now, we prove the case for $\meet$. For $\meet$ unlike $\join$ we need to prove that $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$. To achieve this, we need to show that assuming $\pi_1$, $\pi_2$ are projections of $\sigma_1\meet\sigma_2(x_1,x_2)$, then for $j\in\{1,2\}$ we have $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)\subseteq\powf p_j(R)$. Since $(\powf p_j)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\powf p_j(R)$, we have $\pi_j\comp(\sigma_1 \meet \sigma_2) (x_1,x_2)\subseteq\powf p_j(R)$, so we have $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$, meaning that $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)=(\powf p_j)^\dagger\comp(\sigma_1\meet\sigma_2)(x_1,x_2)$.\ppnote{The last part of the proof is necessary because the type of the codomain of the definition of $\meet$ is not $(\powf R)^\dagger$, but it is $\powf X\times\powf X$. Perhaps the epi-mono factorization must be used to cope with this in the abstract case.} - - For $j\in\{1,2\}$ we have - \begin{gather}\label{eq:proj-meet} - (\powf p_j)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))=(\powf p_j)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_j)^\dagger\comp\sigma_2(x_1,x_2). - \end{gather} - Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$, we have - \begin{gather*} - \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2), - \end{gather*} - so by~\eqref{eq:proj-meet} we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))$. Similarly, since $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$, we have - \begin{gather*} - (\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2), - \end{gather*} - so by~\eqref{eq:proj-meet} we have $(\powf p_2)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))\subseteq\alpha(x_2)$.\qed -\end{proof} -\begin{lemma}\label{lem:sim-opsim-inc} - Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have: - \begin{enumerate} - \item $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ - \item $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ - \end{enumerate} -\end{lemma} -\begin{proof} - We prove the second clause. - 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)^\dagger\comp\sigma(x_1,x_2),\\ - (\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2). - \end{gather*} - From $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ since $R$ is symmetric we get $\alpha(x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_2,x_1)$, where - \begin{gather*} - (\powf p_1)^\dagger\comp\sigma(x_2,x_1)=(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2). - \end{gather*} - So, from $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. Similarly, we can get the other inequation.\qed -\end{proof} -\begin{lemma}\label{lem:sim-bisim-inc} - Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure, - \begin{enumerate} - \item if $\sigma\appr\beta$ then we have: - \begin{gather*} - \alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2), - \end{gather*} - and if $R$ is symmetric we have - \begin{gather*} - (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_2). - \end{gather*} - \item if $\beta\appr\sigma$ then we have: - \begin{gather*} - (\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2) - \end{gather*} - and if $R$ is symmetric we have - \begin{gather*} - \alpha(x_1)=(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2). - \end{gather*} - \end{enumerate} -\end{lemma} -\begin{proof} - \begin{enumerate} - \item Since $\sigma$ is a simulation structure for an arbitrary $(x_1,x_2)\in R$ we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Since $\sigma\appr\beta$ we have $(\powf p_1)\comp\sigma(x_1,x_2)\subseteq(\powf p_1)\comp\beta(x_1,x_2)$, while $(\powf p_1)\comp\beta(x_1,x_2)=\alpha(x_1)$ by definition of bisimulation. So we have $\alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Then because of the symmetry of $R$ the second clause is easily achievable by using the equations in~\eqref{eq:diag-sym-rel}. - \item This clause can be proven similar to (1). - \end{enumerate}\qed -\end{proof} -\begin{prop} - Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure, - \begin{enumerate} - \item if $\sigma\appr\beta$ then we have: - \begin{gather*} - \beta=\sigma\join ((\powf s)^\dagger\comp\sigma\comp s) - \end{gather*} - \item if $\beta\appr\sigma$ then we have: - \begin{gather*} - \beta=\sigma\meet((\powf s)^\dagger\comp\sigma\comp s) - \end{gather*} - \end{enumerate} -\end{prop} -\begin{proof} - 1. We need to prove that $\sigma\join((\powf s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. - By~\autoref{lem:sim-opsim-inc}.(1), for every $(x_1,x_2)\in R$, we have $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(1), we have $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. So, we have $(\powf p_1)^\dagger\comp\sigma\join(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_1)$, then by~\autoref{lem:proj-dist-set} we have $(\powf p_1)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. - - Also, by~\autoref{lem:sim-bisim-inc}.(1) we have $(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$. So, since we already have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ then by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_2)$. - - 2. We need to prove that $\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. - For $i\in\{1,2\}$, for every $(x_1,x_2)\in R$, we have: - {\small - \begin{align*} - &(\powf p_i)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)\\ - &=(\powf p_i)^\dagger\comp(((\powf p_1)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))\times((\powf p_2)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_2)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)))\\ - &=(\powf p_i)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_i)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2) - \end{align*} - } - - By~\autoref{lem:sim-opsim-inc}.(1), $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)=\alpha(x_1)$, so we have $(\powf p_1)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. - - Also, by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$, so, since by~\autoref{lem:sim-opsim-inc}.(2), we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$, so we have $(\powf p_2)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))=\alpha(x_2)$.\qed -\end{proof} -\begin{cor} - Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then if the bisimulation morphism exists, it is equal with the following morphism: - \begin{gather*} - (\bigjoin_{\sigma\in S}\sigma)\meet(\powf s)^\dagger\comp(\bigjoin_{\sigma\in S}\sigma)\comp s - \end{gather*} -\end{cor} - -\begin{lemma} - For every $S\in \powf R$, - \begin{gather*} - ((\powf p_1)(S),(\powf p_2)(S))\in(\powf R)^\dagger\Leftrightarrow(\powf p_1)(S)\subseteq(\powf p_1)(R),(\powf p_2)(S)\subseteq(\powf p_2)(R) - \end{gather*} -\end{lemma} +%\begin{rem} +% 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, we have the following lemma. The liftability is not used in the proof, but $\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 symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then there there exists a simulation structure $\sigma\in S$ that for every $(x_1,x_2)$, $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. + 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{proof} - Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ for every $(x_1,x_2)$ as the following: - \begin{gather*} - \sigma(x_1,x_2)=(\alpha(x_1), (\powf p_2)^\dagger\comp\delta(x_1,x_2)) - \end{gather*} - We have $\sigma(x_1,x_2)\in(\powf R)^\dagger$, as $\alpha(x_1)\subseteq\powf p_1(R)$ and $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\powf p_2(R)$ are inherited from $\delta$ being a simulation structure. - Also, it obviously is a simulation as $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$. + 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'$. + \qed \end{proof} \begin{prop}\label{prop:sym-rel-bisim} - Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then the following morphism is the bisimulation structure: + Assuming that $R$ is a symmetric relation, $\sigma\c R\to \powf R$ is a witness for $R$ to be a simulation, for which $\powf p_1\comp\sigma=\alpha\comp p_1$, then the following morphism is a witness for $R$ to be a bisimulation: \begin{gather*} - (\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s + \sigma\join(\powf s\comp\sigma\comp s) \end{gather*} \end{prop} \begin{proof} - For every $(x_1,x_2)\in R$ we have + For every $(x_1,x_2)\in R$ by~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:I} we have \begin{gather*} - (\powf p_1)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)= - (\powf p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2), + \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), \end{gather*} - and + and by~\autoref{lem:alph-prod}, $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. Furthermore, by~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:II} we have \begin{gather*} - (\powf p_2)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)= - (\powf p_2)^\dagger\comp((\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2). + \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). \end{gather*} - By~\autoref{lem:alph-prod} there exists a simulation $\delta\in S$ for which we have $(\powf p_1)^\dagger\comp\delta(x_1,x_2)=\alpha(x_1)$. So, $(\powf p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2)=\alpha(x_1)$. Then by the equations in~\eqref{eq:diag-sym-rel} we also get $(\powf p_2)^\dagger\comp((\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=\alpha(x_2)$.\qed -\end{proof} -\section{Symmetric Simulation in Quantaloids} -We generalize~\autoref{prop:sym-rel-bisim} in regular quantaloids. A quantaloid is a category enriched with suplattices. -Abstractly, first we define an operation that we need on morphisms that takes two simulation witnesses of type $R\to(FR)^\dagger$ to a morphism of type $R\to FX\times FX$: -\begin{gather*} - \sigma_1\simeet\sigma_2=(Fp_1)^\dagger\comp\sigma_1\meet(Fp_1)^\dagger\comp\sigma_2\times(Fp_2)^\dagger\comp\sigma_1\meet(Fp_2)^\dagger\comp\sigma_2 -\end{gather*} -\begin{lemma}\label{lem:alph-prod-abs} - Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation witnesses of the type $R\to (FR)^\dagger$, then there exists a simulation witness $\sigma\in S$ that, $(Fp_1)^\dagger\comp\sigma=\alpha\comp p_1$. -\end{lemma} -\begin{proof} - Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ as the following: - \begin{gather*} - \sigma=\brks{(\alpha\comp p_1), (Fp_2)^\dagger\comp\delta} - \end{gather*} - We have $(Fp_1)^\dagger\comp\sigma$. + Since $\powf p_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf p_2\comp(\powf s\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf s\comp\sigma\comp s)$ is a witness for $R$ to be a bisimulation.\qed \end{proof} + \section{Relators} \subsection{Two-way similarity in Hughes-Jacobs} Hughes and Jacobs define two-way similarity as $\leq\cap\leq^\op$. They give a sufficient condition for the two-way similarity to be the bisimilarity. We discuss that this condition does not allow us to say that a symmetric simularity is a bisimilarity. The condition is: