draft polished
This commit is contained in:
partowp
parent
e473cfeabb
commit
97250da9dd
@ -1827,34 +1827,63 @@ Abstractly, first we define an operation that we need on morphisms that takes tw
|
||||
We have $(Fp_1)^\dagger\comp\sigma$.
|
||||
\end{proof}
|
||||
\section{Relators}
|
||||
In this section we want to discuss relators. We set $\rel$ to be the category that has sets as objects and binary relations as morphisms.
|
||||
We answer the question that why there can be multiple simulation structures based on~\autoref{def:sim}.
|
||||
\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:
|
||||
\begin{gather*}
|
||||
\appr;(FR_1)^\dagger;\appr\quad\cap\quad\appr^\op;(FR_2)^\dagger;\appr^\op\qquad\subseteq\qquad(F(R_1\cap R_2))^\dagger
|
||||
\end{gather*}
|
||||
We need the case that $R_1=R_2$, and we refer to it with $R$. So, we need to have
|
||||
\begin{gather*}
|
||||
\appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op\qquad\subseteq\qquad(FR)^\dagger.
|
||||
\end{gather*}
|
||||
Assuming $(x_1,x_2)\quad\in\quad \appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op$ means that there exist $(u,v),(u',v')\in (FR)^\dagger$, such that $x_1\appr u$, $u'\appr x_1$, $v\appr x_2$, and $x_2\appr v'$. We can also use the symmetry of $R$, and then from $(x_1,x_2)\in R$ derive that there exist $(w,z),(w',z')$ such that $x_1\appr z$, $z'\appr x_1$, $w\appr x_2$, and $x_2\appr w'$. But then how can we derive $(x_1,x_2)\in (FR)^\dagger$?
|
||||
|
||||
\todo{Investigate more! Can it be doable really?!}
|
||||
\subsection{Uniqueness of the witness in Hughes-Jacobs definition}
|
||||
In this section we set $\rel$ to be the category that has sets as objects and binary relations as morphisms.
|
||||
We answer the question that why there can be multiple simulation witnesses based on~\autoref{def:sim}, while for the same relation, there is only one witness according to Hughes-Jacobs simulation.
|
||||
\begin{definition}[Hughes-Jacobs Simulation]
|
||||
For a functor $F$, and a poset $\appr$ over $F$ a HuJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to (Fr)^\dagger$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \& R \& Y \\
|
||||
{FX} \& {\appr;(FR)^\dagger;\appr} \& {FY}
|
||||
\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", from=1-2, to=2-2]
|
||||
\arrow["\beta", from=1-3, to=2-3]
|
||||
\arrow["{{Fp_1}_\appr}", from=2-2, to=2-1]
|
||||
\arrow["{{Fp_2}_\appr}"', from=2-2, to=2-3]
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
\end{definition}
|
||||
At the moment we have limited the discussion to the category of sets and we are talking about the powerset functor. We know that $\sigma$ is unique in the following diagram:
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \& R \& X \\
|
||||
{\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}X}
|
||||
X \& R \& Y\\
|
||||
{\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}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["\alpha", from=1-3, to=2-3]
|
||||
\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]
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\alpha(x_2))$.
|
||||
It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\beta(x_2))$.
|
||||
But $\sigma'$ in the following diagram is not unique:
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \& R \& X \\
|
||||
{\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}X}
|
||||
X \& R \& Y \\
|
||||
{\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}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]
|
||||
\arrow["{p_2}", from=1-2, to=1-3]
|
||||
\arrow["{\sigma'}", from=1-2, to=2-2]
|
||||
\arrow["\alpha", from=1-3, to=2-3]
|
||||
\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]
|
||||
@ -1863,17 +1892,17 @@ But $\sigma'$ in the following diagram is not unique:
|
||||
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:
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \& R \& X \\
|
||||
{\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}X} \\
|
||||
{\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}X}
|
||||
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}
|
||||
\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'}", from=1-2, to=2-2]
|
||||
\arrow["\alpha", from=1-3, to=2-3]
|
||||
\arrow["\beta", from=1-3, to=2-3]
|
||||
\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["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]
|
||||
\end{tikzcd}
|
||||
@ -1888,26 +1917,41 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
|
||||
u(\inl w,(x_1,x_2))=(\alpha(x_1),\alpha(x_2))\\
|
||||
u(\inr w)=w
|
||||
\end{gather*}
|
||||
\subsection{Symmetric simulation}
|
||||
\begin{definition}[Relator]
|
||||
Assuming $F$ is a functor on $\Set$, a $F$-relator or simply a relator $\relar$ is a monotone map that sends a morphism of $\Rel$ that is a relation $X\rto Y$ to $FX\rto FY$.
|
||||
\end{definition}
|
||||
|
||||
\begin{definition}[Hermida-Jacobs Simulation]
|
||||
For a relator $\relar$ for a functor $F$, and a poset $\appr$ over $F$ a HJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ such that the following diagram commutes ($;$ is the relation composition):
|
||||
\begin{equation*}
|
||||
For a relator $\relar$ on a functor $F$, and a poset $\appr$ over $F$ a HJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
|
||||
\begin{equation*}\label{def:hej-sim}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
X \& R \& X \\
|
||||
{FX} \& {\appr;(FR)^\dagger;\appr} \& {FX}
|
||||
X \& R \& Y \\
|
||||
{FX} \& {\appr;\relar r;\appr} \& {FY}
|
||||
\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", from=1-2, to=2-2]
|
||||
\arrow["\alpha", from=1-3, to=2-3]
|
||||
\arrow["\beta", from=1-3, to=2-3]
|
||||
\arrow["{{Fp_1}_\appr}", from=2-2, to=2-1]
|
||||
\arrow["{{Fp_2}_\appr}"', from=2-2, to=2-3]
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
\end{definition}
|
||||
\begin{prop}
|
||||
Hughes-Jacobs simulation is an instance of HJ-simulation, where $\relar r=(Fr)^\dagger$.
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
We need to show that $(F-)^\dagger$ is a relator, we need to show that
|
||||
|
||||
\todo{Finish.}
|
||||
\end{proof}
|
||||
\begin{prop}
|
||||
For an arbitrary relator $\relar$ on a functor $F$, if a relation $r$ is a simulation, the witness is unique.
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
It only relies on the fact that ${Fp_1}_\appr$ and ${Fp_2}_\appr$ in~\eqref{def:hej-sim} are jointly monic.\qed
|
||||
\end{proof}
|
||||
\end{document}
|
||||
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user