From ed01ebf5bfdf726dc31f3fc706e783fd8c96e48c Mon Sep 17 00:00:00 2001 From: partowp Date: Sun, 3 May 2026 19:47:03 +0100 Subject: [PATCH] counter-example --- draft/draft.tex | 250 ++++++++++++++++++++++++++---------------------- 1 file changed, 134 insertions(+), 116 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index fd85648..f530fcf 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -289,6 +289,7 @@ \newcommand{\obj}{\mathbf{Obj}} \newcommand{\relar}{\mathbf{R}} \newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}} +\newcommand{\powf}{\mathcal{P}} \newcommand{\simeet}{% \mathbin{% @@ -939,7 +940,7 @@ Lifting from $\BC$ to $\gra(\BC)$ is easy. For $F\c\BC\to\BC$ we define $F_\gra\ \arrow["{Fp_2}", from=1-2, to=2-3] \end{tikzcd} \end{equation*} -This lifting does not work for $\rel$. As an example, if we set $F$ to be the powerset functor $\mathcal{P}$, then $(\mathcal{P}R,\mathcal{P}X)$ is not necessarily a relation anymore. For example, if we take $R=\{(1,0),(0,1),(0,0),(1,1)\}$, then taking $\{\{(1,0),(0,1),(0,0),(1,1)\}\}$ and $\{\{(1,0),(0,1),(0,0)\}\}$ as elements of $\mathcal{P}R$, the morphism $\brks{\mathcal{P}p_1,\mathcal{P}p_2}$ maps them both to $(\{0,1\},\{0,1\})$ so it is not monic. +This lifting does not work for $\rel$. As an example, if we set $F$ to be the powerset functor $\powf$, then $(\powf R,\powf X)$ is not necessarily a relation anymore. For example, if we take $R=\{(1,0),(0,1),(0,0),(1,1)\}$, then taking $\{\{(1,0),(0,1),(0,0),(1,1)\}\}$ and $\{\{(1,0),(0,1),(0,0)\}\}$ as elements of $\powf R$, the morphism $\brks{\powf p_1,\powf p_2}$ maps them both to $(\{0,1\},\{0,1\})$ so it is not monic. To cope with this, we assume the following epi-mono decomposition for $(R,X)\in\rel(\BC)$: \begin{equation*} @@ -1142,7 +1143,7 @@ Another avenue would be to give another definition for simulation that does not Well! This counter example does not work! Because the described order $\appr$ does not satisfy the condition mentioned in Jacobs's paper. The condition is that the order on $FX$ should satisfy the property that for a morphism $f\c X\to Y$ the morphism $Ff\c FX\to FY$ preserves $\appr$. Probably, the only poset that has this property for $\mathbf{Id}$ is $\Delta$. If there is a counter-example, it is true for another functor. \begin{example} - Another counter-example! Assume that $F=\mathcal{P}$, and take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha(x)=X$ for every $x\in X$, and $\sigma$ is defined as below: + Another counter-example! Assume that $F=\powf $, and take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha(x)=X$ for every $x\in X$, and $\sigma$ is defined as below: \begin{gather*} \sigma(w)= \begin{cases} @@ -1150,11 +1151,11 @@ Well! This counter example does not work! Because the described order $\appr$ do R\setminus\{(1,2)\} & w=(1,3) \end{cases} \end{gather*} - In this scenario, $\sigma$ is a simulation, but it is not a bisimulation. It is a simulation since for every $w\in R$ we have $(\mathcal{P}p_1(\sigma(w)))=X$, thus for every $x\in X$, $\alpha(x)=X\subseteq X$. Also, $\mathcal{P}p_2(\sigma(w))\subseteq \alpha(p_2(w))$ as $\alpha(p_2(w))=X$ for every $w\in R$. But it is not a bisimulation, since $\alpha\comp p_2(1,3)=\alpha(3)=X\neq(\mathcal{P}p_2)^\dagger(\sigma(1,3))=\{1,3\}$. + In this scenario, $\sigma$ is a simulation, but it is not a bisimulation. It is a simulation since for every $w\in R$ we have $(\powf p_1(\sigma(w)))=X$, thus for every $x\in X$, $\alpha(x)=X\subseteq X$. Also, $\powf p_2(\sigma(w))\subseteq \alpha(p_2(w))$ as $\alpha(p_2(w))=X$ for every $w\in R$. But it is not a bisimulation, since $\alpha\comp p_2(1,3)=\alpha(3)=X\neq(\powf p_2)^\dagger(\sigma(1,3))=\{1,3\}$. \end{example} % \begin{example} - And another counter-example!!! Assume that $F=\mathcal{P}$, and take $R=X\times X\setminus\{(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below: + And another counter-example!!! Assume that $F=\powf $, and take $R=X\times X\setminus\{(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below: \begin{gather*} \alpha(x)= \begin{cases} @@ -1176,7 +1177,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp\sigma_1(w)= + (\powf p_1)^\dagger\comp\sigma_1(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2,3\} & w=(2,1) \\ @@ -1185,7 +1186,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{2,3\} & w=(2,3) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp\sigma_1(w)= + (\powf p_2)^\dagger\comp\sigma_1(w)= \begin{cases} \{2\} & w=(1,2) \\ \{1,2\} & w=(2,1) \\ @@ -1208,7 +1209,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp\sigma'_1(w)= + (\powf p_1)^\dagger\comp\sigma'_1(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2,3\} & w=(2,1) \\ @@ -1218,7 +1219,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{2,3\} & w=(2,3) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp\sigma'_1(w)= + (\powf p_2)^\dagger\comp\sigma'_1(w)= \begin{cases} \{2,3\} & w=(1,2) \\ \{1,2\} & w=(2,1) \\ @@ -1249,7 +1250,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \beta=\sigma'_1 \end{gather*} \begin{gather*} - (\mathcal{P}s)^\dagger\comp\sigma_1\comp s(w)= + (\powf s)^\dagger\comp\sigma_1\comp s(w)= \begin{cases} \{(1,2),(2,3)\} & w=(1,2) \\ \{(2,1),(2,2)\} & w=(2,1) \\ @@ -1261,7 +1262,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_1\comp s(w)= + (\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma_1\comp s(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2\} & w=(2,1) \\ @@ -1271,7 +1272,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{2,3\} & w=(2,3) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_1\comp s(w)= + (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma_1\comp s(w)= \begin{cases} \{2,3\} & w=(1,2) \\ \{1,2\} & w=(2,1) \\ @@ -1282,7 +1283,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{3\} & w=(3,3) \end{cases} \end{gather*} - In this scenario, $\sigma_1$ is a simulation, but it is not a bisimulation. $\sigma'_1$, $\sigma''_1$ and $(\mathcal{P}s)^\dagger\comp\sigma_1\comp s$ are neither. We can not make $\sigma_1$ bigger here to make it a bisimulation as $\alpha\comp p_1(3,2)=\{3\}\subsetneq\{2,3\}=(\mathcal{P}p_1)^\dagger\comp\sigma_1(3,2)$. + In this scenario, $\sigma_1$ is a simulation, but it is not a bisimulation. $\sigma'_1$, $\sigma''_1$ and $(\powf s)^\dagger\comp\sigma_1\comp s$ are neither. We can not make $\sigma_1$ bigger here to make it a bisimulation as $\alpha\comp p_1(3,2)=\{3\}\subsetneq\{2,3\}=(\powf p_1)^\dagger\comp\sigma_1(3,2)$. The following is also a simulation and not a bisimulation: \begin{gather*} @@ -1297,7 +1298,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp\sigma_2(w)= + (\powf p_1)^\dagger\comp\sigma_2(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2,3\} & w=(2,1) \\ @@ -1306,7 +1307,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{2,3\} & w=(2,3) \\ \{3\} & w\in\{(3,2),(3,3)\} \end{cases} - (\mathcal{P}p_2)^\dagger\comp\sigma_2(w)= + (\powf p_2)^\dagger\comp\sigma_2(w)= \begin{cases} \{2\} & w=(1,2) \\ \{1,2\} & w=(2,1) \\ @@ -1329,7 +1330,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp\sigma'_2(w)= + (\powf p_1)^\dagger\comp\sigma'_2(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2,3\} & w=(2,1) \\ @@ -1339,7 +1340,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{2,3\} & w=(2,3) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp\sigma'_2(w)= + (\powf p_2)^\dagger\comp\sigma'_2(w)= \begin{cases} \{2,3\} & w=(1,2) \\ \{1,2\} & w=(2,1) \\ @@ -1351,7 +1352,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}s)^\dagger\comp\sigma_2\comp s(w)= + (\powf s)^\dagger\comp\sigma_2\comp s(w)= \begin{cases} \{(1,2),(2,3)\} & w=(1,2) \\ \{(2,1),(2,2)\} & w=(2,1) \\ @@ -1363,7 +1364,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_2\comp s(w)= + (\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma_2\comp s(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2\} & w=(2,1) \\ @@ -1373,7 +1374,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{2\} & w=(2,3) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_2\comp s(w)= + (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma_2\comp s(w)= \begin{cases} \{2,3\} & w=(1,2) \\ \{1,2\} & w=(2,1) \\ @@ -1384,7 +1385,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{3\} & w=(3,3) \end{cases} \end{gather*} - $\sigma_2$ is a simulation, $\sigma'_2$ is a bisimulation, and $(\mathcal{P}s)^\dagger\comp\sigma_2\comp s$ is neither. + $\sigma_2$ is a simulation, $\sigma'_2$ is a bisimulation, and $(\powf s)^\dagger\comp\sigma_2\comp s$ is neither. The following is both a simulation and a bisimulation: \begin{gather*} \sigma_3(w)= @@ -1399,7 +1400,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp\sigma_3(w)= + (\powf p_1)^\dagger\comp\sigma_3(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2,3\} & w=(2,1) \\ @@ -1409,7 +1410,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{3\} & w=(3,2) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp\sigma_3(w)= + (\powf p_2)^\dagger\comp\sigma_3(w)= \begin{cases} \{2,3\} & w=(1,2) \\ \{1,2\} & w=(2,1) \\ @@ -1434,7 +1435,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp\sigma_4(w)= + (\powf p_1)^\dagger\comp\sigma_4(w)= \begin{cases} \{1,2,3\} & w=(1,2) \\ \{1,2,3\} & w=(2,1) \\ @@ -1444,7 +1445,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{1,2,3\} & w=(3,2) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp\sigma_4(w)= + (\powf p_2)^\dagger\comp\sigma_4(w)= \begin{cases} \{2,3\} & w=(1,2) \\ \{1,2\} & w=(2,1) \\ @@ -1468,7 +1469,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp\sigma''_4(w)= + (\powf p_1)^\dagger\comp\sigma''_4(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2,3\} & w=(2,1) \\ @@ -1478,7 +1479,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{3\} & w=(3,2) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp\sigma''_4(w)= + (\powf p_2)^\dagger\comp\sigma''_4(w)= \begin{cases} \{2,3\} & w=(1,2) \\ \{1,2\} & w=(2,1) \\ @@ -1490,7 +1491,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}s)^\dagger\comp\sigma_4\comp s(w)= + (\powf s)^\dagger\comp\sigma_4\comp s(w)= \begin{cases} \{(1,1),(1,2),(2,1),(2,2),(2,3)\} & w=(1,2) \\ \{(2,1),(2,2),(2,3),(3,2),(3,3)\} & w=(2,1) \\ @@ -1502,7 +1503,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_4\comp s(w)= + (\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma_4\comp s(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2,3\} & w=(2,1) \\ @@ -1512,7 +1513,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{3\} & w=(3,2) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_4\comp s(w)= + (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma_4\comp s(w)= \begin{cases} \{1,2,3\} & w=(1,2) \\ \{1,2,3\} & w=(2,1) \\ @@ -1523,7 +1524,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{3\} & w=(3,3) \end{cases} \end{gather*} - $\sigma_4$ is a simulation, $\sigma''_4$ is a bisimulation, and $(\mathcal{P}s)^\dagger\comp\sigma_4\comp s$ is neither. + $\sigma_4$ is a simulation, $\sigma''_4$ is a bisimulation, and $(\powf s)^\dagger\comp\sigma_4\comp s$ is neither. The following is also a simulation and not a bisimulation: \begin{gather*} @@ -1539,7 +1540,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp\sigma_5(w)= + (\powf p_1)^\dagger\comp\sigma_5(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2,3\} & w=(2,1) \\ @@ -1549,7 +1550,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{3\} & w=(3,2) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp\sigma_5(w)= + (\powf p_2)^\dagger\comp\sigma_5(w)= \begin{cases} \{2\} & w=(1,2) \\ \{2\} & w=(2,1) \\ @@ -1574,7 +1575,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \end{cases} \end{gather*} \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp\sigma_6(w)= + (\powf p_1)^\dagger\comp\sigma_6(w)= \begin{cases} \{1,2\} & w=(1,2) \\ \{2,3\} & w=(2,1) \\ @@ -1584,7 +1585,7 @@ Well! This counter example does not work! Because the described order $\appr$ do \{3\} & w=(3,2) \\ \{3\} & w=(3,3) \end{cases} - (\mathcal{P}p_2)^\dagger\comp\sigma_6(w)= + (\powf p_2)^\dagger\comp\sigma_6(w)= \begin{cases} \{2\} & w=(1,2) \\ \{1\} & w=(2,1) \\ @@ -1602,10 +1603,10 @@ Well! This counter example does not work! Because the described order $\appr$ do % If we define $\appr$ on simulations as \begin{gather*} - \sigma_1\appr\sigma_2\iff \forall x_1,x_2\in X, (\mathcal{P}p_i)^\dagger\comp\sigma_1(x_1,x_2)\subseteq(\mathcal{P}p_i)^\dagger\comp\sigma_2(x_1,x_2) + \sigma_1\appr\sigma_2\iff \forall x_1,x_2\in X, (\powf p_i)^\dagger\comp\sigma_1(x_1,x_2)\subseteq(\powf p_i)^\dagger\comp\sigma_2(x_1,x_2) \end{gather*} \begin{lemma} - $(Hom(R,(\mathcal{P}R)^\dagger),\appr)$ is a poset. + $(Hom(R,(\powf R)^\dagger),\appr)$ is a poset. \end{lemma} \begin{proof} Reflexivity and transitivity are obvious. We need to prove anti-symmetry.\\ @@ -1630,192 +1631,192 @@ We define $\join$ and $\meet$ on morphisms as follows: \begin{gather*} \forall x_1,x_2\in X,\\ \sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2),\\ - \sigma_1 \meet \sigma_2 (x_1,x_2)= (\mathcal{P}p_1)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_1)^\dagger\comp\sigma_2(x_1,x_2)\times(\mathcal{P}p_2)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_2)^\dagger\comp\sigma_2(x_1,x_2). + \sigma_1 \meet \sigma_2 (x_1,x_2)= (\powf p_1)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2)\times(\powf p_2)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2). \end{gather*} \end{definition} \begin{lemma}\label{lem:proj-dist-set} For relations $R_1$ and $R_2$ the following equation holds: \begin{gather*} - %(\mathcal{P}p_i)^\dagger(R_1\cup R_2)=(\mathcal{P}p_i)^\dagger(R_1)\cup(\mathcal{P}p_i)^\dagger(R_2) - (\mathcal{P}p_i)(R_1\cup R_2)=(\mathcal{P}p_i)(R_1)\cup(\mathcal{P}p_i)(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) \end{gather*} \end{lemma} \begin{proof} We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. - Assuming $x_1\in(\mathcal{P}p_1)^\dagger(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(\mathcal{P}p_1)^\dagger(R_1)$ or $x_1\in(\mathcal{P}p_1)^\dagger(R_2)$, respectively. So, we have $x_1\in (\mathcal{P}p_1)^\dagger(R_1)\cup(\mathcal{P}p_1)^\dagger(R_2)$. + Assuming $x_1\in(\powf p_1)^\dagger(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_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$, respectively. So, we have $x_1\in (\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$. - Now, assuming that $x_1\in(\mathcal{P}p_1)^\dagger(R_1)\cup(\mathcal{P}p_1)^\dagger(R_2)$ either $x_1\in(\mathcal{P}p_1)^\dagger(R_1)$ or $x_1\in(\mathcal{P}p_1)^\dagger(R_2)$. Without loss of generality, we can assume $x_1\in(\mathcal{P}p_1)^\dagger(R_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(\mathcal{P}p_1)^\dagger(R_1\cup R_2)$. + Now, assuming that $x_1\in(\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$ either $x_1\in(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$. Without loss of generality, we can assume $x_1\in(\powf p_1)^\dagger(R_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)^\dagger(R_1\cup R_2)$. % We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. % - % First, we prove $(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. - % Assuming $y_1\in(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}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(\mathcal{P}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(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}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)$. % - % Now, we prove $(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}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} - % \item $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. - % \item $y_1\in(\mathcal{P}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(\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}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)$. % \end{itemize} \qed % \todo{Rewrite the proof according to the statement!} \end{proof} \begin{lemma} - Assuming that $\sigma_1$ and $\sigma_2$ are simulation structures of type $R\to(\mathcal{P}R)^\dagger$, then $\sigma_1 \join \sigma_2$ and $\sigma_1 \meet \sigma_2$ are also simulation structures of the same type. + Assuming that $\sigma_1$ and $\sigma_2$ are simulation structures of type $R\to(\powf R)^\dagger$, then $\sigma_1 \join \sigma_2$ and $\sigma_1 \meet \sigma_2$ are also simulation structures of the same type. \end{lemma} \begin{proof} Since $\sigma_1$ and $\sigma_2$ are simulation structures, for every $(x_1,x_2)\in R$, for $i\in\{1,2\}$ we have: \begin{gather} - \alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_i(x_1,x_2),\\ - (\mathcal{P}p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2). + \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2),\\ + (\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2). \end{gather} - First, we prove the case for $\join$. Since $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_i(x_1,x_2)$ we have the following: + First, we prove the case for $\join$. Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$ we have the following: \begin{gather*} - \alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_1(x_1,x_2)\cup (\mathcal{P}p_1)^\dagger\comp\sigma_2(x_1,x_2) + \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2) \end{gather*} - So, by~\autoref{lem:proj-dist-set} we have $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))$. - Similarly, we have $(\mathcal{P}p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$ that gives the following: + So, by~\autoref{lem:proj-dist-set} we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))$. + Similarly, we have $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$ that gives the following: \begin{gather*} - (\mathcal{P}p_2)^\dagger\comp\sigma_1(x_1,x_2)\cup (\mathcal{P}p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2) + (\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2) \end{gather*} - So, by~\autoref{lem:proj-dist-set} we have $(\mathcal{P}p_2)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))\subseteq\alpha(x_2)$. + So, by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))\subseteq\alpha(x_2)$. - Now, we prove the case for $\meet$. For $\meet$ unlike $\join$ we need to prove that $\sigma_1\meet\sigma_2(x_1,x_2)\in(\mathcal{P}R)^\dagger$. To achieve this, we need to show that assuming $\pi_1$, $\pi_2$ are projections of $\sigma_1\meet\sigma_2(x_1,x_2)$, then for $j\in\{1,2\}$ we have $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)\subseteq\mathcal{P}p_j(R)$. Since $(\mathcal{P}p_j)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\mathcal{P}p_j(R)$, we have $\pi_j\comp(\sigma_1 \meet \sigma_2) (x_1,x_2)\subseteq\mathcal{P}p_j(R)$, so we have $\sigma_1\meet\sigma_2(x_1,x_2)\in(\mathcal{P}R)^\dagger$, meaning that $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)=(\mathcal{P}p_j)^\dagger\comp(\sigma_1\meet\sigma_2)(x_1,x_2)$.\ppnote{The last part of the proof is necessary because the type of the codomain of the definition of $\meet$ is not $(\mathcal{P}R)^\dagger$, but it is $\mathcal{P}X\times\mathcal{P}X$. Perhaps the epi-mono factorization must be used to cope with this in the abstract case.} + Now, we prove the case for $\meet$. For $\meet$ unlike $\join$ we need to prove that $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$. To achieve this, we need to show that assuming $\pi_1$, $\pi_2$ are projections of $\sigma_1\meet\sigma_2(x_1,x_2)$, then for $j\in\{1,2\}$ we have $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)\subseteq\powf p_j(R)$. Since $(\powf p_j)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\powf p_j(R)$, we have $\pi_j\comp(\sigma_1 \meet \sigma_2) (x_1,x_2)\subseteq\powf p_j(R)$, so we have $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$, meaning that $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)=(\powf p_j)^\dagger\comp(\sigma_1\meet\sigma_2)(x_1,x_2)$.\ppnote{The last part of the proof is necessary because the type of the codomain of the definition of $\meet$ is not $(\powf R)^\dagger$, but it is $\powf X\times\powf X$. Perhaps the epi-mono factorization must be used to cope with this in the abstract case.} For $j\in\{1,2\}$ we have \begin{gather}\label{eq:proj-meet} - (\mathcal{P}p_j)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))=(\mathcal{P}p_j)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_j)^\dagger\comp\sigma_2(x_1,x_2). + (\powf p_j)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))=(\powf p_j)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_j)^\dagger\comp\sigma_2(x_1,x_2). \end{gather} - Since $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_i(x_1,x_2)$, we have + Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$, we have \begin{gather*} - \alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_1(x_1,x_2)\cap (\mathcal{P}p_1)^\dagger\comp\sigma_2(x_1,x_2), + \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2), \end{gather*} - so by~\eqref{eq:proj-meet} we have $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))$. Similarly, since $(\mathcal{P}p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$, we have + so by~\eqref{eq:proj-meet} we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))$. Similarly, since $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$, we have \begin{gather*} - (\mathcal{P}p_2)^\dagger\comp\sigma_1(x_1,x_2)\cap (\mathcal{P}p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2), + (\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2), \end{gather*} - so by~\eqref{eq:proj-meet} we have $(\mathcal{P}p_2)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))\subseteq\alpha(x_2)$.\qed + so by~\eqref{eq:proj-meet} we have $(\powf p_2)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))\subseteq\alpha(x_2)$.\qed \end{proof} \begin{lemma}\label{lem:sim-opsim-inc} - Assuming that $\sigma\c R\to(\mathcal{P}R)^\dagger$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have: + Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have: \begin{enumerate} - \item $(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq (\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ - \item $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$ + \item $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ + \item $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ \end{enumerate} \end{lemma} \begin{proof} We prove the second clause. By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have \begin{gather*} - \alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2),\\ - (\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2). + \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2),\\ + (\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2). \end{gather*} - From $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ since $R$ is symmetric we get $\alpha(x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_2,x_1)$, where + From $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ since $R$ is symmetric we get $\alpha(x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_2,x_1)$, where \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp\sigma(x_2,x_1)=(\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2). + (\powf p_1)^\dagger\comp\sigma(x_2,x_1)=(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2). \end{gather*} - So, from $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$. Similarly, we can get the other inequation.\qed + So, from $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. Similarly, we can get the other inequation.\qed \end{proof} \begin{lemma}\label{lem:sim-bisim-inc} - Assuming that $\sigma\c R\to(\mathcal{P}R)^\dagger$ is a simulation structure, and $\beta\c R\to(\mathcal{P}R)^\dagger$ is a bisimulation structure, + Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure, \begin{enumerate} \item if $\sigma\appr\beta$ then we have: \begin{gather*} - \alpha(x_1)=(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2), + \alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2), \end{gather*} and if $R$ is symmetric we have \begin{gather*} - (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_2). + (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_2). \end{gather*} \item if $\beta\appr\sigma$ then we have: \begin{gather*} - (\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2) + (\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2) \end{gather*} and if $R$ is symmetric we have \begin{gather*} - \alpha(x_1)=(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2). + \alpha(x_1)=(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2). \end{gather*} \end{enumerate} \end{lemma} \begin{proof} \begin{enumerate} - \item Since $\sigma$ is a simulation structure for an arbitrary $(x_1,x_2)\in R$ we have $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. Since $\sigma\appr\beta$ we have $(\mathcal{P}p_1)\comp\sigma(x_1,x_2)\subseteq(\mathcal{P}p_1)\comp\beta(x_1,x_2)$, while $(\mathcal{P}p_1)\comp\beta(x_1,x_2)=\alpha(x_1)$ by definition of bisimulation. So we have $\alpha(x_1)=(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. Then because of the symmetry of $R$ the second clause is easily achievable by using the equations in~\eqref{eq:diag-sym-rel}. + \item Since $\sigma$ is a simulation structure for an arbitrary $(x_1,x_2)\in R$ we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Since $\sigma\appr\beta$ we have $(\powf p_1)\comp\sigma(x_1,x_2)\subseteq(\powf p_1)\comp\beta(x_1,x_2)$, while $(\powf p_1)\comp\beta(x_1,x_2)=\alpha(x_1)$ by definition of bisimulation. So we have $\alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Then because of the symmetry of $R$ the second clause is easily achievable by using the equations in~\eqref{eq:diag-sym-rel}. \item This clause can be proven similar to (1). \end{enumerate}\qed \end{proof} \begin{prop} - Assuming that $\sigma\c R\to(\mathcal{P}R)^\dagger$ is a simulation structure, and $\beta\c R\to(\mathcal{P}R)^\dagger$ is a bisimulation structure, + Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure, \begin{enumerate} \item if $\sigma\appr\beta$ then we have: \begin{gather*} - \beta=\sigma\join ((\mathcal{P}s)^\dagger\comp\sigma\comp s) + \beta=\sigma\join ((\powf s)^\dagger\comp\sigma\comp s) \end{gather*} \item if $\beta\appr\sigma$ then we have: \begin{gather*} - \beta=\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s) + \beta=\sigma\meet((\powf s)^\dagger\comp\sigma\comp s) \end{gather*} \end{enumerate} \end{prop} \begin{proof} - 1. We need to prove that $\sigma\join((\mathcal{P}s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. - By~\autoref{lem:sim-opsim-inc}.(1), for every $(x_1,x_2)\in R$, we have $(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(1), we have $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. So, we have $(\mathcal{P}p_1)^\dagger\comp\sigma\join(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_1)$, then by~\autoref{lem:proj-dist-set} we have $(\mathcal{P}p_1)^\dagger\comp(\sigma\join((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. + 1. We need to prove that $\sigma\join((\powf s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. + By~\autoref{lem:sim-opsim-inc}.(1), for every $(x_1,x_2)\in R$, we have $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(1), we have $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. So, we have $(\powf p_1)^\dagger\comp\sigma\join(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_1)$, then by~\autoref{lem:proj-dist-set} we have $(\powf p_1)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. - Also, by~\autoref{lem:sim-bisim-inc}.(1) we have $(\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$. So, since we already have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ then by~\autoref{lem:proj-dist-set} we have $(\mathcal{P}p_2)^\dagger\comp(\sigma\join((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_2)$. + Also, by~\autoref{lem:sim-bisim-inc}.(1) we have $(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$. So, since we already have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ then by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_2)$. - 2. We need to prove that $\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. + 2. We need to prove that $\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. For $i\in\{1,2\}$, for every $(x_1,x_2)\in R$, we have: {\small \begin{align*} - &(\mathcal{P}p_i)^\dagger\comp(\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)\\ - &=(\mathcal{P}p_i)^\dagger\comp(((\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2) \cap (\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2))\times((\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2) \cap (\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2)))\\ - &=(\mathcal{P}p_i)^\dagger\comp\sigma(x_1,x_2) \cap (\mathcal{P}p_i)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2) + &(\powf p_i)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)\\ + &=(\powf p_i)^\dagger\comp(((\powf p_1)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))\times((\powf p_2)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_2)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)))\\ + &=(\powf p_i)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_i)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2) \end{align*} } - By~\autoref{lem:sim-opsim-inc}.(1), $(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2)\subseteq (\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(2) we have $(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2)=\alpha(x_1)$, so we have $(\mathcal{P}p_1)^\dagger\comp(\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. + By~\autoref{lem:sim-opsim-inc}.(1), $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)=\alpha(x_1)$, so we have $(\powf p_1)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. - Also, by~\autoref{lem:sim-bisim-inc}.(2) we have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$, so, since by~\autoref{lem:sim-opsim-inc}.(2), we have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$, so we have $(\mathcal{P}p_2)^\dagger\comp(\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2))=\alpha(x_2)$.\qed + Also, by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$, so, since by~\autoref{lem:sim-opsim-inc}.(2), we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$, so we have $(\powf p_2)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))=\alpha(x_2)$.\qed \end{proof} \begin{cor} - Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then if the bisimulation morphism exists, it is equal with the following morphism: + 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 if the bisimulation morphism exists, it is equal with the following morphism: \begin{gather*} - (\bigjoin_{\sigma\in S}\sigma)\meet(\mathcal{P}s)^\dagger\comp(\bigjoin_{\sigma\in S}\sigma)\comp s + (\bigjoin_{\sigma\in S}\sigma)\meet(\powf s)^\dagger\comp(\bigjoin_{\sigma\in S}\sigma)\comp s \end{gather*} \end{cor} \begin{lemma} - For every $S\in \mathcal{P}R$, + For every $S\in \powf R$, \begin{gather*} - ((\mathcal{P}p_1)^\dagger(S),(\mathcal{P}p_2)^\dagger(S))\in(\mathcal{P}R)^\dagger\Leftrightarrow(\mathcal{P}p_1)(S)\subseteq(\mathcal{P}p_1)(R),(\mathcal{P}p_2)(S)\subseteq(\mathcal{P}p_2)(R) + ((\powf p_1)^\dagger(S),(\powf p_2)^\dagger(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} - Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then there there exists a simulation structure $\sigma\in S$ that for every $(x_1,x_2)$, $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. + 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} Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ for every $(x_1,x_2)$ as the following: \begin{gather*} - \sigma(x_1,x_2)=(\alpha(x_1), (\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)) + \sigma(x_1,x_2)=(\alpha(x_1), (\powf p_2)^\dagger\comp\delta(x_1,x_2)) \end{gather*} - We have $\sigma(x_1,x_2)\in(\mathcal{P}R)^\dagger$, as $\alpha(x_1)\subseteq\mathcal{P}p_1(R)$ and $(\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\mathcal{P}p_2(R)$ are inherited from $\delta$ being a simulation structure. - Also, it obviously is a simulation as $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$. + We have $\sigma(x_1,x_2)\in(\powf R)^\dagger$, as $\alpha(x_1)\subseteq\powf p_1(R)$ and $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\powf p_2(R)$ are inherited from $\delta$ being a simulation structure. + Also, it obviously is a simulation as $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$. \end{proof} \begin{prop}\label{prop:sym-rel-bisim} - Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then the following morphism is the bisimulation structure: + 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 the following morphism is the bisimulation structure: \begin{gather*} - (\bigmeet_{\sigma\in S}\sigma)\join(\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s + (\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s \end{gather*} \end{prop} \begin{proof} For every $(x_1,x_2)\in R$ we have \begin{gather*} - (\mathcal{P}p_1)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)= - (\mathcal{P}p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2), + (\powf p_1)^\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_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2), \end{gather*} and \begin{gather*} - (\mathcal{P}p_2)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)= - (\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2). + (\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 $(\mathcal{P}p_1)^\dagger\comp\delta(x_1,x_2)=\alpha(x_1)$. So, $(\mathcal{P}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 $(\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=\alpha(x_2)$.\qed + 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 \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. @@ -1886,14 +1887,14 @@ At the moment we have limited the discussion to the category of sets and we are \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& R \& Y\\ - {\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}Y} + {\powf X} \& {\subseteq;(\powf R)^\dagger;\subseteq} \& {\powf Y} \arrow["\alpha"', from=1-1, to=2-1] \arrow["{p_1}"', from=1-2, to=1-1] \arrow["{p_2}", from=1-2, to=1-3] \arrow["\sigma", dashed, from=1-2, to=2-2] \arrow["\beta", from=1-3, to=2-3] - \arrow["{{\mathcal{P}p_1}_\subseteq}", from=2-2, to=2-1] - \arrow["{{\mathcal{P}p_2}_\subseteq}"', from=2-2, to=2-3] + \arrow["{{\powf p_1}_\subseteq}", from=2-2, to=2-1] + \arrow["{{\powf p_2}_\subseteq}"', from=2-2, to=2-3] \end{tikzcd} \end{equation*} It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\beta(x_2))$. @@ -1901,7 +1902,7 @@ But $\sigma'$ in the following diagram is not unique: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& R \& Y \\ - {\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}Y} + {\powf X} \& {(\powf R)^\dagger} \& {\powf Y} \arrow["\alpha"', from=1-1, to=2-1] \arrow["\subseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2] \arrow["{p_1}"', from=1-2, to=1-1] @@ -1909,16 +1910,16 @@ But $\sigma'$ in the following diagram is not unique: \arrow["{\sigma'}", from=1-2, to=2-2] \arrow["\beta", from=1-3, to=2-3] \arrow["\subseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3] - \arrow["{{\mathcal{P}p_1^\dagger}}", from=2-2, to=2-1] - \arrow["{{\mathcal{P}p_2^\dagger}}"', from=2-2, to=2-3] + \arrow["{{\powf p_1^\dagger}}", from=2-2, to=2-1] + \arrow["{{\powf p_2^\dagger}}"', from=2-2, to=2-3] \end{tikzcd} \end{equation*} -Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\delta\c(\mathcal{P}R)^\dagger\to\subseteq;(\mathcal{P}R)^\dagger;\subseteq$ that $\sigma=\delta\comp\sigma'$, i.e., the following diagram commutes: +Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\delta\c(\powf R)^\dagger\to\subseteq;(\powf R)^\dagger;\subseteq$ that $\sigma=\delta\comp\sigma'$, i.e., the following diagram commutes: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& R \& Y \\ - {\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}Y} \\ - {\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}Y} + {\powf X} \& {(\powf R)^\dagger} \& {\powf Y} \\ + {\powf X} \& {\subseteq;(\powf R)^\dagger;\subseteq} \& {\powf Y} \arrow["\alpha"', from=1-1, to=2-1] \arrow["{p_1}"', from=1-2, to=1-1] \arrow["{p_2}", from=1-2, to=1-3] @@ -1927,11 +1928,11 @@ Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\d \arrow["id"', from=2-1, to=3-1] \arrow["\delta", from=2-2, to=3-2] \arrow["id", from=2-3, to=3-3] - \arrow["{{\mathcal{P}p_1}_\subseteq}", from=3-2, to=3-1] - \arrow["{{\mathcal{P}p_2}_\subseteq}"', from=3-2, to=3-3] + \arrow["{{\powf p_1}_\subseteq}", from=3-2, to=3-1] + \arrow["{{\powf p_2}_\subseteq}"', from=3-2, to=3-3] \end{tikzcd} \end{equation*} -To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagger)\times R)+(\mathcal{P}R)^\dagger$ and $u\c((\mathcal{P}R^\dagger)\times R)+(\mathcal{P}R)^\dagger\to\subseteq;(\mathcal{P}R)^\dagger;\subseteq$ and then we define $\delta=u\comp c$. Here are the definitions for $c$ and $u$: +To define $\delta$, we define $c\c(\powf R^\dagger)\to((\powf R^\dagger)\times R)+(\powf R)^\dagger$ and $u\c((\powf R^\dagger)\times R)+(\powf R)^\dagger\to\subseteq;(\powf R)^\dagger;\subseteq$ and then we define $\delta=u\comp c$. Here are the definitions for $c$ and $u$: \begin{gather*} c(w)= \begin{cases} @@ -2102,6 +2103,23 @@ The above translation seems to be true in a more general case, where $\spa$ and \begin{proof} (Completeness): We show $\relar$-similarity with $r_s$ and $\hat{\relar}$-similarity with $r_{\hat{s}}$. Also, we show the behabioural equivalence with $r_b$. Since \end{proof} + +Assuming that $\relar$-similarity is complete, does not guarantee that $\hat{\relar}$-similarity is sound and complete. We give a counter-example. Assuming that $\relar$ is a $\powf$-relator that takes $r\c X\rto Y$ to $\powf X\times \powf Y$, then $\hat{\relar} r= \powf X\times\powf Y$ as well. It means that for every coalgebras $(X,\alpha)$, $(Y,\beta)$, $\hat{\relar}$-similarity is equal to $X\times Y$, which is rare to be equal to behavioural equivalence. For example, if we take $X=\{x_1,x_2\}$ and $Y=\{y_1,y_2,y_3\}$, and we define $\alpha$ and $\beta$ as +\begin{gather*} + \alpha(x)= + \begin{cases} + \{x_1,x_2\} & x=x_1 \\ + \{x_2\} & x=x_2 + \end{cases} + \intertext{and} + \beta(y)= + \begin{cases} + \{y_3\} & y=y_1 \\ + Y & y=y_2\\ + \emptyset & y=y_3 + \end{cases} +\end{gather*} +then at least $(x_1,y_3)$ is not in the behavioural equivalence, while it is in $\hat{\relar}$-similarity. \end{document}