%%% Start of LaTeX Document %%%
\documentstyle[11pt]{article}
%\documentstyle[a4,11pt]{article}
%\documentstyle[11pt]{mnotes}    

% 1in margins at left and right
\oddsidemargin=0in
\evensidemargin=0in
\textwidth=6.25in              % A4 paper is 8.25in wide

% 1in margins at top and bottom
\headheight=0pt
\headsep=0pt
\topmargin=0in
\textheight=9.7in              % A4 paper is 11.7in high

\pagestyle{plain}
\setlength{\parindent}{0cm}
\setlength{\parskip}{\medskipamount}
\setlength{\itemsep}{\smallskipamount}

\title{Notes on Using Small Processes to Implement Functional Languages}
\author{
        {\it John Glauert} \\
	{\em jrwg@sys.uea.ac.uk}}
%\reportref{Draft}
\date{Version 4}

\newenvironment{conjecture}{\noindent{\bf Conjecture: }}{}
\newenvironment{conclusion}{\noindent{\bf Conclusion: }}{}
\newenvironment{assignment}[1]{\noindent{\bf Assignment for {#1}: }}{}

\newcommand{\sembrac}[1]{[\![ #1 ]\!]}
\newcommand{\infer}[3]
           {\vspace{.2cm}
            \hbox{${\displaystyle {\frac {#1}{#2}}\hspace{.5cm}{#3}}$}
            \vspace{.2cm}}
% New macros
%\input{john-pi-macros}
% Process notation
\newcommand{\parprocs}[2]{{#1}\,|\,{#2}}
\newcommand{\restrict}[2]{({\nu}\,{#1})\,(\,{#2}\,)}
\newcommand{\replicate}[2]{!\,{#2}}
\newcommand{\guardedrep}[3]{!\,({#2} \cdot {#3})}
\newcommand{\recdef}[2]{{\bf rec} {\recvar {#1}} \cdot {#2}}
\newcommand{\guardedrec}[3]{{\bf rec} {\recvar {#1}} \cdot {#2} \cdot
(\,\parprocs {#3} {\recvar {#1}}\,)}
\newcommand{\recvar}[1]{{#1}}
\newcommand{\agtuse}[2]{\recvar {#1} ({#2})}
\newcommand{\agtdef}[3]{\agtuse {#1} {#2} = {#3}}
\newcommand{\inpact}[3]{{#1}({#2}) \cdot {#3}}
\newcommand{\inpacta}[2]{{#1}({#2})}
\newcommand{\outact}[3]{\overline{#1}\,{#2} \cdot {#3}}
\newcommand{\outacta}[2]{\overline{#1}\,{#2}}
\newcommand{\match}[3]{{#1}={#2} \cdot {#3}}
\newcommand{\inaction}{0}
\newcommand{\pair}[2]{{#1}\,{#2}}
\newcommand{\triv}{}
%\input{john-proc-macros}
% New Process notation
\newcommand{\PruleChange}[3]{{#1}\;?\;{#2} & := & {#3}}
\newcommand{\PruleSpawn}[3]{{#1}\;?\;{#2} & \rightarrow & (\,{#3}\,)}
\newcommand{\Prule}[4]{{#1}\;?\;{#2} & \rightarrow & (\,{#3}\,)\;:=\;{#4}}
\newcommand{\Ppar}[2]{{#1}\,|\,{#2}}
\newcommand{\Pcall}[2]{{#1}\,!\,{#2}}
\newcommand{\Pdef}[2]{{#1}:\,{#2}}
% Translation representation
\newcommand{\transwhere}[3]{& & {\makebox[1.5cm][l]{where}}
{#1}\;?\;{#2}\;\cdot\;(\,{#3}\,)}
\newcommand{\transand}[3]{& & {\makebox[1.5cm][l]{and}}
{#1}\;?\;{#2}\;\cdot\;(\,{#3}\,)}
\newcommand{\F}{Facile}
\newcommand{\Cham}{Chemical Abstract Machine}
\newcommand{\Lc}{$\lambda$--calculus}
\newcommand{\LC}{$\lambda$--Calculus}
\newcommand{\Lx}{$\lambda$--expression}
\newcommand{\Pc}{$\pi$--calculus}
\newcommand{\PC}{$\pi$--Calculus}
\newcommand{\PPC}{Polyadic $\pi$--Calculus}
\newcommand{\PPc}{polyadic $\pi$--calculus}
\newcommand{\RA}{{\em return-address\/} channel}
\newcommand{\Whnf}{weak head--normal form}
% Source representation
\newcommand{\Labs}[2]{\lambda{#1}.\,{#2}}
\newcommand{\Lapp}[2]{{#1}\,{#2}}
\newcommand{\App}[2]{{#1}\,@\,{#2}}
\newcommand{\AppL}[2]{{#1}\,@_L\,{#2}}
\newcommand{\AppE}[2]{{#1}\,@_E\,{#2}}
\newcommand{\Ltriv}{()}
\newcommand{\Lpair}[2]{({#1},{#2})}
% Translation representation
\newcommand{\transexp}[2]{\sembrac{#1}_{#2}}
\newcommand{\transdef}[3]{\transexp{#1}{#2} & = & {#3}}
% End of macros
\begin{document}
\maketitle

\section{Introduction}

Rather than repeat all the previous material, I have started again with the newer styles of translation which I am now using.

First I describe the strategy for reducing the \Lc\ which is to be followed by the translation. This is compared with the earlier strategies discussed.

The bulk of the material is taken directly from a note I produced at ECRC in August 1992. The translation is presented in the \Pc\ and also in a new process formalism which I call {\em object graph rewriting}.

We have been investigating schemes for translating languages using \F\ 
\cite{Facile} concepts into systems of small processes. The ultimate goal
is to exploit the inherent concurrency of the process networks in an implementation
on a parallel machine.

The bulk of the investigation has used process notations which are 
close to the \PPC\ \cite{PolyPi}. Since this notation 
is becoming well know to other researchers, we use it here.
This document 
is an early draft report on the current direction of the work. Various other schemes 
have been considered along the way and are described elsewhere.

This document also introduces a model of communicating agents using process-based, or 
point-to-point, communication. This is in contrast to the channel-based 
communication of CCS \cite{CCS}, and the \Pc\ \cite{Pi}. In fact, the 
model can be seen as a very minimal version of Paragon \cite{Paragon}, 
with a very direct correspondence to the 
graph-rewriting framework in which Paragon has been presented.

The process-communication model results in a very low-level translation of 
\F\ features in which potential implementation data-structures become 
visible. For example, \F\ channels can be 
represented as objects which are manipulated in exactly the same way 
as in the \F\ \Cham\ proposed in \cite{FacileCHAM}.

\subsubsection*{Version 4}

This version is changed a great deal from version 3. It now refers to sequential and call--by--value translations.

\subsubsection*{Version 3}

This revises the document in the light of discussions, posing some more fundamental questions about marked rewriting schemes.

\subsubsection*{Version 2}

This contains more discussion about the process translations, giving the translation scheme and examples of its use.

\subsubsection*{Version 1}

This is the initial release containing many errors no doubt.

\section{\LC\ Questions}

\subsection{\LC\ Syntax}

The language is given by:
\begin{eqnarray*}
e & ::= &  x \mid \Labs{x}{e} \mid \Lapp{e}{e} \\
v & ::= &  \Labs{x}{e}  
\end{eqnarray*}
$v$ is the class of {\Whnf}s for closed terms.

We will begin by being interested just in rewriting closed terms to \Whnf.
The assumption will be that this is the world we are considering. It will be made clear where statements or claims are being made about more general reduction.

\subsection{\LC\ Semantics}
We will define the reduction relation for \Lc\ terms using a set of inference rules.

\subsubsection{Full \LC}
The following rules would apply to full \Lc. We have the $BETA$ rule and a set of rules which allow reduction of a redex in any context:

\begin{center}
\begin{tabular}{lcccl}
$BETA: \:\: (\lambda x.e)\;e' \:{\rightarrow}\: e\,[e'/x]$
& &
$APPL: \:\: {\infer{e \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e''\;e'}
       { }}$
& &
$APPR: \:\: {\infer{e' \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e\;e''}
       { }}$
\end{tabular}

\begin{tabular}{lcl}
$LAMB: \:\: {\infer{e \:{\rightarrow}\: e'}
       {\lambda x.e \:{\rightarrow}\: \lambda x.e'}
       { }}$
\end{tabular}
\end{center}

This reduction relation defines a one--step strategy which allows reduction of any redex. Of course this allows us to choose non--standardizing sequences.

By imposing conditions on the sequences we can get sensible strategies and this can be done in some cases by using different inference rules for identifying redexes. We are rarely going to consider reduction under a $\lambda$ so the $LAMB$ rule will not appear.

\subsubsection{Lazy--\LC}
The following specifies reduction to \Whnf\ using the {\em normal--order} strategy of the lazy--\LC. This has just $BETA$ and the $APPL$
rule:
\begin{center}
\begin{tabular}{lccl}
$BETA: \:\: (\lambda x.e)\;e' \:{\rightarrow}\: e\,[e'/x]$
& &
$APPL: \:\: {\infer{e \:{\rightarrow}\: e''}
       {\Lapp{e}{e'} \:{\rightarrow}\: \Lapp{e''}{e'}}
       { }}$
\end{tabular}
\end{center}

\subsubsection{Eager--\LC}
Adding back the $APPR$ rule gives full \Lc\ but omitting the $LAMB$ rule gives:
\begin{center}
\begin{tabular}{lcccl}
$BETA: \:\: (\lambda x.e)\;e' \:{\rightarrow}\: e\,[e'/x]$
& &
$APPL: \:\: {\infer{e \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e''\;e'}
       { }}$
& &
$APPR: \:\: {\infer{e' \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e\;e''}
       { }}$
\end{tabular}
\end{center}
This allows unrestricted reduction of {\em exposed} redexes, where exposed redexes are those not {\em hidden} by being under a $\lambda$.

\subsubsection{Call--By--Value \LC}
In the following rules, both arguments to an application may be reduced, as before, but a special form of $BETA$ rule is used which insists that the argument is in \Whnf\ before reduction:
\begin{center}
\begin{tabular}{lcccl}
$BETA_v: \:\: (\lambda x.e)\;v \:{\rightarrow}\: e\,[v/x]$
& &
$APPL: \:\: {\infer{e \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e''\;e'}
       { }}$
& &
$APPR: \:\: {\infer{e' \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e\;e''}
       { }}$
\end{tabular}
\end{center}
This is a non-deterministic strategy since operator and operand may be reduced
in either order before beta-reduction.

\subsubsection{Sequential \LC}
The strategy used by programming languages such as SML is call--by--value, but also evaluates arguments strictly left--to--right. This is achieved by a restricted $APPR$ rule which only allows reduction in the second argument of an application once the first has reached \Whnf:
\begin{center}
\begin{tabular}{lcccl}
$BETA_v: \:\: (\lambda x.e)\;v \:{\rightarrow}\: e\,[v/x]$
& &
$APPL: \:\: {\infer{e \:{\rightarrow}\: e''}
       {e\;e' \:{\rightarrow}\: e''\;e'}
       { }}$
& &
$APPR_v: \:\: {\infer{e' \:{\rightarrow}\: e''}
       {v\;e' \:{\rightarrow}\: v\;e''}
       { }}$
\end{tabular}
\end{center}


\section{A Source Language}

For the purpose of investigation we have used a very small language in 
which we can represent all the features of core \F\, along with facilities for 
handling constants and operators as in ML.

\begin{eqnarray*}
e & ::= &  x \mid \Labs{x}{e} \mid \Lapp{e}{e} \mid c \mid () \mid \Lpair{e}{e} 
\end{eqnarray*}

$c$ stands for a constant and $x$ for a variable.
The language is the \Lc\ with constants and pairing. The trivial
value and pairing operator could have been considered as normal constants.

The features of \F\ are encoded in our source language in very much the 
same way as in the sequential and
distributed implementations based on SML \cite{KuoFacile,DistribFacile,MachFacile}.
The functionality is hidden in the definition of the constants $channel$,
$send$, $receive$, and $spawn$.

$channel$ is a function taking a trivial value and returning a channel
value. Every invocation of $channel$ returns a distinct channel value.

The function $send$ takes a pair containing a channel and a value to
be sent on the channel. A trivial value is returned when the output
action has succeeded. The function
has the effect of the SML/\F\ code $({\bf fn}\,(x,y)\,=>\,x!y)$

$receive$ takes a channel as argument and returns a value received as
the result of an input action. It has the
effect $({\bf fn}\,x\,=>\,x?)$.

The essence of \F\ behaviour
expressions is provided by using functions of type $() \rightarrow ()$.
$spawn$ takes such a function and returns a trivial value having
created a process which runs in parallel. The spawned process executes
the behaviour expression  by applying its
representation function to the trivial value,
terminating if the application terminates.

By comparison, the original syntax given for Core \F\ is:
\begin{eqnarray*}
e & ::= & x \mid \Labs{x}{e} \mid \Lapp{e}{e}  \mid {\bf channel} 
  \mid e!e \mid e? \mid {\bf code}(be) \mid {\bf spawn}(be) \\
be & ::= & {\bf terminate}\,\mid\,{\bf activate}\,e\,\mid\,be \| be
\end{eqnarray*}

Although this language provides more programming flexibility, it is sufficient for our implementation experiments to concentrate on the four primitives described above.

% As indicated in \cite{KuoFacile}, \F\ behaviour expressions do not need
% to be represented as a separate class in the source language. Further,
% there is no need for $terminate$ since this can now be represented  by
% $activate\,()$. We can use expression evaluation to spawn parallel
% processes, so there is no need for parallel composition.

\section{Translation to \PPC}

{\em Caveat\/}: Not everything is right in this section. Our previous model which allows
the communication of {\em terms\/} does not map trivially onto the \PPc\ and still
deserves further work. The schemes below are produced by a simple mapping which fails
when pairs of values need to be communicated. A final section outlines a mapping which
addresses these problems.

\subsection{Syntax for the \PPC}

The syntax for the subset of the \PPc\ notation from \cite{PolyPi}
used here is as follows:
\begin{eqnarray*}
p & ::= & \inaction\,\mid\,\inpact{c}{c}{p}\,\mid\,\outact{c}{c}{p}\,\mid\,\parprocs{p}{p}\,\mid\,\restrict{c}{p}\,\mid\,\replicate{X}{p}\,\mid\,\agtuse{A}{\vec{c}}\,\mid\,\agtdef{A}{\vec{c}}{p} \\
\end{eqnarray*}
We adopt the \PPc\ convention of abbreviating the form: $\outact{x}{v}{\inaction}$ to: $\outacta{x}{v}$.
The final two cases are derived forms for defining parametric processes.
We make no use of process sum or match constructs in our present translations.

For those unfamiliar with \cite{PolyPi}, the form $\inpact{c}{c}{p}$ denotes
input of a name on a link, binding the name in parentheses in the following process. $\outact{c}{c}{p}$ denotes synchronous output of a name. $\restrict{c}{p}$ is like the restriction operator of CCS, introducing a new name which is only in scope in the following process. However, the name may
be communicated to other processes, in which case the scope of the name is
extended. $\replicate{X}{p}$ is a replication construct which behave like
an arbitrary number of copies of $p$ composed in parallel. The use of $!$
to introduce replication should not be confused with its use to denote
output in \cite{Facile}.

The main deviation from our previous presentation, apart from change of notation, is the use of $\replicate{X}{p}$ in place of the
form $\recdef{X}{p}$. In \cite{PolyPi} the unfolding of a replication is not considered a reduction
but is a law of the structural congruence. All our uses of replication involve guarded processes, so 
from an operational point of view we will consider that replications are only unfolded immediately
before communication.

\subsection{Translation of the Source Language}

We present the translation of \F\ using channel-based communication.
This allows communication of tupled values, but only an asynchronous form of
communication is required in which all output actions are followed by inaction. 
The operation of the translated process network has been discussed in \cite{ProcsMagic}.

The scheme is closely related to the call-by-value translation of the \Lc\ reported in \cite{FunAsProcs}.
A difference is that evaluation of an application is sequential, as in ML: the function is evaluated to an
abstraction; then the argument is evaluated; and finally the function is applied to the argument. Side effects will be deterministic (in
some sense).

The full translation scheme is:
\begin{eqnarray*}
\transdef {x}{u} {\outacta{u}{x}} \\
\transdef {c}{u} {\outacta{u}{c}} \\
\transdef {\Ltriv}{u} {\outacta{u}{\triv}} \\
\transdef {\Labs{x}{e}}{u} {\restrict{y} {\parprocs {\outacta{u}{y}} {\guardedrep{X} {\inpacta{y}{\pair{b}{x}}} {\transexp{e}{b}} }}} \\
\transdef {\Lapp{e}{e'}}{u} {\restrict{a}{\parprocs {\transexp{e}{a}} {\inpact{a}{y} {\restrict{b}{\parprocs{\transexp{e'}{b}}{\inpact{b}{z} {\outacta{y}{\pair{u}{z}}}}}}}}} \\
\transdef {\Lpair{e}{e'}}{u} {\restrict{a}{\parprocs {\transexp{e}{a}} {\inpact{a}{y} {\restrict{b}{\parprocs{\transexp{e'}{b}}{\inpact{b}{z} {\outacta{u}{\pair{y}{z}}}}}}}}}
\end{eqnarray*}

The scheme here differs from previous schemes in a very minor way; the order of the pair of values
sent to an abstaction by the code for an application has been reversed. This seems to give
a more pleasing appearance to the translation, and ensures that the \RA,
given to all abstractions, is in a fixed position.

All uses of replication have the form $\guardedrep {X} {\inpacta{c}{\vec{v}}} {p}$.
We will later represent this as $\agtuse {A} {\vec{n}}$ with a definintion 
$\agtdef {A} {\vec{n}} {\inpact{c}{\vec{v}} ({\parprocs {p} {\agtuse {A} {\vec{n}}}) }} $  where $\vec{n}$ are the free
names of $\inpact {c} {\vec{v}} {p}$, the body of the replication. I believe Bent's
result easily shows that these are equivalent.

\begin{assignment}{Zurab}
Restricting attention to the \Lc\ subset of the language above, show that the translation is correct in the same way as Milner's call--by--value translation. You will notice that this scheme is active, generating output when a term reaches \Whnf.
\end{assignment}

\subsection{Representation of Arithmetic Operations and \F\ Features}

We now show how the arithmetic operators are handled. A binary
operator like $mul$, the prefix form of multiplication, equivalent to
$(\,{\bf op}\,*\,)$ in ML, takes a pair as argument. The operators
are special forms of abstractions:
\begin{eqnarray*}
\transdef{succ}{u} {\restrict{y} {\parprocs {\outacta{u}{y}} {\guardedrep{X} {\inpacta {y} {\pair{b}{x}}} {\outacta{b}{(x+1)}} } }} \\
\transdef{mul}{u} {\restrict{y} {\parprocs {\outacta{u}{y}} {\guardedrep{X} {\inpacta {y} {\pair{b}{\pair{x}{z}}}} {\outacta{b}{(x*z)}} } }}
\end{eqnarray*}

\subsection{An Example}

The following is the translation of the expression $(Mul(3,4),())$. The correspondence with the translation scheme may be a little unclear as we have transformed replication to parametric definitions. The $Read$ process receives the result and prints it.
\begin{eqnarray*}
& & \restrict {a b c d e} {\parprocs {\parprocs {\parprocs {\parprocs {\outacta {d}{e}} {A( e )}} {B( d, b )}} {C( b, c, a )}} {Read( a )}} \\
Read( f ) & = &\inpact {f}{g} {Print( g )} \\
A( e ) & = &\inpact {e}{\pair{h}{i}} {D( h, i, e )} \\
B( d, b ) & = &\inpact{d}{j}{E( j, b )} \\
C( b, c, a ) & = &\inpact{b}{q}{J( c, a, q )} \\
D( h, i, e ) & = &( \parprocs {Mul( h, i )} {A( e )} ) \\
E( j, b ) & = &\restrict {k l m} {\parprocs{F( k, j, b )} {\parprocs {\outacta{l}{3}} {G( l, m, k )} } } \\
F( k, j, b ) & = &\inpact {k}{n}{\outacta{j}{\pair{b}{n}} } \\
G( l, m, k ) & = &\inpact {l}{o} {H( m, k, o )} \\
H( m, k, o ) & = &( \parprocs {\outacta{m}{4}} {I( m, k, o )} ) \\
I( m, k, o ) & = &\inpact{m}{p} {PairB( k, o, p )} \\
J( c, a, q ) & = &( \parprocs {\outacta {c} {\triv}} {K( c, a, q )} ) \\
K( c, a, q ) & = &\inpact{c}{r}{PairB( a, q, r )} \\
Mul(b, y) & = &{\inpact {y} {\pair{b}{\pair{x}{z}}} {\outacta{b}{(x*z)}} } \\
PairB(b, x, y) & = & {\outacta {u} {\pair{x}{y}}}
\end{eqnarray*}

\subsection{Representation of \F\ Features}

\F\ channels will be implemented using a \Pc\ name introduced by the function $channel$.
Sending and receiving of messages is done using functions similar to those in
the current \F\ implementation. As stated above, the function $send$
has the effect $({\bf fn}\,(x,y)\,=>\,x!y)$ while $receive$ has the
effect $({\bf fn}\,x\,=>\,x?)$.  These functions are applied to the
appropriate expressions to achieve the effect of the \F\
primitives. Hence $e!e'$ becomes $(({\bf fn}\,(x,y)\,=>\,x!y)\,(e,e'))$
and $e?$ becomes $(({\bf fn}\,x\,=>\,x?)\,e)$.  The resulting encoding
of the communication primitives is:
\begin{eqnarray*}
\transdef{channel}{u} {\restrict{y} {\parprocs {\outacta{u}{y}} {\guardedrep{X} {\inpacta{y} {\pair{b}{\triv}}} {\restrict{c}{\outacta{b}{c}}} } }} \\
\transdef{send}{u} {\restrict{y} {\parprocs {\outacta{u}{y}} {\guardedrep{X} {\inpacta{y} {\pair{b}{\pair{c}{v}}} } {\outacta{c}{\pair{b}{v}}} } }} \\
\transdef{receive}{u} {\restrict{y} {\parprocs {\outacta{u}{y}} {\guardedrep{X} {\inpacta{y} {\pair{b}{c}}} {\inpact{c} {\pair{z}{v}} {(\parprocs {\outacta{b}{v}} {\outacta{z}{\triv}})}} } }} 
\end{eqnarray*}

The implementation of communication deserves some explanation. 
$send$ is given the 
identity of the channel and a value to transmit.
It outputs on the channel a pair, the first element of which is its own \RA, and 
the second is the value to be sent. $receive$ takes
in this pair and returns the value on its \RA. It also sends a trivial value on 
the \RA\ for the $send$ which was passed to it.
This has the desired effect of triggering the continuation of the $send$.

$spawn$ takes a function as argument and applies it in parallel with returning 
a trivial value to its caller. The spawned function is passed a \RA\ and a trivial value as argument.
For tidiness, we receive the result of the spawned function, if any, on the \RA:
\begin{eqnarray*}
\transdef{spawn}{u} {\restrict{y} {\parprocs {\outacta{u}{y}} {\guardedrep{X} {\inpacta{y}{\pair{b}{f}}} {(\;\parprocs {\outacta{b}{\triv}} {\restrict{c} {\parprocs {\outacta {f} {\pair{c}{\triv}}} {\inpacta {c} {\triv}} }\;)} }}}}
\end{eqnarray*}

For each of these constant functions it would be possible to assign a single
global channel.
The translation of such a function would just send back the channel name
on $u$. A single copy of the recursive code would then pick up any 
attempt to use the function. For example the translation of a function like $send$
might be:
\begin{eqnarray*}
\transdef{ send }{u} {\outacta {u} {send}}
\end{eqnarray*}

and a program using $send$ would be evaluated in a context:
\begin{eqnarray*}
\restrict{u} {\restrict{send} {\parprocs {\transexp{P}{u}} {\guardedrep{X} {\inpacta {send} {\pair{b}{\pair{c}{v}}} } {\outacta{c}{\pair{b}{v}}} } }}
\end{eqnarray*}

\subsection{Accounting for Variable-Sized Arguments}

It will be clear that the arity of the communications representing arguments and results to functions
will depend on the type. This also applies to the values communicated by $send$ and $receive$. 
The translation we have given assumes that the arity is always one.
A correct translation using the \PPc\ will generate versions of the code according to the type. General forms can be described as follows using notation $\vec{x}$ for transmission or reception of zero or more names. The arity, $|\vec{x}|$, can be determined statically in each case:
\begin{eqnarray*}
\transdef {c}{u} {\outacta{u}{\vec{c}}} \\
\transdef {\Labs{x}{e}}{u} {\restrict{y} {\parprocs {\outacta{u}{y}} {\guardedrep{X} {\inpacta{y}{\pair{b}{\vec{x}}}} {\transexp{e}{b}} } }} \\
\transdef {\Lapp{e}{e'}}{u} {\restrict{a}{\parprocs {\transexp{e}{a}} {\inpact{a}{y} {\restrict{b}{\parprocs{\transexp{e'}{b}}{\inpact{b}{\vec{z}} {\outacta{y}{\pair{u}{\vec{z}}}}}}}}}} \\
\transdef {\Lpair{e}{e'}}{u} {\restrict{a}{\parprocs {\transexp{e}{a}} {\inpact{a}{\vec{y}} {\restrict{b}{\parprocs{\transexp{e'}{b}}{\inpact{b}{\vec{z}} {\outacta{u}{\pair{\vec{y}}{\vec{z}}}}}}}}}} \\
\transdef{send}{u} {\restrict{y} {\parprocs {\outacta{u}{y}} {\guardedrep{X} {\inpacta{y}{\pair{b}{\pair{c}{\vec{v}}}}} {\outacta{c}{\pair{b}{\vec{v}}}} } }} \\
\transdef{receive}{u} {\restrict{y} {\parprocs {\outacta{u}{y}} {\guardedrep{X} {\inpacta{y} {\pair{b}{c}}} {\inpact{c} {\pair{z}{\vec{v}}} {(\parprocs {\outacta{b}{\vec{v}}} {\outacta{z}{\triv}} )} } } }}
\end{eqnarray*}

\section{Translation using Process-Based Communication}

In this section we introduce an alternative translation method based on communication with named processes.
We develop a very simple and highly restrictive model. The model has adequate expressive power for our
purposes, but might not seem attractive for general purpose use.

\subsection{An Informal Description of a Process Model}

% Well, I'm not sure this is the right way to put it but:
The process model manipulates a world of terms forming a many-sorted algebraic struicture:
\begin{itemize}
\item Terms are built up from primitive data values, including a domain of process names, and constructor symbols with fixed arities.
\item A process is a term, holding all the process state, and an associated name.
\item Messages are terms and are directed to named processes.
\end{itemize}
Process names are almost pointers to terms, hence the representation of a process network is 
only a step away from a directed-graph representation. Polymorpic typing should be possible. 

The behaviour of processes is determined by pattern-directed rules which describe what happens when a message is received by a process:
\begin{itemize}
\item Patterns are left-linear open terms: they may contain variables, but variables may not be repeated.
\item Matching of rules is based on two patterns: The sets of variables in the two patterns are disjoint. Neither pattern may be a solitary 
variable, hence every pattern has at least a root symbol.
\item The first pattern of a rule matches the state of the process, the other matches
the incoming message. Pattern variables are bound to corresponding subterms during matching.
\item Every message sent to a process must match exactly one rule.
\item Actions are performed when a rule is matched, substituting values of bound variables in the normal way.
Rules contain no free variables.
\end{itemize}
The condition that a process must handle every incoming message avoids the implication that an implementation might need to store 
messages and retry them later if the process state changes. An alternative semantics 
would be for unmatched messages to be discarded.
Also, the requirement that exactly one rule is matched avoids the need to
specify the semantics of overlapping rules. We are confident that 
pattern matching could be translated into nested match operations in
which case the potential non-determinism would become clear.

When a message is received:
\begin{itemize}
\item A process may create new terms.
\item A process may create new processes and has access to their names.
\item A process may send messages to processes it can name.
\item A process may copy the name of a process it can name. Hence it can send such names to other processes.
\item A process may change its own state. The process name subsequently refers to the new state.
\item A process may not inspect the state of another process.
\end{itemize}

\subsection{Syntax and Informal Semantics}
In the proposed syntax, lower-case identifiers are bound variable names. Other identifiers are constructor symbols.
The most general form for a rule is a pair of patterns, followed by actions
to be performed if a process whose state matches the first pattern receives a message matching the second pattern:
\begin{eqnarray*}
\Prule {ProcState} {MsgPattern} {(Action \cdots Action)} {NewState} \\
\end{eqnarray*}
The actions are zero or more process creations,
zero or more message creations, and an optional revised state for the process.
The syntax $\Pcall {p} {Msg}$ denotes sending a message to a named process, 
while $\Pdef {p} {InitState}$ creates a process with an initial state. 

Processes might be better called objects since they only act when messages are sent to them. When a message arrrives at a process at least one rule should
match the pattern for the process state and the pattern for the message. For the moment we will assume that exactly one rule matches.

We will require that one message is handled completely by a process before
another message is considered. This is very conservative: if a process involves no state change there should be no need for such serialisation; if a process does involve a state change then once all new terms and processes referenced in the new state have been created, and the state has been changed, then other
messages could be handled

Notionally, at least, the actions all occur simultaneously, however, in
practice there are some dependencies:
\begin{itemize}
\item Any new processes and terms are built.
\item The process state is changed if required.
\item Sending of any messages is initiated.
\end{itemize}
Clearly it would be meaningless for any messages sent as a result of invoking
a rule to be processed before processes and terms they reference have been created.

\subsection{Some Examples}

As a first example we will address the hardest case which occurs in the translation of the source 
language given earlier.
This concerns communication which is the only language feature requiring synchronisation. 

The chosen representation of a \F\ channel is exactly like that in the \F\ \Cham\ of \cite{FacileCHAM}.
The state of a channel holds a queue of pending output offers and a queue of pending input requests.
At least one of the queues will be empty.

A channel receives input and output requests and either satisfies the request or queues it. Requests contain
continuations in the form of process names. Hence a receiver sends an $In(r)$ message with the identity of the process to handle the received message. Senders  send $Out(v,s)$ where $v$ is the value to be output and $s$ a process to receive acknowledgement that the communication has succeeded.
Messages are sent to both sender and receiver when
a communication is closed.
\begin{eqnarray*}
\PruleChange {Chan(iq,NOQ)} {In(r)} {Chan(IQ(iq,r),NOQ)} \\
\PruleChange {Chan(NIQ,oq)} {Out(v,s)} {Chan(NIQ,OQ(oq,v,s)} \\
\Prule {Chan(iq,OQ(oq,v,s))} {In(r)} {\Ppar {\Pcall {r} {v}} {\Pcall {s} {Triv}}} {Chan(iq,oq)} \\
\Prule {Chan(IQ(iq,r),oq)} {Out(v,s)} {\Ppar {\Pcall {r} {v}} {\Pcall {s} {Triv}}} {Chan(iq,oq)} \\
\end{eqnarray*}

It is synchronisation of concurrent computations which requires state changes. Here is a program to sum the squares of two numbers using a continuation-passing technique:
\begin{eqnarray*}
\PruleSpawn {Sqr} {Args(res,n)} {\Pcall {res} {Int(n*n)}} \\
\PruleSpawn {Add} {Args(res,x,y)} {\Pcall {res} {Int(x+y)}} \\
\PruleSpawn {SumSq} {Args(res,x,y)} {\Ppar {\Pdef {a} {Sqr}} {\Ppar {\Pdef {b} {YSqr(res,y)}} {\Pcall {a} {Args(b,x)}}}} \\
\PruleSpawn {YSqr(res,y)} {Int(xsq)} {\Ppar {\Pdef {m} {Sqr}} {\Ppar {\Pdef {s} {Sum(res,xsq)}} {\Pcall {m} {Args(s,y)}}}} \\
\PruleSpawn {Sum(res,xsq)} {Int(ysq)} {\Ppar {\Pdef {a} {Add}} {\Pcall {a} {Args(res,xsq,ysq)}}} \\
\PruleSpawn {Start} {Triv} {\Ppar {\Pdef {s} {SumSq}} {\Ppar {\Pdef {p} {Print}} {\Pcall {s} {Args(p,5,12)}}}} \\
\end{eqnarray*}
The program is started by sending a message to a process whose state is $Start$. Of course, in a serious
implementation we would not create a process for simple operations like $Sqr$ and $Add$.

If we want to perform the multiplications in parallel, we then have to collect the two products, which could arrive in either order, and then form the sum. The following technique can be used:
\begin{eqnarray*}
\PruleSpawn {Sqr(r,s)} {Arg(n,L)} {\Pcall {r} {Arg(n*n,s)}} \\
\PruleChange {Add(r,s)} {Arg(x,L)} {AddL(r,s,x)} \\
\PruleChange {Add(r,s)} {Arg(y,R)} {AddR(r,s,y)} \\
\PruleSpawn {AddL(r,s,x)} {Arg(y,R)} {\Pcall {r} {Arg(x+y,s}} \\
\PruleSpawn {AddR(r,s,y)} {Arg(y,L)} {\Pcall {r} {Arg(x+y,s}} \\
\PruleChange {AddL(r,s,x)} {Arg(v,L)} {Clash} \\
\PruleChange {AddR(r,s,y)} {Arg(v,R)} {Clash} \\
\PruleSpawn {SumSq(r,s)} {Args(x,y)} {\Ppar {\Pdef {a} {Add(r,s)}} {\Ppar {\Pdef {l} {Sqr(a,L)}} {\Ppar {\Pdef {r} {Sqr(a,R)}} {\Ppar {\Pcall {l} {Arg(x,L)}} {\Pcall {r} {Arg(y,L)}} }}}} \\
\PruleSpawn {Start} {Triv} {\Ppar {\Pdef {p} {Print}} {\Ppar {\Pdef {s} {SumSq(p,L)}} {\Pcall {s} {Args(5,12)}}}} \\
\end{eqnarray*}
This is not a very illuminating example, but in fact it reflects the sort of processing required in dataflow computing.
For consistency, we should have encoded $SumSq$ in the same way as $Add$.

\section{Translation Scheme}

For the translation scheme targetted at the model with channel-based communication, 
the traslation was 
parameterised with a characteristic channel to which the
generated process network should send a value. The value sent on the characteristic 
channel was a channel name in 
the case of an abstraction. In the case of a constant, the value itself was sent.

Inspection of the scheme shows that each such characteristic channel is associated with a 
particular process and is used only once. The exception to this rule occurs in the case of 
modelling \F\ communication. A similar violation of the rule occurs if call-by-value 
evaluation is programmed.

For the new translation, communication is to processes. Hence the parameter to the 
translation of a syntactic form will be the name of the process to which a result 
is to be sent. In the translation, we will make use of a function $fv()$ which 
will yield a list of the free variables in a \Lx. 

\subsection{Translation of the Source Language}
The translation of a syntactic construct creates some actions which will
form part of the body of a rule, and may also introduce new constructor
symbols and associated rules:
\begin{eqnarray*}
\transdef {x}{u} {\Pcall {u} {Unit(x)}} \\
\transdef {c}{u} {\Pcall {u}{Unit(c)}} \\
\transdef {\Ltriv}{u} {\Pcall {u} {Triv}} \\
\transdef {\Labs{x}{e}}{u} {\Ppar {\Pcall {u} {Unit(y)}} {\Pdef {y} {Y(fv(\Labs{x}{e}))}}} \\
\transwhere {Y(fv(\Labs{x}{e}))} {Doub(b,x)} {\transexp{e}{b}} \\
\transdef {\Lapp{e}{e'}}{u} {\Ppar {\transexp{e}{a}} {\Pdef {a} {A(u,fv(e'))}} } \\
\transwhere {A(u,fv(e'))} {Unit(y)} {\Ppar {\Pdef {b} {B(u,y)}} {\transexp{e'}{b}} } \\
\transand {B(u,y)} {Unit(z)} {\Pcall {y} {Doub(u,z)} } \\
\transdef {\Lpair{e}{e'}}{u} {\Ppar {\transexp{e}{a}} {\Pdef {a} {A(u,fv(e'))}} } \\
\transwhere {A(u,fv(e'))} {Unit(y)} {\Ppar {\Pdef {b} {B(u,y)}} {\transexp{e'}{b}} } \\
\transand {B(u,y)} {Unit(z)} {\Pcall {u} {Doub(y,z)} } \\
\end{eqnarray*}
All the constructor names introduced are distinct. All the process names are distinct
and are different from all the variables used in the source \Lx, with the exception of $x$ in the
translation of an abstraction which stands for itself.

The translation of the various constant functions for arithmetic and the operators of \F\ is as follows:
\begin{eqnarray*}
\transdef {succ}{u} {\Ppar {\Pcall {u} {Unit(f)}} {\Pdef {f} {Succ}} } \\
\transwhere {Succ} {Doub(b,x)} {\Pcall {b} {Unit(x+1)}} \\
\transdef {mul}{u} {\Ppar {\Pcall {u} {Unit(f)}} {\Pdef {f} {Mul}} } \\
\transwhere {Mul} {Doub(b,Pair(x,y))} {\Pcall {b} {Unit(x*y)}} \\
\transdef {channel}{u} {\Ppar {\Pcall {u} {Unit(f)}} {\Pdef {f} {Channel}} } \\
\transwhere {Channel} {Doub(b,Triv)} {\Ppar {\Pcall {b} {Unit(c)}} {\Pdef {c} {Chan(NIQ,NOQ)}} }\\
\transdef {send}{u} {\Ppar {\Pcall {u} {Unit(f)}} {\Pdef {f} {Send}} } \\
\transwhere {Send} {Doub(b,Pair(c,v))} {\Pcall {c} {Out(v,s)}} \\
\transdef {receive}{u} {\Ppar {\Pcall {u} {Unit(f)}} {\Pdef {f} {Receive}} } \\
\transwhere {Receive} {Doub(b,c)} {\Pcall {c} {In(b)}} \\
\transdef {spawn}{u} {\Ppar {\Pcall {u} {Unit(f)}} {\Pdef {f} {Spawn}} } \\
\transwhere {Spawn} {Doub(b,p)} {\Ppar {\Pcall {b} {Unit(Triv)}} {{\Ppar {\Pcall {p} {Doub(Triv,s)}} {\Pdef {s} {Sink}} } } }\\
\transand {Sink} {Unit(Triv)} {} \\
\end{eqnarray*}
The rules for $Chan$ were given earlier.

It should be noted that the types are not really correct here; a typed source language is required, as before. However,
the constructors used correctly reflect the arities of the terms.

\subsection{An Example}

The following is the translation of the expression $(Mul(3,4),())$ under the new scheme:
\begin{eqnarray*}
\PruleSpawn {{\bf Start}} {{\bf Triv}} {\Ppar {\Pdef {d} {B(a)}} {\Ppar {\Pdef {c} {D(d)}} {\Ppar {\Pcall {c} {{\bf Unit}(b)}} {\Ppar {\Pdef {b} {{\bf Mul}}} {\Pdef {a} {{\bf Print}}}}}}} \\
\PruleSpawn {A(a,e)} {{\bf Unit}(f)} {\Ppar {\Pdef {g} {{\bf PairB}}} {\Pcall {g} {{\bf Trip}(a,e,f)}}} \\
\PruleSpawn {B(a)} {{\bf Unit}(e)} {\Ppar {\Pdef {h} {A(a,e)}} {\Pcall {h} {{\bf Unit}({\bf Triv})}}} \\
\PruleSpawn {C(d,i)} {{\bf Unit}(j)} {\Pcall {i} {{\bf Doub}(d,j)}} \\
\PruleSpawn {D(d)} {{\bf Unit}(i)} {\Ppar {\Pdef {l} {C(d,i)}} {\Ppar {\Pdef {k} {F(l)}} {\Pcall {k} {{\bf Unit}(3)}}}} \\
\PruleSpawn {E(l,m)} {{\bf Unit}(n)} {\Ppar {\Pdef {o} {{\bf PairB}}} {\Pcall {o} {{\bf Trip}(l,m,n)}}} \\
\PruleSpawn {F(l)} {{\bf Unit}(m)} {\Ppar {\Pdef {p} {E(l,m)}} {\Pcall {p} {{\bf Unit}(4)}}} \\
\PruleSpawn {Mul} {Doub(b,Pair(x,y))} {\Pcall {b} {Unit(x*y)}} \\
\PruleSpawn {PairB} {Trip(u,x,y)} {\Pcall {u} {Unit(Pair(x,y))}}
\end{eqnarray*}
This translation is a lot shorter than the previous one, and involves fewer reduction steps.

We repeat the previous example for comparison:
\begin{eqnarray*}
& & \restrict {a b c d e} {\parprocs {\outacta {d} {e}} {\parprocs {A(e)} {\parprocs {B(d, b)} {\parprocs {C(b, c, a)} {{\bf Read}(a)}}}}} \\
{\bf Read}(f) & = & \inpact {f} {g} {{\bf Print}(g)} \\
A(e) & = & \inpact {e} {\pair {h} {i}} {D(h, i, e)} \\
D(h, i, e) & = & (\parprocs {{\bf Mul}(h, i)} {A(e)}) \\
B(d, b) & = & \inpact {d} {j} {E(j, b)} \\
E(j, b) & = & \restrict {k l m} {\parprocs {F(k, j, b)} {\parprocs {\outacta {l} {3}} {G(l, m, k)}}} \\
F(k, j, b) & = & \inpact {k} {n} {\outacta {j} {\pair {b} {n}}} \\
G(l, m, k) & = & \inpact {l} {o} {H(m, k, o)} \\
H(m, k, o) & = & (\parprocs {\outacta {m} {4}} {I(m, k, o)}) \\
I(m, k, o) & = & \inpact {m} {p} {{\bf PairB}(k, o, p)} \\
C(b, c, a) & = & \inpact {b} {q} {J(c, a, q)} \\
J(c, a, q) & = & (\parprocs {\outacta {c} {{\bf Triv}}} {K(c, a, q)}) \\
K(c, a, q) & = & \inpact {c} {r} {{\bf PairB}(a, q, r)} \\
Mul(b, y) & = &{\inpact {y} {\pair{b}{\pair{x}{z}}} {\outacta{b}{(x*z)}} } \\
PairB(b, x, y) & = & {\outacta {u} {\pair{x}{y}}}
\end{eqnarray*}

\section{Implementation of the Process-Based Communcation Model}

This section gives some rather random notes on how the second model
might be implemented. Much of the discussion is about seqeuntial
implementation. My feeling is that it would be quite possible to make a
perfectly  reasonable, even good, {\em sequential\/} implementation of
a functional language with the features of \F\ using this model. I
think there is reason to think it would be suitable for parallel
implementation as well.

\subsection{Optimisation}

Many of the rules in the automatically generated code create a process
and immediately send it a message. Since most generated rules only
match  one pattern each, it is possible to expand them out and build
rules with larger numbers of actions.

Most of the code is inherently sequential, so it should reduce to
somthing corresponding to normal expression evaluation.

\subsection{Processing Messages}

The rules are like very primitive methods in an object-oriented model.
Hence the processing of a message is a bit like a procedure call. The
symbol at the head of the term giving the process state is like the
function to be called, with the pattern specifying a case switch to
determine which code is executed.

The symbol at the head might become a code pointer for the routine to
execute, or a huge case statement might be compiled.

All the state of a process is in its term representation. There is no
environment to worry about.

Incoming messages are generally small, so the data might often be held
in registers.

To lock a process to prevent handling of multiple messages, the head
symbol can be changed to trap arrival of further incoming messages.
In general,
I expect interrupts and exceptions to set flags which are tested when
the process network is in a
consistent state, rather than have the possibility of interrupting threads
of control on one processor. However, for a shared memory implementation
it is necessary to consider some locking.

If the actions of a rule generate no messages, a thread of control
terminates. See the first two rules for $Chan$ and the rule $Sink$.

If the actions of a rule generate one message, a sequential thread
continues. The new message can be prepared and control jumps to the
code indicated by the symbol of the target process.

If the actions of a rule generate multiple messages, additional threads
of control are created. See the last two rules for $Chan$ and code for
$spawn$. On a single processor, a stack-based implementation would have
the effect of remembering the work to be done, and returning to it when
the current thread completes (possibly because an attempted
communication blocks). The advantage is that no record of the thread
needs to be placed on a run queue of some sort. With a parallel
machine, the problem is that this potential work is not available for
evaluation on other processors.

There is no need to use a stack at all if messages representing new
threads are created as heap objects a placed on a rudimentary run
queue. Of course, the run queue often {\em is\/} a stack, but would be
composed of heap objects. Since the number of such messages may be a
small proportion of all messages, the cost of creating these very
simple thread descriptors may be acceptable.

\subsection{Parallel Execution}

For parallel execution it is important to consider how code references
are communicated and how code is distributed.

A first assumption is that all the code for a program is present on all
processors. Demand-based distribution of code seems likely to be
complicated and inefficient, since it can be assumed that functions
executed many times are likely to execute on every processor.

It may be possible to arrange for code to be at the same virtual
addresses on every processor so that no transformation is required. If
not, use of a jump table based on the head symbol of the process state
seems the most practical approach.

I do not have sophisticated proposals for load balancing. I tend to
favour the simple ZAPP model \cite{ZAPP}. Under this approach transfer
of work only  takes place when a lightly-loaded processor requests it
from its neighbours (according to whatever connection topology is in
use). Processors try to steal work if their load is below an import
threshold. They permit work to be stolen if their load is above an
export threshold. The export threshold is set some way above the import
threshold to provide some hysteresis in the system. The main effect of
this strategy is that once all processors have a reasonable load, no
time is wasted in load balancing and most work remains local to the
processor which created it.

In our system, this might mean using a simple test in the code for
$spawn$ which would cause the evaluator to decide whether to plant new
threads in the run queue or to stack them. It would stack them when it
was either lightly loaded (and not prepared to export work) or when it
already had a good number  of threads stacked (and therefore has plenty
to satisfy any request from outside). In the latter case, planting
threads in the run queue would resume when threads were stolen by other
processors.

It would probably be
easiest to start with a stackless implementation since then the procedure
for handling all messages is the same. With a stack in use there would
be the chance for a quick entry to the code for a process which bypasses
the code for unpacking the incoming message. However, if there is no
stack, ther probably needs to be more than one run queue, since threads
corresponding to unstarted spawned processes may need to be available for export.

Exporting work introduces inter-processor references and a host of issues.
For garbage collection it is necessary to know where in a structure the references reside. The same information can be used when exporting structures.
I envisage compiling code for each datastructrure to be used within garbage collection, and if the object needs to be exported, needs to contin or be  the target of inter-processor references. Many details need to be worked out in this area.

\subsection{Memory Management}
Memory management in a parallel implementation will require us to keep track of
inter-processor references, as already mentioned. This can be done by having a
system of indirection nodes which contain all such references. There is the obvious
problem of garbage collecting structures which straddle machine boundaries, but
we can probably arrange that only references to channel objects need to be considered.
These would have to be garbage collected separately using a distributed scheme. There
do not appear to be obvious winners in the search for such schemes.

\subsection{Active Messages}
The link with active messages \cite{AM} is that the handling of one of our internal messages
is very similar to the handling of an active message. The main issue to consider is
that attempts to allocate memory could cause a garbage collection, which is not acceptable in an interrupt routine. Hence we may need to classify incoming
messages into those which can be done at interrupt time, and those which must
add a thread to the run queue for later handling.


\begin{thebibliography}{GPM89}

%\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 2, p159-174. (1984) 

\bibitem[{BuSl92}]{ZAPP}
F. W. Burton \& M.R. Sleep:
{\em A Zero Assignment Parallel Processor},
Conference on Functional Languages and Computer Architecture,
(1982)..

\bibitem[{ECGS92}]{AM}
T. v Eicken, D.E. Culler, S.C. Goldstein \& K.E. Schauser,
{\em Active Messages: a Mechanism for Integrated Communication and
Computation},
International Symposium on Computer Architecture '92, ACM. (1992).

%\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[{GLT91}]{SemaPaper}
J. Glauert, L. Leth \& B. Thomsen: 
{\em A New Process Model for Functions},
Semagraph, 1991.

\bibitem[{GPM89}]{Facile}
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[{Parle92}]{Paragon}
P. Anderson, D. Bolton \& P. Kelly:
{\em Paragon Specifications: Structure, Analysis and Implementation}, 
Proc PARLE'92. LNCS 605. June 1992. (1992) 

\bibitem[{GLT92}]{ProcsMagic}
J. Glauert, L. Leth \& B. Thomsen:
{\em Process Models for Functions},
MAGIC Note 25. March 1992. (1992) 

%\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[{Kna91}]{MachFacile}
F. Knabe:
{\em A distributed protocol for the generalized select command},
MAGIC Note 11, July 1991. (1991)

\bibitem[{KC91}]{DistribFacile}
A. Kramer \& F. Cosquer:
{\em Distributing Facile},
MAGIC Note 12. October 1991. (1991) 

\bibitem[{Kuo92}]{KuoFacile}
Kuo, T.-M.:
{\em Magic Facile version 0.3},
MAGIC Note 22, March 1992. (1992)

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

\bibitem[{LT92}]{FacileCHAM}
L. Leth \& B. Thomsen:
{\em Some Facile Chemistry},
ECRC Technical Report ECRC-92-14. May 1992. (1992) 

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

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

\bibitem[{Mil91}]{PolyPi}
R. Milner: 
{\em The \PPC: A Tutorial},
Technical Report ECS-LFCS-91-180, Edinburgh University, October 1991. (1991)

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

\end{thebibliography}

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