From 957a0514a46c2f6414bd2aa81320db0d499f2f55 Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 3 Jul 2026 21:15:38 +0100 Subject: [PATCH] LEM ommitted --- draft/draft.tex | 110 ++++++++++++++++++++++++------------------------ 1 file changed, 54 insertions(+), 56 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 66d9bfd..d635f77 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1989,7 +1989,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a % ((\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} +%\begin{lemma}\label{prop: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} @@ -2017,7 +2017,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a % (\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 +% By~\autoref{prop: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. @@ -2025,7 +2025,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a %\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} +%\begin{lemma}\label{prop: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} @@ -2139,8 +2139,8 @@ We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$: %\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 (\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{prop}\label{lem:alph-prod} +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. +\begin{prop}\label{prop: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} @@ -2148,6 +2148,11 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the 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} +An abstract version of the above proposition is given by Dubut that is the following: +\begin{prop}\label{prop:alph-prod-dubut} + Assuming that $R$ is a relation, and $\sigma\c R\to FR$ is a witness for $R$ to be an AM-simulation, then there exists $\sigma'\c R\to FR$ that is another witness for $R$ to be an AM-simulation, such that $Fp_1\comp\sigma'=\alpha\comp p_1$. +\end{prop}\qed +Now, we prove our main statement. \begin{prop}\label{prop:sym-rel-bisim} Assuming that $R$ is a symmetric relation, and $\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*} @@ -2160,7 +2165,7 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the \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 by~\autoref{lem:alph-prod}, +% and by~\autoref{prop: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)= @@ -2169,13 +2174,26 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the 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 an AM bisimulation.\qed \end{proof} \begin{cor} - Considering~\autoref{lem:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well. + Considering~\autoref{prop:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well. \end{cor} Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor. \subsection{Maybe Functor} -We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_X\cup\{(\bot,x)\mid x\in X\}$. +We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_X\cup\{(\bot,x)\mid x\in X\}$.\\ +Now, we prove that the given order on the maybe functor is a liftable one. +\begin{lemma}\label{lem:maybe-lif} + The order structure on the set-functor $FX=X+1$ is a liftable order. +\end{lemma} +\begin{proof} + By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr (g+1)(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $(g+1)(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases: + \begin{itemize} + \item $h=\bot$: In this case we take $k'=\bot$, then we have $g+1(k')=\bot=h$. + + \item $g+1(k)=h$: In this case we take $k'=k$, then we have $g+1(k')=h$, and they are both an element of $Y$.\qed + \end{itemize} +\end{proof} +So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra $(X,\alpha)$ of the maybe functor, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=(p_1+1)\comp\sigma$. \begin{lemma}\label{lem:maybe-func-set} - Assuming that $R$ is a symmetric AM simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ either + Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ either \begin{gather*} \alpha(x_1),\alpha(x_2)\in X, \end{gather*} @@ -2185,20 +2203,34 @@ We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. \end{gather*} \end{lemma} \begin{proof} - We assume that $\sigma\c R\to R+1$ is the witness that we have for $R$ to be an AM-simulation. We prove the statement by contradiction. If the statement is false, then we either have - \begin{gather*} - \alpha(x_1)\in X\quad\&\quad \alpha(x_2)=\bot, - \end{gather*} - or - \begin{gather*} - \alpha(x_1)=\bot\quad\&\quad \alpha(x_2)\in X. - \end{gather*} - Assuming $\alpha(x_1)\in X\;\&\; \alpha(x_2)=\bot$, then since $R$ is an AM-simulation, by~\eqref{eq:diag-lax-sim}$(p_2+1)\comp \sigma(x_1,x_2)\appr\alpha(x_2)$, we have $(p_2+1)\comp \sigma(x_1,x_2)=\bot$ that entails $\sigma(x_1,x_2)=\bot$. So, we have $(p_1+1)\comp \sigma(x_1,x_2)=\bot$, while $\alpha(x_1)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark - - Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is symmetric, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed + By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $p_1+1\comp\sigma=\alpha\comp p_1$. Since $R$ is symmetric, for every $(x_1,x_2)\in $ we have the following: + \begin{enumerate} + \item $\alpha(x_1)=p_1+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1} + \item $\alpha(x_2)=p_1+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2} + \item $\alpha(x_1)\sappr p_2+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3} + \item $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4} + \end{enumerate} + Now, we have two cases: + \begin{itemize} + \item Assuming $\alpha(x_1)\in X$ then by~\eqref{eq:maybe-func-set-1} we have $p_1+1\comp\sigma(x_1,x_2)\in X$, thus $\sigma(x_1,x_2)\in R$. So, we have $p_2+1\comp\sigma(x_1,x_2)\in X$ that by~\eqref{eq:maybe-func-set-4} means $\alpha(x_2)\in X$. + \item Assuming $\alpha(x_1)=\bot$ then by~\eqref{eq:maybe-func-set-3} we have $p_2+1\comp\sigma(x_2,x_1)=\bot$, thus $\sigma(x_2,x_1)=\bot$. So, we have $p_1+1\comp\sigma(x_2,x_1)=\bot$ that by~\eqref{eq:maybe-func-set-2} means $\alpha(x_2)=\bot$ as well.\qed + \end{itemize} \end{proof} +%\begin{proof} +% We assume that $\sigma\c R\to R+1$ is the witness that we have for $R$ to be an AM-simulation. We prove the statement by contradiction. If the statement is false, then we either have +% \begin{gather*} +% \alpha(x_1)\in X\quad\&\quad \alpha(x_2)=\bot, +% \end{gather*} +% or +% \begin{gather*} +% \alpha(x_1)=\bot\quad\&\quad \alpha(x_2)\in X. +% \end{gather*} +% Assuming $\alpha(x_1)\in X\;\&\; \alpha(x_2)=\bot$, then since $R$ is an AM-simulation, by~\eqref{eq:diag-lax-sim}$(p_2+1)\comp \sigma(x_1,x_2)\appr\alpha(x_2)$, we have $(p_2+1)\comp \sigma(x_1,x_2)=\bot$ that entails $\sigma(x_1,x_2)=\bot$. So, we have $(p_1+1)\comp \sigma(x_1,x_2)=\bot$, while $\alpha(x_1)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark +% +% Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is symmetric, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed +%\end{proof} -\begin{prop} +\begin{prop}\label{prop:sym-sim-bis-maybe} For a $F$-coalgebra $(X,\alpha)$ in $\Set$, such that $FX=X+1$, a symmetric AM-simulation relation $R$ on $X$ is an AM-bisimulation. \end{prop} \begin{proof} @@ -2221,41 +2253,7 @@ We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $(p_i+1)\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $(p_i+1)\comp\beta(x_1,x_2)=\alpha(x_i)\in X$.\qed \end{proof} -Now, we give another proof for this functor. This proof is similar to the proof that we have given for the powerset functor. - -\begin{lemma} - The order structure on the set-functor $FX=X+1$ is a liftable order. -\end{lemma} -\begin{proof} - By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr (g+1)(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $(g+1)(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases: - \begin{itemize} - \item $h=\bot$: In this case we take $k'=\bot$, then we have $g+1(k')=\bot=h$. - - \item $g+1(k)=h$: In this case we take $k'=k$, then we have $g+1(k')=h$, and they are both an element of $Y$.\qed - \end{itemize} -\end{proof} -So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra $(X,\alpha)$ of the maybe functor, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=(p_1+1)\comp\sigma$. - -\begin{prop}\label{prop:sym-rel-bisim-may} - Assuming that $R$ is a symmetric relation, and $\sigma\c R\to R+1$ is a witness for $R$ to be a simulation, for which $(p_1+1)\comp\sigma=\alpha\comp p_1$, then the following morphism is a witness for $R$ to be a bisimulation: - \begin{gather*} - \sigma\join((s+1)\comp\sigma\comp s) - \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}.\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). - \end{gather*} - % 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). - \end{gather*} - 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 an AM bisimulation.\qed -\end{proof} +%Although even in the context that we are at the moment, it does not seem plausible to prove that a symmetric simulation is a bisimulation without having an operator like $\join$ in~\autoref{prop:sym-sim-bis-maybe} that takes two morphisms of the same type and gives one. \section{Relators} \subsection{Two-way similarity in Hughes-Jacobs}