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

\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{\PPdef}[2]{{#1} = {#2}}
\newcommand{\PPstop}[0]{\bf stop}
\newcommand{\PPname}[2]{{#1}:\,{#2}}
\newcommand{\PPpar}[2]{{#1}\,\|\,{#2}}
\newcommand{\PPres}[2]{{#2} \backslash {#1}}
\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}[3]{{#1}={#2} \cdot {#3}}
\newcommand{\nonmatch}[3]{{#1}\neq{#2} \cdot {#3}}
\newcommand{\inaction}{0}
\newcommand{\pair}[2]{{#1}\,{#2}}
\newcommand{\triv}{}
%\input{john-proc-macros}
% New Process notation
\newcommand{\PruleChange}[3]{{#1}\;?\;{#2} & := & {#3}}
\newcommand{\PruleSpawn}[3]{{#1}\;?\;{#2} & \rightarrow & (\,{#3}\,)}
\newcommand{\Prule}[4]{{#1}\;?\;{#2} & \rightarrow & (\,{#3}\,)\;:=\;{#4}}
\newcommand{\Ppar}[2]{{#1}\,|\,{#2}}
\newcommand{\Pcall}[2]{{#1}\,!\,{#2}}
\newcommand{\Pdef}[2]{{#1}:\,{#2}}
% Translation representation
\newcommand{\transwhere}[3]{& & {\makebox[1.5cm][l]{where}}
{#1}\;?\;{#2}\;\cdot\;(\,{#3}\,)}
\newcommand{\transand}[3]{& & {\makebox[1.5cm][l]{and}}
{#1}\;?\;{#2}\;\cdot\;(\,{#3}\,)}
\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{\PPC}{$\pi^\pi$--Calculus}
\newcommand{\PPc}{$\pi^\pi$--calculus}
\newcommand{\RA}{{\em return-address\/} channel}
% Translation representation
\newcommand{\transexp}[2]{\sembrac{#1}_{#2}}
\newcommand{\transdef}[3]{\transexp{#1}{#2} & = & {#3}}
% End of macros
\begin{document}
\maketitle

\section{Introduction}

This version includes a match operation in the \PPc. It also includes a 
translation from \PPc\ to \Pc.

I still retain the distinction between variables and names. However, 
I think that the $\nu$ construct in \PPc\ should take a name rather 
than a variable. Variables should be restricted to input, and in a 
future version I propose that more complex terms might be bound to 
variables, compared by a match, and provided as agent arguments.

\section{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. These are combined in 
the set of {\em terms}, $T$ ranged over by $t$.

Also a set of recursive {\em agent} definitions is assumed: 
$\PPdef{A(x_1,\ldots,x_k)}{S}$. $S$, the class of process {\em scripts}, 
is given by the following syntax:
\begin{eqnarray*}
T & ::= & n \mid x \\
S & ::= & \PPin{x}{S} \mid \PPout{t}{t'}{S} \mid \PPnew{x}{S}{S'} 
\mid \PPmatch{t}{t'}{S}{S'}
\mid A(t_1,\ldots,t_n) \mid \PPstop
\end{eqnarray*}

The intuition is that $S$ is the sequential body of a process.
$S$ can be input $\PPin{x}{S}$ where $x$ binds over $S$
or output $\PPout{t}{t'}{S}$ meaning send $t'$ to $t$ and behave as $S$.
The send will be asynchronous as in the asynchronous \Pc.
$S$ can also spawn a new process $\PPnew{x}{S}{S'}$ where $S$ 
is the body of the new
process. Its name will be bound to $x$ which may be shared 
between the new process
and its creator (which will behave as $S'$).
The match construct $\PPmatch{t}{t'}{S}{S'}$ behaves as $S$ if $t$ 
and $t'$ are the same, otherwise as $S'$.
Recursive processes are dealt with through agent definitions
and $A(t_1,\ldots,t_k)$ behaves as $\PPsub{S}{t_1/x_1,\ldots,t_k/x_k}$ 
where there is a definition $\PPdef{A(x_1,\ldots,x_k)}{S}$.

Parallel {\em processes} form the set $P$ defined by the following syntax:
\begin{eqnarray*}
P & ::= & \PPname{n}{S} \mid \PPpar{P}{P'} \mid \PPoutP{n}{n'} 
\mid \PPres{n}{P}
\end{eqnarray*}

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

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

\section{Semantics}

There is probably an assumption that, initially, scripts only contain
variables, but during reduction communications contain only names.
There are therefore some contextual constraints left vague at this point.
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{\PPname{n}{\PPstop}}{P} & \equiv & P \\
\PPname{n}{A(n_1,\ldots,n_k)} & \equiv & \PPname{n}{\PPsub{S}{n_1/x_1,\ldots,n_k/x_k}}\:,
\hspace{1cm} 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*}
\PPname{n}{\PPout{n'}{n''}{S}} & \rightarrow & 
\PPpar{\PPname{n}{S}}{\PPoutP{n'}{n''}} \\
\PPpar{\PPname{n}{\PPin{x}{S}}}{\PPoutP{n}{n'}} & \rightarrow & 
\PPname{n}{\PPsub{S}{n'/x}} \\
\PPname{n}{\PPnew{x}{S}{S'}} & \rightarrow &
\PPres{n'}{(\PPpar{\PPname{n}{\PPsub{S'}{n'/x}}}
{\PPname{n'}{\PPsub{S}{n'/x}}})}\:,
\hspace{1cm} n' \not\in fn(\PPname{n}{\PPnew{x}{S}{S'}}) \\
\PPname{n}{\PPmatch{n'}{n'}{S}{S'}} & \rightarrow & 
\PPname{n}{S} \\
\PPname{n}{\PPmatch{n'}{n''}{S}{S'}} & \rightarrow & 
\PPname{n}{S'}\:, \hspace{1cm} n' \neq n''
\end{eqnarray*}
The first rule ``releases'' a message from process $n$ to 
process $n'$ with the 
contents $n''$.
The second rule shows how a message is received by process $n$
and the third rule describes the creation of a new process $n'$

A simpler version of the third rule is possible if variables 
and names form one class:
\begin{eqnarray*}
\PPname{n}{\PPnew{x}{S}{S'}} & \rightarrow &
\PPres{x}{(\PPpar{\PPname{x}{S}}{\PPname{n}{S'}})}
\end{eqnarray*}
The final reduction rules handle the match construct. Maybe it is a bad 
idea to make it a reduction, and the structural congruence could be used.

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}
The final cleanup rule for processes might be extended to clean up 
messages as well. I believe we could do this by first eliminating 
messages destined for a stopped process, and then removing the 
process once no further messages could possibly be sent to it. 
This is achieved by these structural rules:
\begin{eqnarray*}
\PPpar{\PPoutP{n}{n''}}{\PPname{n}{\PPstop}} & \equiv & 
{\PPname{n}{\PPstop}} \\
\PPpar{\PPres{n}{(\PPname{n}{\PPstop})}}{P} & \equiv & P
\end{eqnarray*}
\end{observation}

\begin{observation}
If the match is to be included in the structural congruence we have the 
following instead of the reductions for matching:
\begin{eqnarray*}
\PPname{n}{\PPmatch{n'}{n'}{S}{S'}} & \equiv & 
\PPname{n}{S} \\
\PPname{n}{\PPmatch{n'}{n''}{S'}{S}} & \equiv & 
\PPname{n}{S}\:, \hspace{1cm} n' \neq n''
\end{eqnarray*}
I am a bit concerned about whether the names used should be restricted 
in the whole process or not.
The approach suggested by Bent and Lone tried to use a context 
rule to resolve the match:
\begin{eqnarray*}
\PPname{n}{S} \rightarrow \PPname{n}{S''} & \Rightarrow & 
\PPname{n}{\PPmatch{n'}{n'}{S}{S'}} \rightarrow  \PPname{n}{S''} \\
\PPname{n}{S'} \rightarrow \PPname{n}{S''} & \Rightarrow & 
\PPname{n}{\PPmatch{n'}{n''}{S}{S'}} \rightarrow  \PPname{n}{S''} \:, 
\hspace{1cm} n' \neq n''
\end{eqnarray*}
However, I cannot see that his will work in the case where the scripts 
in the match generate new processes, or engage in communication. 
I think we need to think here: what should be considered ane event we can trace? 
The original reduction relation considers releasing a message and spawning 
a process as an event. In the \Pc\ unravelling a replication is not an event.
\end{observation}

\begin{observation}
We have not discussed the initial configuration of a process 
network in this calculus, but I assume it will be something 
like $\PPres{n}{(\PPname{n}{S})}$ for some script $S$. I think 
it should be clear that there will never be any free names in 
the resulting network. However, the congruence rules for matching
would violate this principle.
\end{observation}

\section{Translation of \PPc\ into the \Pc}

The target syntax we use will be for a variant of the 
asynchronous \Pc\ since no process will be guarded by 
output in the resulting \Pc\ network. We include agaent 
definitions rather than replication for recursion and 
matching constructs:
We have assumed that there is a matching construct in the \Pc,
\begin{eqnarray*}
N & ::= & \inpact{n}{n'}{N} \mid \outacta{n}{n'} 
\mid \restrict{n}{N} \mid \parprocs{N}{N'} \mid \match{n}{n'}{N}
\mid \nonmatch{n}{n'}{N} \mid \agtuse{A}{n_1,\ldots,n_k} \mid \inaction
\end{eqnarray*}
$\match{n}{n'}{N}$ acts as $N$ if $n$ and $n'$ are the 
same name, and as $\inaction$ otherwise.  There is 
a variant $\nonmatch{n}{n'}{N}$ with obvious semantics. 

For uses of an agent $A$ there will be a corresponding definition:
\begin{eqnarray*}
\agtdefn{A}{n_1,\ldots,n_k}{N}
\end{eqnarray*}

\begin{observation}
This is not quite the advertised \Pc\ but the official 
version could be used with a bit more effort. I am not 
sure what we should take for the form of matching 
construct. Suggestions?
\end{observation}

The translation is given by three functions
$s\sembrac{S}_n$ where $S$ is a process script and $n$ is a name, 
$d\sembrac{A(x_1,\ldots,x_k) = S}$ for translating agent definitions, and 
$p\sembrac{P}$ where $P$ is a parallel process.
\begin{eqnarray*}
s\sembrac{\PPin{x}{S}}_n & = & \inpact{n}{x}{s\sembrac{S}} \\
s\sembrac{\PPout{t}{t'}{S}}_n & = & 
\parprocs{\outact{t}{t'}{\inaction}}{s\sembrac{S}_n} \\
s\sembrac{\PPnew{x}{S}{S'}}_n & = &
\restrict{n'}{\parprocs{s\sembrac{\PPsub{S}{n'/x}}_{n'}}
{s\sembrac{\PPsub{S'}{n'/x}}_n}}\:,
\hspace{1cm} n' \not\in fn(\PPnew{x}{S}{S'}) \\
s\sembrac{\PPmatch{t}{t'}{S}{S'}}_n & = &
(\parprocs{\match{t}{t'}{s\sembrac{S}_n}}{\nonmatch{t}{t'}{s\sembrac{S'}_n}}) \\
s\sembrac{A(x_1,\ldots,x_k)}_n & = & A(n,x_1,\ldots,x_k) \\
s\sembrac{stop}_n & = & \inaction \\
\\
d\sembrac{A(x_1,\ldots,x_k) = S} & = & A(n,x_1,\ldots,x_k) = s\sembrac{S}_n \:,
\hspace{1cm} n \not\in fn(S)\\
\\
p\sembrac{\PPname{n}{S}} & = & s\sembrac{S}_n \\
p\sembrac{\PPpar{P}{P'}} & = & \parprocs{p\sembrac{P}}{p\sembrac{P'}} \\
p\sembrac{\PPoutP{n}{n'}} & = & \outact{n}{n'}{\inaction} \\
p\sembrac{\PPres{n}{P}} & = & \restrict{n}{p\sembrac{P}}
\end{eqnarray*}

Again, a simpler translation is possible if variables and 
names form one class:
\begin{eqnarray*}
s\sembrac{\PPnew{x}{S}{S'}}_n & = &
\restrict{x}{\parprocs{s\sembrac{S}_{x}}{s\sembrac{S'}_n}}\\
\end{eqnarray*}
\begin{observation}
I have messed around with the agent translation. I think this was necessary.
\end{observation}

It seems rather straightforward to prove the following 
(modulo structural equivalence):
\begin{eqnarray*}
P \rightarrow P' & \Rightarrow & p[P] \rightarrow^* p[P']
\end{eqnarray*}
where $\rightarrow^*$ is the reflexive transitive closure of the 
reduction relation for the \Pc.

For stronger results we should define a notion of equivalence, e.g. barbed
bisimulation could be defined as:

$P \sim Q$ iff
\begin{itemize}
\item $P \rightarrow P'$ then $Q \rightarrow Q'$ and $P' \sim Q'$
\item the reverse
\item $P \uparrow$ iff $Q \uparrow$
\end{itemize}
where $\uparrow$ ({\em commit}) is defined as 
$C[\PPoutP{n}{n'}] \uparrow\ \PPoutP{n}{}$ 
and $C[\PPname{n}{\PPin{x}{S}}] \uparrow\ n?$
and $C$ is a one hole context of processes.

\begin{observation}
The original said $c?$ rather than $n?$. I assume the latter was meant.
\end{observation}

With this we could prove
\begin{eqnarray*}
P \sim Q & \Rightarrow & p\sembrac{P} \approx p\sembrac{Q}
\end{eqnarray*}
where $\approx$ is weak barbed bisimulation on the \Pc.

\section{Translation of \Pc\ into the \PPc}

A proposed translation of the asynchronous \Pc\ is provided. 
It is assumed that the synchronous calculus can be simulated 
adequately by the asynchronous calculus.

The translation is based on the construction of a process network 
to implement the channels of the \Pc. A channel becomes two \PPc\ 
processes, a coordinating process and some more buffering processes!

First, however, a simple definition. A buffer, defined by 
agent $Buf$, forwards messages to a process named $k$:
\begin{eqnarray*}
\PPdefn{Buf(k)}{\PPin{x}{\PPout{k}{x}{Buf(k)}}}
\end{eqnarray*}

We require a buffer which only sends messages on demand. There is a
constraint that no more than one demand/trigger/request 
will be sent until a response has been received. The 
request could arrive before the data value, but requests 
do not need to be queued. Multiple data values may arrive 
before a request and need to be
stored. Below, they are queued rather than stacked.
\begin{eqnarray*}
\PPdefn{SBuf(k)}{\PPin{x}{\PPmatch{x}{k}{TBuf(k)}
{\PPnew{y}{SBuf(k)}{FBuf(k,x,y)}}}} \\
\PPdefn{TBuf(k)}{\PPin{x}{\PPout{k}{x}{SBuf(k)}}} \\
\PPdefn{FBuf(k,v,y)}{\PPin{x}{\PPmatch{x}{k}{k!v.Buf(y)}
{\PPout{y}{x}{FBuf(k,v,y)}}}}
\end{eqnarray*}
$SBuf$ is an empty synchronised buffer, waiting either data or a
trigger. The trigger is a message containing the name $k$ and the expected
response is a data value sent to $k$.

The empty buffer responds to a trigger by becoming an empty triggered
buffer, $TBuf$, and to data by becoming a full buffer, $FBuf$, which knows
about a new $SBuf$ which will hold any further data which arrives.

A triggered buffer $TBuf$ should {\em only} receive data. It
sends the data to $k$ and becomes an empty buffer again.

If a full buffer $FBuf$ receives a trigger, it sends the stored data 
to $k$ and then becomes a relay to the ``tail'' which stores any further 
data. If it
receives further data, it sends it to the tail. The data will pass along a
chain of $FBuf$s until it reaches an $SBuf$ at the end, which creates a new
$SBuf$ and turns itself into an $FBuf$.

Does that make sense? There are many variations possible. Exercises for the
reader:
\begin{enumerate}
\item Generalise it to allow multiple triggers before any data
arrives. 
\item Reduce the proliferation of processes by distinguishing a full
buffer containing one saved message, and an overflowed buffer which has a
tail process to store the rest of the data. 
\item Implement as a stack rather than a queue.
\end{enumerate}
These definitions support a buffer which holds on to data 
until asked to release
it. Such a buffer can be used by a receiver to guarantee that it knows where a
message has come from: if every process which might send it data is such a
buffer, it can select data by polling the appropriate generator. Here is
the coordinating process for a channel:
\begin{eqnarray*}
\PPdefn{Chan(k,n,\hat{n})}{\PPout{n}{k}
{\PPin{a}{\PPout{\hat{n}}{k}{\PPin{v}{\PPout{a}{v}{Chan(k,n,\hat{n})}}}}}}
\end{eqnarray*}

$k$ is the name of the process itself. $n$ is the name of 
the output side
which sends a received return address to $Chan$ on request 
and receives data back from the channel. $\hat{n}$, the
co-name, is the name of the input side which sends received 
data to $Chan$ on request. The $Chan$ process polls for a
return address, then a data value, sending the data value to the
address before repeating.

The configuration in which these are used is:
\begin{eqnarray*}
\PPpar{\PPname{n}{SBuf(k)}}
{\PPpar{\PPname{k}{Chan(k,n,\hat{n})}}{\PPname{\hat{n}}{SBuf(k)}}}
\end{eqnarray*}
\Pc\ channel writers send data to $\hat{n}$, readers send their 
own identity to $n$.

We give a possible translation from asynchronous \Pc\ to \PPc.
Note that the \Pc\ to \PPc\ translation only used asynchronous 
sends. The translation uses a function $r$ with auxiliary 
function $t$ which does the real work. The function $t$ 
carries the name of a \PPc\ process associated with the
translated network. This is needed when simulating \Pc\ 
communication since the channel processes need the name 
of the receiving \PPc\ process. 
A further function $f$ handles
agent definitions
\begin{eqnarray*}
r\sembrac{N} & = & \PPres{m}{(\PPname{m}{t\sembrac{N}_m})}\;, \:\:m \not\in fn(N) \\
\\
t\sembrac{\inpact{n}{n'}{N}}_m & = & \PPout{n}{m}{\PPin{n'}{t\sembrac{N}_m}} \\
t\sembrac{\outacta{n}{n'}}_m & = & \PPout{\hat{n}}{n'}{\PPstop} \\
t\sembrac{\restrict{n}{N}}_m & = & 
\PPnew{n}{SBuf(m)}{\PPnew{\hat{n}}{SBuf(m)}{\PPnew{m'}{t\sembrac{N}_{m'}}
{Chan(m,n,\hat{n})}}}\;, \:\:m' \not\in fn(N) \\
t\sembrac{\parprocs{N}{N'}}_m & = & \PPnew{m'}{t\sembrac{N}_{m'}}
{t\sembrac{N'}_m}\;, \:\:m' \not\in fn(\parprocs{N}{N'}) \\
t\sembrac{\match{n}{n'}{N}}_m & = & 
\PPmatch{n}{n'}{t\sembrac{N}_m}{\PPstop} \\
t\sembrac{\nonmatch{n}{n'}{N}}_m & = & 
\PPmatch{n}{n'}{\PPstop}{t\sembrac{N}_m} \\
t\sembrac{\agtuse{A}{n_1,\ldots,n_k}}_m & = & \agtuse{A}{n_1,\ldots,n_k} \\
t\sembrac{\inaction}_m & = & stop
\end{eqnarray*}
For symmetry it would be possible to create new processes for each process
in $(\parprocs{N}{N'})$ rather than keep one thread in the old process.

A further function $f$ handles
agent definitions:
\begin{eqnarray*}
f\sembrac{\agtdef{A}{n_1,\ldots,n_k}{N}} & = & 
\PPnew{m}{t\sembrac{N}_m}{\PPstop}\;, \:\:m \not\in fn(N)
\end{eqnarray*}

Anyone convinced?

\begin{observation}
I don't know yet if the match can be rendered as derived syntax -- I doubt it.

I suspect that a form of $\nu$ allowing multiple processes to be created in
parallel (more than one extra process) will be needed -- though I imagine a
derived syntax could be developed. So far I have not needed three processes
to all know about each other.
\end{observation}

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