diff --git a/draft/draft.tex b/draft/draft.tex index 82f3eb1..d0966d0 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1203,7 +1203,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} 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 Bisimulation} +\section{Symmetric Simulation is a Bisimulation} \begin{definition}[Graph] In a category $\BC$ a graph is a tuple $(R,X)$ of the following form: \begin{equation*} @@ -2161,6 +2161,30 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a % \end{gather*} % We have $(Fp_1)^\dagger\comp\sigma$. %\end{proof} +\begin{example} +And another counter-example!!! +Assuming that $F$ is the powerset endofunctor over the category of sets and injective maps. Then for every $X$, we define the order on $FX$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder.\\ +We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below: +\begin{gather*} + \alpha(x)= + \begin{cases} + \{1,2\} & x=1 \\ + \{2,3\} & x=2\\ + \{3\} & x=3 + \end{cases} +\end{gather*} +$\sigma$ is defined as below: +\begin{gather*} + \sigma(w)= + \begin{cases} + \{(1,2),(2,2)\} & w=(1,2) \\ + \{(2,1),(2,2)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(1,1)\} & w=(2,2) + \end{cases} +\end{gather*} +$R$ is symmetric, and $\sigma$ is a witness for $R$ to be an AM-simulation, but $R$ is not a bisimulation in the traditional sense because $(2,1)\in R$, and $2\to 3$, but $(3,1)$ or $(3,2)$ are not in $R$. It is easy to see that it is not an AM-bisimulation as well because we can not define a function that can serve as an evidence for it as $3$ does not appear in any pair in $R$, while it exists in $\alpha(2)$. +\end{example} \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: