partowp
3248 lines
162 KiB
TeX
3248 lines
162 KiB
TeX
\documentclass[envcountsect,runningheads,draft]{llncs} % fails
|
|
|
|
\newcommand\hmmax{0}
|
|
\newcommand\bmmax{0}
|
|
|
|
\sloppy
|
|
|
|
\usepackage[nosumlimits,nointlimits,nonamelimits]{amsmath}
|
|
\usepackage{amssymb}
|
|
|
|
\usepackage[colorlinks,linkcolor={blue},citecolor={blue},urlcolor={red},breaklinks=true,final]{hyperref}
|
|
|
|
\renewcommand{\subsectionautorefname}{Section}%
|
|
|
|
\newcommand{\xTo}[1]{\,\xRightarrow{#1}\,}
|
|
%\newcommand{\lbs}[1]{\,\xRightarrow{#1}\,}
|
|
\newcommand{\dhat}[1]{\check{#1}}
|
|
|
|
\usepackage{lineno}
|
|
\linenumbers
|
|
|
|
\usepackage{etoolbox} %% <- for \cspreto, \csappto
|
|
|
|
%% Patch 'normal' math environments:
|
|
\newcommand*\linenomathpatch[1]{%
|
|
\cspreto{#1}{\linenomath}%
|
|
\cspreto{#1*}{\linenomath}%
|
|
\csappto{end#1}{\endlinenomath}%
|
|
\csappto{end#1*}{\endlinenomath}%
|
|
}
|
|
|
|
\linenomathpatch{equation}
|
|
\linenomathpatch{gather}
|
|
\linenomathpatch{multline}
|
|
\linenomathpatch{align}
|
|
\linenomathpatch{alignat}
|
|
\linenomathpatch{flalign}
|
|
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage[final]{graphicx}
|
|
\usepackage{color}
|
|
%\renewcommand\UrlFont{\color{blue}\rmfamily}
|
|
%\urlstyle{rm}
|
|
%
|
|
|
|
\usepackage{etoolbox}
|
|
\usepackage{needspace}
|
|
|
|
\usepackage{hypcap}
|
|
\setcounter{tocdepth}{2}
|
|
|
|
\spnewtheorem{thm}{Theorem}[section]{\bfseries}{\itshape}
|
|
\spnewtheorem{cor}[thm]{Corollary}{\bfseries}{\itshape}
|
|
\spnewtheorem{lem}[thm]{Lemma}{\bfseries}{\itshape}
|
|
\spnewtheorem{prop}[thm]{Proposition}{\bfseries}{\itshape}
|
|
\spnewtheorem{defn}[thm]{Definition}{\bfseries}{\upshape}
|
|
\spnewtheorem{rem}[thm]{Remark}{\bfseries}{\upshape}
|
|
\spnewtheorem{notation}[thm]{Notation}{\bfseries}{\upshape}
|
|
\spnewtheorem{expl}[thm]{Example}{\bfseries}{\upshape}
|
|
\spnewtheorem{assumption}[thm]{Assumption}{\bfseries}{\upshape}
|
|
|
|
\renewenvironment{theorem}{\begin{thm}}{\end{thm}}
|
|
\renewenvironment{corollary}{\begin{cor}}{\end{cor}}
|
|
\renewenvironment{lemma}{\begin{lem}}{\end{lem}}
|
|
\renewenvironment{proposition}{\begin{prop}}{\end{prop}}
|
|
\renewenvironment{definition}{\begin{defn}}{\end{defn}}
|
|
\renewenvironment{remark}{\begin{rem}}{\end{rem}}
|
|
\renewenvironment{example}{\begin{expl}}{\end{expl}}
|
|
|
|
%\renewcommand{\sectionautorefname}{Section}%
|
|
%\renewcommand{\subsectionautorefname}{Section}%
|
|
|
|
\let\vec\relax %
|
|
\usepackage{accents}
|
|
\newcommand\thickbar[1]{\accentset{\rule{.55em}{.6pt}}{#1}}
|
|
|
|
\sloppy
|
|
|
|
\usepackage{wasysym} %Pouya: I added this package for auxillary compositions.
|
|
\usepackage{cancel}
|
|
\usepackage{tikz-cd}
|
|
\usetikzlibrary{arrows.meta}
|
|
\usetikzlibrary{decorations} % Required for all decorations
|
|
\usetikzlibrary{decorations.pathmorphing} % Specifically for 'zigzag'
|
|
|
|
\tikzset{
|
|
commutative diagrams/.cd,
|
|
arrow style = tikz,
|
|
diagrams = {>=stealth},
|
|
row sep = large,
|
|
column sep = huge
|
|
}
|
|
|
|
\usepackage{textcomp}
|
|
|
|
\usepackage{enumitem}
|
|
%\setlist{itemsep=0ex}
|
|
\setlist[itemize]{label={\small$\bullet$}}
|
|
|
|
\BeforeBeginEnvironment{align}{\noindent\ignorespaces}
|
|
|
|
\usepackage{todos}
|
|
\usepackage{proof}
|
|
\usepackage{xspace}
|
|
\usepackage{bm}
|
|
|
|
\input{catprog}
|
|
|
|
%\usepackage{pict2e}
|
|
|
|
%\DeclareRobustCommand{\pigpenA}{%
|
|
% \begingroup\setlength{\untlength}{1em}%
|
|
% \linethickness{.075em}%
|
|
% \begin{picture}(1,.8)
|
|
% \roundcap\roundjoin
|
|
% \polyline(.2,.2)(.8,.2)(.8,.8)
|
|
% \end{picture}%
|
|
% \endgroup
|
|
%}
|
|
|
|
\newcommand{\lbs}[1]{
|
|
\mathrel{%
|
|
\tikz{
|
|
\draw[double, double distance=.75pt, -{Stealth[inset=0pt, angle=75:4pt]}]
|
|
(0,.3) -- node[inner sep=0pt,above=1.75pt,midway] {\scriptsize$#1$} (.5,.3);
|
|
}
|
|
}
|
|
}
|
|
|
|
\newcommand{\pbk}{\arrow[dr, phantom, "\text{\tiny\pigpenA}", pos=0.05]}
|
|
|
|
\newcommand{\Fst}{\Pi_1} %{\oname{Fst}}
|
|
\newcommand{\Snd}{\Pi_2} %{\oname{Snd}}
|
|
\newcommand{\klstar}{\sharp} %% Kleisli star
|
|
\newcommand{\istar}{\dagger}
|
|
|
|
\newcommand{\mSv}{\mS_\val}
|
|
\newcommand{\mSc}{\mS_\com}
|
|
\newcommand{\mSl}{\mS_\lambda}
|
|
|
|
\newcommand{\Sigmas}{\Sigma^\star}
|
|
|
|
\newcommand{\ar}{\oname{ar}}
|
|
|
|
\newcommand{\oWh}{\oname{while}}
|
|
\newcommand{\oIf}{\oname{if}}
|
|
\newcommand{\oPut}{\oname{put}}
|
|
\newcommand{\oGet}{\oname{get}}
|
|
\newcommand{\oSeq}{\oname{seq}}
|
|
|
|
\newcommand{\app}{\,}
|
|
\usepackage{proof}
|
|
\newcommand{\inference}[2]{\infer{~#2~}{~#1~}}
|
|
|
|
\newcommand{\St}{\Gamma}
|
|
|
|
\newcommand{\exend}{\hfill{\rotatebox[origin=c]{45}{$\Box$}}}
|
|
|
|
\makeatletter
|
|
\let\dir@frac\frac
|
|
\newcommand{\inv@frac}[2]{\dir@frac{#2}{#1}}
|
|
|
|
\renewcommand{\frac}{\@ifstar{\inv@frac}{\dir@frac}}
|
|
\makeatother
|
|
|
|
%\renewcommand{\dar}{\kern1.2pt\operatorname{\downarrow}\kern1pt}
|
|
|
|
\newcommand{\G}{\St}
|
|
\newcommand{\D}{\Delta}
|
|
|
|
%\usepackage{txfonts}
|
|
%\usepackage{newtxtext,newtxmath}
|
|
|
|
\newcommand{\mon}{\bullet}
|
|
\newcommand{\monto}{\mathrel{-}\joinrel\mathrel{\bullet}} %{\multimapdot}
|
|
\newcommand{\Pt}{V}
|
|
|
|
\newcommand{\dc}{\mspace{\medmuskip};\mspace{.5\medmuskip}}
|
|
\newcommand{\sep}{,\mspace{\medmuskip}}
|
|
|
|
\newcommand{\xCL}{\textbf{xCL}\xspace}
|
|
\newcommand{\xTCL}{\textbf{xTCL}\xspace}
|
|
\newcommand{\Ty}{\mathsf{Ty}\xspace}
|
|
\newcommand{\Tr}{\mathsf{Tr}\xspace}
|
|
\newcommand{\arty}[2]{#1 \rightarrowtriangle #2}
|
|
\newcommand{\initob}{\textbf{0}}
|
|
\newcommand{\termob}{\textbf{1}}
|
|
\newcommand{\tcomp}{\textsf{comp}}
|
|
\newcommand{\unt}{\mathsf{unit}}
|
|
\newcommand{\true}{\mathsf{true}}
|
|
\newcommand{\false}{\mathsf{false}}
|
|
\newcommand{\bool}{\mathsf{bool}}
|
|
\newcommand{\fpc}{\mathsf{fix}}
|
|
\newcommand{\casec}{\mathsf{if}}
|
|
\newcommand{\ndet}{\oplus} %{\;\ensuremath{\boldsymbol{\pmb{\oplus}}}\;}
|
|
\newcommand{\paral}{\parallel} %{\;\ensuremath{\boldsymbol{\pmb{\mid\mid}}}\;}
|
|
\newcommand{\nDownarrow}{\cancel{\Downarrow}}
|
|
\newcommand{\paralv}{\mathrel{%
|
|
\mathchoice{\PARV}{\PARV}{\scriptsize\PARV}{\tiny\PARV}
|
|
}}
|
|
|
|
\def\PARV{{%
|
|
\setbox0\hbox{$\parallel$}%
|
|
\rlap{\hbox to \wd0{\hss\rule[-.5ex]{.75em}{.12ex}\hss}}\box0
|
|
}}
|
|
|
|
|
|
\usepackage{ifdraft}
|
|
\ifdraft{
|
|
% \usepackage{showframe}
|
|
\usepackage{showlabels}
|
|
\renewcommand{\showlabelfont}{\ttfamily\scriptsize}
|
|
\usepackage[layout=footnote,draft]{fixme}
|
|
|
|
% \usepackage[notcite,notref]{showkeys}
|
|
% \renewcommand*\showkeyslabelformat[1]{%
|
|
% \raisebox{1ex}{\raggedleft{\textit{\tiny #1}}}
|
|
}{
|
|
\usepackage[layout=footnote,final]{fixme}
|
|
}
|
|
|
|
\FXRegisterAuthor{sg}{asg}{SG} % Sergey
|
|
\FXRegisterAuthor{pp}{app}{PP} % Pouya
|
|
|
|
\usepackage{savesym}
|
|
|
|
\savesymbol{degree}
|
|
\savesymbol{leftmoon}
|
|
\savesymbol{rightmoon}
|
|
\savesymbol{fullmoon}
|
|
\savesymbol{newmoon}
|
|
\savesymbol{diameter}
|
|
\savesymbol{emptyset}
|
|
\savesymbol{bigtimes}
|
|
%\savesymbol{blacktriangleright}
|
|
\savesymbol{triangleright}
|
|
|
|
\savesymbol{langle}
|
|
\savesymbol{rangle}
|
|
|
|
\usepackage[matha,mathx]{mathabx}
|
|
|
|
\restoresymbol{other}{langle}
|
|
\restoresymbol{other}{rangle}
|
|
\restoresymbol{other}{emptyset}
|
|
\restoresymbol{other}{triangleright}
|
|
|
|
\usepackage{adjustbox}
|
|
% For size of diagrams.
|
|
|
|
% document specific
|
|
\newcommand{\val}{\mathsf{v}}
|
|
\newcommand{\com}{\mathsf{c}}
|
|
\newcommand{\nats}{\mathbb{N}}
|
|
\newcommand{\ints}{\mathbb{Z}}
|
|
\newcommand{\mS}{\mu\Sigma}
|
|
\newcommand{\bss}{\oname{bs}}
|
|
\renewcommand{\paragraph}[1]{\medskip\noindent{\bfseries\sffamily #1.}}
|
|
\renewcommand{\comp}{\cdot}
|
|
\newcommand{\dist}{\oname{dist}}
|
|
\newcommand{\ldist}{\oname{dist}'}
|
|
\newcommand{\zero}{\oname{o}}
|
|
\newcommand{\suc}{\oname{s}}
|
|
\newcommand{\init}{\oname{init}}
|
|
\newcommand{\primr}{\oname{primr}}
|
|
|
|
\newcommand{\peval}{\frak{p}}
|
|
\newcommand{\teval}{\frak{t}}
|
|
\newcommand{\neval}{\frak{n}}
|
|
\newcommand{\rcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\RIGHTcircle$}}}}
|
|
\newcommand{\lcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\LEFTcircle$}}}}
|
|
\newcommand{\fcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\CIRCLE$}}}}%Pouya: I added these three.
|
|
\newcommand{\tsto}{\leftrightarrow}
|
|
\newcommand{\ba}{\Downarrow}
|
|
%\newcommand{\bba}{\pmb{\Downarrow}}
|
|
\newcommand{\ssim}{\mathrel{\pmb{\sim}}}
|
|
\newcommand{\hatssim }{\mathrel{\hat{\ssim}}}
|
|
\newcommand{\dhatssim }{\mathrel{\dhat{\ssim}}}
|
|
\newcommand{\klplus}{\boxplus}
|
|
\newcommand{\coit}{\mathsf{coit}}
|
|
\newcommand{\itt}{\mathsf{it}}
|
|
\newcommand{\eval}{\mathsf{eval}}
|
|
\newcommand{\refl}{\mathsf{refl}}
|
|
\newcommand{\trans}{\mathsf{trans}}
|
|
\newcommand{\preord}{\mathbf{PreOrd}}
|
|
\newcommand{\rel}{\mathbf{Rel}}
|
|
\newcommand{\spa}{\mathbf{Span}}
|
|
\newcommand{\gra}{\mathbf{Gra}}
|
|
\newcommand{\obj}{\mathbf{Obj}}
|
|
\newcommand{\relar}{\mathbf{R}}
|
|
\newcommand{\emre}{\mathbf{L}}
|
|
\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{\sappr}{\sqsupseteq}
|
|
\newcommand{\Dom}{\mathsf{Dom}}
|
|
|
|
\newcommand{\simeet}{%
|
|
\mathbin{%
|
|
\ooalign{%
|
|
$\sqcap$\cr
|
|
\hidewidth\raisebox{0.2ex}{\scalebox{0.44}{$\otimes$}}\hidewidth\cr
|
|
}%
|
|
}%
|
|
}
|
|
|
|
|
|
\newcommand{\bba}{
|
|
\mathrel{%
|
|
\begin{tikzpicture}[baseline=-6pt]
|
|
\draw[double, double distance=.75pt, -{Stealth[inset=0pt, angle=75:4pt]}] (0,.02) -- (0,-.28);
|
|
\end{tikzpicture}%
|
|
}%
|
|
}
|
|
|
|
\usepackage[final]{listings}
|
|
|
|
\lstset{
|
|
language=Haskell
|
|
%,xleftmargin=2.0cm
|
|
, basicstyle=\small
|
|
, commentstyle=\color{gray}
|
|
, stringstyle=\itshape % string literal style
|
|
, keepspaces=true % keeps spaces in text, useful for keeping indentation of code
|
|
, numbers=none % possible values are (none, left, right)
|
|
, identifierstyle={\itshape}
|
|
, flexiblecolumns={true}
|
|
, showstringspaces={false}
|
|
%,mathescape={true}
|
|
, captionpos=b
|
|
, deletekeywords={join,return,Eval,Left,Either,Right,id,either,Void,Functor,Monad}
|
|
% , morekeywords={Free}
|
|
, emphstyle=\slshape
|
|
, literate={\\}{{$\lambda$}}1 {->}{{$\rightarrow$}}2
|
|
, literate=
|
|
{'}{$\,{}^\prime$\!}1
|
|
{+s}{{$\,$}}1
|
|
{\\}{{$\lambda$}}1
|
|
{lnot}{$\lnot$}3
|
|
{=>}{{$\Rightarrow$}}1
|
|
{<=}{{$\leq$}}1
|
|
{<<-}{{$\in$}}1
|
|
{<<=}{{$\subseteq$}}1
|
|
{>>=}{{$\gg\kern-1pt=$}}1
|
|
{++}{{$\varoplus$}}2
|
|
{|->}{{$\mapsto$}}1
|
|
{->}{{$\rightarrow$}}1
|
|
{->d}{{$\rightarrow_\delta$}}2
|
|
{->b}{{$\rightarrow_\beta$}}2
|
|
{->bd}{{$\rightarrow_{\beta\delta}^*$}}2
|
|
{::=}{{$:=$}}2
|
|
{:=}{{$\mapsto$}}1
|
|
{alpha}{{$\alpha$}}1
|
|
{UU}{{$\cup$}}1
|
|
{All}{{${\forall}\!\!\!\!$}}1
|
|
}
|
|
|
|
|
|
\setcounter{totalnumber}{1} % No two figures in one page
|
|
|
|
\begin{document}\allowdisplaybreaks
|
|
|
|
\let\cedilla\c
|
|
\renewcommand{\c}{\colon}
|
|
|
|
%
|
|
\title{Coalgebraic Simulation.}
|
|
%
|
|
%\titlerunning{Abbreviated paper title}
|
|
% If the paper title is too long for the running head, you can set
|
|
% an abbreviated paper title here
|
|
%
|
|
\author{Sergey Goncharov\inst{1}\orcidID{0000-0001-6924-8766} \and
|
|
Pouya Partow\inst{1}\orcidID{0009-0003-9652-9469}}
|
|
%
|
|
\authorrunning{S.~Goncharov, P.~Partow}
|
|
% First names are abbreviated in the running head.
|
|
% If there are more than two authors, 'et al.' is used.
|
|
%
|
|
\institute{University of Birmingham, UK\\
|
|
\email{\{s.goncharov,p.partow\}@bham.ac.uk}}
|
|
%
|
|
\maketitle % typeset the header of the contribution
|
|
%
|
|
\begin{abstract}
|
|
Hello simulation!
|
|
\end{abstract}
|
|
%
|
|
%
|
|
\section{Relation Lifting}
|
|
\begin{definition}[Natural Order Structure]\label{def:nat-ord}
|
|
A \emph{natural order structure} on a functor $F$ is a poset $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that if $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X'\to X$, $g\c Y\to Y'$, then:
|
|
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
|
\item $\alpha\comp f\appr\beta\comp f$ in $\Hom(X',FY)$. \label{item:nat-ord:I}
|
|
\item $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,FY')$. \label{item:nat-ord:II}
|
|
\end{enumerate}
|
|
\end{definition}
|
|
We want to say that a natural order structure entails an order over a functor defined by Jacobs and Hughes that is a functor of the type $\Set\to\mathbf{Poset}$.
|
|
\begin{prop}
|
|
Assuming that $F\c\Set\to\Set$ is a functor, and we have a natural order structure on $F$, then we have a functor $\tilde{F}\c\Set\to\mathbf{Poset}$, such that $U\comp \tilde{F}=F$, where $U$ is a forgetful functor.
|
|
\end{prop}
|
|
\begin{proof}
|
|
We take $\tilde{F}X=\Hom(1,FX)$. Assuming that $U$ takes every poset to its carrier set, then we have $U\comp\tilde{F}X=FX$ for every object $X$.\qed
|
|
\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'$.
|
|
\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'$.
|
|
\end{definition}
|
|
|
|
\begin{lemma}\label{lem:set-ord-str}
|
|
In $\Set$, assuming that for every set $Y$ we have an order $\leq$ on $\Hom(1,FY)$ that satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, and if for $A\in\Hom(1,FZ)$, $B\in\Hom(1,FY)$, and $g\c Y\to Z$, $h\leq Fg(B)$ in $\Hom(1,FZ)$ there exists $B'\in\Hom(1,FY)$ such that $B'\leq B$ and $B\in\Hom(1,FY)$ and $A=Fg(B')$, then there exists an order structure $\appr$ on $F$ that is a liftable order structure.
|
|
\end{lemma}
|
|
\begin{proof}
|
|
For every $f,g\in\Hom(X,FY)$, we define $f\appr g$ whenever for all $x\in X$, $f(x)\leq g(x)$.
|
|
|
|
Now, assuming $f\c X'\to X$, $\alpha,\beta\c X\to FY$, and $\alpha\appr\beta$, then for every $x'\in X'$, we have $\alpha(f(x'))\leq\beta(f(x'))$, so we have $\alpha\comp f\appr \beta\comp f$. Additionally, if we assume $g\c Y\to Y'$, then since $\leq$ satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, for every $x\in X$ we have $Fg\comp\alpha(x)\leq Fg\comp\beta(x)$.
|
|
|
|
Furthermore, if we have $g\c Y\to Z$, $k\c X\to FY$, $h\c X\to FZ$, and $Fg\comp k\appr h$, then for every $x\in X$ we have $Fg\comp k(x)\leq h(x)$, thus by the assumption of the lemma, for every $x$, there exists a set that we call $k'(x)$, for which we have $Fg(k'(x))\leq h(x)$. So, we have a function $k'\c X\to FY$, such that for every $x$ we have $Fg\comp k'(x)\leq h(x)$ that means $Fg\comp k'\appr h$.
|
|
\qed
|
|
\end{proof}
|
|
\begin{remark}\label{rem:set-ord-str-co}
|
|
The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures.
|
|
\end{remark}
|
|
|
|
\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 $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$.
|
|
|
|
Assuming $z\in h$, since $h\subseteq \powf Fg(k)$, then $z\in\powf Fg(k)$. So, there exists $y'\in k$ such that $Fg(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means $z\in\powf Fg(k')$.\qed
|
|
\end{proof}
|
|
|
|
\begin{example}
|
|
In the category of sets, subset over the powerset functor is an example of a coliftable order structure if the $g$ in~\autoref{def:coliftable-ord} is a surjective. Using~\autoref{rem:set-ord-str-co} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, $g\c Y\to Z$, such that $\powf g(k)\subseteq h$. We define $k'=k\cup\{y\mid g(y)\in h\}$, and we show that $\powf g(k')=h$.
|
|
|
|
Obviously, $\powf g(k')\subseteq h$. Now, assuming $z\in h$ we prove that $z\in \powf g(k')$. Since $g$ is surjective, then exists $A\subseteq Y$ such that $\powf g(A)=h$. By the definition of $k'$, $A\subseteq k'$. So from $z\in h$ we have $z\in \powf g(A)$ that means that exists $a\in A$, such that $g(a)=z$. Now, since $A\subseteq k'$, then $a\in k'$. So, we have $z\in \powf g(k')$.\qed
|
|
\end{example}
|
|
|
|
\begin{remark}
|
|
We give an example that justifies why the $g$ in~\autoref{def:coliftable-ord} should be surjective.
|
|
If we take the surjectivity of $g$ out of~\autoref{def:coliftable-ord}, subset relation over the powerset functor is not an example of a coliftable order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$,
|
|
\begin{gather*}
|
|
g(z)=
|
|
\begin{cases}
|
|
0 & z\in\mathbb{Z}^+ \\
|
|
1 & \mathsf{otherwise}
|
|
\end{cases}
|
|
\end{gather*}
|
|
then
|
|
\begin{gather*}
|
|
\powf g(A)=
|
|
\begin{cases}
|
|
\emptyset & A=\emptyset \\
|
|
\{0\} & A\subseteq \mathbb{Z}^+,A\neq\emptyset\\
|
|
\{1\} & A\subseteq \mathbb{Z}^-\cup\{0\},A\neq\emptyset\\
|
|
\{0,1\} & \mathsf{otherwise}
|
|
\end{cases}
|
|
\end{gather*}
|
|
then no matter what $k\c X\to\powf\mathbb{Z}$ is there will be no $k'\c X\to\powf\mathbb{Z}$, for every $x\in X$, $\powf g(k'(x))=h(x)$, as $\powf g(k'(x))\subseteq\{0,1\}$, while $h(x)=\mathbb{Z}$, so $\powf g(k'(x))\subset h(x)$.
|
|
\end{remark}
|
|
|
|
\begin{remark}
|
|
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}
|
|
\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\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}
|
|
\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}
|
|
|
|
|
|
\section{Coalgebraic Bisimulation}%\label{sec:}
|
|
In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has
|
|
products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\
|
|
such spans $(X \stackrel{p_1}{\leftarrow} R
|
|
\stackrel{p_2}{\to}Y)$ that the morphism $\brks{p_1,p_2}$ is a mono.
|
|
We denote morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$.
|
|
A morphism $R\rto S$ ($R\spto S$) in $\rel(\BC)$
|
|
($\spa(\BC)$) is such a triple of morphisms $(f\c R\to S, g_1\c X_1\to Y_1, g_2\c X_2\to Y_2)$
|
|
in $\BC$ that the following diagram commutes:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{X_1} \& R \& {X_2} \\
|
|
{Y_1} \& S \& {Y_2}
|
|
\arrow["{g_1}"', from=1-1, to=2-1]
|
|
\arrow["{{p_1}}"', from=1-2, to=1-1]
|
|
\arrow["{{p_2}}", from=1-2, to=1-3]
|
|
\arrow["f", from=1-2, to=2-2]
|
|
\arrow["{g_2}", from=1-3, to=2-3]
|
|
\arrow["{q_1}", from=2-2, to=2-1]
|
|
\arrow["{q_2}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
|
|
\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[from=1-1, to=2-1]
|
|
\arrow[from=1-3, to=2-3]
|
|
\arrow["{F\times F}"', from=2-1, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
\end{definition}
|
|
%
|
|
We have notions of bisimulation that may involve relation lifting. An example of a relation lifting is obtained
|
|
by 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*}
|
|
We define a functor of type $(-)^\dagger\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*}
|
|
|
|
So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ that 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*}
|
|
%
|
|
%There exists a well-known notion named relator, instead of relation lifting. A relator does not need to be a functor, but it should be a map of a specific type format that is monotone with respect to inclusion. Also, relators are defined only on $\Set$ unlike relation liftings. %We discuss relators more in depth in the later chapters.
|
|
For the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ and $\spa$ we mean $\rel(\Set)$ and $\spa(\Set)$, accordingly.
|
|
|
|
We can define morphisms in $\rel$ differently by only requesting such functions $g_1$ and $g_2$ that $x\mathrel{R}y$ entails $g_1(x)\mathrel{S}g_2(y)$. Let us
|
|
call such morphisms \emph{anonymous} (because they omit the witnessing part $f$, which is unique for relations but not for general spans). This however yields
|
|
an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.}
|
|
|
|
By varying from anonymous to non-anonymous morphisms and from $\rel$ to $\spa$ we
|
|
can obtain for flavors of bisimulation (\autoref{eq:acz-mend-diag}--\autoref{def:vanila}) --
|
|
\autoref{fig:anonymous_onymous} contains a comprehensible summary.
|
|
|
|
\begin{figure}[t]
|
|
\centering
|
|
\begin{tabular}{|l|c|c|}
|
|
\hline
|
|
& \textbf{Anonymous} & \textbf{Onymous} \\
|
|
\hline
|
|
\textbf{Relations} & Witnessless & Hermida-Jacobs \\
|
|
\hline
|
|
\textbf{Spans} & Vanilla & Aczel-Mendler \\
|
|
\hline
|
|
\end{tabular}
|
|
\caption{Comparison of anonymous and onymous settings for relations and spans.}
|
|
\label{fig:anonymous_onymous}
|
|
\end{figure}
|
|
|
|
%We take $\rel(F)\c\rel(\BC)\to\rel(\BC)$ to be the functor that for an arbitrary functor $F\c\BC\to\BC$ takes a relation $R$, where $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and gives the relation that is the image of the function $\brks{Fp_1,Fp_2}\c FR\to FX\times FY$.
|
|
%\begin{definition}[Bisimulation]
|
|
% For a functor $F\c\BC\to\BC$, a bisimulation is a $\rel(F)$-coalgebra in $\rel$.
|
|
%\end{definition}
|
|
|
|
%\begin{definition}[$F$-Relator]
|
|
% For a set functor $F$, and for sets $X$ and $Y$, an $F$-relator $\relar$ is a map that takes every relation on $X\times Y$ to a relation on $FX\times FY$, and it is monotone with respect to inclusion.
|
|
%\end{definition}
|
|
%Also, for the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ we mean $\rel(\BC)$.
|
|
%
|
|
%\begin{prop}
|
|
% Assuming that $(R,\alpha)$ is a $\rel(F)$-coalgebra, where $\alpha=\beta_1\times\beta_2$ in $\BC\times\BC$, then the following diagram commutes, and vice-versa:
|
|
% \begin{equation*}
|
|
% \begin{tikzcd}[ampersand replacement=\&]
|
|
% {X_1} \& R \& {X_2} \\
|
|
% {FX_1} \& FR \& {FX_2}
|
|
% \arrow["{\beta_1}"', from=1-1, to=2-1]
|
|
% \arrow["{p_1}"', from=1-2, to=1-1]
|
|
% \arrow["{p_2}", from=1-2, to=1-3]
|
|
% \arrow["\beta", from=1-2, to=2-2]
|
|
% \arrow["{\beta_2}", from=1-3, to=2-3]
|
|
% \arrow["{Fp_1}", from=2-2, to=2-1]
|
|
% \arrow["{Fp_2}"', from=2-2, to=2-3]
|
|
% \end{tikzcd}
|
|
% \end{equation*}
|
|
%\end{prop}
|
|
\begin{definition}[Aczel-Mendler Bisimulation]
|
|
\todo{Explain in terms of span morphisms}.
|
|
|
|
|
|
A relation $R\subseteq X\times Y$ is an \emph{Aczel-Mendler bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to FR$ called witness that commutes in the following diagram:
|
|
\begin{equation*}\label{eq:acz-mend-diag}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{X} \& R \& {Y} \\
|
|
{FX} \& FR \& {FY}
|
|
\arrow["{\alpha}"', from=1-1, to=2-1]
|
|
\arrow["{p_1}"', from=1-2, to=1-1]
|
|
\arrow["{p_2}", from=1-2, to=1-3]
|
|
\arrow["\gamma", from=1-2, to=2-2]
|
|
\arrow["{\beta}", from=1-3, to=2-3]
|
|
\arrow["{Fp_1}", from=2-2, to=2-1]
|
|
\arrow["{Fp_2}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
\end{definition}
|
|
Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$
|
|
instead of $\Set$. It is worth noting that with this definition, if $R$ is a
|
|
relation, it does not necassirily mean that $FR$ is a relation as well.
|
|
%
|
|
\begin{definition}[Witnessless Bisimulation]
|
|
A relation $R\subseteq X\times Y$ is a \emph{witnessless bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)^\dagger}\beta(y)$.
|
|
% \begin{equation*}
|
|
% \begin{tikzcd}[ampersand replacement=\&]
|
|
% {X} \& R \& {Y} \\
|
|
% {FX} \& \rel(F)R \& {FY}
|
|
% \arrow["{\alpha}"', from=1-1, to=2-1]
|
|
% \arrow["{p_1}"', from=1-2, to=1-1]
|
|
% \arrow["{p_2}", from=1-2, to=1-3]
|
|
% \arrow["{\beta}", from=1-3, to=2-3]
|
|
% \arrow["{q_1}", from=2-2, to=2-1]
|
|
% \arrow["{q_2}"', from=2-2, to=2-3]
|
|
% \end{tikzcd}
|
|
% \end{equation*}
|
|
\end{definition}
|
|
A more general version of witnessless bisimulation is given by Hughes and Jacobs, where the lifting is an arbitrary lifting not necessarily the one with image factorization that we mentioned here.
|
|
|
|
\begin{definition}[Hermida-Jacobs Bisimulation]
|
|
A relation $R\subseteq X\times Y$ is a \emph{Hermida-Jacobs bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to (FR)^\dagger$ called witness that commutes in the following diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{X} \& R \& {Y} \\
|
|
{FX} \& (FR)^\dagger \& {FY}
|
|
\arrow["{\alpha}"', from=1-1, to=2-1]
|
|
\arrow["{p_1}"', from=1-2, to=1-1]
|
|
\arrow["{p_2}", from=1-2, to=1-3]
|
|
\arrow["\gamma", from=1-2, to=2-2]
|
|
\arrow["{\beta}", from=1-3, to=2-3]
|
|
\arrow["{(Fp_1)^\dagger}", from=2-2, to=2-1]
|
|
\arrow["{(Fp_2)^\dagger}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
\end{definition}
|
|
Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary category $\BC$.
|
|
|
|
\begin{definition}[Vanilla Bisimulation]\label{def:vanila}
|
|
A relation $R\subseteq X\times Y$ is a \emph{vanilla bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)}\beta(y)$.
|
|
% \begin{equation*}
|
|
% \begin{tikzcd}[ampersand replacement=\&]
|
|
% {X} \& R \& {Y} \\
|
|
% {FX} \& FR \& {FY}
|
|
% \arrow["{\alpha}"', from=1-1, to=2-1]
|
|
% \arrow["{p_1}"', from=1-2, to=1-1]
|
|
% \arrow["{p_2}", from=1-2, to=1-3]
|
|
% \arrow["{\beta}", from=1-3, to=2-3]
|
|
% \arrow["{Fp_1}", from=2-2, to=2-1]
|
|
% \arrow["{Fp_2}"', from=2-2, to=2-3]
|
|
% \end{tikzcd}
|
|
% \end{equation*}
|
|
\end{definition}
|
|
We do not know if this definition exists anywhere.
|
|
\begin{prop}
|
|
The following propositions hold in $\Set$:
|
|
\todo{How about proving that 1.3,1.4,1.5 are equivalent to each other, and all together to 1.2 under axiom of choice? }
|
|
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
|
%\item Every Aczel-Mendler bisimulation is a vanilla bisimulation.
|
|
\item Every vanilla bisimulation is an Aczel-Mendler bisimulation.
|
|
\item Every Aczel-Mendler bisimulation is a Hermida-Jacobs bisimulation.
|
|
\item Assuming the axiom of choice, every Hermida-Jacobs bisimulation is an Aczel-Mendler bisimulation.
|
|
\item Every witnessless bisimulation is a Hermida-Jacobs bisimulation.
|
|
%\item Every Hermida-Jacobs bisimulation is a witnessless bisimulation.
|
|
\end{enumerate}
|
|
\end{prop}
|
|
\begin{proof}
|
|
%(I): ???%Assuming $x\mathrel{R}y$, then given by~\eqref{eq:acz-mend-diag} we have $\gamma(x,y)\in FR$, $Fp_1\comp\gamma(x,y)=\alpha(x)$, and $Fp_2\comp\gamma(x,y)=\beta(y)$ that means $\alpha(x)\mathrel{(FR)}\beta(y)$.
|
|
|
|
(I): Since $R$ is a vanilla bisimulation, for every $(x,y)\in R$ we have $\alpha(x)\mathrel{(FR)}\beta(y)$, so we can define $\gamma\c R\to FR$ as $\gamma(x,y)=(\alpha(x),\beta(y))$, and then $\gamma$ commutes in~\eqref{eq:acz-mend-diag}.
|
|
|
|
(II):\autoref{lem:norm-simp}, and given by Staton.
|
|
|
|
(III): Given by Staton, and similar to \autoref{lem:norm-simp}.
|
|
|
|
(IV): Similar to (I) we can define $\gamma(x,y)=(\alpha(x),\beta(y))$ as the witness for $R$ to be a Hermida-Jacobs bisimulation.
|
|
\end{proof}
|
|
\begin{rem}\todo{No, these definitions are just equivalent.}
|
|
For vanilla bisimulation to be a witnessless bisimulation (or vice-versa) for a relation $R$ we need to have $FR\subseteq (FR)^\dagger$ (or $(FR)^\dagger\subseteq FR$), which is rarely true. The condition may not even be true for other relation liftings for these functors.
|
|
\end{rem}
|
|
\begin{rem}
|
|
\todo{No, this does not follow from anythying.}
|
|
To have an Aczel-Mendler bisimulation to be a vanilla bisimulation we need to have $FR\subseteq FX\times FY$ that is a rare condition. It does not hold for powerset functor or maybe functor.
|
|
\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.}
|
|
|
|
%
|
|
\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$.
|
|
\begin{definition}[A Preorder Over a Functor]
|
|
Assuming $F\c\Set\to\Set$ is a functor, we call $\appr\c\Set\to\preord$ an order over the functor $F$ iff the following diagram commutes:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
\& \preord \\
|
|
\Set \& \Set
|
|
\arrow[from=1-2, to=2-2]
|
|
\arrow["\appr", from=2-1, to=1-2]
|
|
\arrow["F"', from=2-1, to=2-2]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
\end{definition}
|
|
%
|
|
|
|
We gave an introduction to Hughes and Jacobs paper. They also have a way to represent simulation relations. In the following, we try to find a suitable formalization for simulation relations, inspired by Hughes and Jacobs.
|
|
\subsection{Relations as \cancel{Pullbacks} Spans(?)}
|
|
We can not show every relation by pullbacks, but we can just show relations of the form
|
|
\begin{gather*}
|
|
\{(a,b)\mid f(a)=g(b)\}
|
|
\end{gather*}
|
|
for some functions $f$ and $g$, when we are in $\Set$, so we can not show every object in $\rel$ using this approach, including $\rel_\appr(F)(R)\appr_{X_2};\rel(F)(R);\appr_{X_1}$ that is the target of simulation. Although we can show $\rel_\appr(F)(R)\appr_{X_2};\rel(F)(R);\appr_{X_1}$ as a span.
|
|
|
|
Assuming, we have a category $\BC$, an object of the category of spans over $\BC$ is $(R,X_1,X_2,p_1,p_2)$ in the form of the following diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
\& R \\
|
|
{X_1} \&\& {X_2}
|
|
\arrow["{p_1}"', from=1-2, to=2-1]
|
|
\arrow["{p_2}", from=1-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
A morhpism from a span $(R,X_1,X_2,p_1,p_2)$ to a span $(S,Y_1,Y_2,q_1,q_2)$ is a morphism $f\c R\to S$ in $\BC$, for which exist $f_1\c X_1\to Y_i$ and $f_2\c X_2\to Y_j$, where $i,j\in\{1,2\}$ and $i\neq j$, and they are in $\BC$, that take part in the following commuting diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{X_2} \& R \& {X_1} \\
|
|
{Y_j} \& S \& {Y_i}
|
|
\arrow["{f_2}"', from=1-1, to=2-1]
|
|
\arrow["{p_2}"', from=1-2, to=1-1]
|
|
\arrow["{p_1}", from=1-2, to=1-3]
|
|
\arrow["f", from=1-2, to=2-2]
|
|
\arrow["{f_1}", from=1-3, to=2-3]
|
|
\arrow["{q_j}", from=2-2, to=2-1]
|
|
\arrow["{q_i}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
We define a $F$-simulation as the coalgebra of the object $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ that has the following structure in $\BC$:
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \& {FX_1} \\
|
|
\& FR \& {FX_1} \\
|
|
{\appr_{X_2}} \& {FX_2} \\
|
|
{FX_2}
|
|
\arrow["{{{{{{{\pi_1}}}}}}}", from=1-1, to=1-2]
|
|
\arrow["{{{{{{{\pi_2}}}}}}}"', from=1-1, to=3-1]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-2]
|
|
\arrow["{{{{{{{\varphi_1}}}}}}}", from=1-2, to=1-3]
|
|
\arrow["{{{{{{{\varphi_2}}}}}}}", from=1-2, to=2-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3]
|
|
\arrow["{{{{{{{i^1_1}}}}}}}", from=1-3, to=1-4]
|
|
\arrow["{{{{{{{i^1_2}}}}}}}", from=1-3, to=2-3]
|
|
\arrow["{{{{{{{Fp_1}}}}}}}", from=2-2, to=2-3]
|
|
\arrow["{{{{{{{Fp_2}}}}}}}"', from=2-2, to=3-2]
|
|
\arrow["{{{{{{{i^2_1}}}}}}}"', from=3-1, to=3-2]
|
|
\arrow["{{{{{{{i^2_2}}}}}}}"', from=3-1, to=4-1]
|
|
\end{tikzcd}
|
|
|
|
%For $F=B(\mS,-)$ this object has the following structure in $\Set$:
|
|
%\begin{equation*}
|
|
% \begin{tikzcd}[ampersand replacement=\&]
|
|
% {\appr_{X_2};\rel(B(\mS,-))(E);\appr_{X_1}} \& {\appr_{X_2};\rel(B(\mS,-))(E)} \& {\appr_{X_2}} \& {B(\mS,X_2)} \\
|
|
% \& {B(\mS,E)} \& {B(\mS,FX_2)} \\
|
|
% {\appr_{X_1}} \& {B(\mS,X_1)} \\
|
|
% {B(\mS,X_1)}
|
|
% \arrow["{\pi_1}", from=1-1, to=1-2]
|
|
% \arrow["{\pi_2}"', from=1-1, to=3-1]
|
|
% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-2]
|
|
% \arrow["{\varphi_1}", from=1-2, to=1-3]
|
|
% \arrow["{\varphi_2}", from=1-2, to=2-2]
|
|
% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=1-2, to=2-3]
|
|
% \arrow["{i^2_1}", from=1-3, to=1-4]
|
|
% \arrow["{i^2_2}", from=1-3, to=2-3]
|
|
% \arrow["{B(\mS,p_2)}", from=2-2, to=2-3]
|
|
% \arrow["{B(\mS,p_1)}"', from=2-2, to=3-2]
|
|
% \arrow["{i^1_1}"', from=3-1, to=3-2]
|
|
% \arrow["{i^1_2}"', from=3-1, to=4-1]
|
|
% \end{tikzcd}
|
|
%\end{equation*}
|
|
%
|
|
%So, we call $\sigma\c E\to \appr_{X_2};\rel(B(\mS,-))(E);\appr_{X_1}$ a $B(\mS,-)$-simulation iff the following diagram commutes:
|
|
%\begin{equation*}
|
|
% \begin{tikzcd}[ampersand replacement=\&]
|
|
% {X_2} \& E \& {X_1} \\
|
|
% {B(\mS,X_2)} \& {\appr_{X_2};\rel(B(\mS,-))(E);\appr_{X_1}} \& {B(\mS,X_1)} \\
|
|
% {\appr_{X_1}} \& {\appr_{X_2};\rel(B(\mS,-))(E)} \& {\appr_{X_2}}
|
|
% \arrow["\beta"', from=1-1, to=2-1]
|
|
% \arrow["{p_2}"', from=1-2, to=1-1]
|
|
% \arrow["{p_1}", from=1-2, to=1-3]
|
|
% \arrow["\sigma", from=1-2, to=2-2]
|
|
% \arrow["\alpha", from=1-3, to=2-3]
|
|
% \arrow["{\pi_2}", from=2-2, to=3-1]
|
|
% \arrow["{\pi_1}"', from=2-2, to=3-2]
|
|
% \arrow["{i_2^1}", from=3-1, to=2-1]
|
|
% \arrow["{\varphi_1}"', from=3-2, to=3-3]
|
|
% \arrow["{i_1^2}"', from=3-3, to=2-3]
|
|
% \end{tikzcd}
|
|
%\end{equation*}
|
|
%
|
|
We show that if we consider a relation $R$ and its opposite are both simulation relations, then $R$ is a bisimulation. To reach to that goal, we give a formal definition of what we mean by the opposite of $R$ in our categorical setting that we show with $R^\op$. $(R^\op,p'_1,p'_2)$ is a span, that is isomorphic to $R$ via morphism $s\c R\to R^\op$ in $\rel$ that we call swap, and it commutes in the following commutative diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{X_2} \& R \& {X_1} \\
|
|
{X_2} \& {R^\op} \& {X_1}
|
|
\arrow["\id"', from=1-1, to=2-1]
|
|
\arrow["{p_2}"', from=1-2, to=1-1]
|
|
\arrow["{p_1}", from=1-2, to=1-3]
|
|
\arrow["s"', from=1-2, to=2-2]
|
|
\arrow["\id", from=1-3, to=2-3]
|
|
\arrow["{p'_1}", from=2-2, to=2-1]
|
|
\arrow["{p'_2}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
\begin{lemma}
|
|
The relation $(\appr_{X_1};\rel(F)(R);\appr_{X_2})^\op$ is isomorphic to $\appr_{X^\op_2};\rel(F)(R^\op);\appr_{X^\op_1}$.
|
|
\end{lemma}
|
|
\begin{proof}
|
|
We set $s_1\c\appr_{X_1}\to\appr^\op_{X_1}$ and $s_2\c\appr_{X_2}\to\appr^\op_{X_2}$ to be the swaps of $\appr_{X_1}$ and $\appr_{X_2}$, respectively. Since we have
|
|
\begin{align*}
|
|
i'^{1}_{1}\comp s_1\comp\varphi_1&\\
|
|
&=i^{1}_{2}\comp\varphi_2\\
|
|
&=Fp_1\comp\varphi_2\\
|
|
&=Fp'_2\comp Fs\comp \varphi_2,
|
|
\end{align*}
|
|
there exists the morphism $s''\c\appr_{X_1};\rel(F)(R)\to\rel(F)(R^\op);\appr_{X_1}^\op$ depicted in the following commutative diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \\
|
|
FR \& {\rel(F)(R^\op);\appr_{X_1}^\op} \& {\appr_{X_1}^\op} \\
|
|
\& {FR^\op} \& {FX_1}
|
|
\arrow["{\varphi_1}", from=1-1, to=1-2]
|
|
\arrow["{\varphi_2}"', from=1-1, to=2-1]
|
|
\arrow["{s''}", dashed, from=1-1, to=2-2]
|
|
\arrow["{s_1}"', from=1-2, to=2-3]
|
|
\arrow["Fs"', from=2-1, to=3-2]
|
|
\arrow["{{{{{\varphi'_2}}}}}", from=2-2, to=2-3]
|
|
\arrow["{{{{{\varphi'_1}}}}}"', from=2-2, to=3-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3]
|
|
\arrow["{{{{{{{{i'^{1}_1}}}}}}}}"', from=2-3, to=3-3]
|
|
\arrow["{{{{{{{{Fp'_2}}}}}}}}", from=3-2, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
Similarily, we get $s''^\mone\c\appr_{X_1};\rel(F)(R)\to\rel(F)(R^\op);\appr_{X_1}^\op$ since
|
|
\begin{align*}
|
|
i^{1}_{2}\comp s_1^\mone\comp\varphi'_2&\\
|
|
&=i'^{1}_{1}\comp\varphi_2'\\
|
|
&=Fp'_2\comp\varphi'_1\\
|
|
&=Fp_1\comp Fs_1^\mone\comp \varphi'_1,
|
|
\end{align*}
|
|
and it is depicted in the following diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{\rel(F)(R^\op);\appr_{X_1}^\op} \& {\appr_{X_1}} \\
|
|
{FR^\op} \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \\
|
|
\& FR \& {FX_1}
|
|
\arrow["{{\varphi'_2}}", from=1-1, to=1-2]
|
|
\arrow["{{\varphi'_1}}"', from=1-1, to=2-1]
|
|
\arrow["{{s''^\mone}}"', dashed, from=1-1, to=2-2]
|
|
\arrow["{s_1^\mone}", from=1-2, to=2-3]
|
|
\arrow["{Fs^\mone}"', from=2-1, to=3-2]
|
|
\arrow["{{\varphi_1}}", from=2-2, to=2-3]
|
|
\arrow["{{\varphi_2}}"', from=2-2, to=3-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3]
|
|
\arrow["{i_2^1}", from=2-3, to=3-3]
|
|
\arrow["{Fp_1}"', from=3-2, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
Obviously, $s''$ and $s''^\mone$ are each other's inverse, thus $\appr_{X_1};\rel(F)(R)$ and $\rel(F)(R^\op);\appr_{X_1}^\op$ are isomorphic.
|
|
\begin{align*}
|
|
Fp'_1\comp\varphi'_1\comp s''\comp\pi_1&\\
|
|
&=Fp'_1\comp Fs\comp\varphi_2\comp\pi_1\\
|
|
&=Fp_2\comp\varphi_2\comp\pi_1\\
|
|
&=i^2_1\comp\pi_2\\
|
|
&=i'^{2}_{2}\comp s_2\comp \pi_2
|
|
\end{align*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \\
|
|
\& {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \& {\rel(F)(R^\op);\appr_{X_1}^\op} \\
|
|
{\appr_{X_2}} \&\& {FR^\op} \\
|
|
\& {\appr_{X_2}^\op} \& {FX_2}
|
|
\arrow["{{{{{{{\pi_1}}}}}}}", from=1-1, to=1-2]
|
|
\arrow["{s'}", dashed, from=1-1, to=2-2]
|
|
\arrow["{{{{{{{\pi_2}}}}}}}"', from=1-1, to=3-1]
|
|
\arrow["{s''}", from=1-2, to=2-3]
|
|
\arrow["{{{{{{\pi'_2}}}}}}", from=2-2, to=2-3]
|
|
\arrow["{{{{{{\pi'_1}}}}}}"', from=2-2, to=4-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3]
|
|
\arrow["{\varphi'_1}", from=2-3, to=3-3]
|
|
\arrow["{{{s_2}}}", from=3-1, to=4-2]
|
|
\arrow["{Fp'_1}", from=3-3, to=4-3]
|
|
\arrow["{i'^{2}_{2}}", from=4-2, to=4-3]
|
|
\end{tikzcd}
|
|
|
|
\begin{align*}
|
|
Fp_2\comp\varphi_2\comp s''^\mone\comp\pi'_2&\\
|
|
&=Fp_2\comp Fs^\mone\comp\varphi'_1\comp\pi'_2\\
|
|
&=Fp'_1\comp\varphi'_1\comp\pi'_2\\
|
|
&=i'^{2}_{2}\comp\pi'_1\\
|
|
&=i^{2}_{1}\comp s_2^\mone\comp\pi'_1
|
|
\end{align*}
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \&\& {\rel(F)(R^\op);\appr_{X_1}^\op} \\
|
|
\& {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \\
|
|
\&\& FR \\
|
|
{\appr_{X_2}^\op} \& {\appr_{X_2}} \& {FX_2}
|
|
\arrow["{{{{{{\pi'_2}}}}}}", from=1-1, to=1-3]
|
|
\arrow["{s'^\mone}"', dashed, from=1-1, to=2-2]
|
|
\arrow["{{{{{{\pi'_1}}}}}}"', from=1-1, to=4-1]
|
|
\arrow["{s''^\mone}", from=1-3, to=2-3]
|
|
\arrow["{{{{{{{\pi_1}}}}}}}", from=2-2, to=2-3]
|
|
\arrow["{{{{{{{\pi_2}}}}}}}"', from=2-2, to=4-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3]
|
|
\arrow["{{{{{{{\varphi_2}}}}}}}", from=2-3, to=3-3]
|
|
\arrow["{{{{{{{Fp_2}}}}}}}", from=3-3, to=4-3]
|
|
\arrow["{{{s_2}^\mone}}"', from=4-1, to=4-2]
|
|
\arrow["{{{{{{{i^2_1}}}}}}}"', from=4-2, to=4-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
So, we could prove that $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ and $\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$ are isomorphic. $(\appr_{X_1};\rel(F)(R);\appr_{X_2})^\op$ is isomorphic to $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ by definition, so it is also isomorphic with $\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$.\qed
|
|
%{\tiny
|
|
% \begin{equation*}
|
|
% \begin{tikzcd}[ampersand replacement=\&]
|
|
% {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \& {\rel(F)(R^\op);\appr_{X_1}^\op} \& {\appr_{X_1}^\op} \& {FX_1} \\
|
|
% \& {FR^\op} \& {FX_1} \\
|
|
% {\appr_{X_2}^\op} \& {FX_2} \\
|
|
% {FX_2}
|
|
% \arrow["{{{{{{\pi'_2}}}}}}"', from=1-1, to=1-2]
|
|
% \arrow["{{{{{{\pi'_1}}}}}}", from=1-1, to=3-1]
|
|
% \arrow["{{{{\varphi'_2}}}}", from=1-2, to=1-3]
|
|
% \arrow[""{name=0, anchor=center, inner sep=0}, "{{{{\varphi'_1}}}}"', from=1-2, to=2-2]
|
|
% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3]
|
|
% \arrow["{{{{{{{i'^{1}_2}}}}}}}", from=1-3, to=1-4]
|
|
% \arrow["{{{{{{{i'^{1}_1}}}}}}}"', from=1-3, to=2-3]
|
|
% \arrow["{{{{{{{Fp'_2}}}}}}}", from=2-2, to=2-3]
|
|
% \arrow["{{{{{{{Fp'_1}}}}}}}", from=2-2, to=3-2]
|
|
% \arrow[""{name=1, anchor=center, inner sep=0}, from=3-1, to=3-2]
|
|
% \arrow["{{{{{{{i'^{2}_1}}}}}}}", from=3-1, to=4-1]
|
|
% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=1-1, to=0]
|
|
% \arrow["{{{{{{{i'^{2}_2}}}}}}}", from=1, to=3-2]
|
|
% \end{tikzcd}
|
|
% \end{equation*}
|
|
%}
|
|
\end{proof}
|
|
\begin{prop}
|
|
Having $\sigma\c R\to\appr_{X_2};\rel(F)(R);\appr_{X_1}$ and $\sigma^\op\c R^{\op}\to\appr_{X_1};\rel(F)(R^{\op});\appr_{X_2}$ gives rise to a morphism $\gamma\c R\to\rel(F)(R)$, and vice-versa.
|
|
\end{prop}
|
|
\begin{proof}
|
|
{\tiny
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
R \&\&\&\& {X_1} \\
|
|
\& {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \& {FX_1} \& {X_1} \\
|
|
\&\& FR \& {FX_1} \& {\appr_{X_1}^\op} \\
|
|
\& {\appr_{X_2}} \& {FX_2} \& {FR^\op} \& {\rel(F)(R^\op);\appr_{X_1}^\op} \\
|
|
{X_2} \& {FX_2} \& {\appr_{X_2}^\op} \&\& {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \\
|
|
\& {X_2} \&\&\&\& {R^\op}
|
|
\arrow["{{{{{p_1}}}}}", from=1-1, to=1-5]
|
|
\arrow["\sigma"', from=1-1, to=2-2]
|
|
\arrow["{{{{{p_2}}}}}"', from=1-1, to=5-1]
|
|
\arrow["\alpha", from=1-5, to=2-5]
|
|
\arrow["{{{{{{\pi_1}}}}}}", from=2-2, to=2-3]
|
|
\arrow["{{{{{{\pi_2}}}}}}"', from=2-2, to=4-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3]
|
|
\arrow["{{{{{{\varphi_1}}}}}}", from=2-3, to=2-4]
|
|
\arrow["{{{{{{\varphi_2}}}}}}", from=2-3, to=3-3]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4]
|
|
\arrow["{{{{{{i^1_1}}}}}}", from=2-4, to=2-5]
|
|
\arrow["{{{{{{i^1_2}}}}}}", from=2-4, to=3-4]
|
|
\arrow["{{s_1}}", from=2-4, to=3-5]
|
|
\arrow["\alpha", from=2-6, to=2-5]
|
|
\arrow["{{{{{{Fp_1}}}}}}", from=3-3, to=3-4]
|
|
\arrow["{{{{{{Fp_2}}}}}}"', from=3-3, to=4-3]
|
|
\arrow["Fs"', from=3-3, to=4-4]
|
|
\arrow["{{{{{{i'^{1}_2}}}}}}", from=3-5, to=2-5]
|
|
\arrow["{{{{{{i'^{1}_1}}}}}}"', from=3-5, to=3-4]
|
|
\arrow["{{{{{{i^2_1}}}}}}"', from=4-2, to=4-3]
|
|
\arrow["{{{{{{i^2_2}}}}}}"', from=4-2, to=5-2]
|
|
\arrow["{{s_2}}"', from=4-2, to=5-3]
|
|
\arrow["{{{{{{Fp'_2}}}}}}", from=4-4, to=3-4]
|
|
\arrow["{{{{{{Fp'_1}}}}}}", from=4-4, to=4-3]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=225}, draw=none, from=4-5, to=3-4]
|
|
\arrow["{{{\varphi'_2}}}", from=4-5, to=3-5]
|
|
\arrow[""{name=0, anchor=center, inner sep=0}, "{{{\varphi'_1}}}"', from=4-5, to=4-4]
|
|
\arrow["\beta"', from=5-1, to=5-2]
|
|
\arrow[""{name=1, anchor=center, inner sep=0}, from=5-3, to=4-3]
|
|
\arrow["{{{{{{i'^{2}_1}}}}}}", from=5-3, to=5-2]
|
|
\arrow["{{{{{\pi'_2}}}}}"', from=5-5, to=4-5]
|
|
\arrow["{{{{{\pi'_1}}}}}", from=5-5, to=5-3]
|
|
\arrow["\beta"', from=6-2, to=5-2]
|
|
\arrow["{{{{{p'_2}}}}}", from=6-6, to=2-6]
|
|
\arrow["{{{{{\sigma^\op}}}}}"', from=6-6, to=5-5]
|
|
\arrow["{{{{{p'_1}}}}}"', from=6-6, to=6-2]
|
|
\arrow["{{{{{{i'^{2}_2}}}}}}", from=1, to=4-3]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=5-5, to=0]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
}
|
|
($\Leftarrow$): We assume that we have the morphism $\gamma\c R\to FR$ such that the following diagram commutes:
|
|
\begin{equation}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{X_2} \& R \& {X_1} \\
|
|
{FX_2} \& FR \& {FX_1}
|
|
\arrow["\beta"', from=1-1, to=2-1]
|
|
\arrow["{p_2}"', from=1-2, to=1-1]
|
|
\arrow["{p_1}", from=1-2, to=1-3]
|
|
\arrow["\gamma", from=1-2, to=2-2]
|
|
\arrow["\alpha", from=1-3, to=2-3]
|
|
\arrow["{Fp_2}", from=2-2, to=2-1]
|
|
\arrow["{Fp_1}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
Since $\appr_{X_1}$ and $\appr_{X_1}$ preorders, they each have a morphism $\refl$ that pre-composed with their projections gives identity. As it is depicted in the following diagram the pullback property of ${\appr_{X_1};\rel(F)(R)}$ gives us $\sigma'\c R\to{\appr_{X_1};\rel(F)(R)}$ in the following commutative diagram:
|
|
\begin{equation}\label{eq:diag-thm-sig'}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
R \& {X_1} \& {FX_1} \\
|
|
\& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \\
|
|
\& FR \& {FX_1}
|
|
\arrow["{p_1}", from=1-1, to=1-2]
|
|
\arrow["{\sigma'}", dashed, from=1-1, to=2-2]
|
|
\arrow["\gamma"', bend right=30, from=1-1, to=3-2]
|
|
\arrow["\alpha", from=1-2, to=1-3]
|
|
\arrow["\refl", from=1-3, to=2-3]
|
|
\arrow["{\varphi_1}", from=2-2, to=2-3]
|
|
\arrow["{\varphi_2}", from=2-2, to=3-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3]
|
|
\arrow["{i_2^1}", from=2-3, to=3-3]
|
|
\arrow["{Fp_1}"', from=3-2, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
Then the pullback property of $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ gives us the existence of $\sigma\c R\to \appr_{X_1};\rel(F)(R);\appr_{X_2}$ in the following commutative diagram:
|
|
\begin{equation}\label{eq:diag-thm-sig}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{X_2} \&\&\& R \\
|
|
\& {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \\
|
|
\&\& FR \\
|
|
{FX_2} \& {\appr_{X_2}} \& {FX_2}
|
|
\arrow["\beta"', from=1-1, to=4-1]
|
|
\arrow["{p_2}"', from=1-4, to=1-1]
|
|
\arrow["\sigma"', dashed, from=1-4, to=2-2]
|
|
\arrow["{\sigma'}", from=1-4, to=2-3]
|
|
\arrow["\gamma", bend left=40, from=1-4, to=3-3]
|
|
\arrow["{\pi_1}", from=2-2, to=2-3]
|
|
\arrow["{\pi_2}"', from=2-2, to=4-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3]
|
|
\arrow["{\varphi_2}", from=2-3, to=3-3]
|
|
\arrow["{Fp_2}", from=3-3, to=4-3]
|
|
\arrow["\refl"', from=4-1, to=4-2]
|
|
\arrow["{i_1^2}"', from=4-2, to=4-3]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
Now, we show that $\sigma$ is a simulation:
|
|
\begin{align*}
|
|
i^1_1\comp\varphi_1\comp\pi_1\comp\sigma&&\\
|
|
&=i^1_1\comp\varphi_1\comp\sigma'&\by{\eqref{eq:diag-thm-sig}}\\
|
|
&=i^1_1\comp\refl\comp\alpha\comp p_1&\by{\eqref{eq:diag-thm-sig'}}\\
|
|
&=\alpha\comp p_1&
|
|
\end{align*}
|
|
\begin{align*}
|
|
i^2_2\comp\pi_2\comp\sigma&&\\
|
|
&=i^2_2\comp\refl\comp\beta\comp p_2&\by{\eqref{eq:diag-thm-sig}}\\
|
|
&=\beta\comp p_2
|
|
\end{align*}
|
|
Considering that $s\c R\to R^\op$ and $s'\c\appr_{X_1};\rel(F)(R);\appr_{X_2}\to\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$ are swapping isomorphisms, We set $\sigma^\op\c R^\op\to\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$ to be $\sigma^\op=s'\comp\sigma\comp s^\mone$. Now, we show that $\sigma'$ is a simulation:
|
|
\begin{align*}
|
|
i'^{1}_{2}\comp\varphi'_2\comp\pi'_2\comp \sigma^\op&\\
|
|
&=i'^{1}_{2}\comp\varphi'_2\comp\pi'_2\comp s'\comp\sigma\comp s^\mone\\
|
|
&=i^{1}_{1}\comp\varphi_1\comp\pi_1\comp\sigma\comp s^\mone\\
|
|
&=\alpha\comp p_1\comp s^\mone\\
|
|
&=\alpha\comp p'_2
|
|
\end{align*}
|
|
\begin{align*}
|
|
i'^{2}_{1}\comp\pi'_1\comp\sigma^\op=&\\
|
|
&=i'^{2}_{1}\comp\pi'_1\comp s'\comp\sigma\comp s^\mone\\
|
|
&=i_2^2\comp\pi_2\comp\sigma\comp s^\mone\\
|
|
&=\beta\comp p_2\comp s^\mone\\
|
|
&=\beta\comp p'_1
|
|
\end{align*}
|
|
\end{proof}
|
|
%
|
|
\subsection{Simulation with one relation composition}
|
|
We recall everything we had in the previous section. Although we want to work with the functor that takes $R\subseteq X_1\times X_2$ and gives $\rel(F)(R);\appr_{X_2}$.
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{\rel(F)(R);\appr_{X_2}} \& FR \& {FX_1} \\
|
|
{\appr_{X_2}} \& {FX_2} \\
|
|
{FX_2}
|
|
\arrow["{{{{{{{{\pi_1}}}}}}}}", from=1-1, to=1-2]
|
|
\arrow["{{{{{{{{\pi_2}}}}}}}}"', from=1-1, to=2-1]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
|
|
\arrow["{Fp_1}", from=1-2, to=1-3]
|
|
\arrow["{{{{{{{{Fp_2}}}}}}}}", from=1-2, to=2-2]
|
|
\arrow["{{{{{{{{i_1}}}}}}}}"', from=2-1, to=2-2]
|
|
\arrow["{{{{{{{{i_2}}}}}}}}"', from=2-1, to=3-1]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
%
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
R \&\&\& {X_1} \\
|
|
\& {\rel(F)(R);\appr_{X_2}} \& FR \& {FX_1} \& {X_1} \\
|
|
\& {\appr_{X_2}} \& {FX_2} \& FR \\
|
|
{X_2} \& {FX_2} \& {\appr_{X_2}^\op} \& {\rel(F)(R);\appr_{X_2}^\op} \\
|
|
\& {X_2} \&\&\& R
|
|
\arrow["{{p_1}}", from=1-1, to=1-4]
|
|
\arrow["\sigma", from=1-1, to=2-2]
|
|
\arrow["{{p_2}}"', from=1-1, to=4-1]
|
|
\arrow["\alpha", from=1-4, to=2-4]
|
|
\arrow["{{{{{{{{{\pi_1}}}}}}}}}", from=2-2, to=2-3]
|
|
\arrow["{{{{{{{{{\pi_2}}}}}}}}}"', from=2-2, to=3-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3]
|
|
\arrow["{{Fp_1}}", from=2-3, to=2-4]
|
|
\arrow["{{Fp_2}}", from=2-3, to=3-3]
|
|
\arrow["\alpha"', from=2-5, to=2-4]
|
|
\arrow["{{{{{{{{{i_1}}}}}}}}}"', from=3-2, to=3-3]
|
|
\arrow["{{{{{{{{{i_2}}}}}}}}}"', from=3-2, to=4-2]
|
|
\arrow["{Fp_1}"', from=3-4, to=2-4]
|
|
\arrow["{Fp_2}", from=3-4, to=3-3]
|
|
\arrow["\beta"', from=4-1, to=4-2]
|
|
\arrow["{i'_1}", from=4-3, to=3-3]
|
|
\arrow["{i'_2}", from=4-3, to=4-2]
|
|
\arrow["{\pi'_1}"', from=4-4, to=3-4]
|
|
\arrow["{\pi'_2}", from=4-4, to=4-3]
|
|
\arrow["\beta", from=5-2, to=4-2]
|
|
\arrow[from=5-5, to=2-5]
|
|
\arrow["{\sigma^\op}"', from=5-5, to=4-4]
|
|
\arrow["{p_2}", from=5-5, to=5-2]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
%
|
|
\begin{prop}
|
|
Assuming $R\subseteq X\times X$, then if we have $\sigma\c R\to\rel(F)(R);\appr_{X}$ as a simulation for $R$, and $R$ is reflexive, then we have $\gamma\c R\to\rel(F)(R)$ as a bisimulation for $R$, and vice-versa.
|
|
\end{prop}
|
|
\begin{proof}
|
|
$(\Rightarrow):$
|
|
\begin{align*}
|
|
Fp_2\comp\pi_1\comp\sigma&&\\
|
|
&=i_1\comp\pi_2\comp\sigma\\
|
|
&=i'_2\comp s\comp\pi_2\comp\sigma\\
|
|
&=
|
|
\end{align*}
|
|
\end{proof}
|
|
\subsection{Using Lax Pullbacks (Comma Objects) to Model Simulation}
|
|
A big concern with this approach is that Comma Objects are defined in a 2-category, so we can not define them in $\Set$, while our main inspirational example is coming from $\Set$.
|
|
|
|
\subsection{Working in $\Set$ First, Like Hughes and Jacobs}
|
|
|
|
\subsection{Choosing a suitable order for our setting}
|
|
Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term.
|
|
\section{Symmetric Simulation is Bisimulation}
|
|
\begin{definition}[Graph]
|
|
In a category $\BC$ a graph is a tuple $(R,X)$ of the following form:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
\& R \& \\
|
|
X \&\& X
|
|
\arrow["{p_1}"', from=1-2, to=2-1]
|
|
\arrow["{p_2}", from=1-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
Graphs over $\BC$ form a category that we show by $\gra(\BC)$.
|
|
\end{definition}
|
|
\begin{definition}[Symmetric Graph]
|
|
A graph $(R,X)$ is symmetric iff there exists an endomorphism $s\c R\to R$, such that the following diagram commutes
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& X \\
|
|
X \& R \& X
|
|
\arrow["\id"', from=1-1, to=2-1]
|
|
\arrow["{p_2}"', from=1-2, to=1-1]
|
|
\arrow["{p_1}", from=1-2, to=1-3]
|
|
\arrow["s", from=1-2, to=2-2]
|
|
\arrow["\id", from=1-3, to=2-3]
|
|
\arrow["{p_1}", from=2-2, to=2-1]
|
|
\arrow["{p_2}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
and $s\comp s=\id$. We call $s$ a \emph{swap} for $R$.
|
|
\end{definition}
|
|
\begin{lemma}\label{lem:gra-sym}
|
|
Symmetry of a graphs over preserved a functor.
|
|
\end{lemma}
|
|
\begin{definition}[Relation]
|
|
A relation in a category $\BC$ is a graph $(R,X)$ where $\brks{p_1,p_2}\c R \to X\times Y$ is monic. Relations over $\BC$ form a category that we show by $\rel(\BC)$.
|
|
\end{definition}
|
|
\begin{definition}[Jointly Monic]
|
|
A pair of morphisms $p_1,p_2\c R\to X$ is jointly monic iff for every pair of morphisms $f,g\c A \to R$ assuming that $p_1\comp f=p_1\comp g$ and $p_2\comp f=p_2\comp g$ then $f=g$.
|
|
\end{definition}
|
|
\begin{prop}\label{prop:rel-joi-mon}
|
|
A graph $(R,X)$ is a relation iff $p_1$ and $p_2$ are jointly monic.
|
|
\end{prop}
|
|
\begin{proof}
|
|
($\Rightarrow$): We assume that for morphisms $f,g\c A\to R$ we have $p_1\comp f=p_1\comp g$ and $p_2\comp f=p_2\comp g$, and we want to prove that $f=g$. Assuming that $\pi_1,\pi_2\c X\times X\to X$ are projections of $X\times X$, then we have:
|
|
\begin{align*}
|
|
\brks{p_1,p_2}\comp f&\\
|
|
=&\brks{p_1\comp f,p_2\comp f}\\
|
|
=&\brks{p_1\comp g,p_2\comp g}\\
|
|
=&\brks{p_1,p_2}\comp g
|
|
\end{align*}
|
|
Since $\brks{p_1,p_2}$ is moinc, from $\brks{p_1,p_2}\comp f=\brks{p_1,p_2}\comp g$ we get $f=g$.
|
|
|
|
($\Leftarrow$): Assuming for some morphisms $f,g\c A\to R$ we have $\brks{p_1,p_2}\comp f=\brks{p_1,p_2}\comp g$ we need to prove $f=g$. From $\brks{p_1,p_2}\comp f=\brks{p_1,p_2}\comp g$ we get $\brks{p_1\comp f,p_2\comp f}=\brks{p_1\comp g,p_2\comp g}$. Assuming that $\pi_1,\pi_2\c X\times X\to X$ are projections of $X\times X$, then we have $\pi_1\comp\brks{p_1\comp f,p_2\comp f}=\pi_1\comp\brks{p_1\comp g,p_2\comp g}$, and then $p_1\comp f=p_1\comp g$. Similarly we also get $p_2\comp f=p_2\comp g$. So, since $p_1$ and $p_2$ are jointly monic, then we have $f=g$.\qed
|
|
\end{proof}
|
|
We need to work with endofunctors over $\BC$ that are lifted over $\rel(\BC)$, for which we need to first define endofunctors lifted over $\gra(\BC)$.
|
|
Lifting from $\BC$ to $\gra(\BC)$ is easy. For $F\c\BC\to\BC$ we define $F_\gra\c\gra(\BC)\to\gra(\BC)$ as a functor that takes a graph $(R,X)$, and gives $(FR,FX)$, were $F$ is also applied on legs of the graph, i.e., $p_1,p_2\c R\to X$, so, we get the following graph:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
\& FR \& \\
|
|
FX \&\& FX
|
|
\arrow["{Fp_1}"', from=1-2, to=2-1]
|
|
\arrow["{Fp_2}", from=1-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
This lifting does not work for $\rel$. As an example, if we set $F$ to be the powerset functor $\powf$, then $(\powf R,\powf X)$ is not necessarily a relation anymore. For example, if we take $R=\{(1,0),(0,1),(0,0),(1,1)\}$, then taking $\{\{(1,0),(0,1),(0,0),(1,1)\}\}$ and $\{\{(1,0),(0,1),(0,0)\}\}$ as elements of $\powf R$, the morphism $\brks{\powf p_1,\powf p_2}$ maps them both to $(\{0,1\},\{0,1\})$ so it is not monic.
|
|
|
|
To cope with this, we assume the following epi-mono decomposition for $(R,X)\in\rel(\BC)$:
|
|
\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*}
|
|
We can define $(-)^\dagger$ as a functor from $\gra(\BC)\to\rel(\BC)$, then we define $F_\rel\c\rel(\BC)\to\rel(\BC)$ to take $(R,X)$ to the following relation:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
\& {(FR)^\dagger} \& \\
|
|
FX \&\& FX \\
|
|
\& {FX\times FX}
|
|
\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{lemma}\label{lem:norm-simp}
|
|
Assuming that we have the following commutative diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& X \\
|
|
FX \& FR \& FX
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["{{p_1}}"', from=1-2, to=1-1]
|
|
\arrow["{{p_2}}", from=1-2, to=1-3]
|
|
\arrow["{{\sigma}}", from=1-2, to=2-2]
|
|
\arrow["\alpha", from=1-3, to=2-3]
|
|
\arrow["{Fp_1}", from=2-2, to=2-1]
|
|
\arrow["{Fp_2}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
Then there exists $\sigma^\dagger\c R\to(FR)^\dagger$ in the following diagram that is also commutative:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& X \\
|
|
FX \& {(FR)^\dagger} \& FX
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["{{p_1}}"', from=1-2, to=1-1]
|
|
\arrow["{{p_2}}", from=1-2, to=1-3]
|
|
\arrow["{{\sigma^\dagger}}", from=1-2, to=2-2]
|
|
\arrow["\alpha", from=1-3, to=2-3]
|
|
\arrow["{Fp_1^\dagger}", from=2-2, to=2-1]
|
|
\arrow["{Fp_2^\dagger}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
\end{lemma}
|
|
\begin{proof}
|
|
The proof is trivial considering that $\sigma^\dagger=e_{FR}\comp\sigma$, where $e_{FR}$ is the epimorphism in the epi-mono factorization of $\brks{Fp_1,Fp_2}$, as depicted in the following diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& X \\
|
|
FX \& FR \& FX \\
|
|
FX \& {(FR)^\dagger} \& FX
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["{{p_1}}"', from=1-2, to=1-1]
|
|
\arrow["{{p_2}}", from=1-2, to=1-3]
|
|
\arrow["{{\sigma}}", from=1-2, to=2-2]
|
|
\arrow["\alpha", from=1-3, to=2-3]
|
|
\arrow["\id"', from=2-1, to=3-1]
|
|
\arrow["{Fp_1}", from=2-2, to=2-1]
|
|
\arrow["{Fp_2}"', from=2-2, to=2-3]
|
|
\arrow["{e_{FR}}", from=2-2, to=3-2]
|
|
\arrow["\id", from=2-3, to=3-3]
|
|
\arrow["{Fp_1^\dagger}", from=3-2, to=3-1]
|
|
\arrow["{Fp_2^\dagger}"', from=3-2, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
\qed
|
|
\end{proof}
|
|
We show this relation with $F_\rel(R,X)$.
|
|
\begin{definition}[Simulation]\label{def:sim}
|
|
A coalgebra $\sigma\c R\to (FR)^\dagger$ is a simulation over the $F$-coalgebra $\alpha\c X\to FX$ iff the following diagram is lax-commutative:
|
|
\begin{equation}\label{eq:diag-lax-sim}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& X \\
|
|
FX \& (FR)^\dagger \& FX
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["\appr"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
|
|
\arrow["{p_1}"', from=1-2, to=1-1]
|
|
\arrow["{p_2}", from=1-2, to=1-3]
|
|
\arrow["\sigma", from=1-2, to=2-2]
|
|
\arrow["\alpha", from=1-3, to=2-3]
|
|
\arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
|
|
\arrow["{{(Fp_1)^\dagger}}", from=2-2, to=2-1]
|
|
\arrow["{{(Fp_2)^\dagger}}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
\end{definition}
|
|
\todo{Prove that simulation in this sense of this definition is a standard simulation for powerset.}
|
|
\begin{definition}[Bisimulation]\label{def:bisim}
|
|
The morphism $\sigma$ in~\autoref{def:sim} is a bisimulation iff the mentioned diagram is fully commutative.
|
|
\end{definition}
|
|
\begin{remark}
|
|
The mentioned definition of bisimulation is actually, the classical one in the literature that is to have the following commutative diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& X \\
|
|
FX \& (FR)^\dagger \& FX
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["{p_1}"', from=1-2, to=1-1]
|
|
\arrow["{p_2}", from=1-2, to=1-3]
|
|
\arrow["\sigma", from=1-2, to=2-2]
|
|
\arrow["\alpha", from=1-3, to=2-3]
|
|
\arrow["{{(Fp_1)^\dagger}}", from=2-2, to=2-1]
|
|
\arrow["{{(Fp_2)^\dagger}}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
It may look different because we have $FX$ and not $(FX)^\dagger$, but they are the same.
|
|
An object $X\in\obj(\BC)$ is $(X,X)\in\rel(\BC)$ having $\id$ as its legs. Meaning that the $(FX)^\dagger=FX$.
|
|
\end{remark}
|
|
%
|
|
\begin{prop}\label{prop:iff-sim-bsim}
|
|
Assuming that we have a bisimulation $\sigma$ for $R$, we have the following equation:
|
|
\begin{gather*}
|
|
\sigma\comp s=(Fs)^\dagger\comp\sigma
|
|
\end{gather*}
|
|
\end{prop}
|
|
\begin{proof}
|
|
We recall that by~\autoref{lem:gra-sym}, $F_\rel(R,X)$ is symmetric with the swap $(Fs)^\dagger$. Assuming that $\sigma$ is a bisimulation, we have the following commutative diagram:
|
|
\begin{equation}\label{eq:diag-sym-rel}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
\& R \& \\
|
|
X \& R \& X \\
|
|
FX \& (FR)^\dagger \& FX \\
|
|
\& (FR)^\dagger
|
|
\arrow["{p_2}"', bend right=20, from=1-2, to=2-1]
|
|
\arrow["s", from=1-2, to=2-2]
|
|
\arrow["{p_1}", bend left=20, from=1-2, to=2-3]
|
|
\arrow["\alpha"', from=2-1, to=3-1]
|
|
\arrow["{p_1}"', from=2-2, to=2-1]
|
|
\arrow["{p_2}", from=2-2, to=2-3]
|
|
\arrow["\sigma", from=2-2, to=3-2]
|
|
\arrow["\alpha", from=2-3, to=3-3]
|
|
\arrow["{(Fp_2)^\dagger}", bend left=20, from=4-2, to=3-1]
|
|
\arrow["{(Fp_1)^\dagger}", from=3-2, to=3-1]
|
|
\arrow["{(Fp_2)^\dagger}"', from=3-2, to=3-3]
|
|
\arrow["(Fs)^\dagger", from=3-2, to=4-2]
|
|
\arrow["{(Fp_1)^\dagger}"', bend right=20, from=4-2, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
And it entails that the following diagrams are also commutative:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& X \& X \& R \& X \\
|
|
FX \& (FR)^\dagger \& FX \& FX \& (FR)^\dagger \& FX
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["{p_2}"', from=1-2, to=1-1]
|
|
\arrow["{p_1}", from=1-2, to=1-3]
|
|
\arrow["{\sigma\comp s}", from=1-2, to=2-2]
|
|
\arrow["\alpha", from=1-3, to=2-3]
|
|
\arrow["\alpha"', from=1-4, to=2-4]
|
|
\arrow["{p_2}"', from=1-5, to=1-4]
|
|
\arrow["{p_1}", from=1-5, to=1-6]
|
|
\arrow["{(Fs)^\dagger\comp \sigma}", from=1-5, to=2-5]
|
|
\arrow["\alpha", from=1-6, to=2-6]
|
|
\arrow["{(Fp_1)^\dagger}", from=2-2, to=2-1]
|
|
\arrow["{(Fp_2)^\dagger}"', from=2-2, to=2-3]
|
|
\arrow["{(Fp_1)^\dagger}", from=2-5, to=2-4]
|
|
\arrow["{(Fp_2)^\dagger}"', from=2-5, to=2-6]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
So, since $(Fp_1)^\dagger$ and $(Fp_2)^\dagger$ are jointly monic (because $F_\rel(R,X)$ is a relation and~\autoref{prop:rel-joi-mon}) we have $\sigma\comp s=(Fs)^\dagger\comp\sigma$.\qed
|
|
\end{proof}
|
|
%
|
|
\begin{cor}
|
|
Assuming $\sigma_1$ and $\sigma_2$ are simulations of type $R\to (FR)^\dagger$, and $R$ is symmetric and both $\sigma_1$ and $\sigma_2$ satisfy the following property:
|
|
\begin{gather*}
|
|
(Fs)^\dagger\comp\sigma=\sigma\comp s
|
|
\end{gather*}
|
|
Then $\sigma_1=\sigma_2$.
|
|
\end{cor}
|
|
\begin{proof}
|
|
As the mentioned property is equivalent with $\sigma$ being a bisimulation, and bisimulation is unique, then $\sigma_1=\sigma_2$.
|
|
\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*}
|
|
A\to C_1\qquad B\to C_2\qquad C_1\to C_1\qquad C_2\to C_2\qquad C'_2\to C_2
|
|
\end{gather*}
|
|
And finally, we define $\sigma$ as follows:
|
|
\begin{gather*}
|
|
\sigma(w)=
|
|
\begin{cases}
|
|
(\alpha\comp p_1(w),\alpha\comp p_2(w)) & w\neq (B,A) \\
|
|
(C'_2,C_2) & w=(B,A)
|
|
\end{cases}
|
|
\end{gather*}
|
|
|
|
It is easy to check that the conditions $\alpha\comp p_1\appr (Fp_1)^\dagger \comp\sigma$ and $(Fp_2)^\dagger \comp\sigma \appr \alpha\comp p_2$ are satisfied. For every $w\in R$ if $w\neq (B,A)$ then for $i\in\{1,2\}$, we have $\alpha\comp p_i= (Fp_i)^\dagger\comp\sigma$, and for $w=(B,A)$ we have $\alpha\comp p_1(B,A)=C_2\appr C'_2=(Fp_1)^\dagger \comp\sigma(B,A)$, and $\alpha\comp p_2(B,A)=C_1\appr C_2=(Fp_2)^\dagger \comp\sigma(B,A)$.
|
|
And $\sigma$ is not a coalgebraic bisimulation as $\alpha\comp p_1 (B,A)=C_2\neq C'_2=(Fp_1)^\dagger \comp\sigma(B,A)$.
|
|
|
|
An interesting question would be to find out what conditions $\sigma$ should have (maybe we have the answer to this!~\autoref{prop:iff-sim-bsim}), or how it should be constructed (perhaps based on a given poset) so that it will also be a coalgebraic bisimulation if $R$ is symmetric.
|
|
Another avenue would be to give another definition for simulation that does not have this issue.
|
|
|
|
Well! This counter example does not work! Because the described order $\appr$ does not satisfy the condition mentioned in Jacobs's paper. The condition is that the order on $FX$ should satisfy the property that for a morphism $f\c X\to Y$ the morphism $Ff\c FX\to FY$ preserves $\appr$. Probably, the only poset that has this property for $\mathbf{Id}$ is $\Delta$. If there is a counter-example, it is true for another functor.
|
|
|
|
(But still!)We have a counter-example for a symmetric relation $R$ that has a witness to be a simulation, but that morphism does not serve as a witness for $R$ to be a bisimulation. In the category of sets we assume that $F=\mathcal{P}$, and take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha(x)=X$ for every $x\in X$, and $\sigma$ is defined as below:
|
|
\begin{gather*}
|
|
\sigma(w)=
|
|
\begin{cases}
|
|
(X,X) & w\neq (1,3) \\
|
|
(X,X\setminus\{2\}) & w=(1,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
In this scenario, $\sigma$ is a witness for $R$ to be a simulation, but it is not a witness for $R$ to be a bisimulation. $\sigma$ is a witness for $R$ to be a simulation since for every $w\in R$ we have $\alpha(p_1(w))\subseteq((\mathcal{P}p_1)^\ddagger(\sigma(w)))=X$. Also, for every $w\in R$, $((\mathcal{P}p_2)^\ddagger(\sigma(w)))\subseteq\alpha(p_2(w))=X$. But it is not a bisimulation, since $\alpha(p_2(1,3))=\alpha(3)=X\neq(\mathcal{P}p_2)^\ddagger(\sigma(1,3))=X\setminus\{2\}$.
|
|
%
|
|
\begin{example}
|
|
And another counter-example!!! Assume that $F=\powf $, and take $R=X\times X\setminus\{(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below:
|
|
\begin{gather*}
|
|
\alpha(x)=
|
|
\begin{cases}
|
|
\{1,2\} & x=1 \\
|
|
\{2,3\} & x=2\\
|
|
\{3\} & x=3
|
|
\end{cases}
|
|
\end{gather*}
|
|
And $\sigma_1$ is defined as below:
|
|
\begin{gather*}
|
|
\sigma_1(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,2)\} & w=(1,2) \\
|
|
\{(2,1),(3,2)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w\in\{(2,2),(3,2)\} \\
|
|
\{(2,3),(3,3)\} & w=(2,3) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp\sigma_1(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w\in\{(2,2),(3,2)\} \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp\sigma_1(w)=
|
|
\begin{cases}
|
|
\{2\} & w=(1,2) \\
|
|
\{1,2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w\in\{(2,2),(3,2)\} \\
|
|
\{3\} & w=(2,3) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
\sigma'_1(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,2),(2,3)\} & w=(1,2) \\
|
|
\{(2,1),(2,2),(3,2)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w=(2,2) \\
|
|
\{(2,2),(3,3),(3,2)\} & w=(3,2) \\
|
|
\{(2,3),(2,2),(3,3)\} & w=(2,3) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp\sigma'_1(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(3,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp\sigma'_1(w)=
|
|
\begin{cases}
|
|
\{2,3\} & w=(1,2) \\
|
|
\{1,2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(3,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
$\sigma'_1$ is not a simulation!
|
|
\begin{gather*}
|
|
\sigma''_1(w)=
|
|
\begin{cases}
|
|
\{(1,2)\} & w=(1,2) \\
|
|
\{(2,1)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w=(2,2) \\
|
|
\{(3,3)\} & w=(3,2) \\
|
|
\{(3,3)\} & w=(2,3) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
|
|
\begin{gather*}
|
|
\sigma_1\appr\sigma'_1\\
|
|
\sigma_3\appr\sigma'_1\\
|
|
\beta=\sigma'_1
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf s)^\dagger\comp\sigma_1\comp s(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,3)\} & w=(1,2) \\
|
|
\{(2,1),(2,2)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w=(2,2) \\
|
|
\{(3,2),(3,3)\} & w=(3,2) \\
|
|
\{(2,2),(3,3)\} & w=(2,3) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma_1\comp s(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{3\} & w=(3,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma_1\comp s(w)=
|
|
\begin{cases}
|
|
\{2,3\} & w=(1,2) \\
|
|
\{1,2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(3,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
In this scenario, $\sigma_1$ is a simulation, but it is not a bisimulation. $\sigma'_1$, $\sigma''_1$ and $(\powf s)^\dagger\comp\sigma_1\comp s$ are neither. We can not make $\sigma_1$ bigger here to make it a bisimulation as $\alpha\comp p_1(3,2)=\{3\}\subsetneq\{2,3\}=(\powf p_1)^\dagger\comp\sigma_1(3,2)$.
|
|
|
|
The following is also a simulation and not a bisimulation:
|
|
\begin{gather*}
|
|
\sigma_2(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,2)\} & w=(1,2) \\
|
|
\{(2,1),(3,2)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w=(2,2) \\
|
|
\{(2,3),(3,3)\} & w=(2,3) \\
|
|
\{(3,3)\} & w\in\{(3,2),(3,3)\}
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp\sigma_2(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w\in\{(3,2),(3,3)\}
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp\sigma_2(w)=
|
|
\begin{cases}
|
|
\{2\} & w=(1,2) \\
|
|
\{1,2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{3\} & w=(2,3) \\
|
|
\{3\} & w\in\{(3,2),(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
\sigma'_2(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,2),(2,3)\} & w=(1,2) \\
|
|
\{(2,1),(2,2),(3,2)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w=(2,2) \\
|
|
\{(3,3),(3,2)\} & w=(3,2) \\
|
|
\{(2,3),(3,3)\} & w=(2,3) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp\sigma'_2(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{3\} & w=(3,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp\sigma'_2(w)=
|
|
\begin{cases}
|
|
\{2,3\} & w=(1,2) \\
|
|
\{1,2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(3,2) \\
|
|
\{3\} & w=(2,3) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf s)^\dagger\comp\sigma_2\comp s(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,3)\} & w=(1,2) \\
|
|
\{(2,1),(2,2)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w=(2,2) \\
|
|
\{(3,3),(3,2)\} & w=(3,2) \\
|
|
\{(3,3)\} & w=(2,3) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma_2\comp s(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{3\} & w=(3,2) \\
|
|
\{2\} & w=(2,3) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma_2\comp s(w)=
|
|
\begin{cases}
|
|
\{2,3\} & w=(1,2) \\
|
|
\{1,2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(3,2) \\
|
|
\{3\} & w=(2,3) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
$\sigma_2$ is a simulation, $\sigma'_2$ is a bisimulation, and $(\powf s)^\dagger\comp\sigma_2\comp s$ is neither.
|
|
The following is both a simulation and a bisimulation:
|
|
\begin{gather*}
|
|
\sigma_3(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,2),(2,3)\} & w=(1,2) \\
|
|
\{(2,1),(2,2),(3,2)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w=(2,2) \\
|
|
\{(2,3),(3,3)\} & w=(2,3) \\
|
|
\{(3,2),(3,3)\} & w=(3,2) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp\sigma_3(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp\sigma_3(w)=
|
|
\begin{cases}
|
|
\{2,3\} & w=(1,2) \\
|
|
\{1,2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{3\} & w=(2,3) \\
|
|
\{2,3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
The following is also a simulation and not a bisimulation:
|
|
\begin{gather*}
|
|
\sigma_4(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,2),(3,2),(2,3),(3,3)\} & w=(1,2) \\
|
|
\{(1,1),(2,1),(1,2),(2,2),(3,2)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w=(2,2) \\
|
|
\{(2,3),(3,3)\} & w=(2,3) \\
|
|
\{(1,2),(2,2),(3,2),(2,3),(3,3)\} & w=(3,2) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp\sigma_4(w)=
|
|
\begin{cases}
|
|
\{1,2,3\} & w=(1,2) \\
|
|
\{1,2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{1,2,3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp\sigma_4(w)=
|
|
\begin{cases}
|
|
\{2,3\} & w=(1,2) \\
|
|
\{1,2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{3\} & w=(2,3) \\
|
|
\{2,3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
\sigma''_4(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,2),(2,3)\} & w=(1,2) \\
|
|
\{(2,1),(2,2),(3,2)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w=(2,2) \\
|
|
\{(2,3),(3,3)\} & w=(2,3) \\
|
|
\{(3,2),(3,3)\} & w=(3,2) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp\sigma''_4(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp\sigma''_4(w)=
|
|
\begin{cases}
|
|
\{2,3\} & w=(1,2) \\
|
|
\{1,2\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{3\} & w=(2,3) \\
|
|
\{2,3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf s)^\dagger\comp\sigma_4\comp s(w)=
|
|
\begin{cases}
|
|
\{(1,1),(1,2),(2,1),(2,2),(2,3)\} & w=(1,2) \\
|
|
\{(2,1),(2,2),(2,3),(3,2),(3,3)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,3)\} & w=(2,2) \\
|
|
\{(2,1),(2,2),(2,3),(3,2),(3,3)\} & w=(2,3) \\
|
|
\{(3,2),(3,3)\} & w=(3,2) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma_4\comp s(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma_4\comp s(w)=
|
|
\begin{cases}
|
|
\{1,2,3\} & w=(1,2) \\
|
|
\{1,2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{1,2,3\} & w=(2,3) \\
|
|
\{2,3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
$\sigma_4$ is a simulation, $\sigma''_4$ is a bisimulation, and $(\powf s)^\dagger\comp\sigma_4\comp s$ is neither.
|
|
|
|
The following is also a simulation and not a bisimulation:
|
|
\begin{gather*}
|
|
\sigma_5(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,2)\} & w=(1,2) \\
|
|
\{(2,2),(3,2)\} & w=(2,1) \\
|
|
\{(1,1),(2,1)\} & w=(1,1) \\
|
|
\{(2,2),(3,2)\} & w=(2,2) \\
|
|
\{(2,3),(3,3)\} & w=(2,3) \\
|
|
\{(3,3)\} & w=(3,2) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp\sigma_5(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp\sigma_5(w)=
|
|
\begin{cases}
|
|
\{2\} & w=(1,2) \\
|
|
\{2\} & w=(2,1) \\
|
|
\{1\} & w=(1,1) \\
|
|
\{2\} & w=(2,2) \\
|
|
\{3\} & w=(2,3) \\
|
|
\{3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
The following is also a simulation and not a bisimulation:
|
|
\begin{gather*}
|
|
\sigma_6(w)=
|
|
\begin{cases}
|
|
\{(1,2),(2,2)\} & w=(1,2) \\
|
|
\{(2,1),(3,1)\} & w=(2,1) \\
|
|
\{(1,2),(2,1)\} & w=(1,1) \\
|
|
\{(2,3),(3,3)\} & w=(2,2) \\
|
|
\{(2,3),(3,3)\} & w=(2,3) \\
|
|
\{(3,2)\} & w=(3,2) \\
|
|
\{(3,3)\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
(\powf p_1)^\dagger\comp\sigma_6(w)=
|
|
\begin{cases}
|
|
\{1,2\} & w=(1,2) \\
|
|
\{2,3\} & w=(2,1) \\
|
|
\{1,2\} & w=(1,1) \\
|
|
\{2,3\} & w=(2,2) \\
|
|
\{2,3\} & w=(2,3) \\
|
|
\{3\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
(\powf p_2)^\dagger\comp\sigma_6(w)=
|
|
\begin{cases}
|
|
\{2\} & w=(1,2) \\
|
|
\{1\} & w=(2,1) \\
|
|
\{2\} & w=(1,1) \\
|
|
\{3\} & w=(2,2) \\
|
|
\{3\} & w=(2,3) \\
|
|
\{2\} & w=(3,2) \\
|
|
\{3\} & w=(3,3)
|
|
\end{cases}
|
|
\end{gather*}
|
|
\begin{gather*}
|
|
\sigma'_2=\sigma'_5=\sigma'_6=\sigma_3=\sigma''_4
|
|
\end{gather*}
|
|
\end{example}
|
|
%
|
|
If we define $\appr$ on simulations as
|
|
\begin{gather*}
|
|
\sigma_1\appr\sigma_2\iff \forall x_1,x_2\in X, (\powf p_i)^\dagger\comp\sigma_1(x_1,x_2)\subseteq(\powf p_i)^\dagger\comp\sigma_2(x_1,x_2)
|
|
\end{gather*}
|
|
\begin{lemma}
|
|
$(Hom(R,(\powf R)^\dagger),\appr)$ is a poset.
|
|
\end{lemma}
|
|
\begin{proof}
|
|
Reflexivity and transitivity are obvious. We need to prove anti-symmetry.\\
|
|
\todo{Finish!}
|
|
\end{proof}
|
|
Then we have
|
|
\begin{equation*}
|
|
\begin{tikzcd}
|
|
{\sigma_6} && {\sigma_1} \\
|
|
{\sigma_5} & {\sigma_2} & {\sigma_3} & {\sigma_4}
|
|
\arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
|
|
\arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=1-3, to=2-4]
|
|
\arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=2-1, to=2-2]
|
|
\arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
|
|
\arrow["\sqsubseteq"{description}, draw=none, from=2-2, to=2-3]
|
|
\arrow["\sqsubseteq"{description}, draw=none, from=2-3, to=2-4]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest are simulations.
|
|
\todo{So, $\sigma_3$ is a unique witness of bisimulation. How can we characterize it among all witnesses of simulation.}
|
|
%\begin{definition}\label{def:join-meet}
|
|
%We define $\join$ and $\meet$ on morphisms as follows:
|
|
%\begin{gather*}
|
|
% \forall x_1,x_2\in X,\\
|
|
% \sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2),\\
|
|
% \sigma_1 \meet \sigma_2 (x_1,x_2)= (\powf p_1)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2)\times(\powf p_2)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2).
|
|
%\end{gather*}
|
|
%\end{definition}
|
|
%\begin{lemma}\label{lem:proj-dist-set}
|
|
% For relations $R_1$ and $R_2$ the following equation holds:
|
|
% \begin{gather*}
|
|
% %(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2)
|
|
% (\powf p_i)(R_1\cup R_2)=(\powf p_i)(R_1)\cup(\powf p_i)(R_2)
|
|
% \end{gather*}
|
|
%\end{lemma}
|
|
%\begin{proof}
|
|
% We prove the lemma for the case that $i=1$. The proof is the same for $i=2$.
|
|
% Assuming $x_1\in(\powf p_1)^\dagger(R_1\cup R_2)$ then exists $x_2$ that $(x_1,x_2)\in R_1\cup R_2$, thus either $(x_1,x_2)\in R_1$ or $(x_1,x_2)\in R_2$, so we have $x_1\in(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$, respectively. So, we have $x_1\in (\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$.
|
|
%
|
|
% Now, assuming that $x_1\in(\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$ either $x_1\in(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$. Without loss of generality, we can assume $x_1\in(\powf p_1)^\dagger(R_j)$, where $j\in\{1,2\}$.
|
|
% Then there exists $x_2$ that $(x_1,x_2)\in R_j$, then we have $(x_1,x_2)\in R_1\cup R_2$ that gives $x_1\in(\powf p_1)^\dagger(R_1\cup R_2)$.
|
|
% % We prove the lemma for the case that $i=1$. The proof is the same for $i=2$.
|
|
% %
|
|
% % First, we prove $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$.
|
|
% % Assuming $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$ then exists $y_2$ that we have either $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $(y_1,y_2)\in\sigma(x_1,x_2)$. So, we have either $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$.
|
|
% %
|
|
% % Now, we prove $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have:
|
|
% % \begin{itemize}
|
|
% % \item $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$.
|
|
% % \item $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in\sigma(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$.
|
|
% % \end{itemize} \qed
|
|
% % \todo{Rewrite the proof according to the statement!}
|
|
%\end{proof}
|
|
%\begin{lemma}
|
|
% Assuming that $\sigma_1$ and $\sigma_2$ are simulation structures of type $R\to(\powf R)^\dagger$, then $\sigma_1 \join \sigma_2$ and $\sigma_1 \meet \sigma_2$ are also simulation structures of the same type.
|
|
%\end{lemma}
|
|
%\begin{proof}
|
|
% Since $\sigma_1$ and $\sigma_2$ are simulation structures, for every $(x_1,x_2)\in R$, for $i\in\{1,2\}$ we have:
|
|
% \begin{gather}
|
|
% \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2),\\
|
|
% (\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2).
|
|
% \end{gather}
|
|
% First, we prove the case for $\join$. Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$ we have the following:
|
|
% \begin{gather*}
|
|
% \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2)
|
|
% \end{gather*}
|
|
% So, by~\autoref{lem:proj-dist-set} we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))$.
|
|
% Similarly, we have $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$ that gives the following:
|
|
% \begin{gather*}
|
|
% (\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2)
|
|
% \end{gather*}
|
|
% So, by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))\subseteq\alpha(x_2)$.
|
|
%
|
|
% Now, we prove the case for $\meet$. For $\meet$ unlike $\join$ we need to prove that $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$. To achieve this, we need to show that assuming $\pi_1$, $\pi_2$ are projections of $\sigma_1\meet\sigma_2(x_1,x_2)$, then for $j\in\{1,2\}$ we have $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)\subseteq\powf p_j(R)$. Since $(\powf p_j)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\powf p_j(R)$, we have $\pi_j\comp(\sigma_1 \meet \sigma_2) (x_1,x_2)\subseteq\powf p_j(R)$, so we have $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$, meaning that $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)=(\powf p_j)^\dagger\comp(\sigma_1\meet\sigma_2)(x_1,x_2)$.\ppnote{The last part of the proof is necessary because the type of the codomain of the definition of $\meet$ is not $(\powf R)^\dagger$, but it is $\powf X\times\powf X$. Perhaps the epi-mono factorization must be used to cope with this in the abstract case.}
|
|
%
|
|
% For $j\in\{1,2\}$ we have
|
|
% \begin{gather}\label{eq:proj-meet}
|
|
% (\powf p_j)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))=(\powf p_j)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_j)^\dagger\comp\sigma_2(x_1,x_2).
|
|
% \end{gather}
|
|
% Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$, we have
|
|
% \begin{gather*}
|
|
% \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2),
|
|
% \end{gather*}
|
|
% so by~\eqref{eq:proj-meet} we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))$. Similarly, since $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$, we have
|
|
% \begin{gather*}
|
|
% (\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2),
|
|
% \end{gather*}
|
|
% so by~\eqref{eq:proj-meet} we have $(\powf p_2)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))\subseteq\alpha(x_2)$.\qed
|
|
%\end{proof}
|
|
%\begin{lemma}\label{lem:sim-opsim-inc}
|
|
% Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have:
|
|
% \begin{enumerate}
|
|
% \item $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$
|
|
% \item $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$
|
|
% \end{enumerate}
|
|
%\end{lemma}
|
|
%\begin{proof}
|
|
% We prove the second clause.
|
|
% By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
|
|
% \begin{gather*}
|
|
% \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2),\\
|
|
% (\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2).
|
|
% \end{gather*}
|
|
% From $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ since $R$ is symmetric we get $\alpha(x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_2,x_1)$, where
|
|
% \begin{gather*}
|
|
% (\powf p_1)^\dagger\comp\sigma(x_2,x_1)=(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2).
|
|
% \end{gather*}
|
|
% So, from $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. Similarly, we can get the other inequation.\qed
|
|
%\end{proof}
|
|
%\begin{lemma}\label{lem:sim-bisim-inc}
|
|
% Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure,
|
|
% \begin{enumerate}
|
|
% \item if $\sigma\appr\beta$ then we have:
|
|
% \begin{gather*}
|
|
% \alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2),
|
|
% \end{gather*}
|
|
% and if $R$ is symmetric we have
|
|
% \begin{gather*}
|
|
% (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_2).
|
|
% \end{gather*}
|
|
% \item if $\beta\appr\sigma$ then we have:
|
|
% \begin{gather*}
|
|
% (\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)
|
|
% \end{gather*}
|
|
% and if $R$ is symmetric we have
|
|
% \begin{gather*}
|
|
% \alpha(x_1)=(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2).
|
|
% \end{gather*}
|
|
% \end{enumerate}
|
|
%\end{lemma}
|
|
%\begin{proof}
|
|
% \begin{enumerate}
|
|
% \item Since $\sigma$ is a simulation structure for an arbitrary $(x_1,x_2)\in R$ we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Since $\sigma\appr\beta$ we have $(\powf p_1)\comp\sigma(x_1,x_2)\subseteq(\powf p_1)\comp\beta(x_1,x_2)$, while $(\powf p_1)\comp\beta(x_1,x_2)=\alpha(x_1)$ by definition of bisimulation. So we have $\alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Then because of the symmetry of $R$ the second clause is easily achievable by using the equations in~\eqref{eq:diag-sym-rel}.
|
|
% \item This clause can be proven similar to (1).
|
|
% \end{enumerate}\qed
|
|
%\end{proof}
|
|
%\begin{prop}
|
|
% Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure,
|
|
% \begin{enumerate}
|
|
% \item if $\sigma\appr\beta$ then we have:
|
|
% \begin{gather*}
|
|
% \beta=\sigma\join ((\powf s)^\dagger\comp\sigma\comp s)
|
|
% \end{gather*}
|
|
% \item if $\beta\appr\sigma$ then we have:
|
|
% \begin{gather*}
|
|
% \beta=\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)
|
|
% \end{gather*}
|
|
% \end{enumerate}
|
|
%\end{prop}
|
|
%\begin{proof}
|
|
% 1. We need to prove that $\sigma\join((\powf s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure.
|
|
% By~\autoref{lem:sim-opsim-inc}.(1), for every $(x_1,x_2)\in R$, we have $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(1), we have $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. So, we have $(\powf p_1)^\dagger\comp\sigma\join(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_1)$, then by~\autoref{lem:proj-dist-set} we have $(\powf p_1)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$.
|
|
%
|
|
% Also, by~\autoref{lem:sim-bisim-inc}.(1) we have $(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$. So, since we already have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ then by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_2)$.
|
|
%
|
|
% 2. We need to prove that $\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure.
|
|
% For $i\in\{1,2\}$, for every $(x_1,x_2)\in R$, we have:
|
|
% {\small
|
|
% \begin{align*}
|
|
% &(\powf p_i)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)\\
|
|
% &=(\powf p_i)^\dagger\comp(((\powf p_1)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))\times((\powf p_2)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_2)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)))\\
|
|
% &=(\powf p_i)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_i)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)
|
|
% \end{align*}
|
|
% }
|
|
%
|
|
% By~\autoref{lem:sim-opsim-inc}.(1), $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)=\alpha(x_1)$, so we have $(\powf p_1)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$.
|
|
%
|
|
% Also, by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$, so, since by~\autoref{lem:sim-opsim-inc}.(2), we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$, so we have $(\powf p_2)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))=\alpha(x_2)$.\qed
|
|
%\end{proof}
|
|
%\begin{cor}
|
|
% Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then if the bisimulation morphism exists, it is equal with the following morphism:
|
|
% \begin{gather*}
|
|
% (\bigjoin_{\sigma\in S}\sigma)\meet(\powf s)^\dagger\comp(\bigjoin_{\sigma\in S}\sigma)\comp s
|
|
% \end{gather*}
|
|
%\end{cor}
|
|
%
|
|
%\begin{lemma}
|
|
% For every $S\in \powf R$,
|
|
% \begin{gather*}
|
|
% ((\powf p_1)(S),(\powf p_2)(S))\in(\powf R)^\dagger\Leftrightarrow(\powf p_1)(S)\subseteq(\powf p_1)(R),(\powf p_2)(S)\subseteq(\powf p_2)(R)
|
|
% \end{gather*}
|
|
%\end{lemma}
|
|
%\begin{lemma}\label{prop:alph-prod}
|
|
% Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then there there exists a simulation structure $\sigma\in S$ that for every $(x_1,x_2)$, $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$.
|
|
%\end{lemma}
|
|
%\begin{proof}
|
|
% Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ for every $(x_1,x_2)$ as the following:
|
|
% \begin{gather*}
|
|
% \sigma(x_1,x_2)=(\alpha(x_1), (\powf p_2)^\dagger\comp\delta(x_1,x_2))
|
|
% \end{gather*}
|
|
% We have $\sigma(x_1,x_2)\in(\powf R)^\dagger$, as $\alpha(x_1)\subseteq\powf p_1(R)$ and $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\powf p_2(R)$ are inherited from $\delta$ being a simulation structure.
|
|
% Also, it obviously is a simulation as $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$.
|
|
%\end{proof}
|
|
%\begin{prop}\label{prop:sym-rel-bisim}
|
|
% Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then the following morphism is the bisimulation structure:
|
|
% \begin{gather*}
|
|
% (\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s
|
|
% \end{gather*}
|
|
%\end{prop}
|
|
%\begin{proof}
|
|
% For every $(x_1,x_2)\in R$ we have
|
|
% \begin{gather*}
|
|
% (\powf p_1)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=
|
|
% (\powf p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2),
|
|
% \end{gather*}
|
|
% and
|
|
% \begin{gather*}
|
|
% (\powf p_2)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=
|
|
% (\powf p_2)^\dagger\comp((\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2).
|
|
% \end{gather*}
|
|
% By~\autoref{prop:alph-prod} there exists a simulation $\delta\in S$ for which we have $(\powf p_1)^\dagger\comp\delta(x_1,x_2)=\alpha(x_1)$. So, $(\powf p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2)=\alpha(x_1)$. Then by the equations in~\eqref{eq:diag-sym-rel} we also get $(\powf p_2)^\dagger\comp((\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=\alpha(x_2)$.\qed
|
|
%\end{proof}
|
|
%\section{Symmetric Simulation in Quantaloids}
|
|
%We generalize~\autoref{prop:sym-rel-bisim} in regular quantaloids. A quantaloid is a category enriched with suplattices.
|
|
%Abstractly, first we define an operation that we need on morphisms that takes two simulation witnesses of type $R\to(FR)^\dagger$ to a morphism of type $R\to FX\times FX$:
|
|
%\begin{gather*}
|
|
% \sigma_1\simeet\sigma_2=(Fp_1)^\dagger\comp\sigma_1\meet(Fp_1)^\dagger\comp\sigma_2\times(Fp_2)^\dagger\comp\sigma_1\meet(Fp_2)^\dagger\comp\sigma_2
|
|
%\end{gather*}
|
|
%\begin{lemma}\label{prop:alph-prod-abs}
|
|
% Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation witnesses of the type $R\to (FR)^\dagger$, then there exists a simulation witness $\sigma\in S$ that, $(Fp_1)^\dagger\comp\sigma=\alpha\comp p_1$.
|
|
%\end{lemma}
|
|
%\begin{proof}
|
|
% Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ as the following:
|
|
% \begin{gather*}
|
|
% \sigma=\brks{(\alpha\comp p_1), (Fp_2)^\dagger\comp\delta}
|
|
% \end{gather*}
|
|
% We have $(Fp_1)^\dagger\comp\sigma$.
|
|
%\end{proof}
|
|
\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:
|
|
% \begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
|
% \item $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$\label{item:sim-opsim-inc:I1}
|
|
% \item $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$\label{item:sim-opsim-inc:II1}
|
|
% \end{enumerate}
|
|
%\end{lemma}
|
|
%\begin{proof}
|
|
% By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
|
|
% \begin{align}
|
|
% \alpha(x_1)\subseteq&\;\powf p_1\comp\sigma(x_1,x_2),\label{eq:alpha_x_11}\\
|
|
% \powf p_2\comp\sigma(x_1,x_2)\subseteq&\;\alpha(x_2).\label{eq:alpha_x_21}
|
|
% \end{align}
|
|
% (I): Since $R$ is symmetric $(x_2,x_1)\in R$, so from \eqref{eq:alpha_x_21} we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$.
|
|
% Therefore:
|
|
% \begin{align*}
|
|
% \powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)=&\; \powf p_2\comp\sigma\comp s(x_1,x_2)\\
|
|
% =&\; \powf p_2\comp\sigma (x_2,x_1)\\
|
|
% \subseteq&\;\alpha(x_1)\\
|
|
% \subseteq&\; \powf p_1\comp\sigma(x_1,x_2) & \by{\eqref{eq:alpha_x_11}}
|
|
% \end{align*}
|
|
% %
|
|
% (II): Analogously, from~\eqref{eq:alpha_x_11} by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$.
|
|
% Therefore:
|
|
% \begin{align*}
|
|
% \powf p_2\comp\sigma(x_1,x_2)\subseteq&\; \alpha(x_2) &\by{\eqref{eq:alpha_x_21}}\\
|
|
% \subseteq&\; \powf p_1\comp\sigma(x_2,x_1) \\
|
|
% =&\; \powf p_1\comp\sigma\comp s(x_1,x_2) \\
|
|
% =&\;\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2).&
|
|
% \end{align*}
|
|
% \qed
|
|
%\end{proof}
|
|
\begin{lemma}\label{lem:sim-opsim-inc}
|
|
In a category $\BC$, assuming that $F$ has a natural order structure $\appr$, and $\sigma\c R\to F R$ is witness for a symmetric relation $R$ to be an AM-simulation on $F$-coalgebra $(X,\alpha)$, then we have:
|
|
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
|
\item $F p_1\comp F s\comp\sigma\comp s\appr F p_1\comp\sigma$\label{item:sim-opsim-inc:I}
|
|
\item $F p_2\comp\sigma\appr F p_2\comp F s\comp\sigma\comp s$\label{item:sim-opsim-inc:II}
|
|
\end{enumerate}
|
|
\end{lemma}
|
|
\begin{proof}
|
|
By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
|
|
\begin{align}
|
|
\alpha\comp p_1\appr&\;F p_1\comp\sigma,\label{eq:alpha_x_1}\\
|
|
F p_2\comp\sigma\appr&\;\alpha\comp p_2.\label{eq:alpha_x_2}
|
|
\end{align}
|
|
(I): Since $R$ is symmetric and $\appr$ is a natural order structure, from \eqref{eq:alpha_x_2} we get $F p_2\comp\sigma\comp s\appr\alpha\comp p_2\comp s$.
|
|
Therefore:
|
|
\begin{align*}
|
|
F p_1\comp F s\comp\sigma\comp s=&\; F p_2\comp\sigma\comp s\\
|
|
\appr&\;\alpha\comp p_2\comp s\\
|
|
=&\;\alpha\comp p_1\\
|
|
\appr&\; F p_1\comp\sigma & \by{\eqref{eq:alpha_x_1}}
|
|
\end{align*}
|
|
%
|
|
(II): Analogously, from~\eqref{eq:alpha_x_1} since $R$ is symmetric and $\appr$ is a natural order structure, we get $\alpha\comp p_1\comp s\appr F p_1\comp\sigma\comp s$.
|
|
Therefore:
|
|
\begin{align*}
|
|
F p_2\comp\sigma\appr&\; \alpha\comp p_2 &\by{\eqref{eq:alpha_x_2}}\\
|
|
=&\; \alpha\comp p_1\comp s\\
|
|
\appr&\; F p_1\comp\sigma\comp s \\
|
|
=&\;F p_2\comp F s\comp\sigma\comp s.&
|
|
\end{align*}
|
|
\qed
|
|
\end{proof}
|
|
We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
|
|
\begin{gather*}
|
|
\forall x_1,x_2\in X,\\
|
|
\sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2).
|
|
\end{gather*}
|
|
%\begin{lemma}
|
|
% Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\join\sigma_2$ is also a witness that $R$ is an Aczel-Mendler simulation.
|
|
%\end{lemma}
|
|
%\begin{proof}
|
|
% \todo{Finish.}
|
|
%\end{proof}
|
|
\begin{lemma}\label{lem:proj-dist-set}
|
|
For relations $R_1$ and $R_2$ the following equation holds:
|
|
\begin{gather*}
|
|
%(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2)
|
|
\powf p_i(R_1\cup R_2)=\powf p_i(R_1)\cup(\powf p_i)(R_2)
|
|
\end{gather*}
|
|
\end{lemma}
|
|
\begin{proof}
|
|
We prove the lemma for the case that $i=1$. The proof is the same for $i=2$.
|
|
Assuming $x_1\in\powf p_1(R_1\cup R_2)$ then exists $x_2$ that $(x_1,x_2)\in R_1\cup R_2$, thus either $(x_1,x_2)\in R_1$ or $(x_1,x_2)\in R_2$, so we have $x_1\in\powf p_1R_1$ or $x_1\in\powf p_1R_2$, respectively. So, we have $x_1\in \powf p_1R_1\cup\powf p_1R_2$.
|
|
|
|
Now, assuming that $x_1\in\powf p_1R_1\cup\powf p_1R_2$ either $x_1\in\powf p_1R_1$ or $x_1\in\powf p_1R_2$. Without loss of generality, we can assume $x_1\in\powf p_1R_j$, where $j\in\{1,2\}$.
|
|
Then there exists $x_2$ that $(x_1,x_2)\in R_j$, then we have $(x_1,x_2)\in R_1\cup R_2$ that gives $x_1\in\powf p_1(R_1\cup R_2)$.\qed
|
|
% We prove the lemma for the case that $i=1$. The proof is the same for $i=2$.
|
|
%
|
|
% First, we prove $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$.
|
|
% Assuming $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$ then exists $y_2$ that we have either $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $(y_1,y_2)\in\sigma(x_1,x_2)$. So, we have either $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$.
|
|
%
|
|
% Now, we prove $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have:
|
|
% \begin{itemize}
|
|
% \item $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$.
|
|
% \item $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in\sigma(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$.
|
|
% \end{itemize} \qed
|
|
% \todo{Rewrite the proof according to the statement!}
|
|
\end{proof}
|
|
%\begin{rem}
|
|
% Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\meet\sigma_2$ is not necessarily a witness that $R$ is an Aczel-Mendler simulation.
|
|
%\end{rem}
|
|
Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this.
|
|
\begin{prop}\label{prop:alph-prod}
|
|
Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then there exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, such that $\powf p_1\comp\sigma'=\alpha\comp p_1$.
|
|
\end{prop}
|
|
\begin{proof}
|
|
We define $\sigma'(x_1,x_2)=\{(x'_1,x'_2)\mid x'_1\in\alpha\comp p_1(x_1,x_2)\;,\;(x'_1,x'_2)\in\sigma(x_1,x_2)\}$. We have $\sigma'\subseteq\sigma$ that gives $\powf p_2\comp\sigma'\subseteq\powf p_2\comp\sigma$. Additionally, we have $\powf p_1\comp\sigma'\subseteq\alpha\comp p_1$.
|
|
Furthermore, if $x'_1\in\alpha\comp p_1(x_1,x_2)$, since $\alpha\comp p_1\subseteq \powf p_1\comp\sigma$ then $x'_1\in\powf p_1\comp\sigma(x_1,x_2)$. Let $(x'_1,x'_2)\in\sigma(x_1,x_2)$. By definition of $\sigma'$, we have $(x'_1,x'_2)\in\sigma'(x_1,x_2)$, so $x'_1\in\powf p_1\comp\sigma'(x_1,x_2)$ that means $\alpha\comp p_1\subseteq \powf p_1\comp\sigma'$ as well. So, $\sigma'$ is another witness for $R$ to be an AM simulation, and we have $\alpha\comp p_1=\powf p_1\comp\sigma'$.
|
|
\qed
|
|
\end{proof}
|
|
An abstract version of the above proposition is given by Dubut that is the following:
|
|
\begin{prop}\label{prop:alph-prod-dubut}
|
|
Assuming that $R$ is a relation, and $\sigma\c R\to FR$ is a witness for $R$ to be an AM-simulation, then there exists $\sigma'\c R\to FR$ that is another witness for $R$ to be an AM-simulation, such that $Fp_1\comp\sigma'=\alpha\comp p_1$.
|
|
\end{prop}\qed
|
|
Now, we prove our main statement.
|
|
\begin{prop}\label{prop:sym-rel-bisim}
|
|
Assuming that $R$ is a symmetric relation, and $\sigma\c R\to \powf R$ is a witness for $R$ to be a simulation, for which $\powf p_1\comp\sigma=\alpha\comp p_1$, then the following morphism is a witness for $R$ to be a bisimulation:
|
|
\begin{gather*}
|
|
\sigma\join(\powf s\comp\sigma\comp s)
|
|
\end{gather*}
|
|
\end{prop}
|
|
\begin{proof}
|
|
For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:I} we have
|
|
\begin{gather*}
|
|
\powf p_1\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
|
|
\powf p_1\comp\sigma(x_1,x_2).
|
|
\end{gather*}
|
|
% and by~\autoref{prop:alph-prod},
|
|
Recall that $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:II} we have
|
|
\begin{gather*}
|
|
\powf p_2\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
|
|
\powf p_2\comp(\powf s\comp\sigma\comp s)(x_1,x_2).
|
|
\end{gather*}
|
|
Since $\powf p_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf p_2\comp(\powf s\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf s\comp\sigma\comp s)$ is a witness for $R$ to be an AM bisimulation.\qed
|
|
\end{proof}
|
|
\begin{cor}
|
|
Considering~\autoref{prop:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well.
|
|
\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$.
|
|
%\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*}
|
|
% \alpha(x_1)\in X\Rightarrow \alpha(x_2)\in X\\
|
|
% \alpha(x_1)=\bot \Rightarrow \alpha(x_2)=\bot
|
|
% \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.}:
|
|
%% \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}
|
|
%% \item $\alpha(x_1)\sappr Fp_2\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}
|
|
%% \item $\alpha(x_2)\sappr Fp_2\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4}
|
|
%% \end{enumerate}
|
|
% For every $(x_1,x_2)$ we have
|
|
% \begin{enumerate}
|
|
% \item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1},
|
|
% \item $\alpha(x_2)\sappr Fp_2\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\
|
|
%% \end{enumerate}
|
|
% and since $R$ is symmetric, we have
|
|
%% \begin{enumerate}
|
|
% \item $\alpha(x_2)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2},
|
|
% \item $\alpha(x_1)\sappr Fp_2\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3},
|
|
% \end{enumerate}
|
|
% Now, we have two cases:
|
|
% \begin{itemize}
|
|
% \item Assuming $\alpha(x_1)\in X$ then by~\eqref{eq:maybe-func-set-1} we have $Fp_1\comp\sigma(x_1,x_2)\in X$, thus $\sigma(x_1,x_2)\in R$. So, we have $Fp_2\comp\sigma(x_1,x_2)\in X$ that by~\eqref{eq:maybe-func-set-4} means $\alpha(x_2)\in X$.
|
|
% \item Assuming $\alpha(x_1)=\bot$ then by~\eqref{eq:maybe-func-set-3} we have $Fp_2\comp\sigma(x_2,x_1)=\bot$, thus $\sigma(x_2,x_1)=\bot$. So, we have $Fp_1\comp\sigma(x_2,x_1)=\bot$ that by~\eqref{eq:maybe-func-set-2} means $\alpha(x_2)=\bot$ as well.\qed
|
|
% \end{itemize}
|
|
%\end{proof}
|
|
%%\begin{proof}
|
|
%% We assume that $\sigma\c R\to R+1$ is the witness that we have for $R$ to be an AM-simulation. We prove the statement by contradiction. If the statement is false, then we either have
|
|
%% \begin{gather*}
|
|
%% \alpha(x_1)\in X\quad\&\quad \alpha(x_2)=\bot,
|
|
%% \end{gather*}
|
|
%% or
|
|
%% \begin{gather*}
|
|
%% \alpha(x_1)=\bot\quad\&\quad \alpha(x_2)\in X.
|
|
%% \end{gather*}
|
|
%% Assuming $\alpha(x_1)\in X\;\&\; \alpha(x_2)=\bot$, then since $R$ is an AM-simulation, by~\eqref{eq:diag-lax-sim}$(p_2+1)\comp \sigma(x_1,x_2)\appr\alpha(x_2)$, we have $(p_2+1)\comp \sigma(x_1,x_2)=\bot$ that entails $\sigma(x_1,x_2)=\bot$. So, we have $(p_1+1)\comp \sigma(x_1,x_2)=\bot$, while $\alpha(x_1)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark
|
|
%%
|
|
%% Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is symmetric, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed
|
|
%%\end{proof}
|
|
%
|
|
%\begin{prop}\label{prop:sym-sim-bis-maybe}
|
|
% For a $F$-coalgebra $(X,\alpha)$ in $\Set$, such that $FX=X+1$, a symmetric AM-simulation relation $R$ on $X$ is an AM-bisimulation.
|
|
%\end{prop}
|
|
%\begin{proof}
|
|
% By~\autoref{lem:maybe-func-set} for every $(x_1,x_2)\in R$, we either have
|
|
% \begin{gather*}
|
|
% \alpha(x_1)=\bot\quad\&\quad \alpha(x_2)=\bot,
|
|
% \end{gather*}
|
|
% or
|
|
% \begin{gather*}
|
|
% \alpha(x_1)\in X\quad\&\quad \alpha(x_2)\in X.
|
|
% \end{gather*}
|
|
% We define $\beta$ as a witness for $R$ to be an AM-bisimulation as follows:
|
|
% \begin{gather*}
|
|
% \beta(x_1,x_2)=
|
|
% \begin{cases}
|
|
% \bot & \alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot \\
|
|
% (\alpha(x_1),\alpha(x_2)) & \alpha(x_1)\in X\;\&\;\alpha(x_2)\in X
|
|
% \end{cases}
|
|
% \end{gather*}
|
|
% Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $Fp_i\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$.
|
|
% Now, we are left to prove that if $\alpha(x_1)\in X$ and $\alpha(x_2)\in X$ then $\beta(x_1,x_2)\in R$ that means that the codomain of $\beta$ is indeed $R+1$. We assume $\alpha(x_i)\in X$. Since $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$ we have $\beta(x_1,x_2)\in R$.
|
|
% \qed
|
|
%\end{proof}
|
|
%%%%%%Second proof:
|
|
\begin{prop}\label{prop:sym-sim-bis-may}
|
|
For a $F$-coalgebra $(X,\alpha)$ in $\Set$, such that $FX=X+1$, a symmetric AM-simulation relation $R$ on $X$ is an AM-bisimulation.
|
|
\end{prop}
|
|
\begin{proof}
|
|
We prove that $\sigma$ also is a witness for $R$ to be an AM-bisimulation. For every $(x_1,x_2)\in R$ we have
|
|
% \begin{enumerate}
|
|
% \item $\alpha(x_1)=(p_1+1)\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1},
|
|
% \item $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\
|
|
% % \end{enumerate}
|
|
% and since $R$ is symmetric, we have
|
|
% % \begin{enumerate}
|
|
% \item $\alpha(x_2)=(p_1+1)\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2},
|
|
% \item $\alpha(x_1)\sappr (p_2+1)\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3},
|
|
% \end{enumerate}
|
|
% Followed by $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$ we have the following cases:
|
|
% \begin{itemize}
|
|
% \item $\alpha(x_2)=(p_2+1)\comp\sigma(x_1,x_2)$: In this case, we already have $\sigma$ as a witness for $R$ to be a bisimulation.
|
|
% \item $p_2+1\comp\sigma(x_1,x_2)=\bot$: In this case, we have
|
|
% \begin{align*}
|
|
% (p_2+1)\comp\sigma(x_1,x_2)=\bot,&\\
|
|
% \Rightarrow&\sigma(x_1,x_2)=\bot,\\
|
|
% \Rightarrow&(p_1+1)\comp\sigma(x_1,x_2)=\bot,\\
|
|
% \Rightarrow&\alpha(x_1)=\bot,&\eqref{eq:maybe-func-set-1}\\
|
|
% \Rightarrow&(p_2+1)\comp\sigma(x_2,x_1)=\bot,&\eqref{eq:maybe-func-set-3}\\
|
|
% \Rightarrow&\sigma(x_2,x_1)=\bot,\\
|
|
% \Rightarrow&(p_1+1)\comp\sigma(x_2,x_1)=\bot,\\
|
|
% \Rightarrow&\alpha(x_2)=\bot,&\eqref{eq:maybe-func-set-2}\\
|
|
% \Rightarrow&\alpha(x_2)=(p_1+1)\comp\sigma(x_1,x_2).
|
|
% \end{align*}
|
|
% \end{itemize}\qed
|
|
\begin{enumerate}
|
|
\item $\alpha\comp p_1=(p_1+1)\comp\sigma$\label{eq:maybe-func-set-1},
|
|
\item $\alpha\comp p_2\sappr (p_2+1)\comp\sigma$\label{eq:maybe-func-set-2},\\
|
|
and since $R$ is symmetric, we have
|
|
\end{enumerate}
|
|
Followed by~\eqref{eq:maybe-func-set-2} for every $(x_1,x_2)\in R$ we have $\alpha(x_2)=(p_2+1)\comp\sigma(x_1,x_2)$ and $\Dom((p_2+1)\comp\sigma)\subseteq\Dom(\alpha\comp p_2)$. We have
|
|
\begin{align*}
|
|
\Dom((p_2+1)\comp\sigma)&\\
|
|
=&\Dom(\sigma)\\
|
|
=&\Dom((p_1+1)\comp\sigma)\\
|
|
=&\Dom(\alpha\comp p_1)&\by{\eqref{eq:maybe-func-set-1}}\\
|
|
=&\Dom(\alpha\comp p_1\comp s)\\
|
|
=&\Dom(\alpha\comp p_2)
|
|
\end{align*}
|
|
So, we have $\alpha\comp p_2= (p_2+1)\comp\sigma$ as well that means that $\sigma$ also serves as a witness for $R$ to be a bisimulation.
|
|
\end{proof}
|
|
|
|
Now, we want to abstract the given proof for an extensive category that has terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. We use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$.%For every objects $X$ and $Y$, we define $\appr$ on each $\Hom(X,Y+1)$ by saying that for $f,g\in\Hom(X,Y+1)$ we have $f\appr g$ whenever either $f=g$ or $f=\bot$.\sgnote{This abstract order is coarser than (not the concretisation of) the pointwise Set order at \autoref{lem:set-ord-str}: here the \emph{whole} map must be $\bot$, whereas pointwise a map may be $\bot$ on some points and agree elsewhere. Please check the two agree on the hom-sets you actually use, or justify why the coarser order suffices.}
|
|
%Although even in the context that we are at the moment, it does not seem plausible to prove that a symmetric simulation is a bisimulation without having an operator like $\join$ in~\autoref{prop:sym-sim-bis-maybe} that takes two morphisms of the same type and gives one.
|
|
The following lemma is an abstraction of saying that in $\Set$ assuming $f\c X\to Y+1$ and $g\c Y\to Z$, we have $\Dom((g+1)\comp f)=\Dom(f)$ that we have already used multiple times in the concrete proofs.
|
|
\begin{lemma}
|
|
Assuming that $(X_Y,f_Y,i)$ and $(X_Y,p,i)$ are pullbacks in the following diagram, then $p=g\comp f_Y$.
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{X_Y} \& X \\
|
|
Y \& {Y+Q} \\
|
|
Z \& {Z+Q'}
|
|
\arrow["i", tail, from=1-1, to=1-2]
|
|
\arrow["{f_Y}"', from=1-1, to=2-1]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
|
|
\arrow["p"', bend right=50, from=1-1, to=3-1]
|
|
\arrow["f", from=1-2, to=2-2]
|
|
\arrow["{\inl_Y}"', tail, from=2-1, to=2-2]
|
|
\arrow["{g}"', from=2-1, to=3-1]
|
|
\arrow["g+q", from=2-2, to=3-2]
|
|
\arrow["{\inl_Z}"', tail, from=3-1, to=3-2]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
\end{lemma}
|
|
\begin{proof}
|
|
IT simply relies on the fact that injections in an extensive category are assumed to be monic, and that the pullback of a monomorphism gives a monomorphism leg in the pullback's span.
|
|
\end{proof}
|
|
Assuming $f,g\in\Hom(X,Y+1)$, and that $f'\c X_f\rightarrowtail X$ and $g'\c X_g\rightarrowtail X$, and $X_f$ and $X_g$ are pullbacks of $f$ and $\inl$, and $g$ and $\inl$ accordingly, then $f\appr g$ if there exists $h\c X_f\rightarrowtail X_g$ that commutes in the following diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{X_g} \& X \\
|
|
{X_f}
|
|
\arrow["{g'}", tail, from=1-1, to=1-2]
|
|
\arrow["h", dashed, tail, from=2-1, to=1-1]
|
|
\arrow["{f'}"', tail, from=2-1, to=1-2]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
\begin{lemma}\label{lem: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}
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
\& Z \& \\
|
|
{X_h} \&\& {Z+1} \\
|
|
{X_k} \& X \\
|
|
Y \& {Y+1} \\
|
|
Z \& {Z+1}
|
|
\arrow["{\inl_Z}", tail, from=1-2, to=2-3]
|
|
\arrow["q", from=2-1, to=1-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=2-1, to=2-3]
|
|
\arrow["e"', dashed, from=2-1, to=3-1]
|
|
\arrow["{h_d}", tail, from=2-1, to=3-2]
|
|
\arrow["{k_d}", tail, from=3-1, to=3-2]
|
|
\arrow["{k_Y}"', from=3-1, to=4-1]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-1, to=4-2]
|
|
\arrow["p"', bend right=50, from=3-1, to=5-1]
|
|
\arrow["h"', from=3-2, to=2-3]
|
|
\arrow["k"', from=3-2, to=4-2]
|
|
\arrow["{\inl_Y}"', tail, from=4-1, to=4-2]
|
|
\arrow["g"', from=4-1, to=5-1]
|
|
\arrow["{g+1}"', from=4-2, to=5-2]
|
|
\arrow["{\inl_Z}"', tail, from=5-1, to=5-2]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
We define $k'=k\comp\mathsf{iso}\comp(k_d+1)\comp(e+1)\comp\mathsf{iso}$. We have:
|
|
\begin{align*}
|
|
(g+1)\comp k\comp\mathsf{iso}\comp(k_d+1)\comp(e+1)\comp\mathsf{iso}\\
|
|
(g+1)\comp k\comp\mathsf{iso}\comp(h_d+1)\comp\mathsf{iso}
|
|
\end{align*}
|
|
\todo{Finish! Perhaps, $k'=k\comp\mathsf{iso}\comp(k_d+1)\comp(e+1)\comp\mathsf{iso}$.}
|
|
\end{proof}
|
|
%\begin{proof}
|
|
% For morphisms $h\c X\to Z+1$, $g\c Y\to Z$, and $k\c X\to Y+1$, we assume $h\appr Fg\comp k$ that means we have two cases:
|
|
% \begin{itemize}
|
|
% \item $h=\bot$: In this case we take $k'=\bot$. Now, $k'\appr k$ and $Fg\comp k'=h$.
|
|
% \item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $Fg\comp k'=h$.\qed
|
|
% \end{itemize}
|
|
%\end{proof}
|
|
%To have an abstraction of~\autoref{lem:maybe-func-set} recalling that our category is extensive, we use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$. We take $\brks{\alpha\comp p_1,\alpha\comp p_2}\c R\to (X+1)\times(X+1)$, where $(X+1)\times (X+1)\iso X^2+(2\times X)+1$, and we assume the following pullbacks exist:
|
|
%\begin{equation*}
|
|
% \begin{tikzcd}[ampersand replacement=\&]
|
|
% {R_{X^2}} \& R \& {R_{2\times X}} \& R \\
|
|
% {X^2} \& {X^2+(2\times X)+1} \& {(2\times X)} \& {X^2+(2\times X)+1} \\
|
|
% \& {R_1} \& R \\
|
|
% \& 1 \& {X^2+(2\times X)+1}
|
|
% \arrow["{q_1}", from=1-1, to=1-2]
|
|
% \arrow["{q_2}"', from=1-1, to=2-1]
|
|
% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
|
|
% \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-2, to=2-2]
|
|
% \arrow["{r_1}", from=1-3, to=1-4]
|
|
% \arrow["{r_2}"', from=1-3, to=2-3]
|
|
% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4]
|
|
% \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-4, to=2-4]
|
|
% \arrow["{\mathsf{in}_1}"', from=2-1, to=2-2]
|
|
% \arrow["{\mathsf{in}_2}"', from=2-3, to=2-4]
|
|
% \arrow["{s_1}", from=3-2, to=3-3]
|
|
% \arrow["{s_2}"', from=3-2, to=4-2]
|
|
% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-2, to=4-3]
|
|
% \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=3-3, to=4-3]
|
|
% \arrow["{\mathsf{in}_3}"', from=4-2, to=4-3]
|
|
% \end{tikzcd}
|
|
%\end{equation*}
|
|
%%\begin{equation*}
|
|
%% \begin{tikzcd}[ampersand replacement=\&]
|
|
%% R \& I \& {X^2+(2\times X)+1}
|
|
%% \arrow["e", two heads, from=1-1, to=1-2]
|
|
%% \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}"', bend right=20, from=1-1, to=1-3]
|
|
%% \arrow["m", tail, from=1-2, to=1-3]
|
|
%% \end{tikzcd}
|
|
%%\end{equation*}
|
|
%So, we have the following:
|
|
%\begin{gather*}
|
|
% R\iso R_{X^2}+R_{2\times X}+R_{1}
|
|
%\end{gather*}
|
|
%And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$.
|
|
%\sgnote{This abstraction is unfinished: the crux $R_{2\times X}\iso 0$ (the ``no mixed pairs'' content of \autoref{lem:maybe-func-set}) is stated but not proved, and the subsection ends here. Either complete the argument or mark it clearly as work in progress.}
|
|
\section{Relators}
|
|
\subsection{Two-way similarity in Hughes-Jacobs}
|
|
Hughes and Jacobs define two-way similarity as $\leq\cap\leq^\op$. They give a sufficient condition for the two-way similarity to be the bisimilarity. We discuss that this condition does not allow us to say that a symmetric simularity is a bisimilarity. The condition is:
|
|
\begin{gather*}
|
|
\appr;(FR_1)^\dagger;\appr\quad\cap\quad\appr^\op;(FR_2)^\dagger;\appr^\op\qquad\subseteq\qquad(F(R_1\cap R_2))^\dagger
|
|
\end{gather*}
|
|
We need the case that $R_1=R_2$, and we refer to it with $R$. So, we need to have
|
|
\begin{gather*}
|
|
\appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op\qquad\subseteq\qquad(FR)^\dagger.
|
|
\end{gather*}
|
|
Assuming $(x_1,x_2)\quad\in\quad \appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op$ means that there exist $(u,v),(u',v')\in (FR)^\dagger$, such that $x_1\appr u$, $u'\appr x_1$, $v\appr x_2$, and $x_2\appr v'$. We can also use the symmetry of $R$, and then from $(x_1,x_2)\in R$ derive that there exist $(w,z),(w',z')$ such that $x_1\appr z$, $z'\appr x_1$, $w\appr x_2$, and $x_2\appr w'$. The situation can be illustrated as the following:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
{u'} \&\& u \& v \&\& {v'} \\
|
|
\& {x_1} \&\&\& {x_2} \\
|
|
{z'} \&\& z \& w \&\& {w'}
|
|
\arrow["\appr"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
|
|
\arrow["\appr"{marking, allow upside down}, draw=none, from=1-4, to=2-5]
|
|
\arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
|
|
\arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=3-3]
|
|
\arrow["\appr"{marking, allow upside down}, draw=none, from=2-5, to=1-6]
|
|
\arrow["\appr"{marking, allow upside down}, draw=none, from=2-5, to=3-6]
|
|
\arrow["\appr"{marking, allow upside down}, draw=none, from=3-1, to=2-2]
|
|
\arrow["\appr"{marking, allow upside down}, draw=none, from=3-4, to=2-5]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
|
|
But then how can we derive $(x_1,x_2)\in (FR)^\dagger$?
|
|
|
|
\todo{Investigate more! Can it be doable really?!}
|
|
\subsection{Uniqueness of the witness in Hughes-Jacobs definition}
|
|
In this section we set $\rel$ to be the category that has sets as objects and binary relations as morphisms.
|
|
We answer the question that why there can be multiple simulation witnesses based on~\autoref{def:sim}, while for the same relation, there is only one witness according to Hughes-Jacobs simulation.
|
|
\begin{definition}[Hughes-Jacobs Simulation]
|
|
For a functor $F$, and a poset $\appr$ over $F$ a HuJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to (Fr)^\dagger$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& Y \\
|
|
{FX} \& {\appr;(FR)^\dagger;\appr} \& {FY}
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["{p_1}"', from=1-2, to=1-1]
|
|
\arrow["{p_2}", from=1-2, to=1-3]
|
|
\arrow["\sigma", from=1-2, to=2-2]
|
|
\arrow["\beta", from=1-3, to=2-3]
|
|
\arrow["{{Fp_1}_\appr}", from=2-2, to=2-1]
|
|
\arrow["{{Fp_2}_\appr}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
\end{definition}
|
|
At the moment we have limited the discussion to the category of sets and we are talking about the powerset functor. We know that $\sigma$ is unique in the following diagram:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& Y\\
|
|
{\powf X} \& {\subseteq;(\powf R)^\dagger;\subseteq} \& {\powf Y}
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["{p_1}"', from=1-2, to=1-1]
|
|
\arrow["{p_2}", from=1-2, to=1-3]
|
|
\arrow["\sigma", dashed, from=1-2, to=2-2]
|
|
\arrow["\beta", from=1-3, to=2-3]
|
|
\arrow["{{\powf p_1}_\subseteq}", from=2-2, to=2-1]
|
|
\arrow["{{\powf p_2}_\subseteq}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\beta(x_2))$.
|
|
But $\sigma'$ in the following diagram is not unique:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& Y \\
|
|
{\powf X} \& {(\powf R)^\dagger} \& {\powf Y}
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["\subseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
|
|
\arrow["{p_1}"', from=1-2, to=1-1]
|
|
\arrow["{p_2}", from=1-2, to=1-3]
|
|
\arrow["{\sigma'}", from=1-2, to=2-2]
|
|
\arrow["\beta", from=1-3, to=2-3]
|
|
\arrow["\subseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
|
|
\arrow["{{\powf p_1^\dagger}}", from=2-2, to=2-1]
|
|
\arrow["{{\powf p_2^\dagger}}"', from=2-2, to=2-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\delta\c(\powf R)^\dagger\to\subseteq;(\powf R)^\dagger;\subseteq$ that $\sigma=\delta\comp\sigma'$, i.e., the following diagram commutes:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& R \& Y \\
|
|
{\powf X} \& {(\powf R)^\dagger} \& {\powf Y} \\
|
|
{\powf X} \& {\subseteq;(\powf R)^\dagger;\subseteq} \& {\powf Y}
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["{p_1}"', from=1-2, to=1-1]
|
|
\arrow["{p_2}", from=1-2, to=1-3]
|
|
\arrow["{\sigma'}", from=1-2, to=2-2]
|
|
\arrow["\beta", from=1-3, to=2-3]
|
|
\arrow["id"', from=2-1, to=3-1]
|
|
\arrow["\delta", from=2-2, to=3-2]
|
|
\arrow["id", from=2-3, to=3-3]
|
|
\arrow["{{\powf p_1}_\subseteq}", from=3-2, to=3-1]
|
|
\arrow["{{\powf p_2}_\subseteq}"', from=3-2, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation*}
|
|
To define $\delta$, we define $c\c(\powf R^\dagger)\to((\powf R^\dagger)\times R)+(\powf R)^\dagger$ and $u\c((\powf R^\dagger)\times R)+(\powf R)^\dagger\to\subseteq;(\powf R)^\dagger;\subseteq$ and then we define $\delta=u\comp c$. Here are the definitions for $c$ and $u$:
|
|
\begin{gather*}
|
|
c(w)=
|
|
\begin{cases}
|
|
\inl(w,(x_1,x_2)) & \exists x_1,x_2, \sigma'(x_1,x_2)=w \\
|
|
\inr w & \mathsf{o.w}
|
|
\end{cases}\\
|
|
u(\inl w,(x_1,x_2))=(\alpha(x_1),\alpha(x_2))\\
|
|
u(\inr w)=w
|
|
\end{gather*}
|
|
\subsection{Symmetric simulation}
|
|
\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{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{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$.
|
|
|
|
($\Leftarrow$): If $(r,p_1,p_2)$ is an object in $\spa$, then $r$ is a binary relation from $X$ to $Y$ so, it is a morphism of type $X\rto Y$ in $\rel$.\qed
|
|
\end{proof}
|
|
The above translation seems to be true in a more general case, where $\spa$ and $\rel$ are defined on an arbitrary category (the latter is called an allegory then).
|
|
\begin{definition}[Relator]
|
|
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]\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{eq:hej-sim}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
X \& r \& Y \\
|
|
{FX} \& {\relar r} \& {FY}
|
|
\arrow["\alpha"', from=1-1, to=2-1]
|
|
\arrow["{p_1}"', from=1-2, to=1-1]
|
|
\arrow["{p_2}", from=1-2, to=1-3]
|
|
\arrow["\sigma", from=1-2, to=2-2]
|
|
\arrow["\beta", from=1-3, to=2-3]
|
|
\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{definition}
|
|
|
|
\begin{definition}[Relator-based Simulation]
|
|
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}
|
|
From now on we refer to relator-based simulations of a relator $\relar$ with $\relar$-simulation. If we talk about a HJ-simulation we specify the witness.
|
|
\end{notation}
|
|
|
|
\begin{lemma}\label{lem:sim-simp}
|
|
$r$ being a $\relar$-simulation means that assuming $x\;r\;y$ we have $\alpha(x)\;\relar r\;\beta(y)$.
|
|
\end{lemma}
|
|
\begin{proof}
|
|
$r$ being a $\relar$-simulation means $r\leq\beta^\op\comp\relar r\comp\alpha$, meaning that if $x\;r\;y$ then $x \;\alpha;\relar r;\beta^\op\; y$, and it means that there exist $w\in\relar r$ that its first element is equal with $\alpha(x)$ and its second element is equal with $\beta(y)$, enabling us to say $\alpha(x)\;\relar r\; \beta(y)$.\qed
|
|
\end{proof}
|
|
|
|
\begin{prop}
|
|
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}
|
|
($\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$ 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:
|
|
\begin{gather*}
|
|
\hat{\relar}r=\relar r\cap (\relar(r^\op))^\op
|
|
\end{gather*}
|
|
\end{definition}
|
|
\begin{prop}
|
|
For every relator $\relar$, $\hat{\relar}$ is a relator.
|
|
\end{prop}
|
|
\begin{proof}
|
|
Almost obvious!\qed
|
|
\end{proof}
|
|
\begin{prop}
|
|
Assuming that $\relar$ is a relator, and $r$ and $r^\op$ are both $\relar$-simulations from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ and vice-versa respectively, then $r$ is also a $\hat{\relar}$-simulation.
|
|
\end{prop}
|
|
\begin{proof}
|
|
We need to prove that $x\; r\;y$ gives $\alpha(x)\;\hat{\relar} r\;\beta(y)$.
|
|
$r$ being a $\relar$-simulation means that assuming $x\;r\;y$ we have $\alpha(x)\;\relar r\;\beta(y)$. So, we are left to prove $\alpha(x)\;(\relar (r^\op))^\op\;\beta(y)$. $x\;r\;y$ gives $y\;r^\op\;x$, and $r^\op$ being a $\relar$-simulation from $\beta$ to $\alpha$ gives $\beta(y)\;\relar r^\op\; \alpha(x)$. So, we have $\alpha(x) \;(\relar(r^\op))^\op \;\beta(y)$. \qed
|
|
\end{proof}
|
|
\begin{cor}
|
|
Assuming that $\relar$ is a relator, and $r$ is a symmetric $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to itself, then $r$ is also a $\hat{\relar}$-simulation.
|
|
\end{cor}
|
|
\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{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}
|
|
\begin{proof}
|
|
Assuming $y\; r^\op x$ we have $x\; r\; y$. Since $r$ is $\relar$-simulation we have $\alpha(x)\;\relar r\;\beta (y)$. So, we have $\beta(y)\;(\relar r)^\op\;\alpha(x)$, and since $\relar$ is symmetric we have $\beta(y)\;\relar r^\op\;\alpha(x)$.\qed
|
|
\end{proof}
|
|
|
|
\begin{definition}[Behavioural Equivalence]
|
|
Two states $x$ and $y$ of two coalgebras $(X,\alpha)$ and $(Y,\beta)$ are behaviourally equivalent iff there exist a coalgebra $(Z,\gamma)$ and coalgebra morphisms $f\c(X,\alpha)\to(Z,\gamma)$ and $g\c(Y,\beta)\to(Z,\gamma)$ such that $f(x)=g(y)$. The relation $r$ consisting of all behaviourally equivalent states of these two coalgebras is called behavioural equivalence.
|
|
\end{definition}
|
|
|
|
\begin{definition}[Difunctional Relation]
|
|
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 $\relar$-similarity]
|
|
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{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}\label{prop:difunc-preser}
|
|
Assuming that $\relar$ is a $F$-relator that preserves difunctional relations, then $\hat{\relar}$ does the same.
|
|
\end{prop}
|
|
\begin{proof}
|
|
Assuming $r$ is difunctional, then there exist $f_1,f_2\c FX\to FZ$ and $g_1,g_2\c FY\to FZ$ such that $p\;\relar r\;q$ iff $f_1(p)=g_1(q)$ and $q \;\relar r^\op \;p$ iff $f_2(p)=g_2(q)$. By the definition of $\hat{\relar}$ we have $p\;\hat{\relar}r\;q$ iff $p\;\relar r\;q$ and $p\;(\relar r^\op)^\op\;q$ that is equivalent to say that $\brks{f_1,f_2}(p)=\brks{g_1,g_2}(q)$.\qed
|
|
\end{proof}
|
|
\begin{cor}
|
|
Assuming that $\relar$ is a $F$-relator that preserves difunctional relations, for every symmetric relation $r$ we have $\hat{\relar}r=\relar r$.
|
|
\end{cor}
|
|
\begin{proof}
|
|
$\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}
|
|
|
|
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)=
|
|
\begin{cases}
|
|
\{x_1,x_2\} & x=x_1 \\
|
|
\{x_2\} & x=x_2
|
|
\end{cases}
|
|
\intertext{and}
|
|
\beta(y)=
|
|
\begin{cases}
|
|
\{y_3\} & y=y_1 \\
|
|
Y & y=y_2\\
|
|
\emptyset & y=y_3
|
|
\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}
|
|
\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*}
|
|
\emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}
|
|
\end{gather*}
|
|
\end{definition}
|
|
Egli-Milner relator is not sound or complete, although its symmetrization is sound and complete.
|
|
\begin{prop}
|
|
$\hat{\emre}$-similarity from a coalgebra $(\alpha,X)$ to $(\beta,Y)$ is sound and complete.
|
|
\end{prop}
|
|
\begin{proof}
|
|
We need to prove that for every functions $f\c X\to Z$ and $g\c Y\to Z$, $\hat{\emre}(g^\op\comp f)=(\powf g)^\op\comp\powf f$.
|
|
We have $S\;\hat{\emre}(g^\op\comp f)\;T$ iff $S\;\emre(g^\op\comp f)\;T$ and $T\;\emre(f^\op\comp g)\;S$. Then we have
|
|
\begin{align*}
|
|
S\;\emre(g^\op\comp f)\;T&\\
|
|
&\iff\forall x\in S,\exists y\in T, x\;g^\op\comp f\; y\\
|
|
&\iff \forall x\in S,\exists y\in T,z\in Z, x\;f\;z\; , \; y\;g\;z,
|
|
\end{align*}
|
|
and
|
|
\begin{align*}
|
|
T\;\emre(f^\op\comp g)\;S&\\
|
|
&\iff\forall y\in T,\exists x\in S, y\;f^\op\comp g\; x\\
|
|
&\iff \forall y\in T,\exists x\in S, z\in Z, x\;f\;z\; , \; y\;g\;z.
|
|
\end{align*}
|
|
It is equivalent with the following:
|
|
\begin{gather*}
|
|
\forall x\in S,\exists y\in T, f(x)=g(y),\\
|
|
\forall y\in T,\exists x\in S, f(x)=g(y).
|
|
\end{gather*}
|
|
Equivalently, $Im(f\mid_S)=Im(g\mid_T)$, and we call images $U$ that is in $\powf Z$. So, we equivalently have
|
|
\begin{align*}
|
|
S\;\powf f\;U,\; T\;\powf g\;U&\\
|
|
&\iff S\;\powf f\;U,\; U\;(\powf g)^\op\;T\\
|
|
&\iff S\;(\powf g)^\op\comp\powf f\;T
|
|
\end{align*}\qed
|
|
\end{proof}
|
|
For every relation $r\rto X\to Y$ $\emre r=\subseteq\;\emre r=\emre r\;\subseteq=\subseteq;\emre r;\subseteq$.
|
|
%\begin{prop}
|
|
% Assuming that $r\c X\rto Y$, then $\subseteq;\hat{\emre}r;\subseteq=\subseteq;\hat{\emre}r$ and $\subseteq;\hat{\emre}r=\hat{\emre}r;\subseteq$.
|
|
%\end{prop}
|
|
|
|
|
|
Barr relator is a generalization of the Egli-Milner relator, where the functor is generalized.
|
|
|
|
\begin{definition}[Barr relator]
|
|
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}
|
|
For every set-functor $F$, the barr relator $\bar{F}$ is symmetric.
|
|
\end{prop}
|
|
\begin{proof}
|
|
Assuming that for a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ we have $r=\pi_2\comp\pi_1^\op$, then we have:
|
|
\begin{align*}
|
|
\hat{\bar{F}}r&\\
|
|
=&\bar{F}r\cap(\bar{F}r^\op)^\op\\
|
|
=&\bar{F}(\pi_2\comp\pi_1^\op)\cap(\bar{F}(\pi_2\comp\pi_1^\op)^\op)^\op\\
|
|
=&\bar{F}(\pi_2\comp\pi_1^\op)\cap(\bar{F}(\pi_1\comp\pi_2^\op))^\op\\
|
|
=&F\pi_2\comp(F\pi_1)^\op\cap(F\pi_1\comp (F\pi_2)^\op)^\op\\
|
|
=&F\pi_2\comp(F\pi_1)^\op\cap F\pi_2\comp (F\pi_1)^\op\\
|
|
=&F\pi_2\comp(F\pi_1)^\op\\
|
|
=&\bar{F}r
|
|
\end{align*}\qed
|
|
\end{proof}
|
|
\begin{prop}
|
|
$\hat{L}$ is a Barr relator.
|
|
\end{prop}
|
|
\begin{proof}
|
|
\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:
|
|
% 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
|
|
\end{gather*}
|
|
\end{definition}
|
|
|
|
\begin{prop}
|
|
For every functor $F\c\Set\to\Set$, the symmetrization of the mid-lax Bar relator is equal with the Barr relator.
|
|
\end{prop}
|
|
\begin{proof}
|
|
% Where there exist $\pi_1\c A\to X$ and $\pi_2\c A\to Y$ such that $r=\pi_2\comp\pi_1^\op$, we assume that $s \;\hat{\overrightarrow{F}}r\; t$, and we need to show that $s\;F\pi_2\comp(F\pi_1)^\op\;t$. Considering that $r^\op=\pi_1\comp\pi_2^\op$, we have:
|
|
% \begin{align*}
|
|
% s \;\hat{\overrightarrow{F}}r\; t&\\
|
|
% &\iff s\;\overrightarrow{F}r\;t\qquad\&\qquad s \;(\overrightarrow{F}r^\op)^\op\; t\\
|
|
% &\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\appr\comp(F\pi_2)^\op)^\op\;t\\
|
|
% &\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t
|
|
% \end{align*}
|
|
% Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
|
|
% \begin{gather*}
|
|
% w\;F\pi_2\comp\appr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t
|
|
% \end{gather*}
|
|
% And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
|
|
% \begin{align*}
|
|
% &w\;\appr\; v \qquad\&\qquad w\;\appr\; v\\
|
|
% \iff&(F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\
|
|
% \iff&(F\pi_1)^\op(s)\;=\; (F\pi_2^\op)(t)\\
|
|
% \iff&s\; F\pi_2\comp(F\pi_1)^\op\;t\\
|
|
% \iff&s\;\bar{F}r\;t
|
|
% \end{align*}
|
|
% So we have $\hat{\overrightarrow{F}}\leq \bar{F}$.
|
|
% Now, we are left to show that $\bar{F}\leq\hat{\overrightarrow{F}}$. For that, reading the given proof from the end to the starting point is sufficient.
|
|
\todo{Finish.}
|
|
\end{proof}
|
|
|
|
\begin{prop}
|
|
For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ the following propositions hold:
|
|
\begin{enumerate}
|
|
\item $\powf\pi_2\comp\subseteq\comp(\powf\pi_1)^\op\quad=\quad\subseteq\comp \powf\pi_2\comp(\powf\pi_1)^\op$
|
|
\item $\powf\pi_1\comp\subseteq\comp(\powf\pi_2)^\op\quad=\quad\subseteq\comp \powf\pi_1\comp(\powf\pi_2)^\op$
|
|
\end{enumerate}
|
|
\end{prop}
|
|
\begin{proof}
|
|
Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op\quad=\quad\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op$.
|
|
|
|
Assuming $x \mathrel{\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op} y$, then exist $z$ and $z'$ such that
|
|
\begin{gather*}
|
|
z \mathrel{(\powf\pi_i)} x,\\
|
|
z \mathrel{\subseteq} z',\\
|
|
z'\mathrel{(\powf\pi_j)} y.
|
|
\end{gather*}
|
|
Then from $z \mathrel{\subseteq} z'$ we get $\powf\pi_j(z)\mathrel{\subseteq}y$. So, we have $z\mathrel{\subseteq\comp \powf\pi_j} y$, thus $x\mathrel{\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$.
|
|
|
|
Now, assuming $x \mathrel{\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
|
|
\begin{gather*}
|
|
z\mathrel{(\powf\pi_i)} x,\\
|
|
z \mathrel{(\powf\pi_j)} y',\\
|
|
y' \mathrel{\subseteq} y.
|
|
\end{gather*}
|
|
We take the set $w=z\cup (\powf\pi_i(z)\times y)$ for which we have $z\subseteq w$ and $\powf\pi_j(w)=y$. So, we have $w \mathrel{(\powf\pi_j)} y$, $z\mathrel{\subseteq} w$, and $z\mathrel{(\powf\pi_i)} x$ that gives $x \mathrel{\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op} y$.\qed
|
|
\end{proof}
|
|
|
|
%\begin{lemma}
|
|
% Assuming that $F\pi_1$ and $F\pi_2$ are monotone with respect to $\sqsubseteq$ that is an order over $F$, then the following propositions hold:
|
|
% \begin{enumerate}
|
|
% \item $F\pi_2\comp\sqsupseteq\comp(F\pi_1)^\op\quad=\quad\sqsupseteq\comp F\pi_2\comp(F\pi_1)^\op$
|
|
% \item $F\pi_1\comp\sqsupseteq\comp(F\pi_2)^\op\quad=\quad\sqsupseteq\comp F\pi_1\comp(F\pi_2)^\op$
|
|
% \end{enumerate}
|
|
%\end{lemma}
|
|
%\begin{proof}
|
|
% Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\sqsupseteq\comp(F\pi_i)^\op\quad=\quad\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op$.
|
|
%
|
|
% Assuming $x \mathrel{F\pi_j\comp\sqsupseteq\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that
|
|
% \begin{gather*}
|
|
% z \mathrel{(F\pi_i)} x,\\
|
|
% z \mathrel{\sqsubseteq} z',\\
|
|
% z'\mathrel{(F\pi_j)} y.
|
|
% \end{gather*}
|
|
% Then from $z \mathrel{\sqsubseteq} z'$ we get $F\pi_j(z)\mathrel{\sqsubseteq}y$. So, we have $z\mathrel{\sqsupseteq\comp F\pi_j} y$, thus $x\mathrel{\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op} y$.
|
|
%
|
|
% Now, assuming $x \mathrel{\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
|
|
% \begin{gather*}
|
|
% z\mathrel{(F\pi_i)} x,\\
|
|
% z \mathrel{(F\pi_j)} y',\\
|
|
% y' \mathrel{\sqsubseteq} y.
|
|
% \end{gather*}
|
|
%\end{proof}
|
|
\begin{prop}
|
|
For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ is either the maybe monad, the subdistribution monad or $FX=\powf(X\times A)$, where $A$ is a set of labels, then the following propositions hold:
|
|
\begin{enumerate}
|
|
\item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$
|
|
\item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$
|
|
\end{enumerate}
|
|
\end{prop}
|
|
\begin{proof}
|
|
\todo{Finish.}
|
|
\end{proof}
|
|
%\begin{definition}[Natural Order Structure]\label{def:nat-ord}
|
|
% A \emph{natural order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that if $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X'\to X$, $g\c Y\to Y'$, then:
|
|
% \begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
|
% \item $\alpha\comp f\appr\beta\comp f$ in $\Hom(X',FY)$. \label{item:nat-ord:I}
|
|
% \item $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,FY')$. \label{item:nat-ord:II}
|
|
% \end{enumerate}
|
|
%\end{definition}
|
|
|
|
|
|
%\begin{prop}
|
|
% For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a coliftable order structure $\appr$, the following propositions hold:
|
|
% \begin{enumerate}
|
|
% \item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$
|
|
% \item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$
|
|
% \end{enumerate}
|
|
%\end{prop}
|
|
%\begin{proof}
|
|
% Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\appr\comp(F\pi_i)^\op\quad=\quad\appr\comp F\pi_j\comp(F\pi_i)^\op$.
|
|
%
|
|
% Assuming $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that
|
|
% \begin{gather*}
|
|
% z \mathrel{(F\pi_i)} x,\\
|
|
% z \mathrel{\appr} z',\\
|
|
% z'\mathrel{(F\pi_j)} y.
|
|
% \end{gather*}
|
|
% Then from $z \mathrel{\appr} z'$ since $\appr$ is a coliftable order structure by~\ref{item:nat-ord:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$.
|
|
%
|
|
% Now, assuming $x \mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
|
|
% \begin{gather*}
|
|
% z\mathrel{(F\pi_i)} x,\\
|
|
% z \mathrel{(F\pi_j)} y',\\
|
|
% y' \mathrel{\appr} y.
|
|
% \end{gather*}
|
|
% 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:
|
|
\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$
|
|
\item If $\appr$ is both liftable and coliftable, all the following are equal:
|
|
\begin{itemize}
|
|
\item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad$
|
|
\item $F\pi_2\comp(F\pi_1)^\op\comp\appr$
|
|
\item $\appr\comp F\pi_2\comp(F\pi_1)^\op$
|
|
\item $\appr\comp F\pi_2\comp(F\pi_1)^\op\comp\appr$
|
|
\end{itemize}
|
|
\end{enumerate}
|
|
\end{prop}
|
|
\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{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$.
|
|
%
|
|
% Assuming $z\in\powf g(k')$, then there exists $y'\in \{y\mid g(y)\in h\}$ that $z=g(y')$, so $z\in h$ and $\powf g(k')\subseteq h$.
|
|
%
|
|
% Assuming $z\in h$, since $h\subseteq \powf g(k)$, then $z\in\powf g(k)$. So, there exists $y'\in k$ such that $g(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means $z\in\powf g(k')$.\qed
|
|
%\end{example}
|
|
|
|
\begin{definition}[Natural Relator]
|
|
An $F$-relator $\relar$ is called \emph{natural}, whenever for every relation $r\c X\rto Y$, and all functions $f\c A\to X$, and $g\c B\to Y$, we have $\relar (g^\op\comp r\comp f)=(Fg)^\op\comp\relar r\comp Ff$.
|
|
\end{definition}
|
|
\begin{definition}[Relaional Connector]
|
|
A natural $F$-relator $\relar$ is a \emph{relational connector}, whenever for every set $X$, $\id_{FX}\subseteq\relar\id_X$.
|
|
\end{definition}
|
|
\begin{definition}[Normal Relator]
|
|
An $F$-relator $\relar$ is \emph{normal}, whenever for every set $X$, $\id_{FX}=\relar\id_X$.
|
|
\end{definition}
|
|
\begin{prop}
|
|
Every normal relational connect is difunctionally functorial.\qed
|
|
\end{prop}
|
|
|
|
\begin{prop}
|
|
Assuming that a set-functor $F$ has a liftable order structure $\appr$, then the $F$-relator $\relar r=\appr\comp Fr$ is natural.
|
|
\end{prop}
|
|
\begin{proof}
|
|
\begin{align*}
|
|
\relar (g^\op\comp r\comp f)&\\
|
|
=&\appr\comp F(g^\op\comp r\comp f)\\
|
|
=&\appr\comp(Fg)^\op\comp Fr\comp Ff\\
|
|
=&(Fg)^\op\comp\appr\comp Fr\comp Ff&\by{\autoref{lem:liftable}}\\
|
|
=&(Fg)^\op\comp\relar r\comp Ff
|
|
\end{align*}\qed
|
|
\end{proof}
|
|
\begin{remark}
|
|
One may wonder if the above proposition is true for $F$-relators $r\mapsto Fr\comp\appr$ or $r\mapsto \appr\comp Fr\comp\appr$, where the order structure $\appr$ over $F$ is coliftable. But it may not be the case because the surjectivity condition on the $g$ in~\autoref{def:coliftable-ord} prevents the same reasoning.
|
|
\end{remark}
|
|
\begin{prop}
|
|
Symmetrization of a natural relator, is natural.
|
|
\end{prop}
|
|
\begin{proof}
|
|
Assuming $\relar$ is a natural $F$-relator, we prove that $\hat{\relar}$ is natural as well. Assuming $r\c X\rto Y$, $f\c A\to X$, and $g\c B\to Y$, by naturality of $\relar$ we have $\relar (g^\op\comp r\comp f)=Fg^\op\comp \relar r\comp Ff$. Then we have:
|
|
\begin{align*}
|
|
\hat{\relar}(g^\op\comp r\comp f)&\\
|
|
=&\relar(g^\op\comp r\comp f)\cap(\relar(f^\op\comp r^\op\comp g))^\op\\
|
|
=&(Fg)^\op\comp\relar r\comp Ff\cap((Ff)^\op\comp\relar r^\op\comp Fg)^\op\\
|
|
=&(Fg)^\op\comp\relar r\comp Ff\cap (Fg)^\op\comp(\relar r^\op)^\op\comp Ff
|
|
\end{align*}
|
|
So we are left to prove
|
|
\begin{gather*}
|
|
(Fg)^\op\comp\relar r\comp Ff\cap (Fg)^\op\comp(\relar r^\op)^\op\comp Ff=(Fg)^\op\comp(\relar r\cap(\relar r^\op)^\op)\comp Ff
|
|
\end{gather*}
|
|
because then we will have $\hat{\relar}(g^\op\comp r\comp f)=(Fg)^\op\comp\hat{\relar}\comp Ff$. We have
|
|
\begin{align*}
|
|
(t,s)\in &(Fg)^\op\comp\relar r\comp Ff\cap (Fg)^\op\comp(\relar r^\op)^\op\comp Ff,\\
|
|
&\iff(t,s)\in (Fg)^\op\comp\relar r\comp Ff\quad\&\quad (t,s)\in (Fg)^\op\comp(\relar r^\op)^\op\comp Ff,\\
|
|
&\iff Ff(t) \mathrel{(\relar r)} Fg(s) \quad\&\quad Ff(t) \mathrel{(\relar r^\op)^\op} Fg(s),\\
|
|
&\iff Ff(t) \mathrel{(\relar\cap(\relar r^\op)^\op)} Fg(s),\\
|
|
&\iff t\mathrel{((Fg)^\op\comp(\relar\cap(\relar r^\op)^\op)\comp Ff)} s.
|
|
\end{align*}
|
|
It worth noting that when we have $(t,s)\in (Fg)^\op\comp\relar r\comp Ff$, it mean that there exist $t'$ and $s'$ that $(t,t')\in Ff$, $(t',s')\in \relar r$, and $(s',s)\in Fg^\op$. Since $Ff$ and $Fg$ are functions, then $t'=Ff(t)$ and $s'=Fg(s)$, and these are unique elements. The uniqueness enables us in the above reasoning to go from the second line to the third line.\qed
|
|
\end{proof}
|
|
\begin{prop}
|
|
If $\appr$ is an order structure on $F$ that for every sets $X$ and $Y$, $(\Hom(X,FY),\appr)$ is antisymmetric as well (making the posets), then the symmetrization of the left-lax Barr relator of $F$ and $\appr$ is normal.
|
|
\end{prop}
|
|
\begin{proof}
|
|
We show the left-lax Barr relator with $\relar$. We have:
|
|
\begin{align*}
|
|
\hat{\relar}\id&\\
|
|
=&\relar\id\cap(\relar\id^\op)^\op\\
|
|
=&\appr\comp F\id\cap (\appr\comp F\id^\op)^\op\\
|
|
=&\appr\cap\sappr\\
|
|
=&\id
|
|
\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.
|
|
\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.
|
|
\end{cor}
|
|
Perhaps if we can relax the definition of liftable by allowing $g$ to be a relation rather than a function, we can have a lax Barr relator that its symmetrization is a normal lax extension. Well, this idea actually does not work because if $g$ is supposed to be a relation, then $F$ can not be a set-functor, but it should be a functor on $\rel$, and it is already a big assumption.
|
|
\begin{prop}
|
|
For a natural order structure $\appr$ on a set-functor $F$, if for every $f\in\Hom(X,FY)$ we have $Ff\comp\appr=\appr\comp Ff$, then $\appr$ is coliftable.
|
|
\end{prop}
|
|
\begin{proof}
|
|
\todo{Investigate if it's true! If it is, is naturality necessary? It is really weird! If having a liftable order structure forces every witness for AM-simulation to have the left cell of the lax diagram as equality, and subset on powerset functor is a liftable order structure, then what is the counter-example number 4 that you have?!}
|
|
\end{proof}
|
|
\begin{prop}
|
|
Assuming that $\relar$ is a difunctionally functorial relator, then the symmetrization of the relator that takes $r\c X\rto Y$ to $\relar r\comp\appr$ is a sound 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 symmetrization of 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.}
|
|
\end{proof}
|
|
\subsection{Symmetrization of a lax Barr relator}
|
|
\begin{prop}
|
|
Assuming $F$ is the maybe functor $FX=X+1$, then the syemmetrization of the left-lax Barr relator of $F$ is a Barr-relator.
|
|
\end{prop}
|
|
\begin{proof}
|
|
We have the following:
|
|
\begin{align*}
|
|
\appr\comp\bar{F}r\cap(\appr\comp\bar{F}r^\op)^\op&\\
|
|
=&\appr\comp\bar{F}r\cap(\appr\comp F\pi_1\comp(F\pi_2)^\op)^\op\\
|
|
=&\appr\comp\bar{F}r\cap F\pi_2\comp(F\pi_1)^\op\comp\sappr\\
|
|
=&\appr\comp\bar{F}r\cap \bar{F}r\comp\sappr
|
|
\end{align*}
|
|
We prove that $\appr\comp\bar{F}r\cap \bar{F}r\comp\sappr=\bar{F}r$. It is obvious that $\bar{F}r\subseteq(\appr\comp\bar{F}r)$, and $\bar{F}r\subseteq(\bar{F}r\comp\sappr)$. Assuming $x\mathrel{(\appr\comp\bar{F}r\cap \bar{F}r\comp\sappr)} y$ then we have $x\mathrel{(\appr\comp\bar{F}r)} y$ and $x\mathrel{(\bar{F}r\comp\sappr)} y$, so by $x\mathrel{(\appr\comp\bar{F}r)} y$ there exists $y'$ such that $x\mathrel{\bar{F}r}y'$ and $y'\appr y$. In fact, $y'\appr y$ gives either of the following cases:
|
|
\begin{itemize}
|
|
\item $y=y'$: In this case we directly have $x\mathrel{\bar{F}r}y$.
|
|
\item $y'=\bot$: In this case we have $x\mathrel{\bar{F}r}\bot$ that means $x\mathrel{(\pi_2+1\comp(\pi_1+1)^\op)}\bot$ so there exists $z$ such that $\pi_2+1(z)=\bot$ that entails $z=\bot$ meaning that $x=\bot$. Recalling $x\mathrel{(\bar{F}r\comp\sappr)} y$, there exists $x'$ such that $x'\appr x$ and $x' \mathrel{\bar{F}r}y$. Since $x=\bot$ then $x'\appr x$ gives $x'=\bot$ that entails $x=x'$. So, from $x'\mathrel{\bar{F}r}y$ we have $x\mathrel{\bar{F}r}y$.
|
|
\end{itemize}
|
|
So, we have $(\appr\comp\bar{F}r)\subseteq\bar{F}r$ that entails $(\appr\comp\bar{F}r\cap \bar{F}r\comp\sappr)\subseteq\bar{F}r$.\qed
|
|
\end{proof}
|
|
\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.}
|
|
\end{document}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|