%%% Start of LaTeX Document %%%
\documentstyle[11pt]{article}
%\documentstyle[a4,11pt]{article}
%\documentstyle[11pt]{mnotes}

% 1in margins at left and right
\oddsidemargin=0in
\evensidemargin=0in
\textwidth=6.25in              % A4 paper is 8.25in wide

% 1in margins at top and bottom
\headheight=0pt
\headsep=0pt
\topmargin=0in
\textheight=9.7in              % A4 paper is 11.7in high

\pagestyle{plain}
\setlength{\parindent}{0cm}
\setlength{\parskip}{\medskipamount}
\setlength{\itemsep}{\smallskipamount}

\title{Proving Properties of Pi in the Sky Calculus}
\author{
        {\it John Glauert, Zurab Khasidashvili} \\
       }
%\reportref{Draft}
%\date{}

%\newcommand{\comment}[1]{} % Comment out text. JRWG
\newcommand{\comment}[1]{\{\{{\sf #1}\}\}} % Highlight text. JRWG

\newenvironment{observation}{\noindent{\bf Observation: }}{}
\newenvironment{conjecture}{\noindent{\bf Conjecture: }}{}
\newenvironment{conclusion}{\noindent{\bf Conclusion: }}{}
\newenvironment{assignment}[1]{\noindent{\bf Assignment for {#1}: }}{}

\newcommand{\sembrac}[1]{[\![ #1 ]\!]}
\newcommand{\infer}[3]
           {\vspace{.2cm}
            \hbox{${\displaystyle {\frac {#1}{#2}}\hspace{.5cm}{#3}}$}
            \vspace{.2cm}}
% New macros
% Pi Sky
%\input{PiSkyMacros}
% Pi Sky
\newcommand{\PPin}[2]{?{#1} \cdot {#2}}
\newcommand{\PPoutP}[2]{{#1}\,!\,{#2}}
\newcommand{\PPout}[3]{\PPoutP{#1}{#2} \cdot {#3}}
\newcommand{\PPnew}[3]{{\nu}\,{#1} \cdot {#2} \cdot {#3}}
\newcommand{\PPmatch}[4]{[{#1} = {#2}\,:\,{#3}];\,{#4}}
\newcommand{\PPmatches}[3]{{#1},\,{#2}\,:\,{#3}}
\newcommand{\PPabs}[2]{\lambda{#1}\,{#2}}
\newcommand{\PPdef}[2]{{#1} = {#2}}
\newcommand{\PPstop}[0]{Stop}
\newcommand{\PPempty}[0]{()}
\newcommand{\PPname}[2]{{#1}:\,{#2}}
\newcommand{\PPpar}[2]{{#1}\,\|\,{#2}}
\newcommand{\PPres}[2]{\nu{#1}\,{#2}}
\newcommand{\PPsub}[2]{{#1}\{{#2}\}}
\newcommand{\PPdefn}[2]{{#1} & = & {#2}}
%\input{john-pi-macros}
% Process notation
\newcommand{\parprocs}[2]{{#1}\,|\,{#2}}
\newcommand{\restrict}[2]{({\nu}\,{#1})\,({#2})}
\newcommand{\replicate}[2]{!\,{#2}}
\newcommand{\guardedrep}[3]{!\,({#2} \cdot {#3})}
\newcommand{\recdef}[2]{{\bf rec} {\recvar {#1}} \cdot {#2}}
\newcommand{\guardedrec}[3]{{\bf rec} {\recvar {#1}} \cdot {#2}
\cdot (\,\parprocs {#3} {\recvar {#1}}\,)}
\newcommand{\recvar}[1]{{#1}}
\newcommand{\agtuse}[2]{\recvar {#1} ({#2})}
\newcommand{\agtdef}[3]{\agtuse {#1} {#2} = {#3}}
\newcommand{\agtdefn}[3]{\agtuse {#1} {#2} & = & {#3}}
\newcommand{\inpact}[3]{{#1}({#2}) \cdot {#3}}
\newcommand{\inpacta}[2]{{#1}({#2})}
\newcommand{\outact}[3]{\overline{#1}\,{#2} \cdot {#3}}
\newcommand{\outacta}[2]{\overline{#1}\,{#2}}
\newcommand{\match}[4]{{#1}={#2} \cdot {#3} \; : \; {#4}}
\newcommand{\inaction}{0}
\newcommand{\pair}[2]{{#1}\,{#2}}
\newcommand{\triv}{}
%\input{john-proc-macros}
% New Process notation
\newcommand{\Ppar}[2]{{#1},\;{#2}}
\newcommand{\Pcall}[2]{{#1}\,!\,{#2}}
\newcommand{\Pdef}[2]{{#1}:{#2}}
\newcommand{\Prule}[5]{\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}} &
\rightarrow & \Ppar{\Pdef{#1}{#5}}{#4}}
\newcommand{\PruleChange}[4]{\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}} &
\rightarrow & \Pdef{#1}{#4}}
\newcommand{\PruleSpawn}[4]{\Prule{#1}{#2}{#3}{#4}{#2}}
% Translation representation
\newcommand{\transwhere}[4]{& & {\makebox[1.5cm][l]{where}}
\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}}  \rightarrow
\Ppar{\Pdef{#1}{#2}}{#4}}
\newcommand{\transand}[4]{& & {\makebox[1.5cm][l]{and}}
\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}}  \rightarrow
\Ppar{\Pdef{#1}{#2}}{#4}}
\newcommand{\PPwhere}[2]{where & & {#1} \; = \; {#2}}
\newcommand{\PPand}[2]{and & & {#1} \; = \; {#2}}
\newcommand{\F}{Facile}
\newcommand{\Cham}{Chemical Abstract Machine}
\newcommand{\Lc}{$\lambda$--calculus}
\newcommand{\LC}{$\lambda$--Calculus}
\newcommand{\Lx}{$\lambda$--expression}
\newcommand{\Pc}{$\pi$--calculus}
\newcommand{\PC}{$\pi$--Calculus}
\newcommand{\TPC}{Term--$\pi$--Calculus}
\newcommand{\TPc}{term--$\pi$--calculus}
\newcommand{\PPC}{$\pi^\pi$--Calculus}
\newcommand{\PPc}{$\pi^\pi$--calculus}
\newcommand{\TPPC}{Term--$\pi^\pi$--Calculus}
\newcommand{\TPPc}{term--$\pi^\pi$--calculus}
\newcommand{\OGRe}{OGRe}
\newcommand{\RA}{{\em return-address\/} channel}
% Source representation
\newcommand{\Labs}[2]{\lambda{#1}.\,{#2}}
\newcommand{\Lapp}[2]{{#1}\,{#2}}
\newcommand{\Ltriv}{()}
\newcommand{\Lpair}[2]{({#1},{#2})}
% Translation representation
\newcommand{\transexp}[2]{\sembrac{#1}_{#2}}
\newcommand{\transdef}[3]{\transexp{#1}{#2} & = & {#3}}

%
% Zurab macros
%
\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}{Lemma}[section]
\newtheorem{cor}{Corollary}[section]
\newtheorem{ex}{Example}[section]
\newtheorem{rem}{Remark}[section]
\newtheorem{prop}{Proposition}[section]
\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{proof}{\noindent{\bf Proof }}{}
\newtheorem{deff}{Definition}[section]
\newcommand{\notation}{{\bf Notation }}
\newcommand{\note}{{\bf Note }}
%
\newcommand{\Tr}[1]{Theorem~\ref{#1}}
\renewcommand{\Pr}[1]{Proposition~\ref{#1}}
\newcommand{\Cr}[1]{Corollary~\ref{#1}}
\newcommand{\Lr}[1]{Lemma~\ref{#1}}
\newcommand{\Dr}[1]{Definition~\ref{#1}}
\newcommand{\bd}{\begin{deff}\em}
\newcommand{\bdl}[1]{\begin{deff}\em\label{#1}}
\newcommand{\bl}{\begin{lem}\em}
\newcommand{\bll}[1]{\begin{lem}\em\label{#1}}
\newcommand{\bp}{\begin{prop}\em}
\newcommand{\bpl}[1]{\begin{prop}\em\label{#1}}
\newcommand{\bt}{\begin{thm}\em}
\newcommand{\btl}[1]{\begin{thm}\em\label{#1}}
\newcommand{\bel}[1]{\begin{ex}\em\label{#1}}
\newcommand{\bc}{\begin{cor}\em}
\newcommand{\bcl}[1]{\begin{cor}\em\label{#1}}
\newcommand{\bproof}{\begin{proof}}
\newcommand{\eproof}{\end{proof}}
\newcommand{\ed}{\end{deff}}
\newcommand{\el}{\end{lem}}
\newcommand{\ep}{\end{prop}}
\newcommand{\et}{\end{thm}}
\newcommand{\ee}{\end{ex}}
\newcommand{\ec}{\end{cor}}
%
% Equivalence relations
\newcommand{\lles}{\lhd}
\newcommand{\leeqv}{\approx_L}
\newcommand{\fwb}{\approx_f}
\newcommand{\wb}{\approx_w}
\newcommand{\fwbs}{fairly weakly bisimilar}
\newcommand{\sbi}{\sim}
%
%reductin/action relations
%
\newcommand{\ar}{\rightarrow}
\newcommand{\dar}{\Rightarrow}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\newcommand{\dred}[1]{\mbox{$\stackrel{#1}{\dar}$}}
\newcommand{\doar}{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
\newcommand{\ddoar}{\mbox {$\,\ \Rightarrow\kern-0.7em\Rightarrow\ $}}
\newcommand{\dored}[1]{\mbox{$\stackrel{#1}{\doar}$}}
\newcommand{\ddored}[1]{\mbox{$\stackrel{#1}{\ddoar}$}}
%
\newcommand{\PPinpac}[2]{{#1}\,\downarrow\,{#2}}
\newcommand{\PPoutac}[2]{{#1}\,\uparrow\,{#2}}
\newcommand{\tra}[1]{t\sembrac{#1}}
%
\newcommand{\john}[1]{\{{\bf John:~\sf #1}\}} % Highlight text.
\newcommand{\zurab}[1]{\{{\bf Zurab:~\sf #1}\}} % Highlight text.
\newcommand{\delete}[1]{} % Comment out text.
%\newcommand{\suppress}[1]{\{\{{\sf #1}\}\}} % Highlight text.
\newcommand{\suppress}[1]{} % Comment out text.
%
% End of macros
\begin{document}
\maketitle

\section{Correctness of the simulation of \Pc\ by \PPc}

\john{
Bent and Lone,

Here Zurab is working towards a method of proving that weak bisimulation
is preserved by translation from \Pc\ to \PPc. I think he is aiming for a
very general method which will be interesting anyway. However, maybe there
are much simpler ways to do it used in the concurrency community -- Zurab
and I really come from a rewriting background.

Note especially a discussion about creation and deletion of {\em channel
ports}.

We would very much like comments (i.e. help!). If there are technical
questions which need to go between you and Zurab, please do not worry
about communicating directly -- copying to me if you like.
}

\subsection{Counterexample to preservation of strong bisimulation}



$P=0 \sbi \restrict{n}{\outact{n}{n'}{0}}=Q$, but

$t\sembrac{P}=\PPempty \not\sbi \PPres{n}
{\PPres{m}{(\PPpar{\PPoutP{n}{Put(n',m)}}{\PPname{m}{\PPin{m'}
{\PPabs{m''}{\PPempty}}}})}}=t\sembrac{Q}$, since $t\sembrac{P}$ can
commit
a $\tau$-action, while $t\sembrac{P}$ cannot.




\subsection{A classification of named process occurrences}



We call (named, output, or other) process occurrences which are inside
input or conditional scripts {\em locked\/} or {\em guarded\/} processes.
We call unguarded named processes {\em ports}, since they can communicate
externally. In the \PPc\ processes obtained by translation of \Pc\
processes, we distinguish the following kinds of ports:

\begin{enumerate}
\item
{\em Unrestricted\/} or {\em external\/} or {\em observable
channel-ports}:

$\PPname{n}{Chan(q)}$ in $\PPres{\bf m}{(\PPname{n}{Chan(q)}\,\Vert\,
P})\,\Vert\, Q$ with $n\not\in \bf m$.

\item
{\em Restricted\/} or {\em internal\/} or {\em unobservable
channel-ports}:

$\PPname{n}{Chan(q)}$ in $\PPres{\bf m}{(\PPname{n}{Chan(q)}\,\Vert\,
P})\,\Vert\, Q$ with $n\in \bf m$.

\item
{\em Restricted\/} or {\em internal\/} {\em address-ports}, generated say
by translation of guarded \Pc\ processes:

$\PPname{m}{\PPin{n'}{\PPabs{m'}{\PPempty}}}$ in
$\PPres{m}{(\PPname{n}{Chan(EQ)}\,\Vert\,\PPpar{\PPoutP{n}{Get(m)}}{\PPname{
m}{\PPin{n'}{\PPabs{m'}{\PPempty}}}})}$

\end{enumerate}




{\bf Convention $(a)$:} Below we assume that every \PPc\ process contains
exactly one channel process $\PPname{n}{Chan(q)}$ iff it contains an
unguarded output process $\PPoutP{n}{t}$ and doesn't contain an unguarded
process named $n$ (i.e., a port named $n$) which is not a channel-port.

In particular, in the course of derivation, some guards may get removed
and
guarded output processes may become unguarded, e.g, in the following
example, where $p\not=l\not=n$:

$\PPname{m}{  \PPin{l}{ \PPabs{n}{\PPoutP{p}{r}}  }} \,\Vert\,
\PPoutP{m}{s}\,\ar\, \PPname{m}{ \PPabs{l} {\PPoutP{p}{r} }}\equiv
\PPoutP{p}{r}$

 Thus, we need to put $\PPname{p}{Chan(EQ)}$ in parallel with
$\PPoutP{p}{r}$, i.e., replace $\PPoutP{p}{r}$ by
$\PPname{p}{Chan(EQ)}\,\Vert\,\PPoutP{p}{r}$.
On the other hand, after $\tau$ or external output actions, an unguarded
output (sub)process may disappear, as in the following example:

$\PPname{m}{Chan(q)}\,\Vert\, \PPoutP{m}{Get(p)}\,\Vert\, Q\,\ar
\,\PPname{m}{Chan(q')}\,\Vert\,Q$.

 Here we need to remove $\PPname{m}{Chan(q')}$ in the right side iff
$q'=EQ$ and $Q$ doesn't contain an unguarded output on $m$.

\john{
You know I am uneasy about this convention. Since $Chan$ is not a special
part of the definition of \PPc, I don't like the idea of them arbitrarily
being created and destroyed. I would rather do what I have suggested in
the
documents and create {\em every} channel port which might be required and
then {\em garbage collect} any not required. The garbage collection is
justified by showing that $\PPpar{\PPname{n}{\PPin{x}{S}}}{P} \sbi P$ if
$n
\not\in fn(P)$ since no process of the form $\PPoutP{n}{v}$ could arise to
interact with $\PPname{n}{\PPin{x}{S}}$. This is the format of an unused
channel.
}

\zurab{If we follow your suggestion, your encoding will not preserve weak
bisimulation. Indeed, take two \Pc\ processes $N=P\,\Vert\,
\restrict{m}{\inpact{m}{x}{\outact{n}{n'}{0}}}$ and $Q=P\,\Vert\,
\restrict{m}{\inpact{m}{x}{0}}$. Then $N\wb Q$, but
$\tra{N}\not\wb\tra{Q}$
since $\tra{Q}$ cannot mutch actions of $\tra{N}$ that use the channel at
$n$.
}

\john{
This seems like a deep problem to me. In \Pc\ unused or unusable names,
like $n$ above, can be added and removed without anyone being able to
observe the difference. However, in the \PPc\ translation, names become
processes and observable actions can occur. This arises because the \PPc\
version reveals a finer granularity since communication offers become
messages.

It seems to me that this might relate to LCCS using the buffer processes
in Lone's thesis. Using \Pc\ notation for a process which relays from a
name $n$ to $m$: $B = \replicate{X}{\inpact{n}{x}{\outact{m}{x}{0}}}$,
when can we say that $P$ is essentially the same as
$\restrict{m}{\parprocs{B}{P\{m/n\}}}$, where $m \not\in fn(P)$?
}


\subsection{A classification of action (derivation) steps}


We distinguish {\em internal\/} or $\tau$-steps, and {\em external\/}
steps. The internal steps can be of the following $6$ types, where $k\geq
1$ in (2) and (4)  and $k\geq 0$ in $(1)$ and $(3)$:

\begin{enumerate}
\item[(1)]
$\begin{array}{l}
 \PPname{n}{Chan(IQ(m_1,IQ(m_2,IQ(\ldots,IQ(m_k,EQ)\ldots )}\,\Vert\,
\PPoutP{n}{Get(p)} \,\red{\tau}\, \\
\quad\quad\quad\quad\quad\quad
\PPname{n}{Chan(IQ(p,IQ(m_1,IQ(m_2,IQ(\ldots,IQ(m_k,EQ)\ldots )}
\end{array}$


\item[(2)]
$\begin{array}{l}
 \PPname{n}{Chan(IQ(m_1,IQ(m_2,IQ(\ldots,IQ(m_k,EQ)\ldots )}\,\Vert\,
\PPoutP{n}{Put(p,l)} \,\red{\tau}\,    \\
\quad\quad\quad\quad\quad\quad\
\PPoutP{m_1}{p} \,\Vert\, \PPoutP{l}{Sync} \,\Vert\,
\PPname{n}{Chan(IQ(m_2,IQ(\ldots,IQ(m_k,EQ)\ldots )}
\end{array}$

\item[(3)]
$\begin{array}{l}
 \PPname{n}{Chan(OQ(m_1,l_1,OQ(m_2,l_2,OQ(\ldots,OQ(m_k,l_k,EQ)\ldots
)}\,\Vert\, \PPoutP{n}{Put(p,r)} \,\red{\tau}\, \\
\quad\quad\quad\quad\quad\quad
\PPname{n}{Chan(OQ(p,r,OQ(m_1,l_1,OQ(m_2,l_2,OQ(\ldots,OQ(m_k,l_k,EQ)\ldots )}
\end{array}$


\item[(4)]
$\begin{array}{l}
 \PPname{n}{Chan(OQ(m_1,l_1,OQ(m_2,l_2,OQ(\ldots,OQ(m_k,l_k,EQ)\ldots
)}\,\Vert\, \PPoutP{n}{Get(p)} \,\red{\tau}\, \\
\quad\quad\quad\quad\quad\quad
\PPoutP{p}{m_1} \,\Vert\, \PPoutP{l_1}{Sync} \,\Vert\,
\PPname{n}{Chan(OQ(m_2,l_2,OQ(\ldots,OQ(m_k,l_k,EQ)\ldots )}
\end{array}$


\item[(5)]
A name passing step to a process with a restricted address-name.

$\PPres{m}({\PPoutP{m}{n}\,\Vert\,\PPname{m}{\PPin{l}Q}})\,\red{\tau}\,
\PPres{m}{(\PPname{m}{\{n/l\}Q})}$


\item[(6)]
A $Sync$ passing step to a process with a restricted address-name.

$\PPres{m}({\PPoutP{m}{Sync}\,\Vert\,\PPname{m}{\PPin{l}Q}})\,\red{\tau}\,
\PPres{m}({\PPname{m}{\{Sync/l\}Q}})$

\end{enumerate}


Similarly, the external steps can be of the following $4$ types, where
$k\geq 1$ in (8) and (10)  and $k\geq 0$ in $(7)$ and $(9)$:

\begin{enumerate}
\item[(7)]
$\begin{array}{l}
 \PPname{n}{Chan(IQ(m_1,IQ(m_2,IQ(\ldots,IQ(m_k,EQ)\ldots )}
\,\red{\PPinpac{n}{Get(p)}}\, \\
\quad\quad\quad\quad\quad\quad
\PPname{n}{Chan(IQ(p,IQ(m_1,IQ(m_2,IQ(\ldots,IQ(m_k,EQ)\ldots )}
\end{array}$


\item[(8)]
$\begin{array}{l}
 \PPname{n}{Chan(IQ(m_1,IQ(m_2,IQ(\ldots,IQ(m_k,EQ)\ldots )}
\,\red{\PPinpac{n}{Put(p,l)}}\,    \\
\quad\quad\quad\quad\quad\quad\
\PPoutP{m_1}{p} \,\Vert\, \PPoutP{l}{Sync} \,\Vert\,
\PPname{n}{Chan(IQ(m_2,IQ(\ldots,IQ(m_k,EQ)\ldots )}
\end{array}$

\item[(9)]
$\begin{array}{l}
 \PPname{n}{Chan(OQ(m_1,l_1,OQ(m_2,l_2,OQ(\ldots,OQ(m_k,l_k,EQ)\ldots )}
\,\red{\PPinpac{n}{Put(p,r)}}\, \\
\quad\quad\quad\quad\quad\quad
\PPname{n}{Chan(OQ(p,r,OQ(m_1,l_1,OQ(m_2,l_2,OQ(\ldots,OQ(m_k,l_k,EQ)\ldots )}
\end{array}$


\item[(10)]
$\begin{array}{l}
 \PPname{n}{Chan(OQ(m_1,l_1,OQ(m_2,l_2,OQ(\ldots,OQ(m_k,l_k,EQ)\ldots )}
\,\red{\PPinpac{n}{Get(p)}}\, \\
\quad\quad\quad\quad\quad\quad
\PPoutP{p}{m_1} \,\Vert\, \PPoutP{l_1}{Sync} \,\Vert\,
\PPname{n}{Chan(OQ(m_2,l_2,OQ(\ldots,OQ(m_k,l_k,EQ)\ldots )}
\end{array}$

\end{enumerate}


The external output steps

$\,\,(11)\,\,\,\,\,
\PPres{n_1}{\PPres{n_2}{\ldots\PPres{n_k}({\PPoutP{n}{t}\,\Vert \,P)}}}
\, \red{\PPoutac{n}{t}} \, \PPres{n_1}{\PPres{n_2}{\ldots\PPres{n_k}{P}}}$

 cannot be committed by a process $Q$ because of the convention $(a)$,
since for any unlocked output subprocess $\PPoutP{n}{t}$ of $Q$, the
latter
should contain a port named $n$, therefore no context can contain another
process named $n$ (because of the restrictions we impose on \PPc\
processes
-- no different occurrences of processes with the same name).


{\bf Convention $(b)$:} We disallow input of terms other than $Put$- or
$Get$-terms (i.e., terms of the form $Put(p,l)$ and $Get(p)$ where $p$ and
$l$ are names). This is because input of other terms would `abolish' the
corresponding channel-port -- will make it a dead process. Although the
channel-port must be restored because of the convention $(a)$, the
argument
of the abolished script would be impossible to recover. We anyway don't
need this kinds of steps to simulate \Pc\ derivations.


\begin{ex}\em
Consider a \Pc\ $\tau$-step $P=\restrict{n}{\inpact{n}{n'}{0} \,\Vert\,
\outact{n}{n''}{0} }\,\red{\tau}\,\restrict{n}{0\,\Vert\,0}\equiv 0= Q$.
We
have that

$\tra{P}=\PPres{n}{(\PPpar{\PPname{n}{Chan(EQ)}}{\PPres{m}{(\PPpar{\PPoutP{n
}{Get(m)}}{\PPname{m}{\PPin{n'} {\PPabs{m'}{t\sembrac{0}}}}})}\,\Vert\,
\PPres{l}{(\PPpar{\PPoutP{n}{Put(n'',l)}}{\PPname{l}{\PPin{l'}
 {\PPabs{l''}{t\sembrac{0}}}}})} })}\equiv
\PPres{n}{\PPres{m}{\PPres{l}{(\PPname{n}{Chan(EQ)}\,\Vert\,
\PPoutP{n}{Get(m)}\,\Vert\, \PPname{m}{\PPin{n'}
{\PPabs{m'}{\PPempty}}}\,\Vert\, \PPoutP{n}{Put(n'',l)}\,\Vert\,
\PPname{l}{\PPin{l'} {\PPabs{l''}{\PPempty}}} )}}} \,\red{(1)} \equiv \\
\PPres{n}{\PPres{m}{\PPres{l}{(\PPname{n}{Chan(IQ(m,EQ))} \,\Vert\,
\PPname{m}{\PPin{n'} {\PPabs{m'}{\PPempty}}}\,\Vert\,
\PPoutP{n}{Put(n'',l)}\,\Vert\, \PPname{l}{\PPin{l'}
{\PPabs{l''}{\PPempty}}} )}}} \,\red{(2)} \equiv \\
\PPres{n}{\PPres{m}{\PPres{l}{\PPname{n}{(Chan(EQ)} \,\Vert\,
\PPoutP{m}{n''} \,\Vert\, \PPoutP{l}{Sync} \,\Vert\, \PPname{m}{\PPin{n'}
{\PPabs{m'}{\PPempty}}}\,\Vert\, \PPname{l}{\PPin{l'}
{\PPabs{l''}{\PPempty}}} )}}} \,\red{(5)}\,\, \red{(6)} \equiv \\
\PPres{n}{\PPres{m}{\PPres{l}{(\PPname{n}{Chan(EQ)} \,\Vert\,
\PPname{m}{\PPabs{m'}{\PPempty}}\,\Vert\,
\PPname{l}{\PPabs{l''}{\PPempty}}
)}}} \equiv  \\
\PPres{n}{\PPres{m}{\PPres{l}{(\PPname{n}{Chan(EQ)} \,\Vert\, \PPempty
\,\Vert\,\PPempty )}}}  \equiv (by \,\,\, convention \,\,\, (a) \equiv 0
=\tra{Q}$.

Similarly, an output \Pc\ action is translated  into a group of four \PPc\
steps.
\end{ex}

\subsection{Correctness proof method}


This section discribes a method for a proof of preservation of weak
bisimulation by the encoding of \Pc\ into \PPc. We idea of the proposed
method is to reduce the set of \PPc\ derivations, for which we need to
check possibility of weak simulation, from the set of all derivations to
the set of all {\em canonical\/} derivations.  The correctness proof is
reduced to proving \Lr{L.can.match.} (still open), although we need in
addition to prove Lemmas \ref{L.ca.can.rep.} and \ref{L.canon.qua-can.}
(also open).

\bd
In \Pc\ and \PPc: we call a derivation $D:P\red{a}P_1\red{a_1}\ldots$ {\em
fair\/} if every `redex' in any $P_i$ is either contracted or destroyed,
i.e., no redex has residuals in every consequent term.
\ed

In \PPc, the notion of residual must be the same as the traditional notion
of residual in rewriting theory. For example, in
$P=\PPname{n}{Chan(IQ(m,EQ))}\,\Vert\,\PPoutP{n}{Put(r,l)}\,\Vert\,\PPoutP{n
}{Get(p)}$ we have two redexes, and after contracting the left one
$P\ar\PPname{n}{Chan(EQ)}\,\Vert\,\PPoutP{m}{r}\,
\Vert\,\PPoutP{l}{Sync}\,\Vert\,\PPoutP{n}{Get(p)}=Q$, the redex
$\PPname{n}{Chan(EQ)}\,\Vert\,\PPoutP{n}{Get(p)}$ is a new redex because
say the $?$ symbol of $Chan$ in $Q$ is new, not a descendant of $?$ of
$Chan$ in $P$ because the latter $?$ was `used' in the step $P\ar Q$. This
is reasonable, since contraction of the left redex after the right one
would communicate $r$ to $p$ rather than to $m$: $P\,\ar\,
\PPname{n}{Chan(IQ(p,IQ((m,EQ)))}\,\Vert\,\PPoutP{n}{Put(r,l)}\,\ar\,
\PPname{n}{Chan(IQ(m,EQ))}\,\Vert\,\PPoutP{p}{r}\,\Vert\,\PPoutP{l}{Sync}$.



\bd
We call processes $P$ and $Q$ {\em fairly weakly bisimilar}, written
$P\fwb
Q$, if for any fair derivation $D:P\red{a}P_1\red{a_1}\ldots$, there is a
(fair) derivation $D':Q\dred{a}Q_1\dred{a_1}\ldots$, and vice versa, where
$\dred{a}=\dored{\tau}\red{a}\dored{\tau}$. We say that $D'$ {\em weakly
matches\/} $D$.
\ed



\bt
In \Pc\ and \PPc: $P\wb Q$ iff $P\fwb Q$.

\bproof
Let $WB$ and $FWB$ be largest weak and fair weak bisimulations
respectively, i.e., the sets of all pairs of weakly, respectively fairly
weakly, bisimilar processes. We show that $WB=FWB$.

$(WB\subseteq FWB)$: Let $P\wb Q$, and let
$D:P\red{a}P_1\red{a_1}P_2\red{a_2}\ldots$ be fair. By $P\wb Q$, there is
$Q_1$ such that $Q\dred{a}Q_1$ and $P_1\wb Q_1$. Similarly, there is $Q_2$
such that $Q_1\dred{a}Q_2$ and $P_2\wb Q_2$, and so on. Hence
$D':Q\dred{a}Q_1\dred{a_1}Q_2\dred{a_2}\ldots$ weakly matches $D$.

$(FWB\subseteq WB)$: Let $P\fwb Q$, and let $P\red{a}P_1$. Then there is
$Q_1$ such that $Q\dred{a}Q_1$ and $P_1\fwb Q_1$ (since a derivation $D_1$
starting from $P_1$ is fair iff so is $a+D_1$). Similarly, for any
$P_1\red{a_1}P_2$ there is $Q_1\dred{a}Q_2$ such that $P_2\fwb Q_2$, and
so
on. So $FWB$ is a weak bisimulation, therefore contained in $WB$ (the
largest weak bisimulation).

\eproof
\et



\bll{L.le.equi.const.}
In \Pc\ and \PPc: $D:P\red{a}P_1\red{a_1}P_2\red{a_2}\ldots$ and
$D':Q\red{b}Q_1\red{b_1}Q_2\red{b_2}\ldots$ are permutation equivalent iff
$D'$ can be obtained from $D$ by a sequence of permutations such that, for
any $n$, there is $k_n$ such that all the permutation steps after the
first
$n_k$ steps doesn't affect the initial part of the length $n$ of the
obtained derivation.

\bproof
Easy.
\eproof
\el



\bll{L.can,match.all.}
Let a fair derivation $D^*:P\red{a}P_1\red{a_1}P_2\red{a_2}\ldots$ in a
residual structure has a weakly matching derivation
$D'^*:Q\dred{a}Q_1\dred{a_1}Q_2\dred{a_2}\ldots$ such that $\red{a_i}$ and
$\red{a_{i+1}}$ are permutable iff so are $\dred{a_i}$ and
$\dred{a_{i+1}}$. Then for any $D$ such that $D\leeqv D^*$ there is $D'$
that weakly matches $D$ and such that $D'\leeqv D'^*$.

\bproof
Since $D^*\leeqv D$, we have by \Lr{L.le.equi.const.} that $D$ is the
limit
of a sequence of derivations $D^*=D_0, D_1, D_2,\ldots$ such that
$D_{i+1}$
is obtained from $D_i$ by permutation of $\red{a_{k_i}}$ with its next
step
$\red{a_{k_i+1}}$. Let $D'^*=D'_0, D'_1,D'_2,\ldots$ be the sequence of
derivations obtained by the corresponding permutation transformation,
i.e.,
$D'_{i+1}$ is obtained from $D'_i$ by permutation of $\dred{a_{k_i}}$ with
$\dred{a_{k_i+1}}$. Obviously, since $D'_0$ matches $D_0$, $D'_1$ matches
$D_1$. Similarly, we get that $D'_i$ matches $D_i$ for every $i$. And
since
the permutation transformation is such that $k_i$ tends to infinity when
$i$ tends to infinity, it follows that $D'$ matches $D$.
\eproof
\el


\bd
We call a $\pi^\pi$-derivation {\em canonical\/} if it is a translation of
a
$\pi$-derivation. We call a \PPc\ term {\em regular\/} if it is the
translation of a \Pc\ term. We call a \PPc\ term {\em quasi-regular\/} if
it is a derivative of a regular term.
\ed


\bd
We call a derivation $D:P_0\red{a_0}P_1\red{a_1}P_2\red{a_2}\ldots$ {\em
quasi-canonical\/} if $P_0$ is regular and, for any $k=4\cdot i$, the step
$a_k$ is of one of the types $(1), (3), (7), (9)$; $a_{k+1}$ is of type
$(2)$ or $(8)$, $(4)$ or $(10)$,  $(2)$ or $(8)$, or $(4)$ or $(10)$,
respectively, and uses the same port; $a_{k+2}$ is of type $(5)$,
$a_{k+3}$ is of type $(6)$, and $a_{k+2}$ and $a_{k+3}$ are created by
$a_{k+1}$.
\ed


In a quasi-canonical derivation that is not canonical, a (regular) process
can input say $Get(p)$ and then input $Put(p,l)$ at the same channel-port,
and this is not a part of a group of steps that correspond to a
$\pi$-step,
internal or external.  If we allow external actions of only types $(8)$
and
$(10)$, then every quasi-canonical derivation is canonical.

\bll{L.ca.can.rep.}
For any fair derivation $D$ in $\pi^\pi$ starting from a regular term
there
is a quasi-canonical fair derivation $D'$ such that $D\leeqv D'$.
\el


\bll{L.canon.qua-can.}
Let \PPc\ regular processes $P$ and $Q$ be such that any canonical fair
derivation $D:P\doar$ can be matched by a derivation $D':Q\doar$. Then any
quasi-canonical fair derivation $D^*:P\doar$ can be matched by a
derivation
$D'^*:Q\doar$.
\el



\bll{can,mat.imp.fa.bi.}
Let \PPc\ regular processes $P$ and $Q$ be such that any canonical fair
derivation $D^*:P\doar$ can be matched by a derivation $D'^*:Q\doar$, and
vice versa. Then $P\fwb Q$, hence $P\wb Q$.

\bproof
To show $P\fwb Q$, we need to show that for any fair $D:P\doar$ there is
its weakly matching $D':Q\doar$. By \Lr{L.ca.can.rep.}, there is a
quasi-canonical fair $D_c:P\red{a}P_1\red{a_1}P_2\red{a_2}\ldots$ such
that
$D_c\leeqv D$. By the assumption and \Lr{L.canon.qua-can.}, there is a
$D'_c:Q\dred{a}Q_1\dred{a_1}Q_2\dred{a_2}\ldots$ that weakly matches
$D_c$.
Hence, by \Lr{L.can,match.all.}, there is $D'\leeqv D'_c$ that matches
$D$.
\eproof
\el




\bll{L.can.match.}
Let $D:P\red{a}P_1\red{a_1}P_2\red{a_2}\ldots$ be a fair $\pi$-derivation,
let $D':Q\dred{a}Q_1\dred{a_1}Q_2\dred{a_2}\ldots$ be its weakly matching
$\pi$-derivation, and let $D^*$ and $D'^*$ be the (canonical) translations
of $D$ and $D'$, respectively. Then $D'^*$ matches $D^*$.
\el


\bt
The encoding $\tra{ }$ of the \Pc\ into the \PPc\ preserves fair weak
bisimulation, hence preserves weak bisimulation.

\bproof
We need to show that $P\fwb Q$ in the \Pc\ implies $\tra{P}\fwb\tra{Q}$ in
the \PPc. So let $P\fwb Q$. By \Lr{L.can.match.}, any canonical derivation
starting from $\tra{P}$ can be matched by a derivation starting from
$\tra{Q}$, and vice versa. Thus the theorem follows from
\Lr{can,mat.imp.fa.bi.}.

\delete{So let $P\fwb Q$, and let $D:\tra{P}\doar$ be a fair derivation.
We
need to show that a fair derivation $D':\tra{Q}\doar$ matches $D$. Indeed,
by \Lr{L.ca.can.rep.}, $\tra{P}$ has a canonical fair derivation
$D_c\leeqv
D$. By \Lr{L.can.match.}, $D_c$ has a matching canonical fair
$D'_c:\tra{Q}\doar$. Hence, by \Lr{L.can,match.all.}, $D$ has a matching
fair derivation $D':\tra{Q}\doar$ too. this concludes the proof.}
\eproof
\et

\end{document}





