From f573e583eb40cab0144873403c93791880e49683 Mon Sep 17 00:00:00 2001 From: partowp Date: Thu, 30 Apr 2026 17:15:13 +0100 Subject: [PATCH] more wrtiting --- draft/draft.tex | 65 ++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 56 insertions(+), 9 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 6cc5417..6f71ba2 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1939,9 +1939,9 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge \begin{notation} From now on, we show relations with small letters, and for two relations $r_1$ and $r_2$ by $r_1\leq r_2$ we mean $r_1\subseteq r_2$. Also, we show the category of relations over set that we represent by spans with $\spa$, and $\rel$ is the category of sets and binary relations between them. \end{notation} -\begin{prop} +\begin{lemma}\label{lem:rel-span-equiv} $r\c X\rto Y$ is a morphism in $\rel$ iff there is an object $(r,p_1,p_2)$ in $\spa$. -\end{prop} +\end{lemma} \begin{proof} ($\Rightarrow$): $r\c X\rto Y$ being a morphism in $\rel$ means that in $\Set$ there exist an object $r$ with a unique mono of type $r\to X\times Y$ that is a pairing that we show with $\brks{p_1,p_2}$. So, $(r,p_1,p_2)$ form an object in $\spa$. @@ -1952,9 +1952,9 @@ The above translation seems to be true in a more general case, where $\spa$ and 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] +\begin{definition}[Hermida-Jacobs Simulation]\label{def:hej-sim} For a relator $\relar$ on a functor $F$ a HJ-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ 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{equation}\label{eq:hej-sim} \begin{tikzcd}[ampersand replacement=\&] X \& r \& Y \\ {FX} \& {\relar r} \& {FY} @@ -1966,11 +1966,19 @@ The above translation seems to be true in a more general case, where $\spa$ and \arrow["{{(Fp_1)}^\relar}", from=2-2, to=2-1] \arrow["{{(Fp_2)}^\relar}"', from=2-2, to=2-3] \end{tikzcd} - \end{equation*} + \end{equation} \end{definition} \begin{definition}[Relator-based Simulation] - Given a relator $\relar$, a relation $r\c X\rto Y$ is an $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r\leq \alpha;\relar r;\beta^\op$, i.e, if $(x,y)\in r$ entails $(\alpha(x),\beta(y))\in\relar r$, for all $x\in X$ and $y\in Y$. + Given a relator $\relar$, a relation $r\c X\rto Y$ is a $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r\leq \alpha;\relar r;\beta^\op$, i.e, if $(x,y)\in r$ entails $(\alpha(x),\beta(y))\in\relar r$, for all $x\in X$ and $y\in Y$. +\end{definition} + +\begin{definition}[Symmetric Relator] + A relator $\relar$ is symmetric if and only if for every relation $r$ we have $\relar(r^\op)=(\relar r)^\op$. +\end{definition} + +\begin{definition}[Relator-based Bisimulation] + Given a relator $\relar$, a relation $r\c X\rto Y$ is a $\relar$-bisimulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r$ is a $\relar$-simulation, and $\relar$ is a symmetric relator. \end{definition} \begin{notation} @@ -1985,16 +1993,18 @@ The above translation seems to be true in a more general case, where $\spa$ and \end{proof} \begin{prop} - A relation $r$ is a $\relar$-simulation if and only if it is a HJ-simulation with the witness $\sigma\c r\to\relar r$. + For a relator $\relar$ of a functor $F$, a relation $r$ is a $\relar$-simulation from $\alpha\c X\to FX$ to $\beta\c Y\to FY$ iff it is a HJ-simulation with the witness $\sigma\c r\to\relar r$. \end{prop} \begin{proof} - \todo{Finish} + ($\Rightarrow$): $r$ being a $\relar$-simulation means that $x\;r\;y$ gives $\alpha(x)\;\relar r\;\beta(y)$. Since $r$ and $\relar r$ are both relations, by~\autoref{lem:rel-span-equiv} there exist objects $(r,p_1,p_2)$ and $(\relar r,(Fp_1)^\relar,(Fp_2)^\relar)$ in $\spa$. We define $\sigma\c r\to\relar r$ to be $\sigma(x,y)=(\alpha(x),\beta(y))$. $\sigma$ commutes in~\eqref{eq:hej-sim}, so we have a HJ-simulation. + + ($\Leftarrow$): Assuming we have a $\sigma$ that commutes in~\eqref{eq:hej-sim}, we want to prove that if $x\;r\;y$ we have $\alpha(x)\;\relar r\;\beta(y)$. By~\eqref{eq:hej-sim} we have $\alpha\comp p_1=(Fp_1)^\relar\comp\sigma$ and $\alpha\comp p_2=(Fp_2)^\relar\comp\sigma$. It means that since $x\;r\;y$ then exists $w\in\relar r$, such that $\sigma(x,y)=w$, where $(Fp_1)^\relar(w)=\alpha(x)$ and $(Fp_2)^\relar(w)=\beta(y)$. So, we have $\alpha(x) \;\relar r \;\beta(y)$.\qed \end{proof} \begin{prop} For an arbitrary relator $\relar$ on a functor $F$, if a relation $r$ is a HJ-simulation, the witness is unique. \end{prop} \begin{proof} - It only relies on the fact that ${(Fp_1)}^\relar_\appr$ and ${(Fp_2)}^\relar_\appr$ in~\eqref{def:hej-sim} are jointly monic.\qed + It only relies on the fact that ${(Fp_1)}^\relar$ and ${(Fp_2)}^\relar$ in~\eqref{def:hej-sim} are jointly monic.\qed \end{proof} \begin{definition} We call $\hat{\relar}$ a symmetrization of a relator $\relar$ iff for a relation $r$ it is defined as follows: @@ -2015,6 +2025,43 @@ The above translation seems to be true in a more general case, where $\spa$ and \begin{remark} If we want to have the previous corollary for two different coalgebras $\alpha\c X\to FX$ and $\beta\c X\to FX$, we need to assume that $r^\op$ is also a $\relar$-simulation from $\beta$ to $\alpha$. \end{remark} +\begin{prop} + $\hat{\relar}$ is a symmetric relator, i.e., every $\hat{\relar}$-simulation is actually a $\hat{\relar}$-bisimulation. +\end{prop} +\begin{proof} + \begin{align*} + \hat{\relar}(r^\op)&\\ + &=\relar(r^\op)\cap(\relar (r^\op)^\op)^\op\\ + &=\relar(r^\op)\cap(\relar r)^\op\\ + &=(\relar r)^\op\cap\relar(r^\op)\\ + &=(((\relar r)^\op\cap\relar(r^\op))^\op)^\op\\ + &=(\relar r\cap(\relar(r^\op))^\op)^\op\\ + &=(\hat{\relar}r)^\op + \end{align*}\qed +\end{proof} +\begin{definition}[Behavioural Equivalence] + Assuming $F\c\Set\to\Set$, behavioural equivalence from a $F$-coalgebra $(X,\alpha)$ to a $F$-coalgebra $(Y,\beta)$ is a relation $r\subseteq X\times Y$, such that there exists a coalgebra $(Z,\gamma)$ and morphisms $f\c(X,\alpha)\to(Z,\gamma)$ and $g\c(Y,\beta)\to(Z,\gamma)$ for every $(x,y)\in r$, $f(x)=g(y)$. +\end{definition} + +\begin{definition} + A relation $r\c X\rto Y$ is difunctional iff there are functions $f\c X\to Z$ and $g\c Y\to Z$ such that for every $(x,y)\in R$ we have $f(x)=g(y)$. +\end{definition} + +\begin{definition}[Soundness and Completeness of Relators] + A relator $\relar$ is sound iff the $\relar$-similarity from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ is less than or equal to their behavioural equivalence, and it is complete iff it is greater than or equal to their behavioural equivalence. +\end{definition} + +\begin{thm} + Let $\relar$ be a relator for a functor $F$: + \begin{enumerate} + \item If for all functions $f\c X\to A$ and $g\c Y\to A$, $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$, then $\relar$-similarity is complete. + \item If $\relar$ preserves difunctional relations and for every epi-cospan $(f\c X\to A,g\c Y\to A)\in\Set$, $\relar(g^\op\comp f)\leq(Fg)^\op\comp Ff$, then $\relar$-similarity is sound. + \end{enumerate}\qed +\end{thm} + +\begin{prop} + $\hat{\relar}$ is sound and complete. +\end{prop} \end{document}