2336 lines
104 KiB
TeX
2336 lines
104 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{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
|
|
\newcommand{\powf}{\mathcal{P}}
|
|
\newcommand{\sappr}{\sqsupseteq}
|
|
|
|
\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{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}
|
|
%
|
|
\begin{definition}[Relation Lifting]
|
|
Assuming $F\c\Set\to\Set$ is a functor, then we call $\rel(F)\c\rel\to\rel$ a relation lifting of $F$, where the following diagram commutes:
|
|
\begin{equation*}
|
|
\begin{tikzcd}[ampersand replacement=\&]
|
|
\rel \&\& \rel \\
|
|
{\Set\times\Set} \&\& {\Set\times\Set}
|
|
\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 take $\rel(F)\c\rel\to\rel$ to be the functor that for an arbitrary functor $F$ 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\Set\to\Set$, a bisimulation is a $\rel(F)$-coalgebra in $\rel$.
|
|
\end{definition}
|
|
%
|
|
\begin{prop}
|
|
Assuming that $(R,\alpha)$ is a $\rel(F)$-coalgebra, where $\alpha=\beta_1\times\beta_2$ in $\Set\times\Set$, 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}
|
|
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["\sqsubseteq"{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["\sqsubseteq"{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}
|
|
\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}$, $\sqsubseteq=\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.
|
|
\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{lem: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{lem: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{lem: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}
|
|
\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*}
|
|
\end{proof}
|
|
\begin{prop}
|
|
$\hat{L}$ is a Barr relator.
|
|
\end{prop}
|
|
\begin{proof}
|
|
\todo{Finish.}
|
|
\end{proof}
|
|
|
|
\begin{definition}[One-sided 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 $\sqsubseteq$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{one-sided Barr relator} iff 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\sappr\comp(F\pi_1)^\op
|
|
\end{gather*}
|
|
\end{definition}
|
|
|
|
\begin{prop}
|
|
For every functor $F\c\Set\to\Set$, the symmetrization of the one-sided 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\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\sappr\comp(F\pi_2)^\op)^\op\;t\\
|
|
&\iff s\;F\pi_2\comp\sappr\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\sappr\; 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\;\sappr\; v \qquad\&\qquad w\;\appr\; v\\
|
|
\iff&(F\pi_1)^\op(s)\;\sappr\; (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.
|
|
\end{proof}
|
|
|
|
\begin{lemma}
|
|
The following propositions hold:
|
|
\begin{enumerate}
|
|
\item $\powf\pi_2\comp\supseteq\comp(\powf\pi_1)^\op\quad=\quad\supseteq\comp \powf\pi_2\comp(\powf\pi_1)^\op$
|
|
\item $\powf\pi_1\comp\supseteq\comp(\powf\pi_2)^\op\quad=\quad\supseteq\comp \powf\pi_1\comp(\powf\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 $\powf\pi_j\comp\supseteq\comp(\powf\pi_i)^\op\quad=\quad\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op$.
|
|
|
|
Assuming $x \mathrel{\powf\pi_j\comp\supseteq\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{\supseteq\comp \powf\pi_j} y$, thus $x\mathrel{\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$.
|
|
|
|
Now, assuming $x \mathrel{\supseteq\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\supseteq\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}
|
|
Assuming that $\relar$ is a relator over $F\c\Set\to\Set$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then the relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr relator.
|
|
\end{prop}
|
|
\begin{proof}
|
|
\todo{Finish.}
|
|
\end{proof}
|
|
|
|
\end{document}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|