% Parle '92 Paper
\documentstyle[a4,11pt]{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{{\Large\bf Asynchronous Mobile Processes and Graph Rewriting}}
\author{
        {\it J. Glauert\thanks{Partially supported by ESPRIT BRA 3074: Semagraph}}\\
	School of Information Systems\\
	University of East Anglia\\
	Norwich NR4 7TJ, UK\\
	\\
	Tel: +44 603 592671 \\
	Fax: +44 603 507720 \\
	Email: jrwg@sys.uea.ac.uk \\ 
	}
\date{19th November, 1991}
%\date{To appear in Proc. of CHALMERS WORKSHOP ON CONCURRENCY,

%Environments
\newtheorem{defi}{Definition}[subsection]
\newtheorem{thm}{Theorem}[subsection]
\newtheorem{lemma}{Lemma}[subsection]
\newtheorem{prop}{Proposition}[subsection]
\newtheorem{cor}{Corollary}[subsection]
\newtheorem{ex}{Example}[subsection]
%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{fact}{Fact}[section]
\newtheorem{lemmaa}[fact]{Lemma}
\newtheorem{thmm}[fact]{Theorem}
\newtheorem{corr}[fact]{Corollary}
\newtheorem{notation}[fact]{Notation}
\newtheorem{propp}[fact]{Proposition}
\newtheorem{exx}[fact]{Example}
\newtheorem{defii}[fact]{Definition}

\newenvironment{definition}{\begin{defii}\rm}{\null\hfill $\Box$ \end{defii}}
\newenvironment{example}{\begin{exx}\rm}{\end{exx}}

\newenvironment{proof}{\vspace{3 mm}{\noindent \bf Proof}\rm}{\null\hfill
$\Box$\\ \vspace{3 mm}}
%%%%%%%%%%%%%%%%


%\newenvironment{proof}{{\bf Proof.}}{\hfill $\Box$}
%\newenvironment{framedfigure}[1]{\begin{figure}
%			   		\mbox{}\hrulefill\mbox{}\\\\}
%						%text
%					{\mbox{}		\\\\
%					\mbox{}\hrulefill\mbox{}
%				\end{figure}}
%%%%%%%%%%%%%%%%%%%%%

\newcommand{\myline}{\mbox{}\\\mbox{}\hrulefill\mbox{}\\\\}
\newcommand{\qed}{\hfill $\Box$}
\newcommand{\fed}[1]{{\bf #1}}
\newcommand{\ov}[1]{\overline{#1}}
\newcommand{\compf}{\overline{\vspace{12pt}}}
\newcommand{\un}[1]{\underline{#1}}
\newcommand{\mynot}[1]{\,\,\,\not{\!\!\!#1}}
\newcommand{\cat}[1]{{\bf #1}}

%Arrows
\newcommand{\ioi}{\;\;\Leftrightarrow\;\;}
\newcommand{\ra}{\longrightarrow}
\newcommand{\inta}{\succ\!\rightarrow}
\newcommand{\finta}{\succ\!\rightarrow\hspace{-.35cm}\rightarrow}
\newcommand{\notinta}{\inta\hspace{-5mm}\not\hspace{5mm}}
\newcommand{\con}{\downarrow}
\newcommand{\wcon}{\Downarrow}
\newcommand{\dvr}{\uparrow}
\newcommand{\wdvr}{\Uparrow}
\newcommand{\wra}{\Longrightarrow}
\newcommand{\der}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\fder}[1]{\stackrel{\!#1}
	{\longrightarrow\hspace{-.6cm}\longrightarrow}}
\newcommand{\wder}[1]{\stackrel{#1}{\Longrightarrow}}
\newcommand{\fun}{\longrightarrow}
\newcommand{\parfun}{\rightharpoonup}
%%%%%%%%%%%%%%%%%%%


% Denotations, Angles, Box and Diamond

\newcommand{\den}[1]{[\![#1]\!]}
\newcommand{\fden}[1]{[\![\!|#1|\!]\!]}
\newcommand{\ran}{\rangle}
\newcommand{\lan}{\langle}
\newcommand{\diam}[1]{\lan #1 \ran}
\newcommand{\ddiam}[1]{\lan\cdot #1\cdot\ran}
\newcommand{\bbox}[1]{[ #1 ]}
\newcommand{\dbox}[1]{[\cdot #1\cdot]}


%Preorder,equivalence and other relations

\newcommand{\equidef}{\stackrel{``def''}{=\!\!=}}
\newcommand{\preorder}[1]{\raisebox{-.6ex}{\raisebox{.95ex}
				{$#1$}$\!\!\!\!\!\scriptscriptstyle \sim$}}
\newcommand{\Mord}{\;\presim_M\;}
%\newcommand{\Meq}{{\;\preorder{-}}_M\;}
\newcommand{\eq}{\mathrel{%\lower.2ex
             \hbox{${\stackrel{-}{\scriptscriptstyle \sim}}$}}}
\newcommand{\Meq}{\eq_M} 
\newcommand{\presim}{\mathrel{\lower.2ex
             \hbox{${\stackrel{\sqsubset}{\scriptscriptstyle \sim}}$}}}
\newcommand{\altpreord}{\mathrel{\lower.2ex
             \hbox{${\stackrel{\sqsubset}{\scriptscriptstyle \approx}}$}}}
\newcommand{\wpresim}{\mathrel{\lower.2ex
          \hbox{${\stackrel{\sqsubset}{\scriptscriptstyle \approx}}$}}}
\newcommand{\lt}{\sqsubseteq}
\newcommand{\must}{\;\un{must}\; }
\newcommand{\mustnot}{\;\un{m\!\!\!\not u st}\; }
\newcommand{\prleq}{\sqsubseteq_E}

%Simple symbols

\newcommand{\ac}{{\cal A}}
\newcommand{\cB}{{\cal B}}
%\newcommand{\cu}{{\cal u}}
\newcommand{\si}{\sigma}
\newcommand{\ff}{f\!f}
\newcommand{\tr}{t\!\!t}
\newcommand{\f}[1]{f_{in}^{#1}\uplus f_{out}^{#1}}


%Big sums, unions, etc.

\newcommand{\osum}{\sum\!\!\!\!\!\!\circ\,\,\,}%internal sum
\newcommand{\osumdis}{\sum\!\!\!\!\!\!\circ\,\,\,\,\,}%internal sum displayed
\newcommand{\oss}{\sum\!\!\!\!\!\!\circ\,\,\,\,\,}%the same as osumdis
\newcommand{\udot}{\cup\!\!\!\!\!\,\!\,\cdot\,\,\,}
\newcommand{\Lor}[1]{\bigcup_{#1}}
\newcommand{\Land}[1]{\bigcap_{#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%Structure of formulas

\newcommand{\casedef}[4]% case definition
	{\left\{ \begin{array}{ll}
		#1 & #2 \\
		#3 & #4
		\end{array}\right.}




\newcommand{\mafrac}[2]{\begin{array}{c}
				{#1}	\\
				\hline{#2}\\
			\end{array}

			}
\newcommand{\ITE}[3]
		{\;If\; #1 \;\begin{array}[t]{l}
				Then\; #2 \\
				Else\; #3
			      \end{array}
		   }
\newtheorem{theorem}{Theorem}[section]
\newtheorem{nlemma}{Lemma}[section]
\newtheorem{ndefinition}[theorem]{Definition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{nnotation}[theorem]{Notation}
\newtheorem{nexample}[theorem]{Example}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{conjecture}[theorem]{Conjecture}
\newcounter{LLN}
\newcommand{\beginit} {
                         \begin{list}{\hfill{\rm \arabic{LLN}.}
}{\usecounter{LLN}
                         \setlength{\leftmargin}{\leftmarginii}
                         \setlength{\itemsep}{\smallskipamount}}}

\newcommand{\nonconsys}{nondeterministic and concurrent systems}
\newcommand{\lcal}{$\lambda$--Calculus}
\newcommand{\pcal}{$\pi$--Calculus}
\newcommand{\ahob}{applicative higher order bisimulation}
\newcommand{\ahos}{applicative higher order simulation}
%\newcommand{\presim}{\stackrel{\scriptscriptstyle\sqsubset}
%                     {\scriptscriptstyle\sim}}
%\newcommand{\wpresim}{\stackrel{\scriptscriptstyle\sqsubset}
%                     {\scriptscriptstyle\approx}}
\newcommand{\Pbrac}[1]{\{\!\mid #1 \mid\!\}}
\newcommand{\para}{\|}
\newcommand{\PPr}{\mbox{\sl Pr}}
\newcommand{\CPr}{\mbox{\sl CPr}}
\newcommand{\RPr}{\mbox{\sl RPr}}
\newcommand{\FPr}{\mbox{\sl FPr}}
\newcommand{\CFPr}{\mbox{\sl CFPr}}
\newcommand{\Prminus}{\mbox{\sl Pr}^-}
\newcommand{\CPrminus}{\mbox{\sl CPr}^-}
\newcommand{\Id}{\mbox{\sl Id}}
\newcommand{\CR}{\mbox{\sl CR}}
\newcommand{\ACR}{\mbox{\sl ACR}}
\newcommand{\ACRS}{\mbox{\sl ACR}^{\ast}}
\newcommand{\CRS}{\mbox{\sl CR}^{\ast}}
\newcommand{\WCR}{\mbox{\sl WCR}}
\newcommand{\IWCR}{\mbox{\sl IWCR}}
\newcommand{\IWCRS}{\mbox{\sl IWCR}^{\ast}}
\newcommand{\WCRminus}{\mbox{\sl WCR}^-}
\newcommand{\WCRminusS}{\mbox{\sl WCR}^{-\ast}}
\newcommand{\SPEC}{\mbox{\sl SPEC}}
\newcommand{\IMP}{\mbox{\sl IMP}}
\newcommand{\Names}{\mbox{\sl Names}}
\newcommand{\Act}{\mbox{\sl Act}}
\newcommand{\Actminus}{\mbox{\sl Act}^-}
\newcommand{\CAct}{\mbox{\sl CAct}}
\newcommand{\FAct}{\mbox{\sl FAct}}
\newcommand{\CFAct}{\mbox{\sl CFAct}}
\newcommand{\Actdownarrow}{\mbox{\sl Ev}}
\newcommand{\CHOCS}{\mbox{\sl CHOCS}}
%\newcommand{\cat}[1]{{\bf #1}}
\newcommand{\Slim}[1]{\mbox{\sl #1}}
\newcommand{\slim}[1]{\;\mbox{\sl #1}\;}
\newcommand{\ol}[1]{\overline{#1}}
\newcommand{\pbefore}{\;\mbox{$before$}\;}
\newcommand{\bresult}{\;\mbox{\tt result}\;}
\newcommand{\presult}{\;\mbox{$result$}\;}
\newcommand{\displace}{\leftarrow\!\!\!\mid}
\newcommand{\rec}{{\tt rec}}
\newcommand{\recpx}{\rec\,x.\tau.(p\backslash a)}
\newcommand{\subrecpx}[1]{#1[\recpx/x]}
\newcommand{\ypx}{Y_x[p]}
\newcommand{\subypx}[1]{#1[\ypx/x]}
\newcommand{\Rres}{R^{\backslash}}
\newcommand{\Rsim}{\sim\! R\!\sim}
\newcommand{\Rhat}{\widehat{\Rsim}}
\newcommand{\HAT}[1]{\widehat{#1}}
\newcommand{\HATHAT}[1]{\widehat{\widehat{#1}}}
\newcommand{\TILDE}[1]{\widetilde{#1}}
\newcommand{\bvar}{\mbox{\tt var}\;}
\newcommand{\bobj}{\mbox{\tt obj}\;}
\newcommand{\bmethod}{\mbox{\tt method}\;}
\newcommand{\bclass}{\mbox{\tt class}\;}
\newcommand{\binherits}{\mbox{\tt inherits}\;}
\newcommand{\bbody}{\mbox{\tt body}\;}
\newcommand{\bcreate}{\mbox{\tt create}\;}
\newcommand{\bstart}{\mbox{\tt start}\;}
\newcommand{\emptysort}{\mbox{\tt \O}\;}
\newcommand{\emptyrho}{\rho_{\emptysort}}
\newcommand{\bproc}{\mbox{\tt proc}\;}
\newcommand{\is}{\;\mbox{\tt is}\;}
\newcommand{\bif}{\mbox{\tt if}\;}
\newcommand{\bthen}{\;\mbox{\tt then}\;}
\newcommand{\belse}{\;\mbox{\tt else}\;}
\newcommand{\pif}{\mbox{$if$}\;}
\newcommand{\pthen}{\;\mbox{$then$}\;}
\newcommand{\pelse}{\;\mbox{$else$}\;}
\newcommand{\bwhile}{\mbox{\tt while}\;}
\newcommand{\bdo}{\;\mbox{\tt do}\;}
\newcommand{\bpar}{\;\mbox{\tt par}\;}
\newcommand{\ppar}{\;\mbox{$par$}\;}
\newcommand{\binput}{\mbox{\tt input}\;}
\newcommand{\boutput}{\mbox{\tt output}\;}
\newcommand{\bskip}{\mbox{\tt skip}\;}
\newcommand{\bbegin}{\mbox{\tt begin}\;}
\newcommand{\bend}{\;\mbox{\tt end}}
\newcommand{\bcall}{\mbox{\tt call}\;}
\newcommand{\bvalue}{\mbox{\tt value}\;}
\newcommand{\bref}{\mbox{\tt ref}\;}
\newcommand{\sembrac}[1]{[\![ #1 ]\!]}
\newcommand{\setof}[2]{\{ #1 \: : \: #2 \}}
\newcommand{\Psetof}[2]{\Pbrac{ #1 \: | \: #2 }}
\newcommand{\arrow}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\warrow}[1]{\stackrel{#1}{\Longrightarrow}}
\newcommand{\trans}[3]{#1 \arrow{#2} #3}
\newcommand{\wtrans}[3]{#1 \warrow{#2} #3}
\newcommand{\skil}{\ \raisebox{-4.5pt}{\rule{1pt}{5mm}} \ }
\newcommand{\nonarrow}[1]{\stackrel{#1}{\not\rightarrow}}
\newcommand{\wnonarrow}[1]{\stackrel{#1}{\not\Longrightarrow}}
\newcommand{\bigL}{{\cal L}}
\newcommand{\bigb}{{\cal B}}
\newcommand{\bighb}{{\cal H\!\!B}}
\newcommand{\bigwhb}{{\cal W\!\!H\!\!B}}
\newcommand{\bigwhpb}{{\cal W\!\!H\!\!P\!\!B}}
\newcommand{\bigawhb}{{\cal A\!W\!\!H\!\!B}}
\newcommand{\bigiwhb}{{\cal I\!W\!\!H\!\!B}}
\newcommand{\bigahb}{{\cal A\!\!H\!\!B}}
\newcommand{\bigp}{{\cal P}}
\newcommand{\bigpminus}{{\cal P}^-}
\newcommand{\bigcp}{{\cal C\!\!P}}
\newcommand{\bigfp}{{\cal F\!\!P}}
\newcommand{\bigfcp}{{\cal F\!\!C\!\!P}}
\newcommand{\bigcpminus}{{\cal C\!\!P}^-}
\newcommand{\bighpb}{{\cal H\!\!P\!\!B}}
\newcommand{\bis}{bisimulation}
\newcommand{\SGamma}{{\scriptstyle \Gamma}}
\newcommand{\SPhi}{{\scriptstyle \Phi}}
\newcommand{\infer}[3]
           {\vspace{.2cm}
            \hbox{${\displaystyle {\frac {#1}{#2}}\hspace{.5cm}{#3}}$}
            \vspace{.2cm}}
\newcommand{\SFP}{{\bf SFP}}
\newcommand{\LLC}{Lazy--$\lambda$--Calculus}
\newcommand{\OOP}{object oriented programming}
\newcommand{\OOOP}{Object oriented programming}
\newcommand{\OOL}{object oriented programming language}
\newcommand{\Lazytrans}{\underline{\ }\!\Downarrow\!\underline{\ }}
\newcommand{\bigAB}{{\cal A\!\!B}}
\newcommand{\lapprox}{\approx_{\lambda}}
\newcommand{\lvapprox}{\approx_{\lambda v}}
\newcommand{\res}[1]{\backslash #1}
\newcommand{\lsub}[2]{\{#1/#2\}}
\newcommand{\ren}[2]{[#1\mapsto #2]}
\newcommand{\simdot}{\stackrel{\cdot}{\sim}}
\newcommand{\ahbsim}{\stackrel{:}{\sim}}
\newcommand{\ahbapprox}{\stackrel{:}{\approx}}
\newcommand{\tausim}{\ahbsim_{\tau}}
\newcommand{\tausub}[2]{[#1/#2]_{\tau}}
\newcommand{\Cp}[2]{\rec\, X.#1.(#2\mid X)}
\newcommand{\trig}[2]{#1\Rightarrow#2}
\newcommand{\loc}[1]{\lfloor #1}
\newcommand{\tausubqx}{\tausub{q}{x}}
\newcommand{\lsubbx}{\{b/x\}}
\newcommand{\lsubcx}{\{c/x\}}
\newcommand{\Cpbq}{(\trig{b}{\sembrac{q}})}
\newcommand{\Cpcq}{(\trig{c}{\sembrac{q}})}
%===========================================================================
%	END OF PROOF BOX
%
%  The complexity of the macro necessary to get a little box on the
%  right-hand-side at the end of a proof is amazing.  It really does
%  have to be this long!  Otherwise you're liable to get it at the
%  beginning of the next line, or even on the next page.
%
%\def\sqr#1#2{{\vcenter{\vbox{\hrule height.#2pt
     %\hbox{\vrule width.#2pt height#1pt \kern#1pt
           %\vrule width.#2pt}
     %\hrule height.#2pt}}}}
%\def\square{\mathchoice\sqr34\sqr34\sqr{2.1}3\sqr{1.5}3}
\def\pushright#1{{%        set up
   \parfillskip=0pt            % so \par doesnt push \square to left
   \widowpenalty=10000         % so we dont break the page before \square
   \displaywidowpenalty=10000  % ditto
   \finalhyphendemerits=0      % TeXbook exercise 14.32
  %
  %                 horizontal
   \leavevmode                 % \nobreak means lines not pages
   \unskip                     % remove previous space or glue
   \nobreak                    % don't break lines
   \hfil                       % ragged right if we spill over
   \penalty50                  % discouragement to do so
   \hskip.2em                  % ensure some space
   \null                       % anchor following \hfill
   \hfill                      % push \square to right
   {#1}                        % the end-of-proof mark (or whatever)
  %
  %                   vertical
   \par}}                      % build paragraph

% prefer proofs with statements, also space after
%\def\qed{\pushright{$\square$}\penalty-700 \smallskip}
\def\qed{\pushright{$\Box$}\penalty-700 \smallskip}

%===========================================================================
\newcommand{\BExp}{\mbox{\sl BExp}}
\newcommand{\Ev}{\mbox{\sl Ev}}
\newcommand{\Val}{\mbox{\sl Val}}
\newcommand{\PVar}{\mbox{\sl PVar}}
\newcommand{\DVar}{\mbox{\sl DVar}}
\newcommand{\Exp}{\mbox{\sl Exp}}
\newcommand{\Chan}{\mbox{\sl Chan}}
\newcommand{\FCPr}{\mbox{\sl FCPr}}
\newcommand{\eab}{strong extensional applicative prebisimulation}
%\newcommand{\presim}{\mathrel{\lower.2ex
%             \hbox{${\stackrel{\sqsubset}{\scriptscriptstyle \sim}}$}}}
%\newcommand{\wpresim}{\mathrel{\lower.2ex
%         \hbox{${\stackrel{\sqsubset}{\scriptscriptstyle \approx}}$}}}
\begin{document}
\maketitle
\begin{abstract}
Honda and Tokoro provide a formal system for communicating systems developed from Milner's $\pi$--calculus. Unlike other formalisms, their work is based on asynchronous communication primitives.

This paper proposes some minor but practically significant extensions to a model based on asynchronous communication and shows how the resulting system may be mapped very directly onto a graph rewriting system.

While the model based on asynchronous communication permits the most direct translation, a related model using synchronous communication may be implemented in a similar manner.

{\bf Keywords}: Parallel programming paradigms, Semantics of parallelism, Implementation of parallel languages.

The paper is not for consideration for a Poster Session.
\end{abstract}
\newpage
\section{Introduction}
The calculus of communicating systems of Milner \cite{Mil80} has provided a fertile theory for the study of concurrent process networks. CCS can describe regular systems, but cannot express systems with an arbitrary  dynamic structure.

\subsection{Synchronous and Asynchronous Process Calculi}
There have been two main approaches to extending CCS to model process networks which can evolve dynamically. One approach supports higher order processes which may be communicated as values. An example is the language CHOCS of Thomsen \cite{Tho89}. Another approach allows the communication of link names which then act as references to processes. The early work by Engberg and Neilson on ECCS \cite{EnN86} provided the foundation for the $\pi$--calculus \cite{MPW89} and LCCS developed by Leth \cite{Leth91}. Influenced by the Chemical Abstract Machine of Berry and Boudol \cite{BeBo90}, Milner has recast parts of the $\pi$--calculus allowing an elegant representation of functions as process networks \cite{Mil90}. The subset language omits both matching and summation, and provides a replication construct in place of recursively defined agents.

While all these calculi are based on a synchronous model of communication, Honda and Tokoro base an object-oriented formalism on asynchronous communication \cite{Hon91}. They develop an asynchronous concept of bisimulation and provide a mapping from the language of Milner \cite{Mil90} to their asynchronous form. This mapping, and other uses of the asynchronous formalism, rely on techniques for sequentialisation of events. One contribution of the current paper is to show that great simplifications can be made to these techniques if the messages communicated over links are allowed to be tuples rather than single values.

\subsection{Practical Application of Process Calculi}
A number of studies have been made of the relationship between process notations and functional
programming. Early work by Kennaway and Sleep used the LNET model \cite{KeSl82} and
Thomsen used higher order processes of CHOCS \cite{Tho89,Tho90}. Milner \cite{Mil90},
and Leth \cite{Leth91}, show how an arbitrary lambda expression may be converted to a network of
processes whose behaviour simulates reduction of the original $\lambda$--expression. Such work has been
primarily motivated by a desire to explore the theoretical relationship between the formalisms, rather
than to provide an efficient implementation of the Lambda Calculus.

There is increasing interest in using concepts from process calculi as the basis for practical implementations of concurrent programming languages. The language Facile \cite{GPM89} aims to
integrate
functional and process styles. Concurrency primitives have been proposed for Standard ML \cite{BMT91}.
The author is collaborating with the Facile project at ECRC to study implementation techniques for such integrated languages.
Early work considers encoding the functional
components of a program as a network of processes so that the complete language may be converted to process form.
\cite{GLT91} describes a new translation of the $\lambda$--Calculus into a process notation which has advantages over those proposed by Milner or Leth as it supports a mixture of lazy and eager evaluation strategies
using techniques similar to \cite{Bur84}. While Milner and Leth consider only the pure
$\lambda$--Calculus, it is shown how constant data values and their operations may be included in the
translations.

In this paper we explore the relationship with asynchronous communication models and show that with such
a model,
process networks may be translated very naturally into a generalised graph rewriting
system (GRS). A translation to the practical GRS language Dactl \cite{GKSS88} is presented. 

\section{A Process Notation}
The process notation described in this section has features corresponding to those of ECCS
\cite{EnN86},
the $\pi$--Calculus \cite{MPW89} and LCCS \cite{Leth91}. All may be regarded as extensions to CCS
allowing the communication of link names and hence allow dynamic process networks to be generated.
However, in common with \cite{Hon91} we adopt an asynchronous communication model and restrict ourselves to features corresponding to the subset of the $\pi$--Calculus used in \cite{Mil90}.

We will name the asynchronous language ACPL for Asynchronous-Communication Process Language. It has a synchronous counterpart named SCPL.

\subsection{Syntax of ACPL}
The forms of agent, or process, allowed are equivalent to those of \cite{Hon91} but using the syntax of LCCS. In the syntax below, $P$ and $Q$ are agents, $A$ an agent identifier, $x$ a
link, and $y$ a value or link name:
\begin{description}
  \item [{\makebox [6cm][l] {Asynchronous Output}}]  $x!y$ \\
Send value $y$ on link $x$.
  \item [{\makebox [6cm][l] {Input}}]  $x?y .\,P$ \\
Receive a value on link $x$ and bind the value to $y$ in subsequent behaviour $P$.
  \item [{\makebox [6cm][l] {Restriction}}]  $P \res{x}$ \\
$x$ is the name of a link which may only be used within $P$. For many purposes this may be seen as the
declaration of the link $x$.
  \item [{\makebox [6cm][l] {Parallel Composition}}]  $( P | Q )$ \\
$P$ and $Q$ continue concurrently and may interact via shared links. Binary composition is illustrated
but an arbitrary number of agents may be composed including zero which gives inaction.
  \item [{\makebox [6cm][l] {Agent Definition}}]  $P : A(x_1,\ldots,x_n) = Q$ \\
$A$ is an agent identifier of arity n which may be used in $P$. $x_1,\ldots,x_n$ are distinct names and may be free names in
$Q$. $Q$ may contain agent identifiers, including $A$, and free names from $P$.
  \item [{\makebox [6cm][l] {Defined Agent}}]  $A(y_1,\ldots,y_n)$ \\
A corresponding agent definition of the form $A(x_1,\ldots,x_n) = Q$ must be in scope. The defined
agent behaves like $Q\{y_1/x_1,\ldots,y_n/x_n\}$.
\end{description}
Hence parallel composition and repetition is supported, 
but not summation (choice).
$?$ and $\res{}$ are name binding constructs yielding the obvious
notion of free and bound names.
% We let $fn(P)$ denote the set of free names in $P$.

We will allow communication of tuples of values as atomic events:
\begin{description}
  \item [{\makebox [6cm][l] {Asynchronous Tupled Output}}]  $x!(q,r)$ \\ 
Send pair of values $q$ and $r$ on link $x$.
  \item [{\makebox [6cm][l] {Tupled Input}}]  $x?(q,r) .\,P$ \\
Receive a pair of values on link $x$. Bind the first value to $q$ and the second to $r$ in subsequent
behaviour $P$.
\end{description}
Such a pair of input values may be bound to a single name, as long as the name is only used as an
output
value later.

Note that in this notation output actions are always followed by inaction as in \cite{Hon91}. Hence other techniques are required to make subsequent computation depend on reception of a message by another agent.

\subsection{Syntax of SCPL}
The synchronous notation differs only in the notation for output actions:
\begin{description}
  \item [{\makebox [6cm][l] {Synchronous Output}}]  $x!y .\,P$ \\
Send value $y$ on link $x$ and continue with behaviour $P$.
  \item [{\makebox [6cm][l] {Synchronous Tupled Output}}]  $x!(q,r) .\,P$ \\ 
Send pair of values $q$ and $r$ on link $x$ and continue with behaviour $P$.
\end{description}

The operational semantics of the notations will not not discussed in detail here since \cite{Hon91} and \cite{Mil90} provide a sound basis.

\subsection{Sequentialisation and Tupled Communication}
Under synchronous as well as asynchronous calculi there is a need for care when multiple values are to be be exchanged between agents. In an example from \cite{MPW89} agent $P$ is to communicate the pair of values $(u,v)$ to {\em either} agent $Q$ {\em or} $R$.
We may express communication of a pair of values directly in ACPL by:
\begin{eqnarray*}
( P | Q | R ): & & \\
& & P\,=\,x!(u,v): \\
& & Q\,=\,x?(y,z)\,.\,Q': \\
& & R\,=\,x?(y,z)\,.\,R'
\end{eqnarray*}
Since the pair of values $(u,v)$ is transmitted as an indivisible action, either $Q$ receives the pair, or $R$ does.
This considerably simplifies the code needed by other models as will be seen.

If we are restricted to communicating single values we might think of writing:
\begin{eqnarray*}
( P | Q | R ): & & \\
& & P\,=\,x!u\,.\,x!v: \\
& & Q\,=\,x?y\,.\,x?z\,.\,Q': \\
& & R\,=\,x?y\,.\,x?z\,.\,R'
\end{eqnarray*}
However, it is possible that $u$ might be received by $Q$ and $v$ by $R$, or vice versa.
Note that this is a program in SCPL.

To solve this problem, Milner {\em et al} develop the concept of {\em molecular actions} in which a temporary private channel is used as a capability to ensure that a single agent receives both values:
\begin{eqnarray*}
( P | Q | R ): & & \\
& & P\,=\,(x!t\,|\,t!u\,.\,t!v)\res{t}: \\
& & Q\,=\,x?s\,.\,s?y\,.\,s?z\,.\,Q': \\
& & R\,=\,x?s\,.\,s?y\,.\,s?z\,.\,R'
\end{eqnarray*}
$s$ is not free in $Q'$ or $R'$.

Under an asynchronous communication regime, we cannot use output actions to guard further actions, but sequentialisation is possible. As in \cite{MPW89}, Honda and Tokoro communicate a private channel to the recipient. However, in their solution to the problem, the recipient sends back a series of link names on which the pair of data values $(u,v)$ will be transmitted:
\begin{eqnarray*}
( P | Q | R ): & & \\
& & P\,=\,(\,x!t\,|\,t?a.\,(\,a!u\,|\,t?b.\,b!v\,)\,)\res{t}: \\
& & Q\,=\,x?s.\,(\,s!c\,|\,c?y.\,(\,s!c\,|\,c?z.\,Q'\,)\,)\res{c}:
\end{eqnarray*}
Only $Q$ is shown, $R$ being similar. $s$ and $c$ are not free in $Q'$. Note that sequentialisation is achieved within ACPL and hence without using output actions as guards.

\subsection{Output Guards using Asynchronous Communication}
In all the examples above we have assumed that the process $P$ is inactive after the pair of values has been transmitted, as required by ACPL. The use of molecular actions in the style of \cite{MPW89} required the use of output guards, but the scheme of \cite{Hon91} shows that such guards can be avoided.

However, the synchronous languages do permit output guards so it is of interest to see if ACPL can model the same behaviour. We will consider messages consisting of a single value, $u$, bound to $y$ in the recipients. Using SCPL the example will be:
\begin{eqnarray*}
( P | Q | R ): & & \\
& & P\,=\,x!u\,.\,P': \\
& & Q\,=\,x?y\,.\,Q': 
\end{eqnarray*}

Honda and Tokoro show that it is indeed possible to model this behaviour with an asynchronous language. In essence, their translation adds an extra acknowledgement link name to the values transmitted in a message. The recipient sends a dummy value to this channel when all values in the message have been received. The sender guards its future behaviour with an input guard receiving on the acknowledgement link:
\begin{eqnarray*}
( P | Q | R ): & & \\
& & P\,=\,(\,x!(u,r)\,|\,r?z.\,P'\,)\res{r}: \\
& & Q\,=\,x?(y,k)\,.\,(\,k!d\res{d}\,|\,Q'\,):  
\end{eqnarray*}
$r$ and $z$ are not free in $P'$. $k$ is not free in $Q'$.

ACPL allows transmission of tuples, so the code above is sufficient. \cite{Hon91} communicate simple values, so the translation is a good deal more involved. The code requires the transmission of a pair of values which would be encoded as follows:
\begin{eqnarray*}
( P | Q | R ): & & \\
& & P\,=\,(\,x!t\,|\,t?a.\,(\,a!u\,|\,t?b.\,b!r\,)\,|\,r?z.\,P'\,)\res{r}\res{t}: \\
& & Q\,=\,x?s.\,(\,s!c\,|\,c?y.\,(\,s!c\,|\,c?k.\,(\,k!d\res{d}\,|\,Q'\,)\,)\,)\res{c}:
\end{eqnarray*}

It should be clear that a model supporting communication of tuples allows a much more concise solution of these problems in both synchronous and asynchronous forms. Such a model is also more practical since fewer communications are required. With tupled communication the number of messages exchanged is 1 in the synchronous case and 2 in the asynchronous case. Communicating a pair of simple values takes 3 message exchanges for a molecular action in the synchronous case and 8 in the asynchronous case (not illustrated).

As the number of values to be communicated increases, the savings of the tupled style get larger. Of course, the message size increases using tupled communication, but under typical implementation schemes, messages have to grow quite substantial before the cost of transmitting the data values becomes comparable with setup cost.

\section{Translation of Lazy $\lambda$--Calculus}
As an example we will build on \cite{Mil90} which provides encodings of the $\lambda$--Calculus in the $\pi$--Calculus. Only closed
terms are considered. The
encodings do not reduce the bodies of abstractions. This is not a problem when
considering the
application of these techniques to functional programming where functional normal forms are not usually
of interest.

The encodings simulate particular reduction strategies. We will consider the encoding of the lazy $\lambda$--Calculus \cite{Abr88} which only performs
$\beta$--reduction on the outermost redex on the left-spine, in other words, normal-order reduction
takes place.
The pure $\lambda$--Calculus is not of great practical use. Constants, such as boolean and integer data
values, and operations on them must be added to make a practical functional language.

\subsection{An Extension of Milner's Lazy $\lambda$--Calculus Scheme} 
The translation scheme is parameterised by the name of a link which will provide a
characteristic handle on the process network for the translated expression. In the scheme below, $x$ is a variable, $c$ is an integer constant, $M$ and $N$ are $\lambda$--expressions, and $Inc$ is the operator returning the successor of its argument:
\begin{eqnarray*} 
\sembrac{ x }_u & = & x!u \\ 
\sembrac{ c }_u & = & u?v\,.\,v!c \\ 
\sembrac{ {\lambda}x.\,M }_u & = & u?(x,v)\,.\,\sembrac{M}_v \\
\sembrac{ M\,N }_u & = & (\,\sembrac{M}_v\;|\;(v!(t,u)\;|\;R:\,R\,=\,t?w.\,(\sembrac{N}_w\,|\,
R)) \res{t}\,) \res{v} \\
\sembrac{ Inc(M) }_{u} & = &
(\,\sembrac{M}_{a}\,|\,(a!s\,|\,s?m\,.\,u?v\,.\,v!(m+1)) \res{s}\,)\res{a}
\end{eqnarray*} 
An abstraction expects to receive a pair providing a link for its argument and a link to form the handle on the
result of the 
application. The code for an application sends such values to the function which will receive the pair when
it has become an application. Evaluation of the argument does not proceed until the application
requests
the argument by giving it an argument link $w$ via the $t$ channel. 
The argument, but not the function, may be used several times and hence a recursive defined agent is used.

Constants must be modelled by process networks which behave correctly within the translation
scheme. Abstractions and variables wait to be given the names of links on which to communicate, while
applications evolve until they simulate abstractions.
As a data value may be an argument, it must behave in the same way as an abstraction. Processes representing constants
will expect to be sent the name of a link and will respond with the value along the link.
An $Inc$ operator requests the value of its argument by giving it a result channel $s$ and receiving the value $m$. It then acts exactly like the translation of a constant, awaiting its own result channel on $u$ and returning the value $m+1$ as required.

\subsection{An Example Translation}
We will consider translation of a very simple expression:
\begin{eqnarray*} 
\sembrac{ ({\lambda}x.Inc(x))\,3 }_u & = & (\,f?(x,q).\,(x!a\,|\,(\,a!s\,|\,s?m.\,q?v.\,v!(m+1)\,)\res{s})\res{a} \\
& & |\,f!(t,u) \\
& & |\,R:R=t?w.\,(w?v.\,v!3|R)\,)\res{f}\res{t}
\end{eqnarray*}

A $\lambda$--expression acting as a program is expected to reduce to a constant, rather than an abstraction. To extract the value from a program, $P$, we would produce a network of
the form: 
\begin{eqnarray*}
(\,\sembrac{P}_{u}\,|\,Read(u)\,) \res{u}\,:\,Read(w) & = &
(\,w!c\,|\,c?v\,.\,Print(\,v\,)\,)\,\res{c}\,
\end{eqnarray*}
and $Print$ will display the final result. 

\section{Process Notation and Graph Rewriting} 
Process networks in the asynchronous style described in \cite{Hon91} and in ACPL may be easily translated into generalised graph
rewriting systems. The discussion below uses the practical graph rewriting language Dactl
\cite{GKSS88,GKS91}.
Dactl provides a notation for describing computational objects in terms of directed graphs and for
describing programs in terms of pattern-directed graph transformation rules. Although the syntax is different, the model of graph rewriting is the same as in {\sc Lean} \cite{LEAN}. A restricted form of this rewriting model underlies Term Graph Rewriting \cite{BEGKPS87}.

Dactl may be used as a
vehicle
for comparing implementation techniques and computational strategies since it provides fine control of the rewriting process. Also, since it has a
well-defined operational semantics, it may be used as an intermediate code for language implementation.

Studies using Dactl have shown that implementations of a range of declarative languages may be  made
using graph rewriting as a common computational model \cite{CONPAR}. In addition to translation of
functional programming and term rewriting languages \cite{CTOD}, which are traditionally associated
with
graph rewriting, Dactl has been used successfully to translate full GHC on which is based the kernel
language adopted by the Japanese Fifth Generation Computer Systems project \cite{FGCS88}.

Graph rewriting also shows promise for supporting the integration of different programming styles.
\cite{PanH} reports early work on integration of functional and concurrent logic languages, while the
work reported in \cite{GLT91} and this paper arises from a study of the integration of functional and process-based
programming.

\subsection{The Graph Rewriting Language Dactl}

The nodes of a Dactl graph are labelled with a symbol which indicates that the node plays the role of
an
{\em operator} at the root of a rule application, a {\em data constructor}, or an {\em overwritable}. The role of
operators and constructors will be familiar. The novel feature is the use of
overwritable nodes which may be modified as a side-effect of rule application. This enables Dactl to
express many more computations than the conventional graph rewriting used to
implement functional languages. Overwritables may model von Neumann storage cells, semaphores, and the
logic variable. Overwritable nodes will be used in this paper to model the contents of communication
channels.

Each node has a distinct identifier. From a node leads a sequence of arcs to successor nodes. Arcs
point
from an operator node to its arguments, or from a data constructor to its sub-terms. A Dactl graph may
be represented by listing the definitions of the nodes giving their identifier, symbol, and a sequence
of identifiers for the successor nodes. Repetition of identifiers is used to indicate sharing in a
graph:
{\tt
\begin{verbatim}
a: Append[ c c ],
c: Cons[ o n ],
o: 1,
n: Nil
\end{verbatim}
}
Symbols are integers or identifiers starting in upper-case, while node identifiers start in lower-case.
A node definition may replace one of the occurrences of the node identifier, and redundant identifiers
may be removed allowing the equivalent shorthand form:
{\tt
\begin{verbatim}
a: Append[ c:Cons[ 1 Nil ] c ]
\end{verbatim}
}
Dactl rules contain a {\em pattern} to be matched and a body, or {\em contractum}, to replace the
occurrence of the pattern in the graph, or {\em redex}. Patterns are Dactl graphs but may contain node
identifiers lacking a definition which will match an arbitrary node.

The contractum of a rule contains new graph structure to be built, which may reference nodes matched by
the pattern, and one or more {\em redirections}, which indicate that the source of the redirection
should be overwritten by the target. In classic term rewriting rules there will always be a redirection
overwriting the root of the redex with the root of the contractum. In such rules the pattern and
contractum are separated by the symbol {\tt =>}. This is shorthand for a form with an explicit
overwrite using {\tt ->} as separator.

Computation under the Dactl model proceeds by identifying a subgraph matching the pattern of a
rewriting
rule and replacing it by the contractum of the rule. If more than one rule matches, an arbitrary choice
may be made about which rule to apply; fairness is not assumed. To control the order of evaluation,
attempts to match the rules against the graph only begin at {\em active} nodes. Such nodes are marked
with a $*$ in the representation of a Dactl graph. The pattern of a rule contains no such markings,
since the matching process is insensitive to markings, but the contractum may use markings to nominate
further nodes at which rewriting may take place. If multiple active nodes arise they may be considered
in any order, or even in parallel if there is no conflict between possible rewritings.

Nodes may also be created {\em suspended} waiting for {\em notification} that a successor has been
rewritten to a stable form. This enables a rule to create a dataflow graph in which certain nodes are
active and will produce results which awaken parent nodes once all arguments are available. Suspension
is indicated by one or more {\tt \#} markings. Each notification removes one suspension, the node
becoming active when the last suspension is removed. Notification takes place when an active node is
considered for rewriting, but not rule matches. This is typically because the node in question is a
constructor or overwritable. Arcs which will form notification paths are marked with $\hat{\;}$.
The following examples show some rules with markings and the execution sequence for functional versions
of append, and a version using the logic variable.
{\tt
\begin{verbatim}
RULE
{1}  FunApp[Cons[u x] y] => #Cons[u ^*FunApp[x y]];
{2}  FunApp[Nil y]       => *y;
{3}  FunApp[p1 p2]       => #FunApp[^*p1 p2];
\end{verbatim}
}
The example is a strict function which rewrites to a data constructor node, {\tt Cons}, which is
suspended waiting for completion of a recursive invocation of the function before notifying the parents
of the original node. The final rule applies if the first argument is not yet in the form of
a list. The argument is activated and the {\tt FunApp} application will be reconsidered when the
argument has been rewritten.

Using explicit redirections we could write the first rule as follows:
{\tt
\begin{verbatim}
{1}  r:FunApp[Cons[u x] y] -> c:#Cons[u ^*FunApp[x y]], r:=c;
\end{verbatim}
}

We will illustrate evaluation of a Dactl graph using an example with sharing, indicating the rule
applied at each step, or a hyphen when no rule matches and notification occurs:
{\tt
\begin{verbatim}
       *FunApp[ c:Cons[ o:1 n:Nil ] l ]
=>{1}  #Cons[ o:1 ^s:*FunApp[n c:Cons[o n:Nil]] ]
=>{2}  #Cons[ o:1 ^c:*Cons[o n:Nil] ]
=>{-}  *Cons[ o:1 c:Cons[o n:Nil] ]
=>{-}  Cons[ o:1 c:Cons[o n:Nil] ]
\end{verbatim}
}
The computation terminates when no active nodes remain.

The following rules illustrate a version of append from logic programming. Here the result of the
rewrite indicates success or failure of a predicate and results are communicated by instantiation of
shared variables.
{\tt
\begin{verbatim}
RULE
{1}  LogApp[Cons[u x] y r:Var] => *LogApp[x y w:Var], r:=*Cons[u w];
{2}  LogApp[Nil y r:Var]       => *SUCCEED, r:=*y;
{3}  LogApp[p:Var q r:Var]     => #LogApp[^p q r];
\end{verbatim}
}
The result of the first rule depends on the success of a recursive use of the predicate. The variable
{\tt r} is bound to a {\tt Cons} node whose second argument is a new variable which will be
instantiated
by the recursive call. The {\tt Cons} node is made active in order to notify any computation suspended
waiting for the variable to be instantiated. The final rule illustrates the case when the critical first
argument is not instantiated. The call suspends waiting for some other computation to instantiate the
variable (using one of the first two rules, for example).

We illustrate these rules in action with two calls to {\tt LogApp} which share a variable:
{\tt
\begin{verbatim}
       *LogApp[Nil Cons[1 Nil] v:Var], *LogApp[v Cons[2 Nil] w:Var]
=>{3}  *LogApp[Nil Cons[1 Nil] v:Var], #LogApp[^v Cons[2 Nil] w:Var]
=>{2}  *SUCCEED, v:*Cons[1 Nil], #LogApp[^v Cons[2 Nil] w:Var]
=>{-}  *SUCCEED, *LogApp[v:Cons[1 Nil] Cons[2 Nil] w:Var]
=>{1}  *SUCCEED, w:*Cons[1 x], *LogApp[Nil Cons[2 Nil] x:Var]
=>{2}  *SUCCEED, w:*Cons[1 x], x:*Cons[2 Nil], *SUCCEED
=>...
\end{verbatim}
}
In the first step, the right-hand {\tt LogApp} predicate finds a variable and suspends until it is
instantiated. The second step instantiates the variable as a side-effect. The third step finds no match
on the list value assigned to variable {\tt v}, and reactivates the suspended
{\tt LogApp} predicate.

As a final illustration, we consider the modelling of buffered communication channels. A channel will
consist of an overwritable {\tt Chan} whose argument is a list acting as a stack of available values.
To output to the channel, a rule simply overwrites the channel to contain a list prefixed with the new
value. To input from a channel, a rule must test for available input. If the channel contains the empty
list, the operation is suspended until input is available. Otherwise the channel is rewritten containing
the tail of the original list.

Some example rules in this style are:
{\tt
\begin{verbatim}
RULE
{1}  Put[c:Chan[v] d] -> c:= *Chan[Cons[d v]];
{2}  Get[c:Chan[Cons[d v]]] -> *Use[d], c:=*Chan[v];
{3}  Get[c] -> #Get[^c]; 
\end{verbatim}
}

In the illustration of the rules in action below the first attempt to read from the channel suspends on
finding the empty channel {\tt Chan[Nil]}.
Note the final state with the channel empty again:
{\tt
\begin{verbatim}
       *Get[c],  *Put[c 2],  c:Chan[n:Nil]
=>{3}  #Get[^c], *Put[c 2],  c:Chan[n:Nil]
=>{1}  #Get[^c],  c:*Chan[Cons[2 n:Nil]]
=>{-}  *Get[c],   c:Chan[Cons[2 n:Nil]]
=>{2}  *Use[2],   c:Chan[n:Nil]
=>...
\end{verbatim}
}

\subsection{Translating an ACPL Network to Standard Form}

Before describing the translation of a ACPL process network to a GRS, it will be shown that any network may
be expressed in a standard form
which makes heavy use of defined agents. 
If $A$ stands for an agent identifier then we will define a sub-language of ACPL in which the only forms allowed
are: 
\[
\begin{array}{l}
P::= x!y \skil x?y.A \skil (A\,|\cdots|\,A) \skil A  \skil P \res{x} \skil P: A = P 
\end{array}
\]
Furthermore, we only permit the agent definitions to be at the outermost level (no agent definitions
within agent definitions), and they may contain no free
variables. Any ACPL expression can be converted to this form as will be shown below. Equivalent
forms of the translation of the example ${\lambda}x.Inc(x))\,3$ are shown for illustration: 

The original program is:
\begin{eqnarray*} 
& & (\,(\,f?(x,q).\,(x!a\,|\,a!s\,|\,s?m.\,q?v.\,v!(m+1)\,)\res{s}\res{a} \\
& & \;\;|\,f!(t,u) \\
& & \;\;|\,R:\,R=\,t?w.\,(w?v.\,v!3\,|\,R) \\
& & \;\;)\res{f}\res{t}\\
& & |\,Read(u) \\
& & )\res{u}: \\
& & Read(w)=\,(\,w!c\,|\,c?v.\,Print(v)\,)\res{c}
\end{eqnarray*}

Adding additional agent definitions to satisfy the reduced syntax, and also using an agent definition $Put$ for all output operations:
\begin{eqnarray*} 
P: P= & & \\
& & (\,Q:\,Q= \\
& & \;\;(\,A:\,A=\,f?(x,q).\,B:\,B=\,(Put(x,a)\,|\,Put(a,s)\,|\,C: \\
& & \;\;\;\;\;\;C=\,s?m.\,D:\,D=\,q?v.\,Put(v,(m+1)))\res{s}\res{a} \\
& & \;\;|\,Put(f,(t,u)) \\
& & \;\;|\,R:\,R=\,t?w.\,E:\,E=\,(F:\,F=\,w?v.\,Put(v,3)\,|\,R) \\
& & \;\;)\res{f}\res{t}\\
& & |\,Read(u) \\
& & )\res{u}: \\
& & Read(w)=\,(\,Put(w,c)\,|\,G:\,G=\,c?v.\,Print(v)\,)\res{c}: \\
& & Put(x,v)=\,x!v
\end{eqnarray*}


Adding parameters to avoid free variables: 
\begin{eqnarray*} 
P: P= & & \\
& & (\,Q(u):\,Q(u)= \\
& & \;\;(\,A(f):\,A(f)=\,f?(x,q).\,B(x,q):\,B(x,q)=\,(Put(x,a)\,|\,Put(a,s)\,|\,C(s,q): \\
& & \;\;\;\;\;\;C(s,q)=\,s?m.\,D(q,m):\,D(q,m)=\,q?v.\,Put(v,(m+1)))\res{s}\res{a} \\
& & \;\;|\,Put(f,(t,u)) \\
& & \;\;|\,R(t):\,R(t)=\,t?w.\,E(w,t):\,E(w,t)=\,(F(w):\,F(w)=\,w?v.\,Put(v,3)\,|\,R(t)) \\
& & \;\;)\res{f}\res{t}\\
& & |\,Read(u) \\
& & )\res{u}: \\
& & Read(w)=\,(\,Put(w,c)\,|\,G(c):\,G(c)=\,c?v.\,Print(v)\,)\res{c}: \\
& & Put(x,v):\,Put(x,v)=\,x!v
\end{eqnarray*}

All definitions can now be pulled to the top level: 
\begin{eqnarray*} 
P:& & P\,=\;(\,Q(u)\,|\,Read(u)\,)\res{u}: \\
& & Q(u)\,=\;(\,A(f)\,|\,Put(f,(t,u))\,|\,R(t)\,)\res{f}\res{t}: \\
& & A(f)\,=\;f?(x,q).\,B(x,q): \\
& & B(x,q)\,=\;(\,Put(x,a)\,|\,Put(a,s)\,|\,C(s,q)\,)\res{s}\res{a}: \\
& & C(s,q)\,=\;s?m.\,D(q,m): \\
& & D(q,m)\,=\;q?v.\,Put(v,(m+1)): \\
& & R(t)\,=\;t?w.\,E(w,t): \\
& & E(w,t)\,=\;(\,F(w)\,|\,R(t)\,): \\
& & F(w)\,=\;w?v.\,Put(v,3): \\
& & Read(w)\,=\;(\,Put(w,c)\,|\,G(c)\,)\res{c}: \\
& & G(c)\,=\;c?v.\,Print(v) : \\
& & Put(x,v)\,=\;x!v
\end{eqnarray*}

\subsection{Translating a Standard Form ACPL Network to a Graph Rewriting System}

It will be seen that ACPL programs in standard form have a very simple format. It is possible to convert agent definitions in this form directly to Dactl rules.
We will give the translated Dactl code and then describe the translation:
{\tt
\begin{verbatim}
RULE
  INITIAL -> *Q[u], *Read[u], u: NewChan;
  Q[u] -> *A[f], *Put[f Pair[t u]], *R[t], f: NewChan, t: NewChan;
  A[f:Chan[Cons[Pair[x q] r]]] -> *B[x q], f:=*Chan[r];
  A[f:Chan[Nil]] -> #A[^f];
  B[x q] -> *Put[x a], *Put[a s], *C[s q], s: NewChan, a: NewChan;
  C[s:Chan[Cons[m r]] q] -> *D[q m], s:=*Chan[r];
  C[s:Chan[Nil] q] -> #C[^s q];
  D[q:Chan[Cons[v r]] m] -> #Put[v ^*IAdd[m 1]], q:=*Chan[r];
  D[q:Chan[Nil] m] -> #D[^q m];
  R[t:Chan[Cons[w r]]] -> *E[w t], t:=*Chan[r];
  R[t:Chan[Nil]] -> #R[^t];
  E[w t] -> *F[w], *R[t];
  F[w:Chan[Cons[v r]]] -> *Put[v 3], w:=*Chan[r];
  F[w:Chan[Nil]] -> #F[^w];
  Read[w] -> *Put[w c], *G[c], c: NewChan;
  G[c:Chan[Cons[v r]]] -> *Print[v], c:=*Chan[r];
  G[c:Chan[Nil]] -> #G[^c];
\end{verbatim}
}
All Dactl programs start with a graph containing a single node with the symbol {\tt INITIAL}, which replaces $P$ above.
Processes generally correspond to GRS terms. The {\tt *} marks an active process or rewritable term.
Parallel composition, used by $Q$, $B$, $E$, and $Read$ is very straightforward and appears as little more than a change of syntax. Restriction, used in $Q$, $B$, and $Read$
corresponds
to declaration of new links denoted by the term {\tt NewChan}. Links are represented by the overwritable symbol {\tt Chan} which contains a stack of messages which have been sent on the link. {\tt IAdd} is the primitive function for adding integers.

All output actions use the primitive {\tt Put} introduced earlier. To output a pair, the {\tt Pair} constructor is used, as in {\tt Q}. Processes guarded by input actions become two rules: the first matches a non-empty channel, binds the value received, and rewrites the channel having extracted the value; the second applies if the channel is empty and blocks until input {\em is} available. When a pair is input, (for example in {\tt A}), the pattern matches a pair of values for use in the body of the action.

A new channel is defined as the following pattern: 
{\tt
\begin{verbatim}
PATTERN
  NewChan = Chan[Nil]; 
\end{verbatim}
}

The processes {\tt Put} and {\tt Print} are defined as follows: 
{\tt
\begin{verbatim}
RULE
  Put[c:Chan[v] d] -> c := *Chan[Cons[d v]];
  Print[v] -> *PrintF["Result: %d" v];
\end{verbatim}
}
{\tt Put} just inserts the new message at the head of the stack of messages held by the link.

The overall style of execution contrasts strongly with the more conventional
Term Graph Rewriting \cite{BEGKPS87} approach. Instead of representing an
expression as a single rooted term, this
style represents sub-expressions as independent unrooted terms linked by shared
references to nodes representing channels. Execution corresponds more to the actions of the Chemical Abstract Machine
\cite{BeBo90} than a traditional graph reduction machine.

A translator has been written in ML which takes $\lambda$--expressions and converts them to an internal form of ACPL. The process network is converted to standard form, as described above, and is mapped to Dactl. The Dactl code may be executed using an interpreter or compiler developed at UEA. The example above is as produced by the translator, with machine-generated identifiers replaced by more readable ones.

The mapping from $\lambda$--expressions to ACPL used here is based on extensions to the Lazy scheme in \cite{Mil90}. The translator also implements a new scheme reported in \cite{GLT91}.

\subsection{Translating a SCPL Network to a Graph Rewriting System}
It has been shown that communication in the synchronous language can be modelled in the asynchronous language by sending an acknowledgement channel. Using the earlier example we can provide a translation to Dactl.

The SCPL network:
\begin{eqnarray*}
& & S(v)\,=\;(\,P(v,x)\,|\,Q(x)\,)\res{x}: \\
& & P(u,x)\,=\,x!u.\,P': \\
& & Q(x)\,=\,x?y\,.\,Q'(y)
\end{eqnarray*}
can be modelled by the ACPL network:
\begin{eqnarray*}
& & S(v)\,=\;(\,P(v,x)\,|\,Q(x)\,)\res{x}: \\
& & P(u,x)\,=\,(\,x!(u,k)\,|\,k?z.\,P'\,)\res{k}: \\
& & Q(x)\,=\,x?(y,k)\,.\,(\,k!z\res{z}\,|\,Q'(y)\,)
\end{eqnarray*}

Translating the ACPL program yields Dactl rules such as:
{\tt
\begin{verbatim}
RULE
  S[v] -> *P[v x], *Q[x], x:NewChan;
  P[u x] -> *Put[x Pair[u k]], *A[k], k:NewChan;
  A[k:Chan[Cons[z r]]] -> *P', k:=*Chan[r];
  A[k:Chan[Nil]] -> #A[^k];
  Q[x:Chan[Cons[Pair[y k] r]]] ->
          *Q'[y], x:=*Chan[r], *Put[k z], z:NewChan;
  Q[x:Chan[Nil]] -> #Q[^x];
\end{verbatim}
}

Hence the communication mechanism can be used in the normal way. However, optimisations can be made if it is known that a link is being used purely for synchronisation:
\begin{itemize}
  \item No special value $z$ needs to be communicated on the synchronisation channel $k$
  \item The synchronisation channel will be used only once so need not be rewritten once used 
  \item A simpler overwritable structure will suffice in place of a complete link
\end{itemize}

The Dactl code can be simplified to the form below.
The synchronisation value takes the initial value {\tt Wait} when created by $P$ and is overwritten by {\tt Free} when the message is received by $Q$:
{\tt
\begin{verbatim}
RULE
  S[v] -> *P[v x], *Q[x], x:NewChan;
  P[u x] -> *Put[x Pair[u k]], *A[k], k:Wait;
  A[k:Free] -> *P';
  A[k:Wait] -> #A[^k];
  Q[x:Chan[Cons[Pair[y k:Wait] r]]] ->
          *Q'[y], x:=*Chan[r], k:=*Free;
  Q[x:Chan[Nil]] -> #Q[^x];
\end{verbatim}
}

Further, should it be desired, a mixture of synchronous (acknowledged) and asynchronous (unacknowledged) communications can be used. In this case the Dactl code receiving a message would distinguish between classes of values in the message queue. The final example below involves a process $P$ which uses synchronous communication and $R$ which waits for no acknowledgement. Instead of using the constructor {\tt Cons} to build the message stack, we use either {\tt ACons} for asynchronous messages or {\tt SCons} for synchronous messages. For this example specialised rules are used for output.
\begin{eqnarray*}
& & S\,=\;(\,P(x)\,|\,Q(x)\,|\,R(x)\,)\res{x}: \\
& & P(x)\,=\,x!2.\,Print(3): \\
& & Q(x)\,=\,x?y.\,(\,Q(x)\,|\,Print(y)\,): \\
& & R(x)\,=\,(\,x!4\,|\,Print(5)\,)
\end{eqnarray*}

{\tt
\begin{verbatim}
RULE
  S -> *P[x], *Q[x], *R[x], x:NewChan;
  P[x:Chan[s]] -> x:=*Chan[SCons[2 s k:Wait]], *A[k];
  A[k:Free] -> *Print[3];
  A[k:Wait] -> #A[^k];
  R[x:Chan[s]] -> x:=*Chan[ACons[4 s]], *Print[ 5];
  Q[x:Chan[SCons[y r k:Wait]]] ->
          *Q[x], x:=*Chan[r], k:=*Free, *Print[y];
  Q[x:Chan[ACons[y r]]] -> *Q[x], x:=*Chan[r], *Print[y];
  Q[x:Chan[Nil]] -> #Q[^x];
\end{verbatim}
}

\section{Conclusions} 
This paper has explored some practical extensions to the theory of process calculi with asynchronous communication in the style of \cite{Hon91}. 

Although the process language is rich enough to support all the facilities used in \cite{Mil90}, the language 
lacks the choice (sum) operators and hence avoids the need to retract communication
offers. It also adopts a different approach to the repetition construct proposed there.
\cite{Hon91} show how the repetition construct might be expressed in ACPL, but the Dactl translation would compute indefinitely, generating increasing numbers of copies of the
repeated process through internal actions. Instead, we use recursively defined agents as in earlier models and rely on such processes having dependencies on external actions to prevent an explosion of the process network.

We have not explored data-dependent matching constructs at this stage. \cite{Hon91} provide a theoretically elegant approach to selections, but we feel that a more direct approach will be required for our rather practical purposes. The match construct of the $\pi$--calculus may be suitable.

It has been shown that the language ACPL based on asynchronous communication principles may be mapped to a graph rewriting notation. This opens up the
question of whether graph rewriting might lead to a suitable low-level
implementation route for such process notations, and for programming languages
integrating functional and process styles. It is also shown that the requirements of synchronous communication may be satisfied with comparatively little overhead.

\subsection*{Acknowledgements}
The author would like to thank Alessandro Giacalone, Lone Leth, and Bent Thomsen of ECRC, Munich, and members of the Dactl project at UEA for many useful discussions and much support,
and to acknowledge the financial support of the ESPRIT programme through the Semagraph BRA.

\begin{thebibliography}{BEGKPS87}

\bibitem[{Abr88}]{Abr88}
S. Abramsky:
{\em The Lazy Lambda Calculus}.
Chapter 4 in D. Turner (ed.),
{\em Research Topics in Functional Programming}, 
pp. 65-116, Addison Wesley. (1988)

\bibitem[{BEGKPS87}]{BEGKPS87}
H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W. Glauert, J.R.
Kennaway, M.J. Plasmeijer, \& M.R. Sleep:
{\em Term Graph Rewriting}.
Proc. PARLE 87, Springer LNCS 259, p141-158. (1987) 

\bibitem[{BEGKPS89}]{LEAN}
H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W. Glauert, J.R.
Kennaway, M.J. Plasmeijer, \& M.R. Sleep:
{\em Lean: An Intermediate Language Based on Graph Rewriting}.
Parallel Computing, Vol 9, p163-177. (1989)

\bibitem[{BeBo90}]{BeBo90}
G. Berry \& G. Boudol:
{\em The  Chemical Abstract Machine}.
Proc. POPL 90, p 81-94. (1990) 

\bibitem[{BMT91}]{BMT91}
D. Berry, R. Milner, \& D.N. Turner:
{\em A semantics for ML concurrency primitives}.
Laboratory for Foundations of Computer Science,
Edinburgh University. (1991)

\bibitem[{Bur84}]{Bur84}
F.W. Burton: 
{\em Annotations to Control Parallelism and Reduction Order in
the Distributed Evaluation of Functional Programs}.
TOPLAS, Vol 6, No 4, p159-174. (1984) 

\bibitem[{EnN86}]{EnN86}
U. Engberg \& M. Nielsen: 
{\em A Calculus of Communicating Systems with Label Passing}.
Report DAIMI PB-205, Computer Science Department, University of Aarhus. (1984) 

\bibitem[{GPM89}]{GPM89}
A. Giacalone, P. Mishra, \& S. Prasad:
{\em Facile: A Symmetric Integration of Concurrent and
Functional Programming}.
IJPP, Vol 18, No 2, p121-160. (1989) 

\bibitem[{GKSS88}]{GKSS88}
J.R.W. Glauert, J.R. Kennaway, M.R. Sleep, \& G.W. Somner:
{\em Final specification of Dactl}.
Internal Report SYS-C88-11, University of East Anglia. (1988) 

\bibitem[{GKS91}]{GKS91}
J.R.W. Glauert, J.R. Kennaway, \& M.R. Sleep:
{\em Dactl: An Experimental Graph Rewriting Language}
Proc. 4th International Workshop on Graph Grammars, Bremen, 1990.
Springer LNCS 532. (1991)

\bibitem[{GHKP88}]{CONPAR}
J.R.W. Glauert, K. Hammond, J.R. Kennaway \& G.A. Papadopoulos:
{\em  Using Dactl to Implement Declarative Languages}.
CONPARÕ88, Manchester, UK, Sept. 12-16, Vol. 1, pp. 89-94. (1988)

\bibitem[{GlaPap88}]{FGCS88}
J.R.W. Glauert \& G.A. Papadopoulos:
{\em A Parallel Implementation of GHC}.
Proceedings International Conference on Fifth Generation Computer Systems. ICOT, Tokyo, December 1988.
(1988)

\bibitem[{GlaPap91}]{PanH}
J.R.W. Glauert \& G.A. Papadopoulos:
{\em Unifying Concurrent Logic and Functional Languages in a Graph Rewriting Framework}.
Proceedings, 3rd Panhellenic Computer Science Conference, Athens, May 1991. (1991)

\bibitem[{GLT91}]{GLT91}
J.R.W. Glauert, L. Leth \& B. Thomsen:
{\em A New Translation of Functions as Processes}.
SemaGraph '91 Symposium, December 1991. (1991)

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

\bibitem[{KeSl82}]{KeSl82}
J.R. Kennaway \& M.R. Sleep:
{\em Expressions as Processes}.
Proc. Lisp and FP, August 1982, p.21-28. (1982) 

\bibitem[{Ken90}]{CTOD}
J.R. Kennaway:
{\em Implementing Term Rewrite Languages in Dactl}.
Theor. Comp. Sci. 72, p.225-250. (1990)

\bibitem[{Leth91}]{Leth91}
L. Leth:
{\em Functional Programs as Reconfigurable Networks of
Communicating Processes}.
Ph.D Thesis, Imperial College, London University. (1991) 

\bibitem[{Mil80}]{Mil80}
R. Milner:
{\em Calculus of Communicating Systems}.
Springer LNCS 92. (1980)

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

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

\bibitem[{Tho89}]{Tho89}
B. Thomsen:
{\em A Calculus of Higher Order Communicating Systems}.
Proceedings of POPL 89, pp. 143-154,
The Association for Computing Machinery. (1989)

\bibitem[{Tho90}]{Tho90}
B. Thomsen:
{\em Calculi for Higher Order Communicating Systems}.
Ph.D. Thesis, Imperial College, London University. (1990)

\end{thebibliography} 
 
\end{document} 
}
