%Lone and Bent,
%
%Thank you for the latex examples.
%
%Here is my attempt at converting my document to latex. I had some
%problems because the latex system on our Suns is not too good, but a version
%on Macs worked. It took me much longer than expected.
%
%Could you send something back as soon as possible? Ideally by early afternoon
%tomorrow! I realise it is a lot to ask. Feel free to edit other parts of the
%paper.
%
%John
%
%Dear John,
%
%Here is a new version of our paper. We have corrected a few typos
%and we have added the operational semantics stuff and some stuff 
%about the correctness of the translations of lazy and call-by-value 
%evaluation.
%We hope that you will write an abstract, then
%we think that the paper is ready for submission so if you have
%no further changes then go ahead.
%Please send us a Latex copy of the final version.
%Now we will go back to the ESPRIT proposal writing!! Big sigh.
%
%Regrads,
%
%Lone and Bent.
%
\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 A New Translation of Functions as Processes}}
\author{
        {\it J. Glauert}\\
	School of Information Systems\\
	University of East Anglia\\
	Norwich NR4 7TJ, UK\\
        \and
        {\it L. Leth and B. Thomsen}\\
        European Computer-Industry Research Centre\\
        Arabellastrasse 17\\
        D-8000 Munich 81, Germany}
%\date{DRAFT}
%\date{To appear in Proc. of CHALMERS WORKSHOP ON CONCURRENCY,
%Baastad, Sweden, May 27 - 31, 1991}


%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}
Abstract to be written.
\end{abstract}
\section{Introduction}
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 \cite{Tho89,Tho90}. Milner \cite{Mil89},
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. This 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.

Such work is of particular interest when considering implementation of languages  which aim to integrate
functional and process styles, such as Facile \cite{GPM89}. By encoding the functional
components of a program as a network of processes, the complete language may be converted to processes
for semantic purposes at least.

This paper describes a new translation of the $\lambda$--Calculus into a process notation which is more
efficient than those proposed by Milner or Leth in terms of the number of communication events occurring
during reduction of a $\lambda$--expression.
%%%% substantiate

Both lazy and eager evaluation strategies are supported, and a mixture of strategies may be employed
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.

Programs in the process language may be translated very naturally into a generalised graph rewriting
system (GRS). A translation to the practical GRS language Dactl \cite{GKSS88} is presented. 
The style of execution of
such a GRS is rather different from the traditional term-based translation of a functional language.

\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.
\subsection{Syntax}
The forms of agent, or process, allowed are a subset of those of LCCS with the addition of defined
agents from the $\pi$--Calculus. 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 [4cm][l] {Output}}]  $x!y . P$ \\
Send value $y$ on link $x$ and continue with behaviour $P$.
  \item [{\makebox [4cm][l] {Input}}]  $x?y . P$ \\
Receive a value on link $x$ and bind the value to $y$ in subsequent behaviour $P$.
  \item [{\makebox [4cm][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 [4cm][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 [4cm][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$ may be free names in
$Q$. $Q$ may contain agent identifiers, including $A$, and free names from $P$.
  \item [{\makebox [4cm][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).

The form $\;{\bf rec}\,X\,.\,P\;$
is allowed as syntactic sugar for: $\;X\,:\,X\,=\,P\;$.
$?$ 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 [4cm][l] {Tupled Output}}]  $x!(q,r) . P$ \\ 
Send pair of values $q$ and $r$ on link $x$ and continue with behaviour $P$.
  \item [{\makebox [4cm][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.

\subsection{Operational Semantics}
The operational semantics of the process notation is given in terms of
a labelled transition system. There are four kinds of actions, ranged
over by $\alpha$: input actions $x?y$, output actions $x!z$, output
of restricted name $x\res{y}$ and internal actions $\tau$. We let
$c(\alpha)$ denote the communication channel of an action, e.g. 
$x$ above. $?$ and $\res{}$ are name binders and $bn(\alpha)$ denotes
the bound name of an action, e.g. $y$ above.

The transition relation is defined as the smallest relation satisfying
the axiom and rules in Figure \ref{opsem}.

\begin{figure}
\rule{\textwidth}{.5pt}\\
\begin{tabular}{rl}
  & \\
\mbox{Output} &
$\trans{x!y.P}{x!y}{P}$ \\
  & \\
\mbox{Input} &
$\trans{x?y.P}{x?z}{P\{z/y\}}$ \\
 & \\
\mbox{Res}  &
$\infer{\trans{P}{\alpha}{P'}}
      {\trans{P\res{x}}{\alpha}{P'\res{x}}}
      {,x \neq c(\alpha)}$  \\
 & \\
\mbox{Open}  &
$\infer{\trans{P}{y!x}{P'}}
      {\trans{P\res{x}}{y\res{z}}{P'\{z/x\}}}
      {,z \not\in fn(P\res{x})}$  \\
 & \\
\mbox{Par}  &
$\infer{\trans{P}{\alpha}{P'}}
      {\trans{P\mid Q}{\alpha}{P'\mid Q}}
      {,bn(\alpha)\cup fn(Q) = \emptyset}$  \\
 & \\
\mbox{Com}  &
$\infer{\trans{P}{x?y}{P'}\;\;\trans{Q}{x!y}{Q'}}
      {\trans{P\mid Q}{\tau}{P'\mid Q'}}
      {}$  \\
 & \\
\mbox{Close}  &
$\infer{\trans{P}{x?y}{P'}\;\;\trans{Q}{x\res{y}}{Q'}}
      {\trans{P\mid Q}{\tau}{(P'\mid Q')\res{y}}}
      {}$  \\
 & \\
\mbox{Agents}  &
$\infer{\trans{P\{y_1/x_1,\ldots,y_n/x_n\}}{\alpha}{P'}}
      {\trans{A(y_1,\ldots,y_n)}{\alpha}{P'}}
      {,A(x_1,\ldots,x_n)=P}$  \\
 & \\
\end{tabular}
\mbox{}\\
\rule{\textwidth}{.5pt}
\caption{Operational semantics for Process Notation \label{opsem}}
\end{figure}

The transition relation is itself too shallow a relation to use as an
equivalence between agents. We shall instead use the notion of 
observational equivalence $\approx$ as defined in \cite{Mil89a}.

\section{Translation of Lazy and Call-By-Value $\lambda$--Calculus}
Milner \cite{Mil89} provides encodings of the $\lambda$--Calculus in the $\pi$--Calculus. Only closed
terms are considered. The encodings simulate particular reduction strategies. The
encodings considered here 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.

In particular, the encoding of the lazy $\lambda$--Calculus \cite{Abr88} only performs
$\beta$--reduction on the outermost redex on the left-spine, in other words, normal-order reduction
takes place. In the call-by-value $\lambda$--Calculus $\beta$--reduction of an application is only
performed when the argument as well as the function is an abstraction. Since any such application may be
reduced, multiple reduction sequences may exist for a given term.

Below we will cast Milner's translations into the notation given above.

\subsection{Milner's Lazy  $\lambda$--Calculus Scheme} 
The translation schemes given are parameterised by the name of a link which will provide a
characteristic handle on the process network for the translated expression. 
\begin{eqnarray*} 
\sembrac{ x }_u & = & x!u\,.\,() \\ 
\sembrac{ {\lambda}x.M }_u & = & u?x\,.\,u?v\,.\,\sembrac{M}_v \\
\sembrac{ M N }_u & = & (\,\sembrac{M}_v\;|\;(v!x\,.\,v!u\,.\,{\bf rec}\,X.\,x?w.\,(\sembrac{N}_w\,|\,
X)) \res{x}\,) \res{v} 
\end{eqnarray*} 
An abstraction expects to receive a link for its argument and then 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 them 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 $x$ channel. 
The argument, but not the function, may be used several times.

\subsection{Milner's Call-By-Value $\lambda$--Calculus Scheme} 
\begin{eqnarray*} 
\sembrac{ x }_u & = & u!x\,.\,() \\
\sembrac{ {\lambda}x.M }_u & = & (\,u!y\,.\,{\bf rec}
X.\,y?w\,.\,(w?x\,.\,w?q\,.\,\sembrac{M}_q\,|\,X)\,)
\res{y} \\
\sembrac{ M N }_u & = & (\,\sembrac{M}_f\;|\;f?y\,.\,(\,y!v\,.\,a?z\,.\,v!z\,.\,v!u\,.()\,)\,
\res{v}\;|\;\sembrac{N}_a\,) \res{f} \res{a}
\end{eqnarray*}

Note that in the translation of an application, both function and argument may be evaluated concurrently
and their execution is coordinated by some apply ``glue'' code which links them together.

It is hard to gain an intuition for the operation of the scheme. An application announces the name of a
link on which the apply glue returns the name of a temporary link used to send it argument and result
links. The argument link name is retrieved from the argument and the result link is the handle on the
application itself. Since only an abstraction will publish a link name, the apply glue cannot complete
its task until both function and argument are abstractions.

\subsection{Comparison of the Schemes} 
If a given $\lambda$--expression is translated by the two schemes, there will not be much relationship
between the resulting process networks. Evaluation of the process networks will be very different in the
two cases. In particular, note that in the lazy scheme an abstraction waits for input, while in the
call-by-value scheme it starts by generating output. 

Here is the translation of ${\lambda}x.x$ under both schemes:
\begin{eqnarray*} 
\mbox{Lazy Scheme:} & & \\
& & \sembrac{ {\lambda}x.x }\;=\;u?x\,.\,u?v\,.\,x!v\,.\,() \\
\mbox{Call-by-value Scheme:} & & \\
& & \sembrac{ {\lambda}x.x }\;=\;(u!y\,.\,{\bf rec}\,X.\,y?w\,.\,(w?x\,.\,w?q\,.\,q!x\,.\,()\,|\,X))
\res{y}
\end{eqnarray*}

\section{A New Translation Scheme} 
Under both schemes above, evaluation of the process network for even a simple $\lambda$--expression
involves a good deal of communication. Also, there is no similarity between lazy and call-by-value
translations. 

Lazy evaluation has the benefit of using a normalising strategy but is fundamentally sequential, since
only one redex may be reduced at a time. Efficient implementations of lazy functional languages, such as
Clean and Haskell, rely on strictness analysis to identify portions of a program which can be evaluated
by value. 

Strict functional languages, such as ML, tend to be associated with more efficient implementations, but
any implementation must be lazy in its approach to conditional computations, for example. 

Any serious implementation must, therefore, combine lazy and call-by-value evaluation. 

A new scheme is introduced for translating $\lambda$--expressions to process networks. By changing the
translation of applications it provides both lazy and call-by-value behaviour. Since a single framework
is used, it is possible for different applications in a single $\lambda$--expression to be encoded as
lazy or eager in the manner of \cite{Bur84}.
 
\subsection{The New Translation Scheme} 
In the translations below, the binary application operator combining $\lambda$-terms is made explicit
and a 
subscript {\sc l} or {\sc v} is added to indicate lazy or call-by-value evaluation respectively:
\begin{eqnarray*}
\sembrac{ x }_u & = & {\bf rec} X.\,u?(p,q)\,.\,(\,x!(p,q).()\,|\,X\,) \\
\sembrac{ {\lambda}x.M }_u & = & {\bf rec} X.\,u?(x,q)\,.\,(\,\sembrac{M}_q\,|\,X\,) \\
\sembrac{ @_V M N }_u & = & (\,\sembrac{M}_f\,|\,f!(a,u).()\,|\,\sembrac{N}_a\,)\,\res{f}\,\res{a} \\
\sembrac{ @_L M N }_u & = & (\,\sembrac{M}_f\,|\,f!(t,u).()\,|\,{\bf
rec}\,X\,.\,t?(p,q)\,.\,(\,a!(p,q).()\,|\,\sembrac{N}_a\,|\,X\,)\,\res{a}\,)\,\res{f}\,\res{t}
\end{eqnarray*}

The following equivalent translations of a bound variable and of $@_L M N$, which do not use explicit
tupled communication, will prove useful later:
\begin{eqnarray*}
\sembrac{ x }_{u} & = & {\bf rec} X.\,u?v\,.\,(\,x!v.()\,|\,X\,) \\
\sembrac{ @_{L} M N }_{u} & = & (\,\sembrac{M}_{f}\;|\;f!(t,u).()\;|\;{\bf
rec}\,X\,.\,t?v\,.\,(a!v.()\,|\,\sembrac{N}_{a}\,|\,X)\,\res{a}\,)\,\res{f}\,\res{t}
\end{eqnarray*}

A lazy translation is provided if every application is treated as $@_{L}$, and a call-by-value
translation results if every application is treated as $@_{V}$.

\subsection{Properties of the New Scheme}

Considering the call-by-value scheme first, it will be seen that abstractions wait for input which is a
pair of values giving argument link and result link. Applications outside abstraction bodies will
evaluate both function and argument concurrently.
 
By contrast, the lazy scheme only causes evaluation of the left spine. Arguments block awaiting the pair
of values indicating that the abstraction concerned is to be applied to an argument. The argument will
be evaluated only if such values arrive; when the argument becomes an abstraction it will receive the
values on link $a$ and will simulate an application of the function.

It will be seen that the apply glue for $@_{L}$ has the effect of providing a buffer process to
the translation of the argument with input link $t$ and output link $a$. Evaluation of the argument is
delayed until the buffer receives a message. This is similar to Milner's lazy scheme. 

Various features of the translation are worth highlighting.
Firstly, there are simplifications gained by communicating pairs of values. Extra temporary links would
be needed if only single values could be communicated. Consider the code for a variable:
\begin{eqnarray*}
{\bf rec} X.\,u?(p,q)\,.\,(\,x!(p,q).()\,|\,X\,)
\end{eqnarray*}
If this were written as: 
\begin{eqnarray*}
{\bf rec} X.\,u?p\,.\,u?q\,.\,(\,x!p\,.\,x!q\,.()\,|\,X\,)
\end{eqnarray*}

it would be possible to interleave messages from two separate agents able to output on link $u$. To
avoid this problem, such agents may first send a link name and then send the two values on that link, as
in Milner's call-by-value scheme:
\begin{eqnarray*}
{\bf rec} X.\,u?t\,.\,(\,t?p\,.\,t?q\,.\,(x!w\,.\,w!p\,.\,w!q\,.())\,\res{w}\,|\,X\,) 
\end{eqnarray*}

Secondly, all output actions in a translated $\lambda$--expressions are 
followed by inaction. As a consequence no processes are dependent on synchronised communication, and an
asynchronous communication model such as \cite{Hon91}
would suffice. This can significantly reduce the complexity of a low-level implementation of such a
process notation as will be shown later. 

Finally, it will be seen that a number of uses of the ${\bf rec}$ construct appear. These are needed to
allow for multiple occurrences of the bound variable in the body of abstractions. When such abstractions
are applied, the argument may be evaluated more than once with different arguments. These uses of ${\bf
rec}$ are not always required. Indeed none would be required for the linear $\lambda$--Calculus. Further
work is required to identify cases where recursion is not required, hence avoiding generation of
redundant processes. It is also clear that links used in non-recursive cases can be garbage collected
after use.

The mixed calculus may be given an operational semantics in terms
of an applicative transition system \cite{Abr88} in the following way:

The relation $M{\Downarrow} N$\index{$M{\Downarrow} N$}
is defined inductively as:

\begin{center}

\begin{tabular}{lcccl}
$\lambda x.M{\Downarrow}\lambda x.M$ & &
$\infer{M{\Downarrow}\lambda x.P\;\; P[x:=N]{\Downarrow} Q}
       {@_L M N{\Downarrow} Q}
       { }$
& &
$\infer{M{\Downarrow}\lambda x.P\;\; N{\Downarrow} Q\;\;
        P[x:=Q]{\Downarrow} L}
       {@_V M N{\Downarrow} L}
       { }$
\end{tabular}
\end{center}

The sublanguage where every application is treated as $@_L$ degenerates
to the Lazy $\lambda$-Calculus, and the sublanguage where every application
is treated as $@_V$ degenerates to the call-by-value $\lambda$-Calculus studied
in \cite{Ong88,Mil89}. As an abstracting equivalence on $\lambda$-terms
we use the notion of applicative bisimulation $\simeq$ as defined in
\cite{Abr88}. For the two sublanguages mentioned above we have the
following desired property:

\begin{theorem}
$\sembrac{M} \approx \sembrac{N} \; \Rightarrow \; M \simeq N$
\end{theorem}

\proof \\
The proof that the new lazy and eager translations behave as desired 
follow the techniques developed by Milner in \cite{Mil89}. The proofs
will appear in a full version of this paper.
\qed

We conjecture that the above theorem also holds for the full language,
but further work 
will be needed to establish the validity of mixed translations. 

\section{Extension to Constants} 
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. 

These 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. Processes representing constants
will expect to be sent the name of a link and will respond with the value along the link. The
translation of variables uses the alternative translations given above since the message received may
not always be a pair of link names. The full translation is as follows where $k$ is a constant:
\begin{eqnarray*}
\sembrac{ x }_{u} & = & {\bf rec}\,X.\,u?v\,.\,(\,x!v.()\,|\,X\,) \\
\sembrac{ k }_{u} & = & {\bf rec}\,X.\,u?v\,.\,(\,v!k.()\,|\,X\,) \\
\sembrac{ \lambda x.M }_{u} & = & {\bf rec}\,X.\,u?(x,q)\,.\,(\,\sembrac{M}_{q}\,|\,X\,) \\
\sembrac{ @_{V} M N }_{u} & = &
(\,\sembrac{M}_{f}\,|\,f!(a,u).()\,|\,\sembrac{N}_{a}\,)\,\res{f}\,\res{a} \\
\sembrac{ @_{L} M N }_{u} & = & (\,\sembrac{M}_{f}\,\,|\,f!(t,u).()\,|\,{\bf
rec}\,X\,.\,t?v.(\,a!v.()\,|\,\sembrac{N}_{a}\,|\,X\,)\,\res{a}\,)\,\res{f}\,\res{t} \\
\end{eqnarray*}

To retrieve the value from a $\lambda$--expression it is necessary to send a channel to it and receive
back the value on the channel. 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. 
An operation such as multiplication would be translated as follows: 
\begin{eqnarray*}
\sembrac{ Mult(M,\,N) }_{u} & = &
(\,\sembrac{M}_{a}\,|\,\,\sembrac{N}_{b}\,|\,(a!x.()\,|\,b!y.()\,|\,x?m\,.y?n\,.\,Const(u,\,n\,\times\,m)\,)\res{x}\res{y}\,)\res{a}\res{b}
\end{eqnarray*}
where $Const$ is defined as: 
\begin{eqnarray*}
Const(\,z,\,c\,)\,=\,z?r\,.\,(\,r!c\,.\,()\,|\,Const(\,z,\,c\,)\,) 
\end{eqnarray*}
The arguments will be evaluated to values concurrently. The $Mult$ code sends channels to each argument
and retrieves the values from them. The behaviour is then the same as that for a constant but yielding
the product of the values. Curried versions can be produced using suitable $\lambda$--expressions such
as $\,{\lambda}x.{\lambda}y.Mult(x,\,y)\,$.
%%%%% Now that IS laziness

\section{Process Notation and Graph Rewriting} 
Process networks such as those described in this paper may be easily translated into generalised graph
rewriting systems. The discussion below uses the practical graph rewriting language Dactl \cite{GKSS88}. 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. It may be used as a vehicle for comparing implementation techniques and computational strategies and also, since it has a well-defined operational semantics, 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 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 operator at the root of a rule application, a data constructor, or an overwritable. The use of overwritable nodes which may be modified as a side-effect of a rule application enables the generalised graph rewriting of 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 defintion 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.

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}
FAppend[Cons[u x] y] => #Cons[u ^*FAppend[x y]]  ; {1}
FAppend[Nil y]       => *y                       ; {2}
FAppend[p1 p2]       => #FAppend[^*p1 p2]        ; {3}
\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 has not been rewritten to the form of a list. The argument is activated and the {\tt FAppend} application will be reconsidered when the argument has been rewritten.

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}
      *FAppend[ c:Cons[ o:1 n:Nil ] l ]
=>{1} #Cons[ o:1 ^s:*FAppend[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}
LAppend[Cons[u x] y r:Var] => *LAppend[x y w:Var], r:=*Cons[u w] ; {1}
LAppend[Nil y r:Var]       => *SUCCEED, r:=*y                    ; {2}
LAppend[p:Var q r:Var]     => #LAppend[^p q r]                   ; {3}
\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 instatiated. 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 LAppend} which share a variable:
{\tt
\begin{verbatim}
      *LAppend[Nil Cons[1 Nil] v:Var], *LAppend[v Cons[2 Nil] w:Var]
=>{3} *LAppend[Nil Cons[1 Nil] v:Var], #LAppend[^v Cons[2 Nil] w:Var]
=>{2} *SUCCEED, v:*Cons[1 Nil], #LAppend[^v Cons[2 Nil] w:Var]
=>{-} *SUCCEED, *LAppend[v:Cons[1 Nil] Cons[2 Nil] w:Var]
=>{1} *SUCCEED, w:*Cons[1 x], *LAppend[Nil Cons[2 Nil] x:Var]
=>{2} *SUCCEED, w:*Cons[1 x], x:*Cons[2 Nil], *SUCCEED
=> 
\end{verbatim}
}
The third step, when there is no match on the value assigned to variable {\tt v}, reactivates the second {\tt LAppend} predicate.

%%%% Now show channels

\subsection{Translating a Process Networks to a Graph Rewriting System}

Before describing the  translation of a 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 sublanguage in which the only forms allowed are: 
\[
\begin{array}{l}
P::= x!y.A \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. It should be clear that any process expression can be converted to this form. Equivalent
forms of the translation of
${\lambda}x.x$ are shown for illustration: 
\begin{eqnarray*}
\sembrac{\,{\lambda}x.x\,}_{u}\,&\,=\,&\,{\bf rec}\,X.\,u?(x,q)\,.\,(\,X\,|\,\,{\bf
rec}\,Y.\,q?v\,.\,(\,Y\,|\,x!v.()\,)\,) 
\end{eqnarray*}
Expanding the syntactic sugar for ${\bf rec}$ gives: 
\begin{eqnarray*}
X:\,X\,=\,u?(x,q)\,.\,(\,X\,|\,Y:\,Y\,=\,q?v\,.\,(\,Y\,|\,x!v.()\,)\,) 
\end{eqnarray*}
Adding additional agent definitions to satisfy the reduced syntax: 
\begin{eqnarray*}
X: & & X\,=\,u?(x,q)\,.\,Z:\,Z\,=\,(\,X\,|\,Y:\,Y\,=\,q?v\,.\,W: \\
& & W\,=\,(\,Y\,|\,Put:\,Put\,=\,x!v.\,Nil:\,Nil\,=\,()\,)\,) 
\end{eqnarray*}
Adding parameters to avoid free variables: 
\begin{eqnarray*}
X(u): & & X(u)\,=\,u?(x,q)\,.\,Z(u,x,q):\,Z(u,x,q)\,=\,(\,X(u)\,|\,Y(x,q): \\
& & Y(x,q)\,=\,q?v\,.\,W(x,q,v):\,W(x,q,v)\,=\,(\,Y(x,q)\,|\,Put(x,v): \\
& & Put(x,v)\,=\,x!v.\,Nil:\,Nil\,=\,()\,)\,)
\end{eqnarray*}
All definitions can now be pulled to the top level: 
\begin{eqnarray*}
X(u): & & X(u)\,=\,u?(x,q)\,.\,Z(u,x,q): \\
& & Z(u,x,q)\,=\,(\,X(u)\,|\,Y(x,q)\,): \\
& & Y(x,q)\,=\,q?v\,.\,W(x,q,v): \\
& & W(x,q,v)\,=\,(\,Y(x,q)\,|\,Put(x,v)\,): \\
& & Put(x,v)\,=\,x!v.\,Nil: \\  
& & Nil\,=\,() 
\end{eqnarray*}
All output operations are followed by a process denoting inaction. The $Put$ action definition can be
used for all output actions.

The Dactl rules below illustrate the translation of this function applied to the constant value $3$:
{\tt
\begin{verbatim}
RULE
  INITIAL => *Read[z], *A[z], z:NewChan; 
  A[z] -> *X[f], *Put[f Cons[a z]], *Const[a 3], f:NewChan, a:NewChan; 
  X[u] -> #Z[u ^xq:*Get[u]]; 
  Z[u Cons[x q] -> *X[u], *Y[x q]; 
  Y[x q] -> #W[x q ^v:*Get[q]]; 
  W[x q v] -> *Y[x q], *Put[x v]; 
  Const[u k] -> #C[u k ^v:*Get[u]]; 
  C[u k v] -> *Const[u k], *Put[v k]; 
  Read[z] => *Get[r], *Put[z r], r:NewChan;
\end{verbatim}
}
Processes generally correspond to GRS terms. The {\tt *} marks an active process or rewritable term.
Parallel composition, used by $Z$ and $W$ is very straightforward. Restriction, used in $A$, corresponds
to declaration of new links denoted by the term {\tt NewChan}. 

Input and Output actions involve the primitives {\tt Get} and {\tt Put}. {\tt Get} takes a channel as
argument and returns the value received, blocking until input is available. Where {\tt Get} is used, as
in {\tt X} and {\tt Y}, the behaviour to follow the input action is marked with {\tt \#} to indicate
that it is blocked until the input action succeeds. The result forms an argument to the following
action. When a pair is input, (for example {\tt x} and {\tt q} in {\tt X}), the pattern for the
subsequent action, ({\tt Z} in this case), matches a pair of values for use in the body of the action.
To output a pair, the {\tt Cons} constructor is used to build the pair, as in {\tt A}.

The primitives {\tt Get} and {\tt Put} are defined as follows: 
{\tt
\begin{verbatim}
RULE
  Put[c:Chan[v] d] => *Terminate, c:= *Chan[Cons[d v]]; 
  Get[c:Chan[Cons[d v]]] => *Id[d], c:=*Chan[v]; 
  Get[c] => #Get[^c]; 
  Id[x] => *x; 
\end{verbatim}
}
A new channel is defined as the following pattern: 
{\tt
\begin{verbatim}
PATTERN
  NewChan = Chan[Nil]; 
\end{verbatim}
}
When values are sent to a channel using {\tt Put}, a non-functional rewrite is
performed which updates the shared channel by adding a new element at the
head of the list of available values. 

To input a value, using {\tt Get}, the channel must be non-empty, which is
detected by the presence of a {\tt Cons}
node at the head of the list of values. The first value is returned, and the
channel updated with the first element removed. If the channel is empty, the
{\tt Get} is blocked until the channel is overwritten to contain some value.
The {\tt Id}
rule is needed for unimportant technical reasons.

It should be noted that this communication scheme is very simple because of the
restricted use of the process model in the translation scheme:
\begin{itemize}
  \item Lack of choice operators avoids the need to retract communication
offers 
  \item Ability to use asynchronous communication removes the need for
synchronising operations 
  \item There is no need to maintain the order of available messages so a stack
may be used
\end{itemize}
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 subexpressions as independent unrooted terms linked by shared
references to nodes representing channels. In this way,
execution corresponds more to the actions of the Chemical Abstract Machine
\cite{BeBo90} than a traditional graph reduction machine.

\section{Conclusions} 
A new scheme for translating $\lambda$--Calculus expressions to process networks has been presented. The
new
model
allows mixing of lazy and call-by-value strategies. Simple data values and
their operators may be incorporated in the translation. 

The process notation used may be related to graph rewriting, opening up the
question of whether graph rewriting might lead to a suitable low-level
implementation route for such process notations and programming languages
integrating functional and process 
styles.

\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[{BeBo90}]{BeBo90}
G. Berry \& G. Boudol:
{\em The  Chemical Abstract Machine}.
Proc. POPL 90, p 81-94. (1990) 

\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[{HonTok91}]{Hon91}
K. Honda and M. Tokoro:
{\em An object calculus for asynchronous communication}.
Proc.\ ECOOP'91, Geneva, July 1991.

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

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

\bibitem[{Mil89a}]{Mil89a}
R. Milner:
{\em Communication and Concurrency}.
Prentice Hall. (1989)

\bibitem[{Mil89b}]{Mil89}
R. Milner: 
{\em Functions as Processes}. 
Technical Report, INRIA Sophia Antipolis, June 1989. (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[{Ong88}]{Ong88}
C-H. L. Ong:
{\em The Lazy Lambda Calculus: An Investigation into the Foundations of
Functional Programming}.
Ph.D. Thesis, Imperial College, London University. (1988)

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