pouya/coalgebraic-simulation
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Merge branch 'master' of https://git.wlog.site/pouya/coalgebraic-simulation

Browse Source
This commit is contained in:
Pouya
2026-08-04 03:26:05 +01:00
parent 4f6689a096 8c1054256a
commit d2a5e4d861
20 changed files with 1801 additions and 79 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+257 -79
View File
@@ -292,6 +292,7 @@
\newcommand{\spto}{\mathrel{\tikz{\draw[-{Stealth}] (0.0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
\newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0.04,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);\draw (0.04,0) -- (0,-0.07);\draw (0.04,0) -- (0,0.07);}}}
\newcommand{\powf}{\mathcal{P}}
\newcommand{\powfi}{\mathcal{P}_{\mathsf{inj}}}
\newcommand{\sappr}{\sqsupseteq}
\newcommand{\Dom}{\mathsf{Dom}}
@@ -303,6 +304,7 @@
}%
}%
}
\newcommand{\sub}{\mathcal{S}}
\newcommand{\bba}{
@@ -404,12 +406,12 @@ We want to say that a natural order structure entails an order over a functor de
\end{proof}
\begin{definition}[Liftable Order Structure]\label{def:liftable-ord}
A \emph{liftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr Fg\comp k$ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k'\appr k$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
A \emph{liftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr Fg\comp k$ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k'\appr k$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.\ppnote{I added the surjection condition on $g$.}
\end{definition}
\begin{definition}[Coliftable Order Structure]\label{def:coliftable-ord}
A \emph{coliftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
A \emph{coliftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
\end{definition}
\begin{lemma}\label{lem:set-ord-str}
@@ -427,13 +429,54 @@ We want to say that a natural order structure entails an order over a functor de
The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures.
\end{remark}
\begin{lemma}\label{lem:liftable}
Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, then for every surjective $f\in\Hom(X,FY)$ we have:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$
\item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$
\end{enumerate}
\end{lemma}
\begin{proof}
$(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$.
Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\sappr)}s$.
$(II)$ Basically, by definition of $\op$ and relation composition we have
\begin{gather*}
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
\end{gather*}
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
\end{proof}
\begin{lemma}\label{lem:coliftable}
Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $f\in\Hom(X,FY)$ we have:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item $Ff\comp\appr\quad=\quad\appr\comp Ff$
\item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$
\end{enumerate}
\end{lemma}
\begin{proof}
$(I)$ Assuming $t\mathrel{(Ff\comp\appr)} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is coliftable, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{(\appr\comp Ff)} x$.
Assuming $t\mathrel{(\appr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:coliftable-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
$(II)$ Basically, by definition of $\op$ and relation composition we have
\begin{gather*}
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
\end{gather*}
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
\end{proof}
\subsection{Powerset Functor}
In this section we discuss set inclusion as an ordering over the powerset functor.
\begin{prop}\label{prop:lift-gen-func}
For a functor $F\c\Set\to\Set$, a functor of the form $\powf F$, where $\powf$ is the powerset functor, the set inclusion is a liftable order structure.
\end{prop}
\begin{proof}
Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf FZ)$, $k\in\Hom(1,\powf FY)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf Fg(k)$, we define $k'\in\powf FY$ that that $k'=\{y\mid Fg(y)\in h\}$. We show that $k'\subseteq k$ and $\powf Fg(k')=h$.
Assuming $y\in k'$ we have $Fg(y)\in h$. Since $h\subseteq \powf Fg(k)$ we have $Fg(y)\in\powf Fh(h)$, so we have $y\in k$ that means $k'\subseteq k$.
Assuming $y\in k'$ we have $Fg(y)\in h$. Since $h\subseteq \powf Fg(k)$ we have $Fg(y)\in\powf Fg(k)$, so we have $y\in k$ that means $k'\subseteq k$.
Assuming $z\in\powf Fg(k')$, then there exists $y'\in k'$ that $z=Fg(y')$, so $z\in h$ and $\powf Fg(k')\subseteq h$.
@@ -473,43 +516,106 @@ We want to say that a natural order structure entails an order over a functor de
We could not prove a general statement like~\autoref{prop:lift-gen-func} for coliftability even if the surgectivity of $g$ remains in the definition. Perhaps more conditions on $F$ in~\autoref{prop:lift-gen-func} are needed. Conditions like preserving surjections and unions that make the statement extremely limited, and meaningless.
\end{remark}
\begin{lemma}\label{lem:liftable}
Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, then for every $f\in\Hom(X,FY)$ we have:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$
\item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$
\end{enumerate}
\end{lemma}
\subsection{Maybe Functor}
The order structure that we can define for this functor is that for sets $X$ and $Y$, and functions $f,g\c X\to Y+1$ we have $f\appr g$ whenever $\Dom(f)\subseteq\Dom(g)$, and for every $x\in\Dom(f)$ we have $f(x)=g(x)$ ($\Dom(f)$ is the domain of a function $f$).
\begin{prop}\label{prop:maybe-lif}
The order structure on the set-functor $FX=X+1$ is a liftable order.
\end{prop}
% By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
% \begin{itemize}
% \item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$.
% \item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed
% \end{itemize}
\begin{proof}
<<<<<<< HEAD
$(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$.
Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\sappr)}s$.
$(II)$ Basically, by definition of $\op$ and relation composition we have
=======
Assuming that $h\in\Hom(X,Z+1)$, $g\c Y\to Z$, $k\in\Hom(X,Y+1)$, such that $h\appr (g+1)\comp k$. We define $k'\in\Hom(X,Y+1)$ as follows:
>>>>>>> 8c1054256a4ef67f109cc6d30f3d3bd050e936cb
\begin{gather*}
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
k'(x)=
\begin{cases}
\bot&x\notin\Dom(h)\\
k(x)&x\in\Dom(h)
\end{cases}
\end{gather*}
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
We have $\Dom((g+1)\comp k')=\Dom(k')$ and $\Dom(k')=\Dom(h)$, so we have $\Dom((g+1)\comp k')=\Dom(h)$. If $x\in\Dom(h)$, then $h(x)=(g+1)\comp k(x)$ and $(g+1)\comp k(x)=(g+1)\comp k'(x)$, so we have $h(x)=(g+1)\comp k'(x)$. So, we have $h=(g+1)\comp k'$. Additionally, $\Dom(k')\subseteq\Dom(k)$, and for every $x\in \Dom(k')$, we have $k'(x)=k(x)$, so we have $k'\appr k$. \qed
\end{proof}
\begin{lemma}\label{lem:coliftable}
Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $f\in\Hom(X,FY)$ we have:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item $Ff\comp\appr\quad=\quad\appr\comp Ff$
\item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$
\end{enumerate}
\end{lemma}
\begin{prop}\label{prop:maybe-colif}
The order structure on the set-functor $FX=X+1$ is a coliftable order.
\end{prop}
\begin{proof}
$(I)$ Assuming $t\mathrel{(Ff\comp\appr)} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is coliftable, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{(\appr\comp Ff)} x$.
Assuming $t\mathrel{(\appr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:coliftable-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
$(II)$ Basically, by definition of $\op$ and relation composition we have
By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $Fg(k)\appr h$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k\appr k'$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
\begin{itemize}
\item $Fg(k)=h$: In this case we take $k'=k$, and then we have $Fg(k')=h$.
\item $Fg(k)=\bot$: It entails that $k=\bot$. We either have $h=\bot$ or $h\in Y$. If $h=\bot$ then we take $k'=k$, and we are done. If $h\in Y$, then by the surjectivity of $g$, there exists $k'$ such that $g(k')=h$ that entails $Fg(k')=h$ as well.\qed
\end{itemize}
\end{proof}
\subsection{Subdistribution Functor}
The subdistribution functor $\sub\c\Set\to\Set$ is defined as $\sub X=\{\mu\c X\to[0,1]\mid \sum_{x\in X}\mu(x)\}$ on objects, and for $\sub f\c \sub X\to\sub Y$, we have
\begin{gather*}
\sub f(\mu)=y\mapsto\sum_{x\in f^{\mone}(y)}\mu(x),
\end{gather*}
on morphisms. We define the ordering on $\sub X$ for $\mu_1,\mu_2\in \sub X$ as
\begin{gather*}
\mu_1\appr \mu_2\iff \forall x\in X, \mu_1(x)\leq\mu_2(x).
\end{gather*}
The definition derives the ordering on morphisms of each hom-set $\Hom(X,\sub Y)$ as usual in $\Set$.
\begin{prop}
The pointwise ordering on $\sub$ is a liftable ordering.
\end{prop}
\begin{proof}
Assuming that $\mu\in SX$, $g\c X\to Y$ is surjective, $\nu\in SY$, and $\nu\appr \sub g(\mu)$, then there exists $\mu'\in \sub X$ such that $\mu'\appr \mu$ and $\sub g(\mu')=h$.\\
The assumption $\nu \appr Sg(\mu)$ means that for every $y \in Y$,
\begin{gather*}
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
\nu(y) \leq Sg(\mu)(y) = \sum_{x \in g^{\mone}(y)} \mu(x).
\end{gather*}
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
We construct $\mu'$ as follows:
\begin{gather*}
\mu'(x)=
\begin{cases}
\frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)&Sg(\mu)(g(x))\neq 0\\
0&Sg(k)(g(x))= 0
\end{cases}
\end{gather*}
First, we need to prove that $\mu'$ is a subdistribution.
For every $x \in X$, $\mu'(x) \ge 0$. We have:
\begin{align*}
\sum_{x \in X} \mu'(x)&\\
=& \sum_{x \in X} \frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)&(Sg(\mu)(g(x))\neq 0)\\
=& \sum_{y \in Y} \sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)&(Sg(\mu)(y)\neq 0)\\
=& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)&(Sg(\mu)(y)\neq 0)\\
=& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)&(Sg(\mu)(y)\neq 0)\\
=& \sum_{y \in Y} \nu(y)\\
\leq& 1
\end{align*}
As for every $x\in X$ that $Sg(\mu)(g(x))=0$, $\mu'(x)=0$, it does not have effect the inequality. Thus $\mu'$ is a subdistribution. Now, we prove $Sg(\mu') = \nu$.
For any $y \in Y$, we have:
\begin{align*}
Sg(\mu')(y)&\\
= &\sum_{x \in g^{\mone}(y)} \mu'(x)\\
= &\sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)&(Sg(\mu)(y)\neq 0)\\
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)&(Sg(\mu)(y)\neq 0)\\
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)&(Sg(\mu)(y)\neq 0)\\
= &\mu(y)
\end{align*}
(If $Sg(\mu)(y) = 0$, then $\nu(y) = 0$, and the sum is $0$ as well, so the equality still holds.) \\
Now, we are left to prove that $\mu'\appr\mu$.
For every $x\in X$, have the following cases:
\begin{itemize}
\item $Sg(\mu)(g(x))= 0$: We have $\mu'(x)=0$, and obviously $\mu'\appr\mu$.
\item $Sg(\mu)(g(x))\neq 0$: We have $\frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)$, and since $\nu\appr Sg(\mu)$ then we have:
\begin{align*}
&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\leq 1\\
\Rightarrow&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\comp \mu(x)\leq \mu(x)
\end{align*}\qed
\end{itemize}
\end{proof}
@@ -1448,6 +1554,35 @@ We show this relation with $F_\rel(R,X)$.
As the mentioned property is equivalent with $\sigma$ being a bisimulation, and bisimulation is unique, then $\sigma_1=\sigma_2$.
\end{proof}
%
\begin{prop}
Assuming that the ordering on the functor $F$ is natural, and gives posets, given witness $\sigma$ for a symmetric object $R$ to be an HJ-simulation, if $(Fs)^\dagger\comp\sigma=\sigma\comp s$, then $\sigma$ is a witness for $R$ to be an $HJ$-bisimulation.
\end{prop}
\begin{proof}
Since $\sigma$ is a witness that $R$ is an $HJ$-simulation we have
\begin{gather*}
\alpha\comp p_1\appr (Fp_1)^\dagger\comp\sigma,\\
(Fp_2)^\dagger\comp\sigma\appr\alpha\comp p_2.
\end{gather*}
So, we have:
\begin{align*}
\alpha\comp p_1\appr (Fp_1)^\dagger\comp\sigma&\\
\Rightarrow&\alpha\comp p_1\comp s\appr (Fp_1)^\dagger\comp\sigma\comp s&\by{naturality of $\appr$}\\
\Rightarrow&\alpha\comp p_1\comp s\appr (Fp_1)^\dagger\comp (Fs)^\dagger\comp\sigma&\by{\eqref{eq:diag-sym-rel}}\\
\Rightarrow&\alpha\comp p_2\appr (Fp_1)^\dagger\comp (Fs)^\dagger\comp\sigma&\by{assumption}\\
\Rightarrow&\alpha\comp p_2\appr (Fp_2)^\dagger\comp\sigma&\by{\eqref{eq:diag-sym-rel}}\\
\Rightarrow&\alpha\comp p_2= (Fp_2)^\dagger\comp\sigma&\by{anti symmetry of $\appr$}
\end{align*}
Similarly we have:
\begin{align*}
(Fp_2)^\dagger\comp\sigma\appr\alpha\comp p_2&\\
\Rightarrow&(Fp_2)^\dagger\comp\sigma\comp s\appr\alpha\comp p_2\comp s&\by{naturality of $\appr$}\\
\Rightarrow&(Fp_2)^\dagger\comp(Fs)^\dagger\comp\sigma\appr\alpha\comp p_2\comp s&\by{\eqref{eq:diag-sym-rel}}\\
\Rightarrow&(Fp_2)^\dagger\comp(Fs)^\dagger\comp\sigma\appr\alpha\comp p_1&\by{assumption}\\
\Rightarrow&(Fp_1)^\dagger\comp\sigma\appr\alpha\comp p_1&\by{\eqref{eq:diag-sym-rel}}\\
\Rightarrow&(Fp_1)^\dagger\comp\sigma=\alpha\comp p_1&\by{anti symmetry of $\appr$}
\end{align*}\qed
\end{proof}
%
Now, we give a counter example of a symmetric relation on $\Set$ that is a simulation according to~\autoref{def:sim}, i.e, exists the morphism $\sigma$ that commutes laxly in~\eqref{eq:diag-lax-sim}, but $\sigma$ is not a coalgebraic bisimulation, although the relation that we give is clearly a bisimulation in the classic sense.
We set $R=\{(A,B),(B,A),(C_1,C_2),(C_2,C_1),(C'_2,C_2),(C_2,C'_2),(C_2,C_2)\}$, $F=\mathbf{Id}$, $\appr=\Delta\cup\{(C_1,C_2),(C_2,C'_2)\}$, and the coalgebra $\alpha$ is defined with the following set of reductions:
\begin{gather*}
@@ -2161,9 +2296,8 @@ 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.\\
\begin{example}\label{ex:sym-sim-bisim-count}
Assuming that the functor is the powerset endofunctor over the category of sets and injective maps. Let us call this functor $\powfi$. For every $X$, we define the order on $\powfi X$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder. Then we define the order over every $\Hom(X,\powfi Y)$ pointwise. We have chosen the category of sets with injective maps because we could not define a functor from $\Set$ to $\preord$ with the mentioned ordering.\\
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)=
@@ -2171,22 +2305,49 @@ We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined
\{1,2\} & x=1 \\
\{2,3\} & x=2\\
\{3\} & x=3
\end{cases}
\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);
\end{tikzpicture}
\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}
\sigma(w)=\{(1,2),(2,1)\}
\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)$.
This counter-example also works as a counter-example for Hughes-Jacobs definition of simulation. Actually, $\appr;(FR)^\dagger;\appr=\powf X\times \powf X$, so $R\subseteq \appr;(FR)^\dagger;\appr$ that means that $R$ is a simulation. Worth noting that they claim that their setting works for an arbitrary category. So, unlike their definition, in the context of the relator-based definitions that only work in $\Set$, this counter-example does not live.
This counter-example also works as a counter-example for Hughes-Jacobs definition of simulation. Actually, $\appr\comp(FR)^\dagger\comp\appr=\powf X\times \powf X$, so $R\subseteq( \appr\comp(FR)^\dagger\comp\appr)$ that means that $R$ is a simulation. Worth noting that they claim that their setting works for an arbitrary category. So, unlike their definition, in the context of the relator-based definitions that only work in $\Set$, this counter-example does not live.
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
\begin{gather*}
\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}
\begin{example}
In~\autoref{ex:sym-sim-bisim-count} we gave a counter-example with an ordering that gives preorders. Now, we slightly change the ordering so that it gives posets. We define $\appr$ as follows:
\begin{gather*}
A\appr B \iff
\end{gather*}
\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:
@@ -2330,39 +2491,8 @@ Now, we prove our main statement.
\end{cor}
Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor.
\subsection{Maybe Functor}
We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for sets $X$ and $Y$, and functions $f,g\c X\to Y+1$ we have $f\appr g$ whenever $\Dom(f)\subseteq\Dom(g)$, and for every $x\in\Dom(f)$ we have $f(x)=g(x)$ ($\Dom(f)$ is the domain of a function $f$).
Now, we prove that the given order on the maybe functor is liftable and coliftable.
\begin{lemma}\label{lem:maybe-lif}
The order structure on the set-functor $FX=X+1$ is a liftable order.
\end{lemma}
\begin{proof}
% By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
% \begin{itemize}
% \item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$.
% \item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed
% \end{itemize}
Assuming that $h\in\Hom(X,Z+1)$, $g\c Y\to Z$, $k\in\Hom(X,Y+1)$, such that $h\appr (g+1)\comp k$. We define $k'\in\Hom(X,Y+1)$ as follows:
\begin{gather*}
k'(x)=
\begin{cases}
\bot&x\notin\Dom(h)\\
k(x)&x\in\Dom(h)
\end{cases}
\end{gather*}
We have $\Dom((g+1)\comp k')=\Dom(k')$ and $\Dom(k')=\Dom(h)$, so we have $\Dom((g+1)\comp k')=\Dom(h)$. If $x\in\Dom(h)$, then $h(x)=(g+1)\comp k(x)$ and $(g+1)\comp k(x)=(g+1)\comp k'(x)$, so we have $h(x)=(g+1)\comp k'(x)$. So, we have $h=(g+1)\comp k'$. Additionally, $\Dom(k')\subseteq\Dom(k)$, and for every $x\in \Dom(k')$, we have $k'(x)=k(x)$, so we have $k'\appr k$. \qed
\end{proof}
\begin{lemma}\label{lem:maybe-colif}
The order structure on the set-functor $FX=X+1$ is a coliftable order.
\end{lemma}
\begin{proof}
By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $Fg(k)\appr h$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k\appr k'$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
\begin{itemize}
\item $Fg(k)=h$: In this case we take $k'=k$, and then we have $Fg(k')=h$.
\item $Fg(k)=\bot$: It entails that $k=\bot$. We either have $h=\bot$ or $h\in Y$. If $h=\bot$ then we take $k'=k$, and we are done. If $h\in Y$, then by the surjectivity of $g$, there exists $k'$ such that $g(k')=h$ that entails $Fg(k')=h$ as well.\qed
\end{itemize}
\end{proof}
So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alpha)$ of a functor with a liftable order, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$.
We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$.\\
Proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alpha)$ of a functor with a liftable order, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$. We have shown that the ordering on the maybe functor is liftable and coliftalbe in~\autoref{prop:maybe-lif} and~\autoref{prop:maybe-colif}
%\begin{lemma}\label{lem:maybe-func-set}
% Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$
% \begin{gather*}
@@ -2371,7 +2501,7 @@ So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alph
% \end{gather*}
%\end{lemma}
%\begin{proof}
% By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. %Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}:
% By~\autoref{prop:alph-prod-dubut} and~\autoref{prop:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. %Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}:
%% \begin{enumerate}
%% \item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}
%% \item $\alpha(x_2)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}
@@ -2515,7 +2645,7 @@ Assuming $f,g\in\Hom(X,Y+1)$, and that $f'\c X_f\rightarrowtail X$ and $g'\c X_g
\arrow["{f'}"', tail, from=2-1, to=1-2]
\end{tikzcd}
\end{equation*}
\begin{lemma}\label{lem:maybe-lif-abs}
\begin{lemma}\label{prop:maybe-lif-abs}
The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order.
\end{lemma}
\begin{proof}
@@ -2981,11 +3111,17 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
$\hat{L}$ is a Barr relator.
\end{prop}
\begin{proof}
We have
\begin{gather*}
\hat{\emre}r=\emre r\cap (\emre r^\op)^\op,\\
\hat{\emre}r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}\cap\{(T,S)\mid x\in S\Rightarrow \exists y\in T, y\;r\;x\}.
\end{gather*}
Assuming that $r=\pi_2\comp(\pi_1)^\op$ we have to prove that $\hat{L}r=\powf\pi_2\comp(\powf\pi_1)^\op$.
\todo{Finish.}
\end{proof}
\begin{definition}[Mid-lax Barr relator]
Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$. Assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{mid-lax Barr relator} if we have:
Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$, and $\pi_1$ and $\pi_2$ are surjective, assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{mid-lax Barr relator} if we have:
% A relator over a functor $F$ is a one-sided Barr relator, shown by $\overrightarrow{F}$, iff for a partial order $\appr$ over $F$, a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have:
\begin{gather*}
\overrightarrow{F}r=F\pi_2\comp\appr\comp(F\pi_1)^\op
@@ -3118,7 +3254,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
% Since $\appr$ is a coliftable order structure by~\autoref{def:coliftable-ord} there exists a $w$ such that $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$, $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed
%\end{proof}
\begin{prop}\label{prop:all-rel-compa}
For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that a set-functor $F$ has an order structure $\appr$, the following propositions hold:
For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $\pi_1$ and $\pi_2$ are surjective, assuming that a set-functor $F$ has an order structure $\appr$, the following propositions hold:
\begin{enumerate}
\item If $\appr$ is liftable, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad F\pi_2\comp(F\pi_1)^\op\comp\appr$
\item If $\appr$ is coliftable, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad \appr\comp F\pi_2\comp(F\pi_1)^\op$
@@ -3134,6 +3270,18 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
\begin{proof}
They all follow in an obvious way from~\autoref{lem:liftable} and~\autoref{lem:coliftable}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed
\end{proof}
\begin{prop}\label{prop:lax-relator-full-comm}
For a functor $F$ with a liftable order we have:
\begin{gather*}
(\bar{F}r\comp\appr)\subseteq(\appr\comp\bar{F}r)
\end{gather*}
\end{prop}
\begin{proof}
Assuming $x \mathrel{(\bar{F}r\comp\appr)} y$ and $\bar{F}r=F\pi_2\comp(F\pi_1)^\op$, then there exist $x'$ and $p$ such that $x\appr x'$, $p\mathrel{F\pi_1}x'$, and $p\mathrel{F\pi_2}y$. So, we have $x\appr F\pi_1(p)$ then by liftability there exists $p'$ such that $p'\appr p$, and $F\pi_1(p')=x$. Then from $p'\appr p$ we get $F\pi_2(p')\appr y$ that is equivalent with $p' \mathrel{(\appr\comp F\pi_2)} y$, and then we have $x \mathrel{(\appr\comp F\pi_2\comp(F\pi_1)^\op)} y$.\qed
\end{proof}
\begin{cor}
Assuming that $r$ is an $(\bar{F}r\comp\appr)$-simulation, then it is an $(\appr\comp\bar{F}r)$-simulation as well.
\end{cor}
%\begin{example}
% In the category of sets, subset over the powerset functor is an example of a liftable order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$.
%
@@ -3209,7 +3357,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
\end{align*}\qed
\end{proof}
\begin{cor}
Since the symmetrization of left-lax Barr relator that is laxed with a lifatble order structure is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator.
Since the symmetrization of left-lax Barr relator with a lifatble order structure is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator.
\end{cor}
\begin{cor}
By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is liftable, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well.
@@ -3255,7 +3403,37 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
\begin{remark}
With a similar argument we can prove that the symmetrization of a right-lax Barr-relator of $F$ is a Barr-relator.
\end{remark}
\todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion.}
\begin{lemma}\label{lem:lax-relator-str}
For a relation $r$, for functions $k_s\c F\pi_1(\bar{F}r)\to\powf FX$ and $k_b\c F\pi_2(\bar{F}r)\to\powf FX$, defined as
\begin{gather*}
k_s(x)=\{(x',y)\mid(x,y)\in\bar{F}r,x'\appr x, (x',y)\notin\bar{F}r\},\\
k_b(x)=\{(x',y)\mid(x,y)\in\bar{F}r,x\appr x', (x',y)\notin\bar{F}r\},
\end{gather*}
we have
\begin{gather*}
(\bar{F}r)\comp\appr=\bar{F}r\cup(\bigcup_{x\in F\pi_1(\bar{F}r)} k_s(x)),\\
(\bar{F}r)\comp\sappr=\bar{F}r\cup(\bigcup_{x\in F\pi_1(\bar{F}r)} k_b(x)).
\end{gather*}
\end{lemma}
\begin{proof}
\todo{Write it down. You have it in your notes.}
\end{proof}
\todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion. See if~\autoref{prop:lax-relator-full-comm} or~\autoref{lem:lax-relator-str} can help!}
\subsection{Symmetric relation}
\begin{prop}
Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a coalgebra $(X,\alpha)$, then $r$ is an $\hat{\relar}$-bisimulation.
\end{prop}
\begin{proof}
$r$ being an $\relar$-simulation means that $r\leq \alpha^\op\comp\relar r\comp\alpha$, and $r$ being symmetric means that $r^\op=r$. So, we need to prove that $r\leq\alpha^\op\comp\hat{\relar} r\comp\alpha$. We have:
\begin{align*}
x \mathrel{(\alpha^\op\comp\hat{\relar} r\comp\alpha)} y&\\
\iff &x\mathrel{(\alpha^\op\comp(\relar r\cap (\relar r)^\op)\comp\alpha)} y\\
\iff &\exists x',y',\quad x\mathrel{\alpha}x'\quad\&\quad y\mathrel{\alpha}y'\quad\&\quad x'\mathrel{(\relar r\cap (\relar r)^\op)}y'\\
\iff &\exists x',y',\quad x\mathrel{\alpha}x'\quad\&\quad y\mathrel{\alpha}y'\quad\&\quad x'\mathrel{\relar r}y'\quad\&\quad x'\mathrel{(\relar r)^\op}y'\\
\iff &\exists x',y',\quad x\mathrel{\alpha}x'\quad\&\quad y\mathrel{\alpha}y'\quad\&\quad x'\mathrel{\relar r}y'\quad\&\quad y'\mathrel{\relar r}x'
\end{align*}
Now, assuming $x\mathrel{r}y$ gives us $x\mathrel{(\alpha^\op\comp\relar r\comp \alpha)} y$ that is equivalent with saying that exist $x'$ and $y'$ such that $x\mathrel{\alpha}x'$, $y\mathrel{\alpha}y'$, and $x'\mathrel{\relar r}y'$. Since $r$ is symmetric, we have $y\mathrel{r} x$ that means that exist $x''$ and $y''$ such that $x\mathrel{\alpha}x''$, $y\mathrel{\alpha}y''$, and $y''\mathrel{\relar r}x''$. On the other hand since $\alpha$ is a function, we have $x''=x'$ and $y''=y'$, so we have $y'\mathrel{\relar r}x'$ that ultimately gives $x\mathrel{(\alpha^\op\comp\hat{\relar}r\comp\alpha)}y$. So, $r$ is an $\hat{\relar}$-bisimulation as well.\qed
\end{proof}
\end{document}