%%% 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{Syntax and Semantics of Pi in the Sky Calculus}
\author{
        {\it John Glauert, Zurab Khasidashvili,
		Lone Leth, and Bent Thomsen} \\
       }
%\reportref{Draft}
\date{Version H}

%\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}}
% End of macros
\begin{document}
\maketitle

\section{History}

This version is denoted {\em Version H\/}. The changes from the last 
version are minor corrections and a new formulation of the translation 
of the \Pc\ which maps to \PPc\ {\em processes\/} rather than 
{\em scripts}. I am sending it to Bent and Lone as they have not 
seen this formulation. Comments would be much appreciated.

\comment{
I am slightly concerned that I am using a variant of the \Pc\ which 
uses parametric process definitions rather than replication. There are, 
however, so many versions of the \Pc\ that I hope I can find one 
which fits! Personally, I have always found replication elegant but 
somehow not realistic as a primitive.
}

{\em Version G\/} works with the formulation of \PPc\ introduced under 
the name \TPPc\ in {\em Version 6\/} which aims to have a more uniform
syntax using a much simplified syntactic class for {\em scripts}.
However, the central role of agent definitions is softened by the
introduction of {\em abstractions} over process names.

This document is very much an outline, with detail and introduction
to be filled in.

\section{Introduction}

Awaits material giving proper motivation and a gentle introduction
to the world of processes and messages we are considering.

The paper gives a definition of the syntax and semantics of \PPc.
We show that the notation is powerful enough to simulate the \Pc,
giving an encoding of \Pc\ terms in the \PPc. We also (will) prove
that the encoding is correct. This encoding represents the names
of the \Pc, which can be though of as unbuffered communication
channels, as \PPc\ processes which act as mailboxes.

We (will) go on to show that any \PPc\ system may be simulated
using the \Pc.

It has been demonstrated that the \Lc\ can be modelled using the \Pc.
Clearly, the \PPc\ can model the \Lc\ through simulation of the
corresponding \Pc. However, a more direct translation is also
presented and (will be) shown to be correct.

We (will) also give a translation of the \PPc\ into
Object Graph Rewriting (\OGRe).

The \Lc\ can be modelled in \OGRe\ via the translation of the
equivalent \PPc\ term. We (will) also give a more direct translation.

\section{\PPC\ Syntax}

We assume a set $N$ of {\em names} ranged over by $n$, $m$,
etc. and a 
disjoint set $X$ of
{\em variables} ranged over by $x$, $y$, $z$ etc. A set $\Sigma$ of 
{\em symbols} raged over by $F$, $G$, etc. each with an associated 
{\em arity} ($\geq 0$) giving the number of arguments it should take. 
These are combined in 
the set of {\em terms}, $T$ ranged over by $t$:
\begin{eqnarray*}
T & ::= & n \mid x \mid F(t_1,\dots,t_n)\:, \:\: where \: arity(F) = n
\end{eqnarray*}

$P$, the class of process, and $S$, the class of process {\em scripts},
are defined in terms of each other.

$S$ is given by the following syntax:
\begin{eqnarray*}
S & ::= & \PPin{x}{S} \mid \PPmatch{x}{t}{S}{S'} \mid \PPabs{n}{P}
\mid A(t_1,\ldots,t_n)
\end{eqnarray*}

Also a set of recursive {\em agent} definitions is assumed: 
$\PPdef{A(x_1,\ldots,x_k)}{S}$. 

The intuition is that $S$ is the sequential body of a process.
An input--guarded script takes the form $\PPin{x}{S}$ where $x$
binds over $S$.
The match construct $\PPmatch{x}{t}{S}{S'}$ tests to see if the term 
bound to $x$ matches the term $t$. The term contains one or more 
symbols, and may contain variables but no bound names. The 
construct behaves as $S$ if the term bound to $x$ matches $t$. 
If the match fails it behaves as $S'$. Variables in $t$ 
and $t'$ are bound in $S$ by a successful match.

Abstractions of the form $\PPabs{n}{P}$ denote scripts which can
release the process network defined by P. This construct can be
used to provide process spawning and to create messages.
In $P$ in $\PPabs{n}{P}$ at most one process should be named $n$.
If there is such a process then it is the continuation of the
process containing the abstraction.

Recursive scripts are dealt with through agent definitions.
I am tempted to say that all free names in the body of the
definition should appear in the head, but as long as capture
of free names is prevented during substitution, I think it
would be possible for free names to appear. These free names
would identify processes existing in the original process
configuration.

Parallel {\em processes} form the class $P$ defined by the
following syntax:
\begin{eqnarray*}
P & ::= & \PPname{n}{S} \mid \PPoutP{n}{t} 
\mid \PPres{n}{P} \mid \PPpar{P}{P'} \mid \PPempty
\end{eqnarray*}
The term $t$ in $\PPoutP{n}{t}$ is closed, meaning that it
contains  only names and symbols.

$\PPname{n}{S}$ is a named process (the idea is similar to 
locations in some versions of  CCS).
$\PPoutP{n}{t}$ is a message $t$ on its way to process $n$ 
and $\PPres{n}{P}$ is restriction.
$\PPpar{P}{P'}$ denotes parallel composition of processes,
and $\PPempty$ is the empty composition. It is assumed that
$P$ and $P'$ 
in $\PPoutP{n}{t}$ are linear
wrt $\PPname{n}{S}$ subcomponents. This just means that named 
processes are unique.

Free names, variables and substitution, with renaming to avoid
name capture, 
are defined in an obvious way. \comment{This should be done but
is left for now.}

\section{\PPC\ Semantics}

There is an assumption that while scripts can contain
variables, during reduction communications contain only names and closed 
terms.
There are therefore some contextual constraints left vague at this point.
A sort discipline seems necessary to ensure that if an agent definition contains 
$\PPoutP{t}{t'}$ then either $t$ is a name, or it is a variable that 
will be bound to a name when the definition is expanded.

The operational semantics below encapsulates some of the assumptions by 
assuming that various terms are instantiated to names before the rules apply.
Suggestions welcomed.

The following structural rules define structural congruence of \PPc\ processes:
\begin{eqnarray*}
\PPres{n'}{\PPres{n}{P}} & \equiv & \PPres{n}{\PPres{n'}{P}} \\
\PPres{n}{P} & \equiv & P\:, \hspace{1cm} n \not\in fn(P) \\
\PPpar{\PPres{n}{P}}{P'} & \equiv & \PPres{n}{(\PPpar{P}{P'})}\:, 
\hspace{1cm} n \not\in fn(P') \\
\PPpar{(\PPpar{P}{P'})}{P''} & \equiv & \PPpar{P}{(\PPpar{P'}{P''})} \\
\PPpar{P}{P'} & \equiv & \PPpar{P'}{P} \\
\PPpar{P}{\PPempty} & \equiv & P \\
\PPname{n}{A(t_1,\ldots,t_k)} & \equiv &
\PPname{n}{\PPsub{S}{t_1/x_1,\ldots,t_k/x_k}}\:,
\hspace{0.5cm} where \:\: \PPdef{A(x_1,\ldots,x_k)}{S}
\end{eqnarray*}

The operational semantics is given as a set of reduction rules 
on processes $P$:
\begin{eqnarray*}
\PPpar{\PPname{n}{\PPin{x}{S}}}{\PPoutP{n}{t}} & \rightarrow & 
\PPname{n}{\PPsub{S}{t/x}} \\
\PPname{n}{\PPmatch{x}{t}{S}{S'}} & \rightarrow & 
\PPname{n}{\sigma(S)}\:, 
\hspace{1cm} \exists \sigma \: : \: x = \sigma(t) \\
\PPname{n}{\PPmatch{x}{t}{S}{S'}} & \rightarrow & 
\PPname{n}{S'}\:, 
\hspace{1cm} \forall \sigma \: : \: x \neq \sigma(t) \\
\PPname{n}{\PPabs{m}{P}} & \rightarrow & {\PPsub{P}{n/m}}
\end{eqnarray*}
Here $\sigma$ is a mapping from variables to closed terms.

The first rule shows how a message is received by process $n$.
The second and third reduction rules handle the match construct.
The final rule applies an abstraction and may involve process
spawning and message creation.

The following rules extend the reduction relation to contexts:
\begin{eqnarray*}
P \rightarrow P' & \Rightarrow & \PPres{n}{P} \rightarrow \PPres{n}{P'} \\
P \rightarrow P' & \Rightarrow & \PPpar{P}{Q} \rightarrow \PPpar{P'}{Q} \\
Q \equiv P, \; P \rightarrow P', \; P' \equiv Q' & \Rightarrow & Q \rightarrow Q'
\end{eqnarray*}

\begin{observation}
An alternative would be to consider application of a name to
an abstraction to be a part of the structural equivalence relation
rather than a reduction. It seems more natural to me that process
spawning and message creation should be accompanied by a reduction.
\end{observation}

\begin{observation}
We have not discussed the initial configuration of a process 
network in this calculus. If we disallow free names in agent
definitions, then, without loss of generality, 
it could take the form $\PPres{n}{(\PPname{n}{A})}$ for some agent
$A$ of arity $0$.
\end{observation}

To spawn a message $t'$ directed to process $t$ and continue with 
a script $S$ we can use an abstraction
$\PPabs{m}{(\PPpar{\PPoutP{t}{t'}}{\PPname{m}{S}})}$. 

To spawn a new process running script $S$, and continue with script $S'$
we can use an abstraction
$\PPabs{m}{\PPres{n}{(\PPpar{\PPname{n}{S}}{\PPname{m}{S'}})}}$.

More complex process networks and numbers of messages may be created
using such abstractions. Abstractions also allow a process to discover
its identity. The script $S$ in the following abstraction finds $n$
bound to its process name: $\PPabs{n}{(\PPname{n}{S})}$.

To terminate a process we can invoke a definition $Stop$ where
$\PPdef{Stop}{\PPabs{n}{\PPempty}}$. An agent $Stop$ with this
definition is assumed to exist in the rest of the paper.

\section{Simulation of \Pc\ by \PPc}

A proposed translation of the \Pc\ is provided. We assume that agent 
definitions take the place of replication in the \Pc.

The translation is based on the use of a process  
to implement a \Pc\ name (communication channel).
A \PPc\ channel process maintains either a queue of requests,
which are provided by $Get$ messages, or a queue of
data values and synchronisation addresses, which are provided 
by $Put$ messages. 
$Get$ messages contain the names of \PPc\ processes to receive data values. 
$Put$ messages contain a value to be sent and the name of a \PPc\ process
to receive a synchronisation message when the communication completes.

Initially, a \Pc\ channel $n$ will be represented by a process with 
script $Chan$ holding an empty queue represented by the symbol $EQ$:
\begin{eqnarray*}
\PPname{n}{Chan(EQ)}
\end{eqnarray*}
\begin{eqnarray*}
\PPdefn{Chan(q)}{\PPin{x}{\PPmatch{x}{Get(n)}{ChGet(n,q)}
  {\PPmatch{x}{Put(v,s)}{ChPut(v,s,q)}{Stop}}}} \\
\PPdefn{ChGet(n,q)}{\PPmatch{q}{OQ(v,s,r)}{Reply(n,v,s,r)}
  {Chan(IQ(n,q))}} \\
\PPdefn{ChPut(v,s,q)}{\PPmatch{q}{IQ(n,r)}{Reply(n,v,s,r)}
  {Chan(OQ(v,s,q))}} \\
\PPdefn{Reply(n,v,s,r)}{\PPabs{m}{(\PPpar{\PPoutP{n}{v}}
  {\PPpar{\PPoutP{s}{Sync}}{\PPname{m}{Chan(r)}}})}}
\end{eqnarray*}
The definitions $ChGet$, $ChPut$, and $Reply$ are added for clarity; a 
single recursive definition could have been used.

The function $t$ maps \Pc\ processes to \PPc\ processes:
\begin{eqnarray*}
t\sembrac{\inpact{n}{n'}{N}} & = &
    \PPres{m}{(\PPpar{\PPoutP{n}{Get(m)}}{\PPname{m}{\PPin{n'}
	{\PPabs{m'}{t\sembrac{N}}}}})} \\
t\sembrac{\outact{n}{n'}{N}} & = &
    \PPres{m}{(\PPpar{\PPoutP{n}{Put(n',m)}}{\PPname{m}{\PPin{m'}
	{\PPabs{m''}{t\sembrac{N}}}}})} \\
t\sembrac{\restrict{n}{N}} & = &
    \PPres{n}{(\PPpar{\PPname{n}{Chan(EQ)}}{t\sembrac{N}})} \\
t\sembrac{\parprocs{N}{N'}} & = &
    \PPpar{t\sembrac{N}}{t\sembrac{N'}} \\
t\sembrac{\inaction} & = & \PPempty \\
t\sembrac{\agtuse{A}{n_1,\ldots,n_k}} & = & \PPres{m}
    {(\PPname{m}{A(n_1,\ldots,n_k)})} \\
\\
f\sembrac{\agtdef{A}{n_1,\ldots,n_k}{N}} & = &
    \PPdef{A(n_1,\ldots,n_k)}{\PPabs{m}{t\sembrac{N}}}
\end{eqnarray*}

For most purposes an asynchronous form of the \Pc\ is adequate.
To simulate the asynchronous \Pc\ we can simplify the definition
of the channel processes and change the translation of output actions:
\begin{eqnarray*}
\PPdefn{AChan(q)}{\PPin{x}{\PPmatch{x}{AGet(n)}{AChGet(n,q)}
{\PPmatch{x}{APut(v)}{AChPut(v,q)}{Stop}}}} \\
\PPdefn{AChGet(n,q)}{\PPmatch{q}{OQ(v,r)}{AReply(n,v,r)}
{Chan(IQ(n,q))}} \\
\PPdefn{AChPut(v,q)}{\PPmatch{q}{IQ(n,r)}{AReply(n,v,r)}
{Chan(OQ(v,q))}} \\
\PPdefn{AReply(n,v,r)}{\PPabs{m}{(\PPpar{\PPoutP{n}{v}}
    {\PPname{m}{AChan(r)}})}} \\
\\
t\sembrac{\inpact{n}{n'}{N}} & = &
    \PPres{m}{(\PPpar{\PPoutP{n}{AGet(m)}}{\PPname{m}{\PPin{n'}
	{\PPabs{m'}{t\sembrac{N}}}}})} \\
t\sembrac{\outacta{n}{n'}} & = &
    \PPoutP{n}{APut(n')} \\
t\sembrac{\restrict{n}{N}} & = &
    \PPres{n}{(\PPpar{\PPname{n}{AChan(EQ)}}{t\sembrac{N}})}
\end{eqnarray*}

The names in the \Pc\ are represented by \PPc\ processes which
start by running the script $Chan(EQ)$. It is the restriction
construct which causes the channel processes to be introduced.
If a \Pc\ term with a free name is translated, no corresponding
channel process is produced. Hence we need to consider carefully
how a \Pc\ term is simulated by the \PPc.

I suggest a possible framework. How do we investigate the properties
of a \Pc\ term, $P$? In general, we might perform an experiment by
placing $P$ in parallel with some probe, represented by $Q$, and
observe the behaviour of the combined system. Without loss of
generality, we can restrict free names of the combination:
\begin{eqnarray*}
\restrict{\vec{a}}{\parprocs{P}{Q}} & where
    & \vec{a} = fn(\parprocs{P}{Q})
\end{eqnarray*}
Hence we would be considering the translation of closed \Pc\ terms.
If such terms are encoded, suitable \PPc\ channel processes will
always be generated.

Firstly, we may be able to use barbed bi-simulation in which it
is mainly a matter of whether processes converge or not which is
at issue.

For comparison, we repeat the translation from \Pc\ to \PPc given
in Version G. The translation uses a function $r$, mapping \Pc\
terms to processes, with auxiliary 
function $t$ which maps \Pc\ terms to scripts. A further function
$f$ maps \Pc\ agent defintions to \PPc\ definitions.

In the following, names $m$ and $m'$ are not in $fn(N)$ or $fn(N')$: 
\begin{eqnarray*}
r\sembrac{N} & = & \PPres{m}{(\PPname{m}{t\sembrac{N}})} \\
\\
t\sembrac{\inpact{n}{n'}{N}} & = &
    \PPabs{m}{(\PPpar{\PPoutP{n}{Get(m)}}{\PPname{m}{\PPin{n'}
	{t\sembrac{N}}}})} \\
t\sembrac{\outact{n}{n'}{N}} & = &
    \PPabs{m}{(\PPpar{\PPoutP{n}{Put(n',m)}}{\PPname{m}{\PPin{m'}
	{t\sembrac{N}}}})} \\
t\sembrac{\restrict{n}{N}} & = &
    \PPabs{m}{(\PPpar{\PPname{n}{Chan(EQ)}}{\PPname{m}
	{t\sembrac{N}}})} \\
t\sembrac{\parprocs{N}{N'}} & = &
    \PPabs{m}{\PPres{m'}{(\PPpar{\PPname{m}{t\sembrac{N}}}
	{\PPname{m'}{t\sembrac{N'}}})}} \\
t\sembrac{\agtuse{A}{n_1,\ldots,n_k}} & = & A(n_1,\ldots,n_k) \\
t\sembrac{\inaction} & = & \PPstop \\
\\
f\sembrac{\agtdef{A}{n_1,\ldots,n_k}{N}} & = &
    \PPdef{A(n_1,\ldots,n_k)}{t\sembrac{N}}
\end{eqnarray*}

For symmetry we could have generated a script which creates a
new \PPc\ process for each process
in $(\parprocs{N}{N'})$. In the translation given, we keep one
thread in the old \PPc\ process.

As above, to simulate the asynchronous \Pc\ we can simplify the
definition of the channel processes and change the translation
of output actions:
\begin{eqnarray*}
\PPdefn{AChan(q)}{\PPin{x}{\PPmatch{x}{AGet(n)}{AChGet(n,q)}
{\PPmatch{x}{APut(v)}{AChPut(v,q)}{Stop}}}} \\
\PPdefn{AChGet(n,q)}{\PPmatch{q}{OQ(v,r)}{AReply(n,v,r)}
{Chan(IQ(n,q))}} \\
\PPdefn{AChPut(v,q)}{\PPmatch{q}{IQ(n,r)}{AReply(n,v,r)}
{Chan(OQ(v,q))}} \\
\PPdefn{AReply(n,v,r)}{\PPabs{m}{(\PPpar{\PPoutP{n}{v}}
    {\PPname{m}{AChan(r)}})}} \\
\\
t\sembrac{\inpact{n}{n'}{N}} & = &
    \PPabs{m}{(\PPpar{\PPoutP{n}{AGet(m)}}{\PPname{m}{\PPin{n'}
	{t\sembrac{N}}}})} \\
t\sembrac{\outacta{n}{n'}} & = &
    \PPabs{m}{\PPoutP{n}{APut(n')}} \\
t\sembrac{\restrict{n}{N}} & = &
    \PPabs{m}{(\PPpar{\PPname{n}{AChan(EQ)}}{\PPname{m}
	{t\sembrac{N}}})} \\
\end{eqnarray*}

\begin{observation}
As before, I am afraid I have not checked any of it too well and a test 
using a simple example is necessary.
\end{observation}

\section{Simulation of \Lc\ by \PPc}

It has been demonstrated that the \Lc\ can be modelled using the \Pc.
Clearly, the \PPc\ can model the \Lc\ through simulation of the
corresponding \Pc. However, a more direct translation is also presented
and (will be) shown to be correct.

\section{Simulation of \PPc\ by \OGRe}

We (will) also give a translation of the \PPc\ into
Object Graph Rewriting (\OGRe).

\section{Simulation of \Lc\ by \OGRe}

The \Lc\ can be modelled in \OGRe\ via the translation of the
equivalent \PPc\ term. We (will) also give a more direct translation.

\end{document}
%%% End of LaTeX Document %%%
