\documentstyle[11pt,a4]{article} 
%\documentstyle[Wiley]{book} 
%\def\sysdetails{} 
% Remove % to suppress system details printed during preparation

\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Authors, change the definitions appropriately:
%\setcounter{chapter}{18} 
%define chapter number (8 in reference version)
\title{A New Process Model for Functions} 
%define short title for running head
%\chaptitle{A New Process Model for Functions} 
%define long title for 1st page of chapter
%\authorhead{Glauert et al} 
%define short author list for running head
\author{J.R.W. Glauert, L. Leth and B. Thomsen} 
%define full author list for 1st page of chapter
\bibliographystyle{alpha}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\firstpage{1} %Final version to contain no page numbers
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\makechaptitle

\date{In: \emph{Term Graph Rewriting: Theory and Practice}, Wiley,  1993}
\maketitle

% Start of Macros
\newtheorem{definition}{\mbox{\sc Definition}}[section] 
\newcommand{\res}[1]{\backslash #1}
\newcommand{\trans}[3]{#1 \arrow{#2} #3}
\newcommand{\arrow}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\infer}[3]
           {\vspace{.2cm}
            \hbox{${\displaystyle {\frac {#1}{#2}}\hspace{.5cm}{#3}}$}
            \vspace{.2cm}}
\newcommand{\sembrac}[1]{[\![ #1 ]\!]}
\newenvironment{proof}{\vspace{3 mm}{\noindent \bf
Proof}\rm}{\null\hfill
$\Box$\\ \vspace{3 mm}}
\newcommand{\qed}{\hfill $\Box$}
\newcommand{\skil}{\ \raisebox{-4.5pt}{\rule{1pt}{5mm}} \ }
%Some abbreviations
\newcommand{\F}{Facile}
\newcommand{\Cham}{Chemical Abstract Machine}
\newcommand{\Lc}{$\lambda$-Calculus}
\newcommand{\LC}{$\lambda$-Calculus}
\newcommand{\LLc}{Lazy-$\lambda$-Calculus}
\newcommand{\LLC}{Lazy-$\lambda$-Calculus}
\newcommand{\ELc}{Eager-$\lambda$-Calculus}
\newcommand{\ELC}{Eager-$\lambda$-Calculus}
\newcommand{\VLc}{Call-by-value-$\lambda$-Calculus}
\newcommand{\VLC}{Call-by-Value-$\lambda$-Calculus}
\newcommand{\Lx}{$\lambda$-expression}
\newcommand{\Pc}{$\pi$-Calculus}
\newcommand{\PC}{$\pi$-Calculus}
\newcommand{\PPC}{Polyadic-$\pi$-Calculus}
\newcommand{\PPc}{Polyadic-$\pi$-Calculus}
\newcommand{\RA}{{\em return-address\/} channel}
\newcommand{\Whnf}{weak head-normal form}
\newcommand{\rec}{{\bf rec}}
% Source representation
\newcommand{\Labs}[2]{\lambda{#1}.\,{#2}}
\newcommand{\Lapp}[3]{{#2}\,@_{#1}\,{#3}}
\newcommand{\LappL}[2]{\Lapp{L}{#1}{#2}}
\newcommand{\LappE}[2]{\Lapp{E}{#1}{#2}}
\newcommand{\Ltriv}{()}
\newcommand{\Lpair}[2]{({#1},{#2})}
\newcommand{\redL}{\rightarrow_L}
\newcommand{\redE}{\rightarrow_E}
% End of Macros

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

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.

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 paper describes a new translation of the \Lc\ into a process
notation, supporting a mixture of evaluation strategies using techniques
similar to \cite{Bur84}. Milner and Leth consider only the pure \Lc\,
while our new translation handles constant data values and their
operations.

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.

\section{The Lazy- and Eager- \LC}
In this section we shall review some aspects of the \LLC\ \cite{Abr88}
and introduce the \ELC. The syntax of both is slightly unconventional as
we use an explicit left-associative operator, $@$, for application. The
operator will be decorated to indicate which calculus is being
considered.
\begin{eqnarray*}
e & ::= &  x \mid \Labs{x}{e} \mid \Lapp{}{e}{e}  
\end{eqnarray*}
where $x$ is taken from a set of variable names.

\subsection{The \LLC}
Terms in the {\em \LLC} may be reduced according to the relation $\redL$
defined as follows:
\begin{definition}
Let $\redL$, lazy reduction, be the smallest relation satisfying:
\begin{center}
\begin{tabular}{lccl}
$APPL: \:\: {\infer{e \:\redL\: e''}
       {\Lapp{}{e}{e'} \:\redL\: \Lapp{}{e''}{e'}}
       { }}$
& &
$BETA: \:\: \Lapp{}{(\lambda x.e)}{e'} \:\redL\: e\,[e'/x]$
\end{tabular}
\end{center}
\end{definition}
The \LLC\ is inherently sequential. Reduction always occurs at the head
of an application sequence, i.e. let $M \equiv M_0 @ M_1 \dots\ M_n \:
(n>0)$ where $M_0$ is not an application, then the only reduction
possible is when $ n \ge 1 $ and $M_0 \equiv \Labs {x}{N}$. In this case
we have $M_0 @ M_1 @ M_2 \dots\ M_n \rightarrow_L N\{M_1/x\} @ M_2 \dots
M_n$ since we will generally consider that expressions to reduce are
closed. There will always be a redex on the left spine unless the whole
expression is an abstraction.

Note that the \LLc\ does not reduce the bodies of abstractions so it 
will
only reduce expressions to \Whnf. This is not a problem when considering
functional programming where functional normal forms are not usually of
interest.

\subsection{The \ELC}
Since we are interested in parallel evaluation of functional programs by
translating them into a formalism for concurrent processes, we do not
have great hopes if we solely base our work on the \LLc. A more eager
evaluation strategy is obtained by adding an extra reduction rule
$APPR$:
\begin{definition}
Let $\redE$, eager reduction, be the smallest relation satisfying:
\begin{center}
\begin{tabular}{lccl}
$APPL: \:\: {\infer{e \:\redE\: e''}
       {\Lapp{}{e}{e'} \:\redE\: \Lapp{}{e''}{e'}}
       { }}$
& &
$APPR: \:\: {\infer{e' \:\redE\: e''}
       {\Lapp{}{e}{e'} \:\redE\: \Lapp{}{e}{e''}}
       { }}$
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{c}
$BETA: \:\: \Lapp{}{(\lambda x.e)}{e'} \:\redE\: e\,[e'/x]$
\end{tabular}
\end{center}
\end{definition}
This allows reduction in both operator and operand in an application. We
shall call this calculus the {\em \ELC}. $\redL$ is clearly contained in
$\redE$.

The \ELC\ introduces some non-determinism to the reduction rules since
for any application with redexes in the operand we may either reduce the
operand or perform the reduction in $\redL$. Since the \LLc\ is
normalising, the \ELc\ may converge whenever the lazy calculus
converges. However, if we continually choose redexes from $\redE$ which
are not needed, then a term with a \Whnf\ may not converge.
%Example of K N Omega

We should remark that the \ELc\ is not the same as the {\em \VLC}.
Call-by-value reduction uses a restricted $BETA$ rule in which the
operand must be a value, $v$, in the form $\Labs{x}{e}$:
\begin{center}
\begin{tabular}{c}
$BETA: \:\: \Lapp{}{(\lambda x.e)}{v} \:\rightarrow_V\: e\,[v/x]$
\end{tabular}
\end{center}
This means that reduction of operator and operand may proceed
non-deterministically, but reduction of a redex may only occur when both
operator and operand have converged. Clearly there are terms
%such as the example above
for which the \VLc\ diverges when the \LLc\ converges and the \ELc\ may
converge.

\subsection{A Mixed Calculus}
The translations presented in this paper support a mixed language in
which the \LLc\ and \ELc\ live together in one calculus. In this case we
annotate the application by $@_L$ or $@_E$ in $M @_L N$ or $M @_E N$ to
indicate which evaluation strategy is to be used. The rules $APPL$ and
$BETA$ apply to both forms of application while $APPR$ applies only to
$@_E$. The effect is similar to \cite{Bur84}. The intuition is that we
may reduce any instance of the $BETA$ rule which can be reached by a
path through the operator position of $@_L$ terms or either argument of
$@_E$ terms.
%Give the full reduction relation @ means @_L or @_E

Languages such a Concurrent Clean % \cite{CleanInBook}
provide facilities
which allow for limited eager evaluation and might well be given a
semantics in the same way as the mixed calculus. Judicious use of the
$@_E$ operator in positions where the operand is needed or strongly
terminating will mean that the convergence properties of the program are
the same as for the \LLC.

\section{A Process Notation}
We present a process notation into which we will translate programs
written in the mixed calculus described in the previous section.
The notation 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 allowing dynamic process networks to be generated.

The significant extension to these earlier notations is that we permit,
as an atomic event, the communication of terms representing arbitrary
tuples of values, although nothing more complicated than pairs is
required for our translations below. This is very nearly equivalent to
the Polyadic-\PC\ \cite{PolyPi} although we would allow nested terms. We
allow a received term to be matched to a pattern of names, or bound to a
single name. Further work is required on a sort discipline for the
calculus to ensure that names bound to structured values are never used
as link names.

We are also very interested in the sub-calculus in which the process
following an output action is always the inactive process. This is in
essence the language of \cite{HoTo91}.
 
\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]{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]{Input}}]  $x?y . P$ \\
Receive a value on link $x$ and bind the value to $y$ in subsequent
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$.
  \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).

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

The form ${\bf rec} X . P$
is allowed as syntactic sugar for $X : X = P$.

%Maybe omit
\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[4cm][r]{Output} &
$\trans{x!y.P}{x!y}{P}$ \\
  & \\
\makebox[4cm][r]{Input} &
$\trans{x?y.P}{x?z}{P\{z/y\}}$ \\
 & \\
\makebox[4cm][r]{Res}  &
$\infer{\trans{P}{\alpha}{P'}}
      {\trans{P\res{x}}{\alpha}{P'\res{x}}}
      {,x \neq c(\alpha)}$  \\
 & \\
\makebox[4cm][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[4cm][r]{Par}  &
$\infer{\trans{P}{\alpha}{P'}}
      {\trans{P\mid Q}{\alpha}{P'\mid Q}}
      {,bn(\alpha)\cup fn(Q) = \emptyset}$  \\
 & \\
\makebox[4cm][r]{Com}  &
$\infer{\trans{P}{x?y}{P'}\;\;\trans{Q}{x!y}{Q'}}
      {\trans{P\mid Q}{\tau}{P'\mid Q'}}
      {}$  \\
 & \\
\makebox[4cm][r]{Close}  &
$\infer{\trans{P}{x?y}{P'}\;\;\trans{Q}{x\res{y}}{Q'}}
      {\trans{P\mid Q}{\tau}{(P'\mid Q')\res{y}}}
      {,y\not\in fn(P)}$  \\
 & \\
\makebox[4cm][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}
\rule{\textwidth}{.5pt}
\caption{Operational semantics for Process Notation \label{opsem}}
\end{figure}

\section{Translation of Lazy and Eager $\lambda$-Calculus}

Milner \cite{Mil90} provides encodings of the \LLc\ and the \VLc\ in the
\Pc.
Only closed terms are considered. The encodings simulate particular
reduction strategies. 

We present a new scheme for translating
$\lambda$--expressions to process networks. The language translated
provides two forms of application operator and also supports constants
denoted by $k$ in the syntax. If all applications are $@_L$ then a lazy
translation results, although it is not quite the same as that of
Milner. The use of $@_E$ throughout yields a translation of the \ELc.
 
\subsection{The New Translation Scheme} 
\begin{eqnarray*}
\sembrac{ x }_{u} & = & \rec\,X.\,u?v\,.\,(\,x!v.()\,|\,X\,) \\
\sembrac{ k }_{u} & = & \rec\,X.\,u?v\,.\,(\,v!k.()\,|\,X\,) \\
\sembrac{ \Labs{x}{M} }_{u} & = &
\rec\,X.\,u?(x,q)\,.\,(\,\sembrac{M}_{q}\,|\,X\,) \\
\sembrac{ \LappL{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} \\
\sembrac{ \LappE{M}{N} }_{u} & = &
(\,\sembrac{M}_{f}\,|\,f!(a,u).()\,|\,
\sembrac{N}_{a}\,)\,\res{f}\,\res{a}
\end{eqnarray*}

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. 
Data values are represented by a set of names disjoint from those used
for links. Functions such as the successor function will be represented
by global names. A process network to implement these functions will
exist in parallel with the program to be evaluated. The network for
$succ$ would be as follows:
\begin{eqnarray*}
 & &
\rec\,X.\,u?(x,q)\,.\,(\,X\,|\,(\,x!t.()\,|\,t?n\,.\,q?r\,.\,
r!(n+1).()\,)\, \res{t}\,)
\end{eqnarray*}
An occurrence of the name $succ$ will be translated like a variable.

It is assumed that programs will reduce to data values. To retrieve the
value from the translation of such 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. 

\subsection{Properties of the New Scheme}
The intuition behind the translation is that the translation of each
syntactic construct is a process network with a special characteristic
link, or {\em handle}, through which the network will communicate. This
link is denoted by $u$ in the translations.

If the process represents a numeric constant, the value received on $u$
will be a link on which the number is to be returned. If the process
encodes an abstraction, $u$ will be sent a pair of links. The first link
of the pair is the handle  on the argument, while the second link is to
be the handle on the process which results when the argument is
substituted in the body of the abstraction.

The encoding of an application links up an abstraction with an argument.
Considering $@_E$ first, we see that neither the encoding of the
operator nor operand are guarded. The process networks concerned will
evolve independently. When the operator reaches \Whnf\ it will be 
waiting
to receive input on its handle. The apply glue code in the translation
sends the resulting abstraction a pair informing it of the operand and
the channel which is to be the handle for the resulting network.

The encoding of $@_L$ guards the operand so that only when the operator
actually requests the value of the operand will it be evaluated. The
extra glue code acts as a buffer, passing on the request from the
operator to the operand network.

A variable simply acts as a buffer, relaying information sent to it to
the handle for the operand provided when the abstraction binding the
variable was applied. The information sent will depend on the type of
the result: if it is a constant then a single return link name will be
sent; if it has a function type then a pair will be sent.

There are simplifications gained by communicating pairs of values. If
only simple names may be communicated, extra temporary links are needed
to prevent interleaving of messages from different agents able to the
handle $u$, as in Milner's call-by-value scheme. The \PPc\ also
overcomes these problems, though we must be aware that the sort of
apparently similar links will depend on the type of the {\Lx}s being
translated.

All output actions in a translated network are followed by inaction. As
a consequence no process is 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.

\subsection{Elimination of Some Recursion}
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.

To eliminate some of the superfluous recursion we may use a more
sophisticated translation scheme based on the observation that terms
in head position do not need recursion. In other words, when a
variable or a $\lambda$-abstraction occurs as an operator in a
$\lambda$-expression there is no need for multiple copies, whereas
occurrence as an operand needs the possibility of producing
various copies of the variable or the $\lambda$-abstraction.

The function application cannot be analysed similarly, so recursion
has to be provided in all cases. This gives us eight rules in the
translation scheme; two for variables (without and with recursion),
two for constants,
two for $\lambda$-abstraction, and one for each of the applications.
The translations involved with recursion are annotated
with $*$:

\begin{eqnarray*}
\sembrac{ x }_{u} & = & u?v\,.\,x!v.() \\
\sembrac{ x }_u^* & = & \rec X . u ? v .( x ! v \mid X) \\
\sembrac{ k }_{u} & = & u?v\,.\,v!k.() \\
\sembrac{ k }_{u}^* & = & \rec\,X.\,u?v\,.\,(\,v!k.()\,|\,X\,) \\
\sembrac{ \Labs{x}{M} }_{u} & = & u?(x,q)\,.\,\sembrac{M}_{q} \\
\sembrac{ \Labs{x}{M} }_{u}^* & = &
\rec\,X.\,u?(x,q)\,.\,(\,\sembrac{M}_{q}\,|\,X\,) \\
\sembrac{ \LappE{M}{N} }_{u} & = & \sembrac{ \LappE{M}{N} }_{u}^* \\
& = &
(\,\sembrac{M}_{f}\,|\,f!(a,u).()\,|\,
\sembrac{N}_{a}^*\,)\,\res{f}\,\res{a}
\\
\sembrac{ \LappL{M}{N} }_{u} & = & \sembrac{ \LappL{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*}

Note that the translation of $\LappL{M}{N}$ only involves one level of
recursion using $\rec$. The recursion in  $\LappE{M}{N}$ comes
indirectly through the use of $\sembrac{N}^*$.


\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 practical
graph rewriting language Dactl \cite{GKS91} is used as the target for
our translation.

\subsection{A Standard From for Process Networks}
In this section we define how to express a process network in a standard
form which makes heavy use of defined agents. This form can then be
implemented very easily as a GRS.

If $A$ stands for an agent identifier then the forms we will allow are: 
\[
\begin{array}{l}
P::= x!y.A \skil x?y.A \skil (A\,|\dots|\,A) \skil P \res{x} \skil P: A
= P 
\end{array}
\]
Also, we restrict  agent definitions to the outermost level, so they may
contain no free variables. It should be clear that any process
expression can be converted to this form by inserting new agent
identifiers and adding appropriate definitions. The transformation is in
four stages. We will use forms of ${\lambda}x.x$ for illustration: 
\begin{eqnarray*}
& & {\bf rec}\,X.\,u?(x,q)\,.\,(\,X\,|\,\,{\bf
rec}\,Y.\,q?v\,.\,(\,Y\,|\,x!v.()\,)\,) 
\end{eqnarray*}
The first stage is to expand the syntactic sugar for ${\bf rec}$ which
was defined such that ${\bf rec} X . P \: \equiv \: X : X = P$. This
gives: 
\begin{eqnarray*}
X: & &
X\,=\,u?(x,q)\,.\,(\,X\,|\,Y:\,Y\,=\,q?v\,.\,(\,Y\,|\,x!v.()\,)\,) 
\end{eqnarray*}
The second stage is to add extra agent definitions to satisfy the
reduced syntax using the rule that $ P \: \equiv \: A : A = P$ where $A$
is a new agent identifier:
\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*}
The third stage is to add parameters to avoid free variables. This uses
the rule that $X : X = P \: \equiv \: X(fn(P)) : X(fn(P)) =
P\{(fn(P))/X\}$:
\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*}
Finally, 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.

\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{GKS91} provides a thorough background to the Dactl language. Here
we review the language features exploited
in the translation of process networks to graph rewriting systems in
this paper.
The nodes of a Dactl graph are labelled with a symbol which indicates
that the node plays the role of
an
{\em operator} at the root of a rule application, a {\em data
constructor}, or an {\em overwritable}. The role of
operators and constructors will be familiar. The novel feature is the
use of
overwritable nodes which may be modified as a side-effect of rule
application. This enables Dactl to
express more computational models than the term-graph rewriting which is
discussed elsewhere in this book. 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.

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:
\begin{verbatim}
  c: Chan[ n ],
  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:
\begin{verbatim}
  c: Chan[ Nil ]
\end{verbatim}
Dactl rules contain a {\em pattern} to be matched and a body, or {\em
contractum}, to replace the
occurrence of the pattern in the graph, or {\em redex}. Patterns are
Dactl graphs but may contain node
identifiers lacking a definition which will match an arbitrary node.

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

To control the order of evaluation,
attempts to match the rules against the graph only begin at {\em active}
nodes, marked
with a $*$ in the representation. If more than one rule matches, an
arbitrary choice
may be made about which rule to apply; fairness is not assumed. 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.

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

Nodes may also be created {\em suspended}, indicated by one or more {\tt
\#} markings, 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. Each notification removes one suspension, the
node
becoming active when the last suspension is removed. Notification
typically takes place when an active node 
has become a
constructor or overwritable. Arcs which will form notification paths are
marked with  \verb+^+.

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

The rules for {\tt Put}
add a value at the head of the
stack of values, while {\tt Get} 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}
}

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

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 {\tt \#} 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{Translation of Standard Form Networks to Dactl}
The Dactl rules below illustrate the translation of the function
${\lambda}x.x$ 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}
}

The communication scheme is very simple because of the
restricted use of the process model in the translation scheme:
lack of a choice operator avoids the need to retract communication
offers; ability to use asynchronous communication removes the need for
synchronising operations; and there is no need to maintain the order of
available messages so a stack
may be used.

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 \Lc\
to the process notation.
Several different translations from \Lc\ 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
\Pc\ translations of Milner
cannot be translated directly. A Form of the \LLc\ translation modified
in a manner inspired by \cite{HoTo91} has been produced. The translation
is extended to handle constants. This has been called {\em 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{ \LappL{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}
\end{eqnarray*}

This translations were compared with {\em NewLazy} and {\em NewEager}.
These correspond to the new translation
converting all applications to lazy or eager form correspondingly. In
addition, the tupled communication of our
notation was exploited to produce an improved version of {\em PiLazy},
called {\em ImpPiLazy}:
\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{ \LappL{M}{N} }_{u} & = &
(\,\sembrac{M}_{v}\,|\,v!(t,u).()\,|\,{\bf
rec}\,X\,.\,t?w.\,(\sembrac{N}_{w}\,|\,X))\res{t}\res{v}
\end{eqnarray*}

The test programs used were:
\begin{eqnarray*}
{\rm IdTest}: & & ({\lambda} x.\,x)\, 99 \\
{\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|rr|} \hline
{\em Translation} & {\em IdTest} & {\em Twice} \\ \hline
NewEager & 4  & 49 \\
NewLazy & 5  & 80 \\
PiLazy & 7  & 94 \\
ImpPiLazy & 4  & 52 \\ \hline
\end {tabular}
\end{center}

Note that the lazy translations allow no parallelism, so our main focus
is on an eager translation, 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}. {\em PiLazy} does not perform well
since we must avoid synchronous communication. However, the improved
version {\em ImpPiLazy} is best
for a purely lazy translation. We have not attempted to reduce recursion
in the new translation.

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

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 eager computation, and
also performs well for lazy computation.

While implementation efficiency is not our primary concern, the final
aim of this work is to investigate
possible techniques for practical parallel implementation of languages
integrating functional and process
styles. The process notation we have developed  may be related to graph
rewriting opening the question of whether graph rewriting can form the
basis for such practical implementations.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Authors, please change the chapter number (8 in the
% reference version) to your chapter number
\bibliography{Chapter18}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\end{document}





