LEM ommitted
This commit is contained in:
partowp
+54
-56
@@ -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}
|
||||
|
||||
Reference in New Issue
Block a user