the homework is under progress
This commit is contained in:
partowp
+61
-2
@@ -936,9 +936,68 @@ We do not know if this definition exists anywhere.
|
||||
\end{rem}
|
||||
\todo{Discuss 4 versions of bisimulation (with witness/without witness, for relations/for spans). Which are equivalent? Which do not make sense?}
|
||||
|
||||
\todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}
|
||||
|
||||
\todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}\\
|
||||
--------------------------------------------------------------
|
||||
\begin{definition}[Aczel-Mendler Bisimulation]
|
||||
In an arbitrary category $\BC$, a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{Aczel-Mendler bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\spa(\BC)$ 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)$.
|
||||
\end{definition}
|
||||
%
|
||||
\begin{definition}[Relation Lifting]
|
||||
Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, where the following diagram commutes:
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
\rel(\BC) \&\& \rel(\BC) \\
|
||||
{\BC\times\BC} \&\& {\BC\times\BC}
|
||||
\arrow["{\rel(F)}", from=1-1, to=1-3]
|
||||
\arrow["{U}"',from=1-1, to=2-1]
|
||||
\arrow["{U}",from=1-3, to=2-3]
|
||||
\arrow["{F\times F}"', from=2-1, to=2-3]
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
\end{definition}
|
||||
\begin{definition}[Abstract Relational Bisimulation]
|
||||
In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{abstract relational 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{\rel(F)p_1}{\leftarrow} \rel(F)R \stackrel{\rel(F)p_2}{\to}FY)$.
|
||||
\end{definition}
|
||||
The given definition is highly abstract. There is a relation lifting that abstracts Barr-relators that are known to be well-behaved relators, and it also gives an interesting notion of bisimulation, called \emph{Hermida-Jacobs bisimulation}.
|
||||
%
|
||||
The lifting is using the image factorization in regular categories. %\ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.}
|
||||
%
|
||||
%\begin{equation*}
|
||||
% \begin{tikzcd}[ampersand replacement=\&]
|
||||
% R \& {R^\dagger} \&\& {X\times X}
|
||||
% \arrow["{e_R}"', two heads, from=1-1, to=1-2]
|
||||
% \arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
|
||||
% \arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
|
||||
% \end{tikzcd}
|
||||
%\end{equation*}
|
||||
For a regular category $\BC$, we define a functor of type $(-)^\clubsuit\c\spa(\BC)\to\rel(\BC)$. It takes every span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the image of its legs:
|
||||
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
R \& {R^\dagger} \&\& {X\times Y}
|
||||
\arrow["{e_R}"', two heads, from=1-1, to=1-2]
|
||||
\arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
|
||||
\arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
Also, for every functor $F\c\BC\to\BC$ we have a trivial lifting to $\spa(\BC)$ that takes every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$, and every morphism $(f,g,w)$ to $(Ff,Fg,Fw)$, and we show it with $\spa(F)$. Since $\rel(\BC)$ is a subcategory of $\spa(\BC)$, we have an inclusion functor $I\c\rel(\BC)\to\spa(\BC)$ as well.
|
||||
So, given a functor $F\c\BC\to\BC$ we define its lifting $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ as $(F-)^\dagger=(\spa(F)I-)^\clubsuit$. $(F-)^\dagger$ takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation:
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
\& {(FR)^\dagger} \& \\
|
||||
FX \&\& FY \\
|
||||
\& {FX\times FY}
|
||||
\arrow["{{{(Fp_1)^\dagger}}}"', from=1-2, to=2-1]
|
||||
\arrow["{{{(Fp_2)^\dagger}}}", from=1-2, to=2-3]
|
||||
\arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2]
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
%
|
||||
\begin{definition}[Hermida-Jacobs Bisimulation]
|
||||
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}
|
||||
\subsection{Coalgebraic Bisimulation in Set}
|
||||
The have two more notions for coalgebraic bisimulation in $\Set$, that is to define them in $\spa_a$ and $\rel_a$.
|
||||
%
|
||||
\section{Coalgebraic Simulation}
|
||||
We show the category of preorders with monotone functions between them with $\preord$. In the diagrams, any arrow that shows a functor, but does not have a label is showing a forgetful functor. Also, we use $\rel$ to refer to the category of binary relations. Assuming $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and $S\in\obj(\rel)$ and $S\subseteq Y_1\times Y_2$, then a morphism $f\c R\to S$ in this category is the pair $(f_1,f_2)$ of morhpisms in $\Set$, where, $f_1\c X_1\to Y_1$ and $f_2\c X_2\to Y_2$, and for each $(x_1,x_2)\in R$ we have $(f_1(x_1),f_2(x_2))\in S$. Also, we show projections of $R\in\obj(\rel)$ with $p_1$ and $p_2$ that are morphisms in $\Set$.
|
||||
|
||||
Reference in New Issue
Block a user