%\documentstyle[a4,11pt]{article}
\documentstyle[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 Process Model for Functions}}
\author{
        {\it J. Glauert\thanks{Partially supported by ESPRIT BRA 3074: Semagraph}}\\
	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{Semagraph '91}
%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}
This paper contributes to the study of the relationship between functional programs and process notions.
Building on the work of Milner \cite{Mil90}, Leth \cite{Leth91}, and Honda and Tokoro \cite{HoTo91}, we provide a new translation of $\lambda$--expressions to networks of processes. The translation has a number of
novel features:
\begin{itemize}
\item The process networks produced are simpler and perform fewer communications than in other models.
\item Both lazy and call-by-value evaluation strategies may be used, and may be combined in one
expression if desired.
\item In addition to the pure $\lambda$--calculus, we are able to translate simple data values and their operators.
\item The model of communication used is essentially asynchronous and will allow a
straightforward implementation.
\item The process notation used may be related directly to a simple practical graph rewriting model.
\end{itemize}
While implementation efficiency is not our primary concern, the aim of this work is to investigate
possible techniques for practical parallel implementation of languages integrating functional and process
styles.
\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}, while Thomsen used higher-order processes \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.
The studies based on extensions to CCS adopt a synchronous model of communication. Honda and Tokoro \cite{HoTo91} show
that asynchronous communication can be used to the same effect. The work presented here is able to take advantage of
such asynchronous models.

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 a language such as Facile \cite{GPM89} which aims to integrate functional and process styles. 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 is presented. The style of execution of such a GRS is rather different from the traditional term-based translation of a functional language. %%%% examples needed

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

A model equivalent to the asynchronous language of \cite{HoTo91} would always follow output actions with inaction.

\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}
  & \\
\makebox[5cm][r]{Output} &
$\trans{x!y.P}{x!y}{P}$ \\
  & \\
\makebox[5cm][r]{Input} &
$\trans{x?y.P}{x?z}{P\{z/y\}}$ \\
 & \\
\makebox[5cm][r]{Res}  &
$\infer{\trans{P}{\alpha}{P'}}
      {\trans{P\res{x}}{\alpha}{P'\res{x}}}
      {,x \neq c(\alpha)}$  \\
 & \\
\makebox[5cm][r]{Open}  &
$\infer{\trans{P}{y!x}{P'}}
      {\trans{P\res{x}}{y\res{z}}{P'\{z/x\}}}
      {,z\not\in fn(P\res{x})}$  \\
 & \\
\makebox[5cm][r]{Par}  &
$\infer{\trans{P}{\alpha}{P'}}
      {\trans{P\mid Q}{\alpha}{P'\mid Q}}
      {,bn(\alpha)\cup fn(Q) = \emptyset}$  \\
 & \\
\makebox[5cm][r]{Com}  &
$\infer{\trans{P}{x?y}{P'}\;\;\trans{Q}{x!y}{Q'}}
      {\trans{P\mid Q}{\tau}{P'\mid Q'}}
      {}$  \\
 & \\
\makebox[5cm][r]{Close}  &
$\infer{\trans{P}{x?y}{P'}\;\;\trans{Q}{x\res{y}}{Q'}}
      {\trans{P\mid Q}{\tau}{(P'\mid Q')\res{y}}}
      {}$  \\
 & \\
\makebox[5cm][r]{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{Mil89}.

\section{Translation of Lazy and Call-By-Value $\lambda$--calculus}
Milner \cite{Mil90} provides encodings of the $\lambda$--calculus in the $\pi$--calculus.
Only closed terms are considered. The encodings simulate particular reduction strategies. 
In no case do the encodings reduce the bodies of abstractions, although 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{description} 
  \item [{\makebox[5cm][l] {Lazy Scheme:}}] $ \sembrac{ \lambda x.x }\;=\;u?x\,.\,u?v\,.\,x!v\,.\,() $
  \item [{\makebox[5cm][l] {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{description}
 
\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} 
%%% wanted small caps l and v below
In the translations below, the binary application operator combining $\lambda$-terms is made explicit and a 
subscript L or 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}.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*}
Note that we may write the translations of a variable and of $@_L M N$ as follows: 
\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*}
These will prove useful later. 
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:
\noindent
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 would suffice. This can significantly reduce the complexity of a low-level implementation of such a process notation as will be shown later. \cite{HoTo91}
shows that sequentialisation is possible using just asynchronous communication, though our use of tupled communication
allows their scheme to be simplified.

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 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,Mil90}. 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 
follows the techniques developed by Milner in \cite{Mil90}.
\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\,*\,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)$.
\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{GKKS91}.

\subsection{The Graph Rewriting Language Dactl}
Dactl provides a notation for
describing computational objects as directed graphs, and for specifying computation in terms of pattern-directed
rewritings of such graphs.
It has been used in studies of the implementation of a range of language styles including functional programming, term
rewriting languages \cite{Ken90}, and concurrent logic languages \cite{GlaPap88}. Graph rewriting also shows promise for
supporting the integration of different programming styles; \cite{GlaPap91} reports early work on integration of
functional and logic languages, while the work reported here arises from a collaborative study investigating
integration of functional and process-based programming.

\cite{GKKS91} in the current proceedings provides a thorough background to the Dactl language and the introductory sections of that paper should
be read to gain a full appreciation of the notation. Here we review the language features exploited
in the translation of process networks to graph rewriting systems in this paper.

Terms to be rewritten in a Dactl program are marked with an active node marking, $*$. Hence a parallel composition of
processes $P$ and $Q$ both using links $x$ and $y$ might be encoded by a graph:
{\tt
\begin{verbatim}
     *P[x y], *Q[x y]
\end{verbatim}
}

A link, or channel, is represented by a special state value, or overwritable node, with symbol {\tt Chan} containing
a list of values representing the queue of messages which have been sent to the link. Below are rules {\tt Put}
which adds a value at the head of the
stack of values, and {\tt Get} which receives a value and then continues with process {\tt Use} which may manipulate
the value received:
{\tt
\begin{verbatim}
RULE
     Put[c:Chan[v] d] -> c:= *Chan[Cons[d v]];
     Get[c:Chan[Cons[d v]]] -> *Use[d], c:= Chan[v];
     Get[c:Chan[Nil]] -> #Get[^c];
\end{verbatim}
}

The initial state of a link is {\tt Chan[Nil]}, a channel with no messages available. Introduction of new channels
is associated with restriction operators in process expressions.

The {\tt Put} rule updates
the channel {\tt c} to contain the message referred to by {\tt d} as the first message in its buffer.
The effect of the active marker
on the updated channel will be to unblock any process attempting to receive on this channel.

The two rules for {\tt Get} describe the behaviour of a process guarded by an input action. The first rule corresponds
to the case where there is input available. The value found in the channel is passed to the {\tt Use} process which is
made active. The channel is updated to reflect the fact that a message has been delivered. The final rule comes into
play if the channel is empty. The \# and \verb+^+ markings indicate that the {\tt Get} process should be suspended 
until the channel
{\tt c} is updated by a {\tt Put} process.
\subsection{Translating a Process Network to a Graph Rewriting System}
Before performing the final translation to a GRS the process network is expressed in a standard form which makes heavy use of defined agents. 
If $A$ stands for an agent identifier then the only forms allowed are: 
\[
\begin{array}{l}
P::= x!y.A \skil x?y.A \skil (A\,|\dots|\,A) \skil A  \skil P \res{x} \skil P: A = P 
\end{array}
\]
Also, we only permit the agent definitions to be at the outermost level, so they may contain no free variables. It should be clear that any process expression can be converted to this form. The forms of ${\lambda}x.x$ are shown as an 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:Chan[Cons[Pair[x q] r]]] -> *Z[u x q], u:= Chan[r]; 
    X[u:Chan[Nil]] -> #X[^u]; 
    Z[u x q] -> *X[u], *Y[x q]; 
    Y[x q:Chan[Cons[v r]]] -> *W[x q v], q:= Chan[r]; 
    Y[x q:Chan[Nil]] -> #Y[x ^q]; 
    W[x q v] -> *Y[x q], *Put[x v]; 
    Const[u:Chan[Cons[v r]] k] -> *C[u k v], u:= Chan[r]; 
    Const[u:Chan[Nil] k] -> #Const[^u k]; 
    C[u k v] -> *Const[u k], *Put[v k]; 
    Read[z] => *Get[r], *Put[z r], r:NewChan;
\end{verbatim}
}
All Dactl programs start with a graph containing a single active node with symbol {\tt INITIAL}. This replaces process
$P$ above.

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}. The following pattern defines such new channels:
{\tt
\begin{verbatim}
PATTERN
    NewChan = Chan[Nil];
\end{verbatim}
}

All Output actions involve the primitive {\tt Put} described earlier.
Processes guarded by an input action become two rules. The first extracts a value from a channel containing input,
while the second applies when no input is available and blocks the process until an output action is performed
on the channel.

To output a pair, the {\tt Pair} constructor is used to build the pair, as in {\tt A}.
When a pair is input, (for example {\tt x} and {\tt q} in {\tt X}), the pattern matches a pair of 
values for use in the body of the action ({\tt Z} in this case).

The processes {\tt Read} and {\tt Put} are defined as follows: 
{\tt
\begin{verbatim}
RULE
    Put[c:Chan[v] d] -> c:= *Chan[Cons[d v]]; 
    Read[z] -> *Put[z r], *Print[r], r: NewChan;
    Print[x:Chan[Cons[v r]]] -> *PrintF["Result: %d" v], x:= Chan[r];
    Print[x:Chan[Nil]] -> #Print[^x];
\end{verbatim}
}

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{Results} 
A translator has been developed which will convert ``programs'' in an extended $\lambda$--calculus
to the process notation.
Several different translations from $\lambda$--calculus to processes have been implemented.
The process networks are converted to the sublanguage which makes heavy use
of agent definitions. This form is then converted to Dactl.

The mapping from process notation to Dactl does not handle non-trivial
processes with output guards (only inaction may follow an output
guard). This enables us to express the new translation directly, but the $\pi$--calculus translations of Milner
cannot be translated directly. Forms modified in a manner inspired by \cite{HoTo91} are used. The first will
be called {\em PiLazy} and the second {\em PiStrict}. To illustrate an operator we use the integer successor
function. The schemes are included for completeness:

{\bf PiStrict}
\begin{eqnarray*}
\sembrac{ x }_{u} & = & u!x.() \\
\sembrac{ k }_{u} & = & u!k.() \\
\sembrac{ {\lambda}x.M }_{u} & = & (u!y.()\,|\,{\bf rec}\,X.\,y?w.\,(w?t.\,(t!d.()\,|\,d?x.\,w?q.\,\sembrac{M}_{q})\res{d}\,|\,X)\,)\res{y} \\
\sembrac{ @_{V} M N }_{u} & = & (\sembrac{M}_{f}\,|\,f?y.\,(y!v.()\,|\,a?z.\,(v!t.()\,|\,t?d.\,(d!z.()|v!u.()))\res{t})\res{v}\,|\,\sembrac{N}_{a}\,)\res{f}\res{a} \\
\sembrac{ Succ(M) }_{u} & = & (\,\sembrac{M}_{a}\,|\,a?m.\,u!(m+1).()\,)\res{a} \\
\end{eqnarray*}
{\bf PiLazy}
\begin{eqnarray*}
\sembrac{ x }_{u} & = & x!u.() \\
\sembrac{ k }_{u} & = & u?v\,.\,v!k.() \\
\sembrac{ {\lambda}x.M }_{u} & = & u?d.\,(\,d!a.()\,|\,a?x.\,u?v.\,\sembrac{M}_{v}\,)\res{a} \\
\sembrac{ @_{L} M N }_{u} & = & (\,\sembrac{M}_{v}\,\,|\,v!d.()\,|\,d?a.\,(a!t.()\,|\,v!u.()\,|\,{\bf rec}\,X\,.\,t?w.\,(\sembrac{N}_{w}\,|\,X))\,\res{t}\,)\,\res{d}\,\res{v} \\
\sembrac{ Succ(M) }_{u} & = & (\,\sembrac{M}_{a}\,|\,(a!s.()\,|\,s?m.\,u?v.\,v!(m+1).())\res{s})\,\res{a}
\end{eqnarray*}
Note that for both of these translations the handling of constants and operators is simple, but abstractions and
applications require many communications.

These translations were compared with {\em NewLazy} and {\em NewStrict}. These correspond to the new translation
converting all applications to lazy or strict form correspondingly. In addition, the tupled communication of our
notation was exploited to produce optimised versions of {\em PiStrict} and {\em PiLazy}, called {\em NewPiStrict} 
and {\em NewPiLazy} respectively:

{\bf NewPiStrict}
\begin{eqnarray*}
\sembrac{ x }_{u} & = & u!x.() \\
\sembrac{ k }_{u} & = & u!k.() \\
\sembrac{ {\lambda}x.M }_{u} & = & (u!y.()\,|\,{\bf rec}\,X.\,y?w.\,(w?(x,q).\,\sembrac{M}_{q}\,|\,X)\,)\res{y} \\
\sembrac{ @_{V} M N }_{u} & = & (\sembrac{M}_{f}\,|\,f?y.\,(y!v.()\,|\,a?z.\,v!(z,u).())\res{v}\,|\,\sembrac{N}_{a}\,)\res{f}\res{a} \\
\sembrac{ Succ(M) }_{u} & = & (\,\sembrac{M}_{a}\,|\,a?m.\,u!(m+1).()\,)\res{a} \\
\end{eqnarray*}

{\bf NewPiLazy}
\begin{eqnarray*}
\sembrac{ x }_{u} & = & x!u.() \\
\sembrac{ k }_{u} & = & u?v\,.\,v!k.() \\
\sembrac{ {\lambda}x.M }_{u} & = & u?(x,v).\,\sembrac{M}_{v} \\
\sembrac{ @_{L} M N }_{u} & = & (\,\sembrac{M}_{v}\,|\,v!(t,u).()\,|\,{\bf rec}\,X\,.\,t?w.\,(\sembrac{N}_{w}\,|\,X))\res{t}\res{v} \\
\sembrac{ Succ(vM) }_{u} & = & (\,\sembrac{M}_{a}\,|\,(a!s.()\,|\,s?m.\,u?v.\,v!(m+1).())\res{s})\,\res{a}
\end{eqnarray*}

The test programs used were:
\begin{eqnarray*}
{\rm IdTest}: & & ({\lambda} x.\,x)\, 99 \\
{\rm Share}: & & ({\lambda} x.\,x*x)\,(2+3) \\
{\rm Twice}: & & ({\lambda} twice. {\lambda} succ. \,twice\,twice\,succ\,0)\,\,({\lambda} f. {\lambda} x. f\,(f\,x))\,\,({\lambda}n. Succ(n)) \\
\end{eqnarray*}

The efficiency measure used is the number of output actions made. In most cases, every output message is consumed.

\begin{center}
\begin {tabular}{|l|rrr|} \hline
{\em Translation} & {\em IdTest} & {\em Share} & {\em Twice} \\ \hline
NewStrict & 4 & 13 & 49 \\
PiStrict & 8 & 12 & 96 \\
NewPiStrict & 5 & 9 & 57 \\ \hline
NewLazy & 5 & 19 & 80 \\
PiLazy & 7 & 20 & 94 \\
NewPiLazy & 4 & 17 & 52 \\ \hline
\end {tabular}
\end{center}

Note that the lazy translations allow no parallelism, so our main focus is on the strict translations, but with
the aim of supporting laziness where it is required. Our translations are superior when function application
is taking place, as in {\em Twice}. The original versions of the $\pi$--calculus translations do not perform well -
since we must avoid synchronous communication. However, the modified versions are comparable with our new translations and
for a purely lazy translation, the {\em NewPiLazy} translation is best. However, for our area of interest,
strict computation, the strict form of the new translation {\em NewStrict} is best.
\section{Conclusions} 
A new scheme for translating $\lambda$--calculus expressions to process networks is 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. 

Some early experimental results are presented based on a translation of process networks to Dactl. The results
show that the new translation is superior for strict computation, and also performs well for lazy computation.

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.),
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[{GlaPap88}]{GlaPap88}
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}]{GlaPap91}
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[{GKKS91}]{GKKS91}
J.R.W. Glauert, J.R. Kennaway, I. King, \& M.R. Sleep:
{\em Dactl: An Experimental Graph Rewriting Language} 
Proceedings, Semagraph `91 Symposium, Nijmegen, December 1991. (1991)

\bibitem[{HonTok91}]{HoTo91}
Honda, K., Tokoro, M.,
{\it An object calculus for asynchronous communication},
Proceedings, ECOOP'91, Geneva, July 1991. (1991)

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

\bibitem[{Ken90}]{Ken90}
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, ICSTM. (1991) 

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

\bibitem[{Mil89}]{Mil89}
R. Milner:
{\em Communication and Concurrency},
Prentice Hall, 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, Department of Computing,
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} 
}
