%%% Start of LaTeX Document %%%
\documentclass[11pt,a4paper]{article}

% 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 L. 1st December 1995}

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

\newcommand{\sembrac}[1]{[\![ #1 ]\!]}
\newcommand{\infer}[3]
           {\vspace{.2cm}
            \hbox{${\displaystyle {\frac {#1}{#2}}\hspace{.5cm}{#3}}$}
            \vspace{.2cm}}
% New macros
\newcommand{\vecsc}[1]{\vec{\textsc{#1}}}
% 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{\PPsum}[2]{{#1}+{#2}}
\newcommand{\PPres}[2]{\nu{#1}\,{#2}}
\newcommand{\PPsub}[2]{{#1}\{{#2}\}}
\newcommand{\PPdefn}[2]{{#1} & = & {#2}}
% 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]{\textbf{rec} {\recvar {#1}} \cdot {#2}}
\newcommand{\guardedrec}[3]{\textbf{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}{}
% New Process notation
\newcommand{\Ppar}[2]{{#1},\;{#2}}
\newcommand{\Pcall}[2]{{#1}\,!\,{#2}}
\newcommand{\Pdef}[2]{{#1}:{#2}}
\newcommand{\Pinact}{Dead}
\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]
	{\textbf{where}}}{\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}} \rightarrow {#4}}}
\newcommand{\transand}[4]{& & {\makebox[1.5cm][l]
	{\textbf{and}}}{\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}} \rightarrow {#4}}}
\newcommand{\PPwhere}[2]{\textbf{where} & & {#1} \; = \; {#2}}
\newcommand{\PPand}[2]{\textbf{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{\MAPc}{mini asynchronous $\pi$--calculus}
\newcommand{\MAPC}{Mini Asynchronous $\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}{\emph{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}}
\newcommand{\defeq}{\stackrel{\triangle}{\;=}}
% End of macros
\begin{document}
\maketitle

\section{Changes}

\emph{Version L} integrates some thoughts on replication from a separate document by moving away from a \Pc\ with agent definitions to one with a restricted form of replication. There is discussion of the varieties of \Pc\ in use in the literature.

There is a significant change from unconditional input with a separate conditional construct to the use of conditional input. The previous forms are still available, but seen as syntactic sugar. Certain processes are made very much simpler as a result.

The history of earlier versions is in the final section.

\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). OGRe is described in ``Parallel
Implementation through Object Graph Rewriting'' by John Glauert.

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 \emph{names} ranged over by $n$, $m$,
etc. A set $\Sigma$ of 
\emph{symbols} ranged over by $F$, $G$, etc. each with an associated 
\emph{arity} ($\geq 0$) giving the number of arguments it should take. 
These are combined in 
the set of \emph{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 \emph{scripts},
are defined in terms of each other.

\subsection{\PPC\ Processes}

Parallel \emph{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*}

$\PPname{n}{S}$ is a named process
(the idea is similar to locations in some versions of  CCS)
running a script $S$.
$\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 named 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 \emph{Scripts}, $S$ are given by the following syntax:
\begin{eqnarray*}
S & ::= & \sum_i\,\PPin{t_i}{S_i} \mid \PPabs{n}{P}
\mid A(t_1,\ldots,t_n)
\end{eqnarray*}

Also a set of recursive \emph{agent} definitions is assumed: 
$\PPdef{A(n_1,\ldots,n_k)}{S}$. 

The intuition is that $S$ is the sequential body of a process.
An input--guarded script takes the form $\sum_i\,\PPin{t_i}{S_i}$.
If a message is directed to the process and matches at least one of the patterns $t_i$ then the process continues with the script given by the corresponding $S_i$. Variables in $t_i$ bind over $S_i$. If more than one pattern matches, the first is taken.

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

In previous versions we permitted the match construct in scripts:
\begin{eqnarray*}
\PPmatch{n}{t}{S}{S'}
\end{eqnarray*}
which 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'$.

This is seen as syntactic sugar in the present version. For each such match we assume a new symbol $Patt$. Then
\begin{eqnarray*}
\PPmatch{n}{t}{S}{S'} & \equiv &
	\PPabs{m}{(\PPpar
		{\PPoutP{m}{Patt(n)}}
		{\PPname{m}{(\PPsum{\PPin{Patt(t)}{S}}{\PPin{Patt(x)}{S'}})}} )}
\end{eqnarray*}
where $m$, and $x$ do not occur in $S$ or $S'$. This script sends to itself a message which will match the first case if $n$ is an instance of $t$ and the second case otherwise. No other message sent to this process will use the symbol $Patt$.

\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(\sum_i\,\PPin{t_i}{Si}) & = & \bigcup_i fn(S_i) \setminus fn(t_i) \\
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 $dn(P) \cap dn(P') = \{\}$ in $\PPpar{P}{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.

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 $\Pinact$, and a structural equivalence rule to garbage collect
processes when the form $\PPres{n}{(\PPname{n}{\Pinact})}$ 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\}$.

\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}{\PPabs{m}{P}} & \equiv & {\PPsub{P}{n/m}} \:, 
	\hspace{1cm} dn(P) \subseteq \{m\}
\end{eqnarray*}
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{\PPoutP{n}{t}}{\PPname{n}{\sum_i\,\PPin{t_i}{S_i}}} & \rightarrow & 
\PPname{n}{\sigma_j(S_j)} \:,
	\hspace{1cm} \exists j \le i, \sigma_j \: : \: t = \sigma_j(t_j)
	\wedge \forall k < j, \sigma  \: : \: t \neq \sigma(t_k)\\
\end{eqnarray*}
$\sigma$ is a mapping from names to terms.
A message is received by process $n$ if it has a script ready for input with a pattern matching the message. Since patterns might overlap, the earliest pattern will be chosen.

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

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$.

\section{Review of \Pc}

The \Pc\ appears in various syntactic forms. The presentation of semantics has also evolved.

The monadic form in \cite{MPW} provides very general choice, a matching construct, and parametric definitions. The simpler, more restricted, form in \cite{FunAsProcs} uses replication and omits choice and matching. It is sufficiently powerful to model the \Lc, however.

The Polyadic \Pc\ in \cite{PolyPi} has guarded choice and replication. Milner shows that conditional computation may be modelled without a match operation and that parametric definitions can be (weakly) simulated by replication. Polyadic communication can be seen as syntactic sugar based on monadic communication.

Meanwhile Honda an Tokoro \cite{HandT} and Boudol \cite{Boudol} (and Glauert \cite{Parle92}) show that the asynchronous calculus, in which processes are not guarded by output actions, has all the required power, and may be used to simulate the synchronous calculus in almost all respects.

There is increasing use of a simplified calculus which is called the \emph{\MAPC}. This has no choice or match construct. Communication is asynchronous and a restricted form of input-guarded replication is used.

We will use such a syntax for the \Pc, though we will consider polyadic communication and synchronous communication. Both of these extensions can be seen as syntactic sugar, but can also be simulated directly in the \PPc.
\begin{eqnarray*}
N & ::= & \inpact{x}{\vec{y}}{N} \mid \; \replicate{A}{\inpact{x}{\vec{y}}{N}}
	\mid \outact{x}{\vec{v}}{N}
	\mid \outacta{x}{\vec{v}}
	\mid \restrict{x}{N} \mid \parprocs{N}{N'} \mid \inaction
\end{eqnarray*}
All features of the full \Pc\ can be simulated by the \MAPc, except perhaps the general choice construct which does not seem to be of interest to anyone. For example, we can provide something like the general case of replication. In
the following, $x \not\in fn(P)$:
\begin{eqnarray*}
Q = \restrict{x}{\parprocs{\outacta{x}{}}
		{\replicate{X}{\inpact{x}{}{(\parprocs{P}{\outacta{x}{}})}}}} &
	\approx & \replicate{X}{P}
\end{eqnarray*}
$Q$ becomes, by a $\tau$ step,
\begin{eqnarray*}
& & \restrict{x}{\parprocs{P}{\parprocs{\outacta{x}{}}
{\replicate{X}{\inpact{x}{}{(\parprocs{P}{\outacta{x}{}})}}}}} \\
& \cong & \parprocs{P}{\restrict{x}{\parprocs{\outacta{x}{}}
{\replicate{Y}{\inpact{x}{}{(\parprocs{P}{\outacta{x}{}})}}}}} \\
& = & \parprocs{P}{Q}
\end{eqnarray*}
So it seems that $Q$ is weakly bisimilar to $\replicate{X}{P}$ using
standard \Pc\ semantics.

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

A proposed translation of the \Pc\ is provided. 
The translation is based on the use of a \PPc\ process  
to implement a \Pc\ name (communication channel).
A \PPc\ channel process coordinates requests for input and output actions using the name. Input requests are provided by $Get$ messages which carry the identity of the process to receive data. Output requests are provided by $APut$ messages which carry
data values.
\begin{eqnarray*}
\PPdefn{Chan}{\PPin{Get(n)}{\PPin{APut(v)}{\PPabs{l}{(\PPpar{\PPoutP{n}{v}}
	{\PPname{l}{Chan}})}}}}
\end{eqnarray*}
Originally, a $Chan$ process will only take a $Get$ message. Outstanding $APut$ messages are only accepted once a $Get$ has been seen. A data message is sent and the script is repeated.

This form supports asynchronous communication. Synchronous communication requires that the sending process is blocked until the communication completes. This is achieved by making the translation of the output guarded process wait for a synchronisation signal $Sync$ when the communication is closed. We use $Put$ messages in place of $APut$ and add the identity of a process to receive the synchronisation message.
\begin{eqnarray*}
\PPdefn{Chan}{\PPin{Get(n)}{\PPin{Put(v,s)}{\PPabs{l}{(\PPpar{\PPoutP{n}{v}}
	{\PPpar{\PPoutP{s}{Sync}}{\PPname{l}{Chan}}})}}}}
\end{eqnarray*}

In the translation below, we support both styles, at the cost of a slightly more sophisticated definition of $Chan$:
\begin{eqnarray*}
\PPdefn{Chan}{\PPin{Get(n)}{(\PPsum
	{\PPin{APut(v)}{\PPabs{l}{(\PPpar{\PPoutP{n}{v}}
		{\PPname{l}{Chan}})}}}
	{\PPin{Put(v,s)}{\PPabs{l}{(\PPpar{\PPoutP{n}{v}}
		{\PPpar{\PPoutP{s}{Sync}}{\PPname{l}{Chan}}})}}}
	)}}
\end{eqnarray*}

In the following we only handle monadic communication. Jeong Ho has extensions to handle the polyadic form.
The function $t$ maps \Pc\ processes to \PPc\ processes:
\begin{eqnarray*}
t\sembrac{\inpact{x}{y}{N}} & = &
    \PPres{m}{(\PPpar{\PPoutP{x}{Get(m)}}{\PPname{m}{\PPin{y}
	{\PPabs{m'}{t\sembrac{N}}}}})} \\
t\sembrac{\replicate{A}{\inpact{x}{y}{N}}} & = &
    \PPres{m}{(\PPname{m}{A(x,\vecsc{n})})} \\
\PPwhere{A(x,\vecsc{n})}{\PPabs{m}{(\PPpar
	{\PPoutP{x}{Get(m)}}
	{\PPname{m}{\PPin{y}{\PPabs{m'}{(\PPpar
		{\PPname{m'}{A(x,\vecsc{n})}}
		{t\sembrac{N}}
		)}}}}
	)}} \\
& & \vecsc{n} \defeq (fn(N) \setminus \{x,y\}) \\
t\sembrac{\outact{x}{v}{N}} & = &
    \PPres{m}{(\PPpar{\PPoutP{x}{Put(v,m)}}{\PPname{m}{\PPin{Sync}
	{\PPabs{m'}{t\sembrac{N}}}}})} \\
t\sembrac{\outacta{x}{v}} & = &
    \PPoutP{x}{APut(v)} \\
t\sembrac{\restrict{x}{N}} & = &
    \PPres{x}{(\PPpar{\PPname{x}{Chan}}{t\sembrac{N}})} \\
t\sembrac{\parprocs{N}{N'}} & = &
    \PPpar{t\sembrac{N}}{t\sembrac{N'}} \\
t\sembrac{\inaction} & = & \PPempty
\end{eqnarray*}

The names in the \Pc\ are represented by \PPc\ processes which
start by running the script $Chan$. 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}$ 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{x}{y}{N}) & = & \{x\} \\
dn(\replicate{A}{\inpact{x}{y}{N}}) & = & \{x\} \\
dn(\restrict{x}{N}) & = & dn(N) \setminus \{x\} \\
dn(\outact{x}{v}{N}) & = & dn(N) \\
dn(\outacta{x}{v}) & = & \{\} \\
dn(\parprocs{N}{N'}) & = & dn(N) \cup dn(N') \\
dn(\inaction) & = & \{\}
\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$.

For similar reasons, in $\replicate{A}{\inpact{x}{y}{N}}$ we require that $dn(N) = \{\}$. Unravelling a replication only happens following an input action, in which case we have $(\parprocs{\PPsub{N}{v/y}}{\replicate{A}{\inpact{x}{y}{N}}})$, where $v$ is the value received. In the new network the replication can receive on $x$ so we require that $\PPsub{N}{v/y}$ cannot.

\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 \Pc\ by \OGRe}

We give a translation of the \Pc\ into Object Graph Rewriting (\OGRe).
The translation below is based on the use of an \OGRe\ process  
to implement a \Pc\ name (communication channel).

\subsection{\OGRe\ Channel Processes}

\OGRe\ may be used to implement a channel process which receives either requests for input, provided by $Get$ messages, or data values, with optional synchronisation addresses, provided 
by $APut$ and $Put$ messages. 
$Get$ messages contain the names of \OGRe\ processes to receive data values. 
$APut$ messages contain a value to be sent.
In addition to a value to be sent,
$Put$ messages also contain the name of an \OGRe\ process
to receive a synchronisation message when the communication completes.

Initially, a \Pc\ channel $n$ will be represented by a process with 
state $Chan$:
\begin{eqnarray*}
\Pdef{n}{Chan}
\end{eqnarray*}
\begin{eqnarray*}
\PruleChange {c} {Chan} {Get(r)} {RChan(r)} \\
\Prule {c} {RChan(r)} {APut(v)}
	{\Pcall {r} {Data(v)}} {Chan} \\
\Prule {c} {RChan(r)} {Put(v,s)}
	{\Ppar {\Pcall {r} {Data(v)}} {\Pcall {s} {Sync}}} {Chan}
\end{eqnarray*}

In the translation of a \Pc\ term, an input action is simulated by a $Get$ message which carries the identity
of an \OGRe\ process which will simulate the term following the action. This
process will wait for a $Data$ message carrying the value from the
corresponding output action when a communication is closed.

An output-guarded action is simulated by a $Put$
message to the \OGRe\ channel process corresponding to the subject of the
action. The $Put$ message carries the value offered and the identity of an
\OGRe\ process which will simulate the \Pc\ term following the action. This
process will wait for a $Sync$ message indicating that the communication has
been closed and the value passed to the corresponding input action.

Asynchronous output is simulated using an $APut$ message which requires no synchronisation.

\subsection{Simulation of \Pc}

The function $q$ maps \Pc\ processes to \OGRe\ processes.
The parameter $m$ is the name of the \OGRe\ process corresponding
to the translated \Pc\ process:

\begin{eqnarray*}
q\sembrac{\inpact{x}{y}{N}}_m & = &
	\Ppar{A(\vecsc{n})}{\Pcall{x}{Get(m)}} \\
	\transwhere{m}{A(\vecsc{n})}{Data(y)}{q\sembrac{N}_m} \\
	& & \vecsc{n} \defeq (fn(N) \setminus \{y\}) \\
q\sembrac{\replicate{A}{\inpact{x}{y}{N}}}_m & = &
	\Ppar{A(x,\vecsc{n})}{\Pcall{x}{Get(m)}} \\
	\transwhere{m}{A(x,\vecsc{n})}{Data(y)}
		{\Ppar
			{\Ppar{\Pdef{m}{A(x,\vecsc{n})}}{\Pcall{x}{Get(m)}}}
			{\Pdef{m'}{q\sembrac{N}_{m'}}}
		} \\
	& & \vecsc{n} \defeq (fn(N) \setminus \{x,y\}) \\
q\sembrac{\outact{x}{v}{N}}_m & = &
	\Ppar{B(\vecsc{n})}{\Pcall{x}{Put(v,m)}} \\
	\transwhere{m}{B(\vecsc{n})}{Sync}{\Pdef{m}{q\sembrac{N}_m}} \\
	& & \vecsc{n} \defeq fn(N) \\
q\sembrac{\outacta{x}{v}}_m & = &
	\Ppar{\Pinact}{\Pcall{x}{APut(v)}} \\
q\sembrac{\restrict{x}{N}}_m & = &
    \Ppar{q\sembrac{N}_m}{\Pdef{x}{Chan}} \\
q\sembrac{\parprocs{N}{N'}}_m & = &
    \Ppar{q\sembrac{N}_m}{\Pdef{m'}{q\sembrac{N'}_{m'}}} \\
q\sembrac{\inaction}_m & = & \Pinact
\end{eqnarray*}

The state $\Pinact$ labels a process which should never receive any further
messages. It remains to be proved that this is the case for every $\Pinact$
process which arises from evaluating the \OGRe\ system generated by $q$ from any \Pc\ term.

The names in the \Pc\ are represented by \OGRe\ processes of the form
$Chan$. It is the restriction
construct which causes the channel processes to be introduced.
When a \Pc\ term with a bound name is translated by the scheme $q$, a
channel process is produced by the translation of the binding restriction.

To account for names which are free in the whole translated term, we add an \OGRe\
process of the form
$\PPname{n}{Chan}$ for each name $n \in fn(P)$ in parallel with
the translation of $P$. The translation of a \Pc\ term $P$ is
$\Pdef{m}{q\sembrac{P}_m}$ where $m \not\in fn(P)$.

The following example shows translation of the term
$R = (\parprocs{\inpact{x}{y}{P}}{\outact{x}{v}{Q}})$ where 
$fn(P) = \{y\}$ and $fn(Q) = \{\}$:
\begin{eqnarray*}
\Pdef{m}{q\sembrac{\parprocs{\inpact{x}{y}{P}}{\outact{x}{v}{Q}}}_m}
& = & 	\Ppar{\Pdef{m}{q\sembrac{\inpact{x}{y}{P}}_m}}
		{\Pdef{m'}{q\sembrac{\outact{x}{v}{Q}}_{m'}}} \\
& = & \Ppar{\Ppar{\Pdef{m}{A}}{\Pcall{x}{Get(m)}}}
		{\Pdef{m'}{q\sembrac{\outact{x}{v}{Q}}_{m'}}} \\
	\transwhere{m}{A}{Data(y)}{\Pdef{m}{q\sembrac{P}_m}} \\
& = & \Ppar{\Ppar{\Pdef{m}{A}}{\Pcall{x}{Get(m)}}}
		{\Pdef{m'}{\Ppar{B}{\Pcall{x}{Put(v,m')}}}} \\
	\transwhere{m}{A}{Data(y)}{\Pdef{m}{q\sembrac{P}_m}} \\
	\transand{m'}{B}{Sync}{\Pdef{m'}{q\sembrac{Q}_{m'}}}
\end{eqnarray*}
Since $x$ is free in $R$ we also add the \OGRe\ process
$\PPname{x}{Chan}$. Assuming the definitions of $A$ and $B$ as defined
above, the network may then evolve as follows:
\begin{eqnarray*}
& & \Ppar{\Ppar{\Pdef{m}{A}}{\Pcall{x}{Get(m)}}}
		{\Ppar {\Pdef{m'}{B}}
			{\Ppar{\Pcall{x}{Put(v,m')}}{\PPname{x}{Chan}}}} \\
& \rightarrow & \Ppar{\Pdef{m}{A}}
		{\Ppar {\Pdef{m'}{B}}
			{\Ppar{\Pcall{x}{Put(v,m')}}{\PPname{x}{RChan(m)}}}} \\
& \rightarrow & \Ppar{\Pdef{m}{A}}
		{\Ppar {\Pdef{m'}{B}}
			{\Ppar{\PPname{x}{Chan}}
				{\Ppar{\Pcall{m}{Data(v)}}{\Pcall{m'}{Sync}}}}} \\
& \rightarrow & \Ppar{\Pdef{m}{q\sembrac{P\{v/y\}}_m}}
		{\Ppar {\Pdef{m'}{B}}
			{\Ppar{\PPname{x}{Chan}}
				{\Pcall{m'}{Sync}}}} \\
& \rightarrow & \Ppar{\Pdef{m}{q\sembrac{P\{v/y\}}_m}}
		{\Ppar {\Pdef{m'}{q\sembrac{Q}_{m'}}}
			{\PPname{x}{Chan}}}
\end{eqnarray*}
Since, by the assumptions we made about free names, $x$ does not appear free
in $P$ or $Q$, the channel process ${\PPname{x}{Chan}}$ can never
receive further messages and can be garbage collected. The resulting network
is the same as $\PPname{m}{q\sembrac{\parprocs{P\{v/y\}}{Q}}_m}$.
$(\parprocs{P\{v/y\}}{Q})$ is, of course, the result of a communication step
in
the original term $(\parprocs{\inpact{x}{y}{P}}{\outact{x}{v}{Q}})$.
Since \Pc\ names are preserved in the translation it will be seen that we
were justified in identifying $q\sembrac{P}_{m}\{v/y\}$ with
$q\sembrac{P\{v/y\}}_m$.

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

\section{History}

\emph{Version K} introduced a translation of \Pc\ into \OGRe. Since we have
a translation of \Pc\ to \PPc, the original aim was to provide a mapping to
\OGRe\ by developing a mapping from \PPc\ to \OGRe. This proved less
straightforward than expected, while a direct mapping to \OGRe\ presented
few problems.

It remains to add a mapping from \OGRe\ to \PPc\ which should compose with the \Pc\ to \OGRe\ mapping to provide an alternative, but obviously equivalent, \Pc\ to \PPc\ mapping.

The document also omits a proper definition of \OGRe\ which will be provided separately.

\emph{Version J} added a little more explanation to Version I.
It also introduced 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 restrict ourselves to the main use of replication which is
always guarded by an input action.

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

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.

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

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

\begin{thebibliography}{MPW89}

\bibitem[{Boudol}]{Boudol}
G. Boudol

\bibitem[{Gla92}]{Parle92}
J.R.W. Glauert:
{\em Asynchronous Mobile Processes
and Graph Rewriting}, 
Proc PARLE'92. LNCS 605. June 1992. (1992) 

\bibitem[{HoTo91}]{HandT}
K. Honda \& M. Tokoro:
{\em An object calculus for asynchronous communication}.
Proc.\ ECOOP'91, Geneva, July 1991.

\bibitem[{Mil90}]{FunAsProcs}
R. Milner: 
{\em Functions as Processes},
Automata, Languages, and Programming. Springer LNCS 443. (1990)
Also: Technical Report INRIA Sophia Antipolis, June 1989. 

\bibitem[{Mil91}]{PolyPi}
R. Milner: 
{\em The \PPC: A Tutorial},
Technical Report ECS-LFCS-91-180, Edinburgh University, October 1991. (1991)

\bibitem[{MPW89}]{MPW}
R. Milner, J. Parrow, \& D. Walker: 
{\em A Calculus of Mobile Processes}, Parts I and II,
Technical Report ECS-LFCS-89-85, Edinburgh University, June 1989. (1989)

\end{thebibliography}

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