From 0ba2dd8c19d116e979b393f19b8c5934f16feeed Mon Sep 17 00:00:00 2001 From: partowp Date: Mon, 4 May 2026 20:29:38 +0100 Subject: [PATCH] ACfull proof --- draft/draft.tex | 51 ++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 40 insertions(+), 11 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index f530fcf..dda809e 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2038,6 +2038,7 @@ 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} @@ -2053,6 +2054,16 @@ The above translation seems to be true in a more general case, where $\spa$ and \end{align*}\qed \end{proof} +\begin{prop} + Assuming that $\relar$ is a symmetric relator, and $r$ is a $\relar$-simulation from a coalgebra $(X,\alpha)$ to itself, then $r^\op_{s}$ is a $\relar$-simulation as well. +\end{prop} +\begin{proof} + It is easy to directly show that $r^\op$ is a $\relar$-simulation.\qed +\end{proof} +\begin{cor} + Assuming that $\relar$ is a symmetric relator, then the $\relar$-simularity from a coalgebra $(X,\alpha)$ to itself is a symmetric relation. +\end{cor} + \begin{prop} Assuming that $\relar$ is a symmetric relator, then for every $r$ that is a $\relar$-simulation, $r^\op$ is also a $\relar$-simulation. \end{prop} @@ -2072,10 +2083,6 @@ The above translation seems to be true in a more general case, where $\spa$ and For a relator $\relar$ the $\relar$-similarity from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ is sound iff it 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{prop} - Assuming that $\relar$ preserves difunctional relations -\end{prop} - \begin{thm} Let $\relar$ be a relator for a functor $F$: \begin{enumerate} @@ -2097,13 +2104,6 @@ The above translation seems to be true in a more general case, where $\spa$ and $\relar$-similarity being symmetric means that for the $f_1$, $f_2$, $g_1$ and $g_2$ in the proof of~\autoref{prop:difunc-preser}, we have $f_1=f_2$ and $g_1=g_2$.\qed \end{proof} -\begin{prop} - Assuming that $\relar$-similarity is symmetric and complete, then $\hat{\relar}$-similarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete. -\end{prop} -\begin{proof} - (Completeness): We show $\relar$-similarity with $r_s$ and $\hat{\relar}$-similarity with $r_{\hat{s}}$. Also, we show the behabioural equivalence with $r_b$. Since -\end{proof} - Assuming that $\relar$-similarity is complete, does not guarantee that $\hat{\relar}$-similarity is sound and complete. We give a counter-example. Assuming that $\relar$ is a $\powf$-relator that takes $r\c X\rto Y$ to $\powf X\times \powf Y$, then $\hat{\relar} r= \powf X\times\powf Y$ as well. It means that for every coalgebras $(X,\alpha)$, $(Y,\beta)$, $\hat{\relar}$-similarity is equal to $X\times Y$, which is rare to be equal to behavioural equivalence. For example, if we take $X=\{x_1,x_2\}$ and $Y=\{y_1,y_2,y_3\}$, and we define $\alpha$ and $\beta$ as \begin{gather*} \alpha(x)= @@ -2120,6 +2120,35 @@ Assuming that $\relar$-similarity is complete, does not guarantee that $\hat{\re \end{cases} \end{gather*} then at least $(x_1,y_3)$ is not in the behavioural equivalence, while it is in $\hat{\relar}$-similarity. + +\begin{prop} + Assuming that $\relar$-similarity is symmetric and complete, then $\hat{\relar}$-similarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete. +\end{prop} +\begin{proof} + (Completeness): We show $\relar$-similarity with $r_s$ and $\hat{\relar}$-similarity with $r_{\hat{s}}$. Also, we show the behabioural equivalence with $r_b$. Since +\end{proof} + +\begin{prop} + Assuming that $\relar$ is a $F$-relator ($F$ is a set functor), that for every functions $f\c X\to Z$ and $g\c Y\to Z$, we have $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$, then $\hat{\relar}$-similarity is complete. +\end{prop} +\begin{proof} + We need to prove that for every functions $f\c X\to Z$ and $g\c Y\to Z$ we have $\hat{\relar}(g^\op\comp f)\geq (Fg)^\op\comp Ff$. By the assumption we have $\relar(g^\op\comp f)\geq(Fg)^\op\comp Ff$. Also, again from the assumption we have $\relar(f^\op\comp g)\geq(Ff)^\op\comp Fg$ that gives $(\relar(f^\op\comp g))^\op\geq(Fg)^\op\comp Ff$. So, we have $\hat{\relar}(g^\op\comp f)\geq F(g)^\op\comp Ff$.\qed +\end{proof} +\begin{prop} + Assuming that $\relar$ is a symmetric relator for a functor $F\c\Set\to\Set$, then the $\relar$-bisimilarity from a coalgebra $\alpha\c X\to FX$ to itself is sound, using the axiom of choice. +\end{prop} +\begin{proof} + We call the bisimilarity relation $r$, and we assume $x_1\;r\;x_2$, now we need to prove that $x_1$ and $x_2$ are behaviourally equivalent. We take $Z=X/r$, where $X/r=\{[x]\mid [x]=\{y\mid x\;r\;y\}\}$. Now, we define the coalgebra homomorphism $f\c X\to X/r$ as $f(x)=[x]$. So, assuming $x_1\;r\;x_2$ gives $f(x_1)=f(x_2)$. Now, assuming that exists a choice function $c\c X/r\to X$ that $c\comp f=\id_X$, we define $\gamma\c X/r\to F(X/r)$, as $\gamma([x])=Ff\comp\alpha\comp c([x])$. Now, we have + \begin{align*} + \gamma\comp f&\\ + &=Ff\comp\alpha\comp c\comp f\\ + &=Ff\comp\alpha. + \end{align*} + So, $x_1$ and $x_2$ are behaviourally equivalent. So, the $\relar$-bisimilarity is sound.\qed +\end{proof} +\begin{cor} + Assuming that a relator $\relar$ over a functor $F\c\Set\to\Set$ satisfies $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$ for every functions $f\c X\to Z$ and $g\c Y\to Z$, then $\hat{\relar}$-bisimilarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete, using the axiom of choice. +\end{cor} \end{document}