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

more editting

Browse Source
This commit is contained in:
partowp 2026-05-05 20:50:52 +01:00
parent 833d86e0ba
commit 03c3abc624
1 changed files with 14 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
draft/draft.tex
View File

@ -2150,7 +2150,7 @@ then at least $(x_1,y_3)$ is not in the behavioural equivalence, while it is in
\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}
\subsection{Egli-Milner relator}
\subsection{Egli-Milner relator and Barr relators}
\begin{definition}
We call the map $\emre\c\rel\to\rel$ the Egli-Milner $\powf$-relator, whenever for every relation $r\c X\rto Y$ it is defined as follows:
\begin{gather*}
@ -2187,20 +2187,29 @@ Egli-Milner relator is not sound or complete, although its symmetrization is sou
&\iff S\;(\powf g)^\op\comp\powf f\;T
\end{align*}\qed
\end{proof}
The symmetrization of the Egli-Milner relator is a Barr-relator. Barr-relator is a generalization of the Egli-Milner relator, where the functor is generalized.
\begin{prop}
Assuming that $r\c X\rto Y$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then $\appr_{X};\hat{\emre};\appr_{Y}=\appr_{X};\hat{\emre}$ and $\appr_{X};\hat{\emre}=\hat{\emre};\appr_{Y}$.
Assuming that $r\c X\rto Y$, then $\subseteq;\hat{\emre};\subseteq=\subseteq;\hat{\emre}$ and $\subseteq;\hat{\emre}=\hat{\emre};\subseteq$.
\end{prop}
Barr relator is a generalization of the Egli-Milner relator, where the functor is generalized.
\begin{definition}
A relator over a functor $F$ is a Barr-relator, shown by $\bar{F}$, iff for 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:
A relator over a functor $F$ is a Barr relator, shown by $\bar{F}$, iff for 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*}
\bar{F}r=F\pi_2\comp(F\pi_1)^\op
\end{gather*}
\end{definition}
\begin{prop}
Assuming that $\relar$ is a relator over $F\c\Set\to\Set$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then the relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr-relator.
$\hat{L}$ is a Barr relator.
\end{prop}
\begin{proof}
\todo{Finish.}
\end{proof}
\begin{prop}
Assuming that $\relar$ is a relator over $F\c\Set\to\Set$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then the relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr relator.
\end{prop}
\begin{proof}
\todo{Finish.}