pouya/coalgebraic-simulation
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

generalized lemma 3.15

Browse Source
This commit is contained in:
partowp
2026-06-29 23:33:06 +01:00
parent 6ff5d92bf2
commit 270f802d80
1 changed files with 51 additions and 17 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+51 -17
View File
@@ -2036,35 +2036,67 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
% We have $(Fp_1)^\dagger\comp\sigma$. % We have $(Fp_1)^\dagger\comp\sigma$.
%\end{proof} %\end{proof}
\subsection{The concrete proof} \subsection{The concrete proof}
%\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}
% 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:I1}
% \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:II1}
% \end{enumerate}
%\end{lemma}
%\begin{proof}
% 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_11}\\
% \powf p_2\comp\sigma(x_1,x_2)\subseteq&\;\alpha(x_2).\label{eq:alpha_x_21}
% \end{align}
% (I): Since $R$ is symmetric $(x_2,x_1)\in R$, so from \eqref{eq:alpha_x_21} we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$.
% Therefore:
% \begin{align*}
% \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_11}}
% \end{align*}
% %
% (II): Analogously, from~\eqref{eq:alpha_x_11} 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_2\comp\sigma(x_1,x_2)\subseteq&\; \alpha(x_2) &\by{\eqref{eq:alpha_x_21}}\\
% \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*}
% \qed
%\end{proof}
\begin{lemma}\label{lem:sim-opsim-inc} \begin{lemma}\label{lem:sim-opsim-inc}
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: In a category $\BC$, assuming that $F$ has a natural order structure $\appr$, and $\sigma\c R\to F R$ is witness for a symmetric relation $R$ to be an AM-simulation on $F$-coalgebra $(X,\alpha)$, then we have:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)] \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 $F p_1\comp F s\comp\sigma\comp s\appr F p_1\comp\sigma$\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} \item $F p_2\comp\sigma\appr F p_2\comp F s\comp\sigma\comp s$\label{item:sim-opsim-inc:II}
\end{enumerate} \end{enumerate}
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
\begin{align} \begin{align}
\alpha(x_1)\subseteq&\;\powf p_1\comp\sigma(x_1,x_2),\label{eq:alpha_x_1}\\ \alpha\comp p_1\appr&\;F p_1\comp\sigma,\label{eq:alpha_x_1}\\
\powf p_2\comp\sigma(x_1,x_2)\subseteq&\;\alpha(x_2).\label{eq:alpha_x_2} F p_2\comp\sigma\appr&\;\alpha\comp p_2.\label{eq:alpha_x_2}
\end{align} \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)$. (I): Since $R$ is symmetric and $\appr$ is a natural order structure, from \eqref{eq:alpha_x_2} we get $F p_2\comp\sigma\comp s\appr\alpha\comp p_2\comp s$.
Therefore: Therefore:
\begin{align*} \begin{align*}
\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)\\ F p_1\comp F s\comp\sigma\comp s=&\; F p_2\comp\sigma\comp s\\
=&\; \powf p_2\comp\sigma (x_2,x_1)\\ \appr&\;\alpha\comp p_2\comp s\\
\subseteq&\;\alpha(x_1)\\ =&\;\alpha\comp p_1\\
\subseteq&\; \powf p_1\comp\sigma(x_1,x_2) & \by{\eqref{eq:alpha_x_1}} \appr&\; F p_1\comp\sigma & \by{\eqref{eq:alpha_x_1}}
\end{align*} \end{align*}
% %
(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)$. (II): Analogously, from~\eqref{eq:alpha_x_1} since $R$ is symmetric and $\appr$ is a natural order structure, we get $\alpha\comp p_1\comp s\appr F p_1\comp\sigma\comp s$.
Therefore: Therefore:
\begin{align*} \begin{align*}
\powf p_2\comp\sigma(x_1,x_2)\subseteq&\; \alpha(x_2) &\by{\eqref{eq:alpha_x_2}}\\ F p_2\comp\sigma\appr&\; \alpha\comp p_2 &\by{\eqref{eq:alpha_x_2}}\\
\subseteq&\; \powf p_1\comp\sigma(x_2,x_1) \\ =&\; \alpha\comp p_1\comp s\\
=&\; \powf p_1\comp\sigma\comp s(x_1,x_2) \\ \appr&\; F p_1\comp\sigma\comp s \\
=&\;\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2).& =&\;F p_2\comp F s\comp\sigma\comp s.&
\end{align*} \end{align*}
\qed \qed
\end{proof} \end{proof}
@@ -2163,7 +2195,7 @@ We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$.
\end{gather*} \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)\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 reflexive, 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 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} \end{proof}
\begin{prop} \begin{prop}
@@ -2189,6 +2221,8 @@ 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 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} \end{proof}
\section{Relators} \section{Relators}
\subsection{Two-way similarity in Hughes-Jacobs} \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: 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: