bluh
This commit is contained in:
partowp
+37
-23
@@ -1001,13 +1001,25 @@ The given definition is highly abstract. There is a relation lifting that abstra
|
||||
In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a \emph{Hermida-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.
|
||||
\end{definition}
|
||||
%
|
||||
\begin{prop}\label{prop:HeJ-AM}
|
||||
In a regular category $\BC$ with the axiom of choice, every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is an Aczel-Mendler bisimulation.
|
||||
\begin{prop}
|
||||
For a regular category $\BC$ with the axiom of choice, assuming that in $\rel(\BC)$, there is a morphism $(g_1,g_2,w)$ from an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ to $(Y_1 \stackrel{q^\dagger_1}{\leftarrow} S^\dagger \stackrel{q^\dagger_2}{\to}Y_2)$, then there exist a morphism $(g_1,g_2,v)$ from $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ to $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$.
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
\todo{Finish.}
|
||||
Having the axiom of choice in a regular category $\BC$ means that for $e_S\c S\to S^\dagger$ there exist a section $s$. We define $v=s\comp w$, then for $i\in\{1,2\}$ we have:
|
||||
\begin{align*}
|
||||
q_i\comp v&\\
|
||||
=&q^\dagger_i\comp e_s\comp v\\
|
||||
=&q^\dagger_i\comp e_s\comp s\comp w\\
|
||||
=&q^\dagger_i\comp w\\
|
||||
=&g_i\comp p_i
|
||||
\end{align*}
|
||||
\qed
|
||||
\end{proof}
|
||||
%
|
||||
\begin{cor}\label{cor:HeJ-AM}
|
||||
For a regular category $\BC$ with the axiom of choice, every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is an Aczel-Mendler bisimulation.
|
||||
\end{cor}
|
||||
%
|
||||
\subsection{Coalgebraic Bisimulation in Set}
|
||||
We have two more notions for coalgebraic bisimulation in $\Set$, that is to define them in $\spa_a$ and $\rel_a$, respectively called \emph{span-based bisimulation} and \emph{relator-based bisimulation}.
|
||||
%
|
||||
@@ -1035,7 +1047,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
|
||||
(3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. Assuming $(x,y)\in R$ there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\qed
|
||||
\end{proof}
|
||||
\begin{cor}
|
||||
Recalling~\autoref{prop:HeJ-AM}, all the four introduced definitions for bisimulation (\autoref{fig:anonymous_onymous}) are equivalent under the axiom of choice.
|
||||
Recalling~\autoref{cor:HeJ-AM}, all the four introduced definitions for bisimulation (\autoref{fig:anonymous_onymous}) are equivalent under the axiom of choice.
|
||||
\end{cor}
|
||||
\begin{figure}[t]
|
||||
\centering
|
||||
@@ -2513,20 +2525,22 @@ We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined
|
||||
\end{cases}\qquad
|
||||
\begin{tikzpicture}[scale=0.1]
|
||||
\tikzstyle{every node}+=[inner sep=0pt]
|
||||
\draw [black] (23.8,-25.2) circle (3);
|
||||
\draw (23.8,-25.2) node {$1$};
|
||||
\draw [black] (42.4,-25.2) circle (3);
|
||||
\draw (42.4,-25.2) node {$2$};
|
||||
\draw [black] (33,-34.6) circle (3);
|
||||
\draw (33,-34.6) node {$3$};
|
||||
\draw [black] (22.477,-22.52) arc (234:-54:2.25);
|
||||
\fill [black] (25.12,-22.52) -- (26,-22.17) -- (25.19,-21.58);
|
||||
\draw [black] (41.077,-22.52) arc (234:-54:2.25);
|
||||
\fill [black] (43.72,-22.52) -- (44.6,-22.17) -- (43.79,-21.58);
|
||||
\draw [black] (26.8,-25.2) -- (39.4,-25.2);
|
||||
\fill [black] (39.4,-25.2) -- (38.6,-24.7) -- (38.6,-25.7);
|
||||
\draw [black] (40.28,-27.32) -- (35.12,-32.48);
|
||||
\fill [black] (35.12,-32.48) -- (36.04,-32.27) -- (35.33,-31.56);
|
||||
\draw [black] (25.6,-20.9) circle (3);
|
||||
\draw (25.6,-20.9) node {$1$};
|
||||
\draw [black] (44.9,-20.9) circle (3);
|
||||
\draw (44.9,-20.9) node {$2$};
|
||||
\draw [black] (34.5,-32) circle (3);
|
||||
\draw (34.5,-32) node {$3$};
|
||||
\draw [black] (24.277,-18.22) arc (234:-54:2.25);
|
||||
\fill [black] (26.92,-18.22) -- (27.8,-17.87) -- (26.99,-17.28);
|
||||
\draw [black] (43.577,-18.22) arc (234:-54:2.25);
|
||||
\fill [black] (46.22,-18.22) -- (47.1,-17.87) -- (46.29,-17.28);
|
||||
\draw [black] (33.177,-29.32) arc (234:-54:2.25);
|
||||
\fill [black] (35.82,-29.32) -- (36.7,-28.97) -- (35.89,-28.38);
|
||||
\draw [black] (42.85,-23.09) -- (36.55,-29.81);
|
||||
\fill [black] (36.55,-29.81) -- (37.46,-29.57) -- (36.73,-28.89);
|
||||
\draw [black] (28.6,-20.9) -- (41.9,-20.9);
|
||||
\fill [black] (41.9,-20.9) -- (41.1,-20.4) -- (41.1,-21.4);
|
||||
\end{tikzpicture}
|
||||
\end{gather*}
|
||||
$\sigma$ is defined as below:
|
||||
@@ -2539,9 +2553,9 @@ This counter-example also works as a counter-example for Hughes-Jacobs definitio
|
||||
|
||||
The mentioned ordering is not liftable. Assuming $h\in\Hom(\nats,\powfi \nats)$, $g\c \nats\to \nats$, and $k\in\Hom(\nats,\powfi \nats)$, and they are defined for every $n$ in $\nats$ as $h(n)=\{2\times n\}$, $g(n)=3\times n$, and $k(n)=\{n\}$, then $|h(n)|=|\powfi g(k(n))|=1$ that means $h\appr\powfi g\comp k$ is satisfied, but there is no $k'$ that $h=\powfi g\comp k$ because we can never have $h(1)=\powfi g\comp k'(1)$, as assuming $k'(1)=\{n\}$, and $n$ must be a natural number, then we should have $2=3\times n$ that is impossible.
|
||||
|
||||
It is the same for HJ-simulation and HJ-bisimulation. We define $\sigma^\dagger\c R\to (\powf R)^\dagger$ as
|
||||
It is the same for HJ-simulation and HJ-bisimulation. We define $\sigma^\dagger\c R\to (\powf R)^\dagger$ as:
|
||||
\begin{gather*}
|
||||
\sigma^\dagger(w)=\{(\{1,2\},\{1,2\})\}.
|
||||
\forall w\in R,\quad\sigma^\dagger(w)=(\{1,2\},\{1,2\})
|
||||
\end{gather*}
|
||||
Indeed, $\sigma^\dagger$ is a witness for $R$ to be an HJ-simulation, but it is not a witness for $R$ to be an HJ-bisimulation. Similar to the case for AM-bisimulation, we can not have a witness for $R$ to be an HJ-bisimulation.
|
||||
\end{example}
|
||||
@@ -2555,11 +2569,11 @@ Indeed, $\sigma^\dagger$ is a witness for $R$ to be an HJ-simulation, but it is
|
||||
\begin{gather*}
|
||||
\forall w\in R,\quad\sigma(w)=\{(1,1),(2,1),(3,1)\}
|
||||
\end{gather*}
|
||||
Additionally we define $\sigma^\dagger$ as follows as a witness for $R$ to be an HJ-simulation:
|
||||
Additionally, we define $\sigma^\dagger$ as follows as a witness for $R$ to be an HJ-simulation:
|
||||
\begin{gather*}
|
||||
\sigma^\dagger(w)=\{(\{1,2,3\},\{1\})\}
|
||||
\forall w\in R,\quad\sigma^\dagger(w)=(\{1,2,3\},\{1\})
|
||||
\end{gather*}
|
||||
Although $R$ is not an AM-bisimulation not an HJ-bisimulation.
|
||||
However, $R$ is not an AM-bisimulation nor an HJ-bisimulation regardless of the choice for the order structure.
|
||||
\end{example}
|
||||
|
||||
\subsection{From Symmetric Simulation To Bisimulation (Aczel-Mendler)}
|
||||
|
||||
Reference in New Issue
Block a user