PF
This commit is contained in:
partowp
+132
-98
@@ -576,38 +576,42 @@ The definition derives the ordering on morphisms of each hom-set $\Hom(X,\sub Y)
|
|||||||
0&Sg(k)(g(x))= 0
|
0&Sg(k)(g(x))= 0
|
||||||
\end{cases}
|
\end{cases}
|
||||||
\end{gather*}
|
\end{gather*}
|
||||||
First, we need to prove that $\mu'$ is a subdistribution.
|
Now, we need to prove that $\mu'$ is a subdistribution, but we do not need to prove it directly. Proving that $\mu'\appr\mu$ entails that $\mu'$ is a subdistribution. So, we prove that $\mu'\appr\mu$.
|
||||||
For every $x \in X$, $\mu'(x) \ge 0$. We have:
|
For every $x\in X$, have the following cases:
|
||||||
|
\begin{itemize}
|
||||||
|
\item $Sg(\mu)(g(x))= 0$: We have $\mu'(x)=0$, and obviously $\mu'\appr\mu$.
|
||||||
|
\item $Sg(\mu)(g(x))\neq 0$: We have $\frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)$, and since $\nu\appr Sg(\mu)$ then we have:
|
||||||
\begin{align*}
|
\begin{align*}
|
||||||
\sum_{x \in X} \mu'(x)&\\
|
&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\leq 1\\
|
||||||
=& \sum_{x \in X} \frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)&(Sg(\mu)(g(x))\neq 0)\\
|
\Rightarrow&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\comp \mu(x)\leq \mu(x)
|
||||||
=& \sum_{y \in Y} \sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)&(Sg(\mu)(y)\neq 0)\\
|
|
||||||
=& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)&(Sg(\mu)(y)\neq 0)\\
|
|
||||||
=& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)&(Sg(\mu)(y)\neq 0)\\
|
|
||||||
=& \sum_{y \in Y} \nu(y)\\
|
|
||||||
\leq& 1
|
|
||||||
\end{align*}
|
\end{align*}
|
||||||
As for every $x\in X$ that $Sg(\mu)(g(x))=0$, $\mu'(x)=0$, it does not have effect the inequality. Thus $\mu'$ is a subdistribution. Now, we prove $Sg(\mu') = \nu$.
|
\end{itemize}
|
||||||
|
% First, we need to prove that $\mu'$ is a subdistribution.
|
||||||
|
% For every $x \in X$, $\mu'(x) \ge 0$. We have:
|
||||||
|
% \begin{align*}
|
||||||
|
% \sum_{x \in X} \mu'(x)&\\
|
||||||
|
% =& \sum_{x \in X} \frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)&(Sg(\mu)(g(x))\neq 0)\\
|
||||||
|
% =& \sum_{y \in Y} \sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)&(Sg(\mu)(y)\neq 0)\\
|
||||||
|
% =& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)&(Sg(\mu)(y)\neq 0)\\
|
||||||
|
% =& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)&(Sg(\mu)(y)\neq 0)\\
|
||||||
|
% =& \sum_{y \in Y} \nu(y)\\
|
||||||
|
% \leq& 1
|
||||||
|
% \end{align*}
|
||||||
|
% As for every $x\in X$ that $Sg(\mu)(g(x))=0$, $\mu'(x)=0$, it does not effect the inequality. Thus $\mu'$ is a subdistribution.
|
||||||
|
Now, we prove $Sg(\mu') = \nu$.
|
||||||
For any $y \in Y$, we have:
|
For any $y \in Y$, we have:
|
||||||
\begin{align*}
|
|
||||||
Sg(\mu')(y)&\\
|
|
||||||
= &\sum_{x \in g^{\mone}(y)} \mu'(x)\\
|
|
||||||
= &\sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)&(Sg(\mu)(y)\neq 0)\\
|
|
||||||
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)&(Sg(\mu)(y)\neq 0)\\
|
|
||||||
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)&(Sg(\mu)(y)\neq 0)\\
|
|
||||||
= &\mu(y)
|
|
||||||
\end{align*}
|
|
||||||
(If $Sg(\mu)(y) = 0$, then $\nu(y) = 0$, and the sum is $0$ as well, so the equality still holds.) \\
|
|
||||||
Now, we are left to prove that $\mu'\appr\mu$.
|
|
||||||
For every $x\in X$, have the following cases:
|
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item $Sg(\mu)(g(x))= 0$: We have $\mu'(x)=0$, and obviously $\mu'\appr\mu$.
|
\item $Sg(\mu)(y) = 0$: We have $\nu(y) = 0$, and the sum is $0$ as well, so the equality holds.\\
|
||||||
\item $Sg(\mu)(g(x))\neq 0$: We have $\frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)$, and since $\nu\appr Sg(\mu)$ then we have:
|
\item $Sg(\mu)(y)\neq 0$:
|
||||||
\begin{align*}
|
\begin{align*}
|
||||||
&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\leq 1\\
|
Sg(\mu')(y)&\\
|
||||||
\Rightarrow&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\comp \mu(x)\leq \mu(x)
|
= &\sum_{x \in g^{\mone}(y)} \mu'(x)\\
|
||||||
\end{align*}\qed
|
= &\sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)\\
|
||||||
\end{itemize}
|
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)\\
|
||||||
|
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)\\
|
||||||
|
= &\nu(y)
|
||||||
|
\end{align*}
|
||||||
|
\end{itemize}\qed
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
|
|
||||||
@@ -1302,6 +1306,7 @@ A big concern with this approach is that Comma Objects are defined in a 2-catego
|
|||||||
\subsection{Choosing a suitable order for our setting}
|
\subsection{Choosing a suitable order for our setting}
|
||||||
Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term.
|
Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term.
|
||||||
\section{Symmetric Simulation is a Bisimulation}
|
\section{Symmetric Simulation is a Bisimulation}
|
||||||
|
\todo{Obviously, this chapter should be changed. All the definitions should be moved to somewhere else. You should start the chapter by giving your counter examples, and then presenting your proofs.}
|
||||||
\begin{definition}[Graph]
|
\begin{definition}[Graph]
|
||||||
In a category $\BC$ a graph is a tuple $(R,X)$ of the following form:
|
In a category $\BC$ a graph is a tuple $(R,X)$ of the following form:
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
@@ -2417,79 +2422,78 @@ We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
|
|||||||
% \todo{Finish.}
|
% \todo{Finish.}
|
||||||
%\end{proof}
|
%\end{proof}
|
||||||
\subsection{Powerset Functor}
|
\subsection{Powerset Functor}
|
||||||
\begin{lemma}\label{lem:proj-dist-set}
|
%\begin{lemma}\label{lem:proj-dist-set}
|
||||||
For relations $R_1$ and $R_2$ the following equation holds:
|
% For relations $R_1$ and $R_2$ the following equation holds:
|
||||||
\begin{gather*}
|
% \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)^\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{gather*}
|
||||||
\end{lemma}
|
%\end{lemma}
|
||||||
\begin{proof}
|
%\begin{proof}
|
||||||
We prove the lemma for the case that $i=1$. The proof is the same for $i=2$.
|
% 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(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$.
|
% 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_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\}$.
|
% 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
|
% 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$.
|
% % 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)$.
|
% % 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)$.
|
% % 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:
|
% % 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}
|
% % \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(\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)$.
|
% % \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
|
% % \end{itemize} \qed
|
||||||
% \todo{Rewrite the proof according to the statement!}
|
% % \todo{Rewrite the proof according to the statement!}
|
||||||
\end{proof}
|
%\end{proof}
|
||||||
%\begin{rem}
|
%%\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.
|
%% 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}
|
%%\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.
|
%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}
|
%\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$.
|
% 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}
|
%\end{prop}
|
||||||
\begin{proof}
|
%\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$.
|
% 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)$. 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'$.
|
% 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
|
% \qed
|
||||||
\end{proof}
|
%\end{proof}
|
||||||
An abstract version of the above proposition is given by Dubut that is the following:
|
%A more abstract version of the following proposition is given by Dubut:
|
||||||
\begin{prop}\label{prop:alph-prod-dubut}
|
%\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$.
|
% 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
|
%\end{prop}\qed
|
||||||
Now, we prove our main statement.
|
%Now, we prove our main statement.
|
||||||
\begin{prop}\label{prop:sym-rel-bisim}
|
%\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:
|
% 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*}
|
% \begin{gather*}
|
||||||
\sigma\join(\powf s\comp\sigma\comp s)
|
% \sigma\join(\powf s\comp\sigma\comp s)
|
||||||
\end{gather*}
|
% \end{gather*}
|
||||||
\end{prop}
|
%\end{prop}
|
||||||
\begin{proof}
|
%\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
|
% 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*}
|
% \begin{gather*}
|
||||||
\powf p_1\comp(\sigma\join(\powf s\comp\sigma\comp s))(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).
|
% \powf p_1\comp\sigma(x_1,x_2).
|
||||||
\end{gather*}
|
% \end{gather*}
|
||||||
% and by~\autoref{prop: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
|
% 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*}
|
% \begin{gather*}
|
||||||
\powf p_2\comp(\sigma\join(\powf s\comp\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).
|
% \powf p_2\comp(\powf s\comp\sigma\comp s)(x_1,x_2).
|
||||||
\end{gather*}
|
% \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
|
% 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}
|
%\end{proof}
|
||||||
\begin{cor}
|
%\begin{cor}
|
||||||
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.
|
% 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}
|
%\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.
|
%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.
|
||||||
|
We prove the stronger statement for $\powf$, where $F$ is an arbitrary endofunctor on $\Set$. The ordering that we consider on this functor is the set inclusion. We recall the following lemma:
|
||||||
\subsection{PF}
|
\begin{lemma}\label{lem:func-dist-set}
|
||||||
\begin{lemma}\label{lem:proj-dist-set-abs}
|
|
||||||
For sets $X$ and $Y$ in $\powf A$, and a function $f\c A\to B$ the following equation holds:
|
For sets $X$ and $Y$ in $\powf A$, and a function $f\c A\to B$ the following equation holds:
|
||||||
\begin{gather*}
|
\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)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2)
|
||||||
\powf f(X\cup Y)=\powf f(X)\cup \powf f(Y)
|
\powf f(X_1\cup X_2)=\powf f(X_1)\cup \powf f(X_2)
|
||||||
\end{gather*}
|
\end{gather*}
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
@@ -2509,7 +2513,37 @@ Now, we make the proof more abstract. We prove the statement for set-functors of
|
|||||||
% \end{itemize} \qed
|
% \end{itemize} \qed
|
||||||
% \todo{Rewrite the proof according to the statement!}
|
% \todo{Rewrite the proof according to the statement!}
|
||||||
\end{proof}
|
\end{proof}
|
||||||
\todo{Finish this proof. With this, you can give the proof for $\powf F$. After you finished this, you can remove the previous sections.}
|
The following statement is proven by Dubut:
|
||||||
|
\begin{prop}\label{prop:alph-prod-dubut-pf}
|
||||||
|
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
|
||||||
|
For arbitrary sets $X$ and $Y$, and functions $f,g\in\Hom(X,\powf FY)$, we define $f\join g$ as follows:
|
||||||
|
\begin{gather*}
|
||||||
|
(f\join g)(x)=f(x)\cup g(x)
|
||||||
|
\end{gather*}
|
||||||
|
\begin{prop}\label{prop:sym-rel-bisim-pf}
|
||||||
|
Assuming that $R$ is a symmetric relation, and $\sigma\c R\to \powf FR$ is a witness for $R$ to be an AM-simulation, then the following morphism is a witness for $R$ to be an AM-bisimulation:
|
||||||
|
\begin{gather*}
|
||||||
|
\sigma\join(\powf Fs\comp\sigma\comp s)
|
||||||
|
\end{gather*}
|
||||||
|
\end{prop}
|
||||||
|
\begin{proof}
|
||||||
|
For every $(x_1,x_2)\in R$ by~\autoref{lem:func-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:I} we have
|
||||||
|
\begin{gather*}
|
||||||
|
\powf Fp_1\comp(\sigma\join(\powf Fs\comp\sigma\comp s))(x_1,x_2)=
|
||||||
|
\powf Fp_1\comp\sigma(x_1,x_2).
|
||||||
|
\end{gather*}
|
||||||
|
% and by~\autoref{prop:alph-prod},
|
||||||
|
Recall that by~\autoref{prop:lift-gen-func}, set inclusion is a liftable ordering, so by~\autoref{prop:alph-prod-dubut-pf}, we have $\powf Fp_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:func-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:II} we have
|
||||||
|
\begin{gather*}
|
||||||
|
\powf Fp_2\comp(\sigma\join(\powf Fs\comp\sigma\comp s))(x_1,x_2)=
|
||||||
|
\powf Fp_2\comp(\powf Fs\comp\sigma\comp s)(x_1,x_2).
|
||||||
|
\end{gather*}
|
||||||
|
Since $\powf Fp_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf Fp_2\comp(\powf Fs\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf Fs\comp\sigma\comp s)$ is a witness for $R$ to be an AM bisimulation.\qed
|
||||||
|
\end{proof}
|
||||||
|
\begin{cor}
|
||||||
|
Assuming that $R$ is a symmetric relation and it is an AM-simulation on a $\powf F$ coalgebra, then $R$ is an AM-bisimulation as well.
|
||||||
|
\end{cor}
|
||||||
|
|
||||||
\subsection{Maybe 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$.\\
|
We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$.\\
|
||||||
|
|||||||
Reference in New Issue
Block a user