%%% 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 J. 29th July 1995}

%\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}

{\em Version J\/} adds a little more explanation to Version I.
It also contains a running example showing how replication is modelled
by a parametric definition and how such a definition can satisfy the
constraints of the sub--calculus.
Davide Sangiorgi seems to use parametric definitions in his thesis.
We will rtestrict ourselves to the main use of replication which is
always guarded by an input action.

{\em Version I\/} changed the reduction relation. If we are to use
{\em barbed-bisimulation\/} related the reduction semantics, then
the reduction relation should only capture the observable events.
I think that means just communication, for now.

{\em Version I\/} introduced some definitions of free and bound
names and also some static constraints to be obeyed by well-formed
processes. I am not entirely happy with this and would value
proposals for improvement! One major change is to try to live
without a separate class of variables in terms.
There is a bit more explanation of the process and script classes.

An extra section is added, defining a sub--calculus of the \Pc\
which may be helpful in defining a more direct translation to \PPc.
If it could be shown that all \Pc\ can be simulated in the sub--calculus,
then an even simpler translation should be possible, since the
sub--calculus is intended to capture the essential properties of \PPc.

{\em Version H\/} contained minor corrections and a new formulation
of the translation 
of the \Pc\ which maps to \PPc\ {\em processes\/} rather than 
{\em scripts}.

{\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 still 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. 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 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.

\subsection{\PPC\ Processes}

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 running a script $S$
(the idea is similar to 
locations in some versions of  CCS).
$\PPoutP{n}{t}$ is a message $t$ on its way to process $n$.
These two forms make up a \PPc\ network and all computation
involves the interaction of names processes and messages.

$\PPres{n}{P}$ denotes restriction of the name $n$ to $P$.
$P$ may contain a process with name $n$, but the name $n$
is bound by the restriction and is not confused with any
other use of the same name in the surrounding context.

$\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. Rules to ensure this are given below.

\subsection{\PPC\ Scripts}

Process {\em Scripts}, $S$ are given by the following syntax:
\begin{eqnarray*}
S & ::= & \PPin{n}{S} \mid \PPmatch{n}{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(n_1,\ldots,n_k)}{S}$. 

\comment{
Hmm. I suppose that means another set of names.
}

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

Abstractions of the form $\PPabs{n}{P}$ allow a process to generate
new processes. The parent process continues to exist if there is a
process named $n$ within $P$. That process takes on the name of
the parent and other processes in $P$ are spawned in parallel.
We will illustrate the power of the construct with some examples:

To spawn a message $t$ directed to process $n$ and continue with 
a script $S$ we can use an abstraction
$\PPabs{m}{(\PPpar{\PPoutP{n}{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 involving numbers of messages may be created
in a similar way. 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.

Recursive scripts are dealt with through agent definitions.
\comment{
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.
}

\subsection{\PPC\ Syntactic Constraints}

It is necessary to define concepts of free and bound names in \PPc.
We will also describe some static constraints to be obeyed by
well--formed processes and scripts.

Free names of processes are given by $fn(P)$. $dn(P)$ identifies
defining names -- free names which name processes in $P$.

Free names of scripts are given by $fn(S)$. 
Names in a term, $t$, are denoted by $fn(t)$.
No free names in scripts or terms are defining names.
\begin{eqnarray*}
fn(\PPname{n}{S}) & = & fn(S) \cup \{n\} \\
dn(\PPname{n}{S}) & = & \{n\} \\
fn(\PPoutP{n}{t}) & = & fn(t) \cup \{n\} \\
dn(\PPoutP{n}{t}) & = & \{\} \\
fn(\PPres{n}{P}) & = & fn(P) \setminus \{n\} \\
dn(\PPres{n}{P}) & = & dn(P) \setminus \{n\} \\
fn(\PPpar{P}{P'}) & = & fn(P) \cup fn(P') \\
dn(\PPpar{P}{P'}) & = & dn(P) \cup dn(P') \\
fn(\PPempty) & = & \{\} \\
dn(\PPempty) & = & \{\} \\
\\
fn(\PPin{n}{S}) & = & fn(S) \setminus \{n\} \\
fn(\PPmatch{n}{t}{S}{S'}) & = &
	(fn(S) \setminus fn(t)) \cup fn(S') \cup \{n\}  \\
fn(\PPabs{n}{P}) & = & fn(P) \setminus \{n\} \\
fn(A(t_1,\ldots,t_k)) & = & fn(t_1) \cup \ldots \cup fn(t_k) \\
\end{eqnarray*}

To ensure that named processes have distinct names, we need to
add the constraint that in $\PPpar{P}{P'}$, we require that
$dn(P) \cap dn(P') = \{\}$. We also want to make sure that every
new process created by use of an abstraction in a script is bound
by some restriction. 
In $\PPabs{n}{P}$, we require that $dn(P) \subseteq  \{n\}$. 
Hence the only possible free named process is $n$ which is bound
in the abstraction.

For parametric definitions $\PPdef{A(n_1,\ldots,n_k)}{S}$ we
require that $fn(S) \subseteq \{n_1,\ldots,n_k\}$. 

Note that the consequence is that no free name in a script is a
defining name. Hence, such a name cannot be bound by input or matching.

\comment{
One rather operational choice would be to ensure that every
potential message has a process to go to. This would mean that
a process could not just die by using a script like $Stop$.
We would need a new form of script for a terminated process,
say $Dead$, and a structural equivalence rule to garbage collect
processes when the form $\PPres{n}{\PPname{n}{Dead}}$ arises.
We would need extra constraints to say that whenever there is a
restriction $\PPres{n}{P}$, $n \in dn(P)$. The constraint for an
abstraction, $\PPabs{n}{P}$, would be strengthened to read
$dn(P) = \{n\}$.
}

\comment{
I have not defined bound names, since they are just names which
occur in some context where they are not free (oh, I seem to have
defined them after all). It seems possible to define everything
in terms of free names so far.
}

\section{\PPC\ Semantics}

A sort discipline seems necessary to ensure that if an agent
definition contains 
$\PPoutP{n}{t'}$ then $n$ 
will be bound to a defined name when the definition is expanded.

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 & \PPres{m}{\PPsub{P}{m/n}} \:, 
	\hspace{1cm} m \not\in fn(P) \\
\PPpar{\PPres{n}{P}}{P'} & \equiv & \PPres{n}{(\PPpar{P}{P'})}\:, 
	\hspace{1cm} n \not\in fn(P') \\
\PPres{n}{\PPempty} & \equiv & \PPempty \\
\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/n_1,\ldots,t_k/n_k}}\:,
\hspace{0.5cm} where \:\: \PPdef{A(n_1,\ldots,n_k)}{S} \\
\PPname{n}{\PPmatch{t}{t'}{S}{S'}} & \equiv & \PPname{n}{\sigma(S)}\:,
	\hspace{1cm} \exists \sigma \: : \: t = \sigma(t') \\
\PPname{n}{\PPmatch{t}{t'}{S}{S'}} & \equiv & \PPname{n}{S'}\:,
	\hspace{1cm} \forall \sigma \: : \: t \neq \sigma(t') \\
\PPname{n}{\PPabs{m}{P}} & \equiv & {\PPsub{P}{n/m}} \:, 
	\hspace{1cm} dn(P) \subseteq \{m\}
\end{eqnarray*}
Here $\sigma$ is a mapping from names to terms used by the rules
handling the match construct.
The final rule applies an abstraction and may involve process
spawning and message creation.

The reduction semantics is given by a single reduction rule
on processes $P$:
\begin{eqnarray*}
\PPpar{\PPname{n}{\PPin{m}{S}}}{\PPoutP{n}{t}} & \rightarrow & 
\PPname{n}{\PPsub{S}{t/m}} 
\end{eqnarray*}

The rule shows how a message is received by process $n$ must have a script
indicating that the process is ready for input.

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}
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}

\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 syntax of \Pc\ processes will be taken as:
\begin{eqnarray*}
N & ::= & \inpact{n}{n'}{N} \mid \outact{n}{n'}{N} \mid \restrict{n}{N}
	\mid \parprocs{N}{N'} \mid \inaction \mid \agtuse{A}{n_1,\ldots,n_k}
\end{eqnarray*}
where parametric definitions take the form:
\begin{eqnarray*}
\agtdef{A}{n_1,\ldots,n_k}{N}
\end{eqnarray*}

We note that we have not allowed for replication, $\replicate{X}{P}$.
We can provide a crude translation of $\replicate{X}{P}$ as
$\agtuse{A}{fn(P)}$ where $\agtdef{A}{fn(P)}{(\parprocs{P}{\agtuse{A}{fn(P)}})}$.

For practical purposes we will want communication to trigger
expansion of replications. The usual form in which we will find
replication is $\replicate{X}{\inpact{x}{w}{P}}$. If we use $n_P$
for $fn(P) \setminus \{x,w\}$ then we can represent the replication as
$\agtuse{A}{x,n_P}$ where
$\agtdef{A}{x,n_P}{\inpact{x}{w}(\parprocs{P}{\agtuse{A}{x,n_P}})}$.

\comment{
I think there are proofs that this translation is equivalent to the
crude translation if the replication takes this form.
}

The translation below 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.

This may be adequate if we are only interested in whether systems
converge or not. However, if we consider a labelled transition system
for \PPc\ we will only observe $\tau$ events from such systems.

A different approach is simply to add \PPc\ processes of the form
$\PPname{n}{Chan(EQ)}$ for each name $n \in fn(P)$ in parallel with
the translation of \Pc\ term $P$.

\section{A Restricted Subcalculus of \PC}

In some very restricted circumstances we do not need to use the
translation based on special \PPc\ channel processes. In these
circumstances we can be sure that for each name, at most one
\Pc\ process in a parallel composition of processes will have an
input prefix for that name at a given time. It will be seen that
this imposes severe restrictions on the possible forms of \Pc\
process, but these restrictions are obeyed by networks generated
by some simulations of the \Lc.

A first observation is that a process cannot receive input on any
name it has received as input -- unless we are to trace the behaviour
of all processes which might send output on a given name. Secondly,
in a parallel composition only one process in the composition can
take input on a given name.

Every symbol, $A$, used in parametric definitions has an arity,
where $0 \leq arity(A)$. In the restricted calculus we will also
associate an input arity, $0 \leq inarity(A) \leq arity(A)$,
which identifies the parameters which can carry names used for input.

We will define a function $dn(N)$ over \Pc\ processes. This will
be similar in effect to the function defined for \PPc\ and will
be used to constrain the form of \Pc\ processes we allow:
\begin{eqnarray*}
dn(\inpact{n}{n'}{N}) & = & \{n\} \\
dn(\outact{n}{n'}{N}) & = & dn(N) \\
dn(\restrict{n}{N}) & = & dn(N) \setminus \{n\} \\
dn(\parprocs{N}{N'}) & = & dn(N) \cup dn(N') \\
dn(\inaction) & = & \{\} \\
dn(\agtuse{A}{n_1,\ldots,n_j,\ldots,n_k}) & = & \{n_1,\ldots,n_j\}, j = inarity(A)
\end{eqnarray*}

We then add some constraints that must be obeyed. Firstly,
in $(\parprocs{N}{N'})$, we require that $dn(N) \cap dn(N') = \{\}$.
Hence no free name may be used for input in both $N$ and $N'$.

Secondly, in $\inpact{n}{n'}{N}$, we require that
$dn(N) \subseteq \{n\}$. Otherwise, after performing input,
the property required for a parallel composition might be violated.
A consequence is that if $N$ contains a parallel composition,
all names used for input must be restricted, except for $n$.

Finally $\agtdef{A}{n_1,\ldots,n_j,\ldots,n_k}{N}$ is only
valid if $dn(N) = \{n_1,\ldots,n_j\}$,
where $j = inarity(A)$.

We note that the restriction on parametric definitions can be
satisfied by the translation of a replication of the form
$\replicate{X}{\inpact{x}{w}{P}}$, discussed above, as long
as $P$ does no further input on $x$ (or any other free name).

The representation is
$\agtuse{A}{x,n_P}$ where
$\agtdef{A}{x,n_P}{\inpact{x}{w}(\parprocs{P}{\agtuse{A}{x,n_P}})}$,
and $inarity(A) = 1$. The reader can check that, under the assumption
that $dn(\agtuse{A}{x,n_P}) = \{x\}$,
$dn(\inpact{x}{w}(\parprocs{P}{\agtuse{A}{x,n_P}})) = \{x\}$ as long
as $dn(P) = \{\}$.

Acceptable forms of replication conforms to the pattern above,
where input triggers replication, and the body of the replication
cannot perform further input on free names. 

\comment{
I suspect it is the case that recursive definitions can only be
meaningful with $inarity$ of 0 or 1.

Jeong Ho, could you see if the above discussion helps in defining
direct translations?
}

\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 %%%
