\documentstyle[12pt,twoside,ueareport]{article}

\ueareportno{SYS-C95-ZZ}
\ueatitle{Catalogue of Small Process Translation Schemes}
\ueaauthor{J.R.W. Glauert}

\title{A Catalogue of Small Process Translation Schemes}

\author{J.R.W. Glauert \\
{\em  jrwg@sys.uea.ac.uk} \\
School of Information Systems,  \\
University of East Anglia,  \\
NORWICH NR4 7TJ, UK}

\input{procmacros}

\newcommand{\newc}[1]{\def{{\x#1}x}{Hello}}

% details: a new list environment
% Could be better!
\def\detailslabel#1{\makebox[3.5cm][l]{\bf #1:}}
\def\details{\list{}{\setlength{\leftmargin}{2cm}\let\makelabel\detailslabel}}
\let\enddetails\endlist


\begin{document}

\maketitle

\section{Introduction}

\newc{k}
%\kx

\end{document}
This document is a catalogue of schemes developed by various people to translate the \LC\ with various extensions to small process notations such as the \PC\ and our newer \PPC.

We aim to present the translations in their original formulation, but also use a standard process notation similar to the  \Pc\ of Milner,
Parrow, and  Walker.

A number of translations obey the restriction of
Honda and Tokoro in which asynchronous communication models are derived by
insisting that output actions are followed by inaction ({\em tail communication}).

In the translations below, the binary application operator combining
$\lambda$-terms is made explicit and a subscript L, V, or S is added
to indicate lazy, call-by-value, or sequential evaluation
respectively. Hence the operators are $@_{L}$, $@_{V}$, and $@_{S}$.

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. Since data values may appear as arguments, they must
behave like abstractions.

Both call-by-value and sequential versions of binary operations are
supported by some schemes. The examples are labelled $Mult_V$ and
$Mult_S$.  Curried versions of the operations can be produced using
suitable $\lambda$--expressions. For example, for the binary operation
$Mult_V$ we can make the curried version
${\lambda}x.{\lambda}y.Mult_V(x,y)$.

For some translations, an expression will automatically yield the
result on its interface channel.  Other translations expect to receive
a result channel before execution takes place. The result will then be
returned on this channel. We describe briefly the characteristics of the translation.

We assume that a program yields a data value as result. For some
schemes it is necessary to add some process structure to extract this
value, using an agent $Print$ to display the final result.  For this
purpose, a rule for translating a whole program is given.


\section{Translation Schemes}

\subsection{Milner's Original Lazy \PC\ Scheme}

\begin{details}
\item [Name] OrigLazy
\item [Origin] Lazy \LC\ translation from Milner's {\em Functions As Processes}.
\item [Syntax] Standard \Lc. No constants or operators.
\item [Semantics] Standard lazy \Lc.
\item [Operation] Abstraction expects argument then result channel. Variable identity communicated to result channel.
\item [Implementation] Uses synchronous communication, so not implemented.
\end{details}

\begin{eqnarray*} 
\sembrac{ x }_u & = & x!u\,.\,() \\ 
\sembrac{ {\lambda}x.M }_u & = & u?x\,.\,u?v\,.\,\sembrac{M}_v \\
\sembrac{ @_{L} 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*}


\subsection{Milner's Original Strict \PC\ Scheme}

\begin{details}
\item [Name] OrigStrict
\item [Origin] Strict \LC\ translation from Milner's {\em Functions As Processes}.
\item [Syntax] Standard \Lc. No constants or operators.
\item [Semantics] Standard sequential \Lc.
\item [Operation] Abstraction announces handle on which it receives  argument then result channel. Result channel identity communicated to variable channel.
\item [Implementation] Uses synchronous communication, so not implemented.
\end{details}

\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{ @_{V} 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*} 

\subsection{Our New Scheme}
Our scheme supports a mixed calculus so there are rules for both forms
of application. For comparison with other schemes, we need a pure
translation. The translation {\em NewLazy} results when every
application is treated as $@_{L}$, and {\em NewStrict} results if
every application is treated as $@_{V}$

{\bf New Scheme}
\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} \\
\sembrac{ Succ(M) }_u & = & ( \sembrac{M}_a\,|\,a!x.()\,|\,x?m.\,{\bf rec}\,X.\,u?v.\,(\,v!(m+1).()\,|\,X\,)\,)\res{x}\res{a} \\
\sembrac{ Mult_V(M,N) }_u & = & ( \sembrac{M}_a | \sembrac{N}_b | a!x.()| b!y.()| x?m.y?n.{\bf rec}X.u?v.(v!(m*n).()|X))\res{x}\res{y}\res{a}\res{b}
\end{eqnarray*}
To translate a program, $P$, we use the rule:
\begin{eqnarray*}
\sembrac{ P } & = & (\,\sembrac{P}_u\,|\,u!c.()\,|\,c?v\,.\,Print(\,v\,)\,)\,\res{c}\res{u}
\end{eqnarray*}
The translations of a variable and of $@_L M N$ are a simplification,
$v$ being shorthand for a pair, say $(p,q)$. The full forms are as
follows:
\begin{eqnarray*}
\sembrac{ x }_u & = & {\bf rec} X.\,u?(p,q)\,.\,(\,x!(p,q).()\,|\,X\,) \\
\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*}

\subsection{Asynchronous $\pi$--Calculus Schemes}
The original translations do not comply with the asynchronous form of
Honda and Tokoro.  We can, however, use their techniques to convert
the translations to asynchronous form. The first will be called {\em
PiLazy} and the second {\em PiStrict}:

{\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} \\
\sembrac{ Mult_V(M,N) }_u & = & (\,\sembrac{M}_a\,|\,\sembrac{N}_b\,|\,a!x.()\,|\,b!y.()\,|\,x?m.\,y?n.\,u?v.\,v!(m*n).()\,)\res{x}\res{y}\res{a}\res{b}
\end{eqnarray*}
To translate a program, $P$, we use the rule:
\begin{eqnarray*}
\sembrac{ P } & = & (\,\sembrac{P}_u\,|\,u!c.()\,|\,c?v\,.\,Print(\,v\,)\,)\,\res{c}\res{u}
\end{eqnarray*}

{\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} \\
\sembrac{ Mult_V(M,N) }_u & = & (\,\sembrac{M}_a\,|\,\sembrac{N}_b\,|\,a?m.\,b?n.\,u!(m*n).()\,)\res{a}\res{b}
\end{eqnarray*}
To translate a program, $P$, we use the rule:
\begin{eqnarray*}
\sembrac{ P } & = & (\,\sembrac{P}_u\,|\,u?v\,.\,Print(\,v\,)\,)\,\res{u}
\end{eqnarray*}
For both of these translations the handling of constants and operators is simple, but abstractions and
applications require many communications.

\subsection{Tupled $\pi$--Calculus Schemes}
The tupled communication of our notation can be exploited to produce
optimised versions of {\em PiLazy} and {\em PiStrict}, called {\em
NewPiLazy} and {\em NewPiStrict} respectively:

{\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(M) }_{u} & = & (\,\sembrac{M}_{a}\,|\,a!s.()\,|\,s?m.\,u?v.\,v!(m+1).()\,)\res{s}\res{a} \\
\sembrac{ Mult_V(M,N) }_u & = & (\,\sembrac{M}_a\,|\,\sembrac{N}_b\,|\,a!x.()\,|\,b!y.()\,|\,x?m.\,y?n.\,u?v.\,v!(m*n).()\,)\res{x}\res{y}\res{a}\res{b}
\end{eqnarray*}
To translate a program, $P$, we use the rule:
\begin{eqnarray*}
\sembrac{ P } & = & (\,\sembrac{P}_u\,|\,u!c.()\,|\,c?v\,.\,Print(\,v\,)\,)\,\res{c}\res{u}
\end{eqnarray*}

{\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} \\
\sembrac{ Mult_V(M,N) }_u & = & (\,\sembrac{M}_a\,|\,\sembrac{N}_b\,|\,a?m.\,b?n.\,u!(m*n).()\,)\res{a}\res{b}
\end{eqnarray*}
To translate a program, $P$, we use the rule:
\begin{eqnarray*}
\sembrac{ P } & = & (\,\sembrac{P}_u\,|\,u?v\,.\,Print(\,v\,)\,)\,\res{u}
\end{eqnarray*}

\subsection{Improved $\pi$--Calculus Schemes}
The {\em NewPiStrict} scheme can be further simplified: the protocol
between an abstraction and an application creates a special link
simply to exchange a pair of values, whereas it is possible just to
communicate the pair directly. The resulting scheme is the best purely
strict scheme investigated so far.

{\bf ImpPiStrict}
\begin{eqnarray*}
\sembrac{ x }_{u} & = & u!x.() \\
\sembrac{ k }_{u} & = & u!k.() \\
\sembrac{ {\lambda}x.M }_u & = & (u!y.()\,|\,{\bf rec}\,X.\,y?(x,q).\,(\,\sembrac{M}_q\,|\,X)\,)\res{y} \\
\sembrac{ @_{V} M N }_u & = & (\,\sembrac{M}_f\,|\,f?y.\,a?z.\,y!(z,u).()\,|\,\sembrac{N}_a\,)\res{f}\res{a} \\
\sembrac{ Succ(M) }_{u} & = & (\,\sembrac{M}_{a}\,|\,a?m.\,u!(m+1).()\,)\res{a} \\
\sembrac{ Mult_V(M,N) }_u & = & (\,\sembrac{M}_a\,|\,\sembrac{N}_b\,|\,a?m.\,b?n.\,u!(m*n).()\,)\res{a}\res{b}
\end{eqnarray*}
To translate a program, $P$, we use the rule:
\begin{eqnarray*}
\sembrac{ P } & = & (\,\sembrac{P}_u\,|\,u?v\,.\,Print(\,v\,)\,)\,\res{u}
\end{eqnarray*}

We are also interested in sequential schemes where the function is to
be evaluated before the argument, so that side effects will be
deterministic. This can be achieved by making simple changes to the
rules for {\em ImpPiStrict} so that there are input guards before the
translation of expressions which are to be delayed.

We use a new apply operator with subscript S.  The rules for binary
operators also enforce sequential operation. The operator is given a
subscript as well:

{\bf SeqPiStrict}
\begin{eqnarray*}
\sembrac{ x }_{u} & = & u!x.() \\
\sembrac{ k }_{u} & = & u!k.() \\
\sembrac{ {\lambda}x.M }_u & = & (u!y.()\,|\,{\bf rec}\,X.\,y?(x,q).\,(\,\sembrac{M}_q\,|\,X)\,)\res{y} \\
\sembrac{ @_{S} M N }_u & = & (\,\sembrac{M}_f\,|\,f?y.\,(\,a?z.\,y!(z,u).()\,|\,\sembrac{N}_a\,)\res{a}\,)\res{f} \\
\sembrac{ Succ(M) }_{u} & = & (\,\sembrac{M}_{a}\,|\,a?m.\,u!(m+1).()\,)\res{a} \\
\sembrac{ Mult_S(M,N) }_u & = & (\,\sembrac{M}_a\,|\,a?m.\,(\,\sembrac{N}_b\,|\,b?n.\,u!(m*n).()\,)\res{b}\,)\res{a}
\end{eqnarray*}
To translate a program, $P$, we use the rule:
\begin{eqnarray*}
\sembrac{ P } & = & (\,\sembrac{P}_u\,|\,u?v\,.\,Print(\,v\,)\,)\,\res{u}
\end{eqnarray*}

These last schemes are entirely compatible with each other. The same
number of communications will take place if a program terminates,
although the sequential apply operator will delay execution of the argument.

We show a combined scheme called {\em MixPiStrict}:

{\bf MixPiStrict}
\begin{eqnarray*}
\sembrac{ x }_{u} & = & u!x.() \\
\sembrac{ k }_{u} & = & u!k.() \\
\sembrac{ {\lambda}x.M }_u & = & (u!y.()\,|\,{\bf rec}\,X.\,y?(x,q).\,(\,\sembrac{M}_q\,|\,X)\,)\res{y} \\
\sembrac{ @_{V} M N }_u & = & (\,\sembrac{M}_f\,|\,f?y.\,a?z.\,y!(z,u).()\,|\,\sembrac{N}_a\,)\res{f}\res{a} \\
\sembrac{ @_{S} M N }_u & = & (\,\sembrac{M}_f\,|\,f?y.\,(\,a?z.\,y!(z,u).()\,|\,\sembrac{N}_a\,)\res{a}\,)\res{f} \\
\sembrac{ Succ(M) }_{u} & = & (\,\sembrac{M}_{a}\,|\,a?m.\,u!(m+1).()\,)\res{a} \\
\sembrac{ Mult_V(M,N) }_u & = & (\,\sembrac{M}_a\,|\,\sembrac{N}_b\,|\,a?m.\,b?n.\,u!(m*n).()\,)\res{b}\res{a} \\
\sembrac{ Mult_{S}(M,N) }_u & = & (\,\sembrac{M}_a\,|\,a?m.\,(\,\sembrac{N}_b\,|\,b?n.\,u!(m*n).()\,)\res{b}\,)\res{a}
\end{eqnarray*}
To translate a program, $P$, we use the rule:
\begin{eqnarray*}
\sembrac{ P } & = & (\,\sembrac{P}_u\,|\,u?v\,.\,Print(\,v\,)\,)\,\res{u}
\end{eqnarray*}

\end{document}

% Extras from here on

\section{Experimental Results}
Translators have been written for all these schemes, except for the original $\pi$--calculus translations. 
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)) \\
{\rm SeqTest}: & & ({\lambda} x. {\lambda} y. \,y)\,(Succ(1))\,(Succ(2))
\end{eqnarray*}
The efficiency measure used is the number of output actions made. In
most cases, every output message is consumed. We also report figures
taken from the Dactl interpreter. They report the total number of
parallel cycles, the mean rewrites per cycle, and the peak rewrites.
These figures will only give a relative indication of the amount of
fine-grain parallelism available.
\begin{center}
\begin {tabular}{|l|r|r|r|r|} \hline
{\em Translation} & {\em IdTest} & {\em Share} & {\em Twice} & {\em SeqTest} \\ \hline
NewStrict & 4 (16 1.62 5) & 13 (29 2.55 09) & 49 (106 2.57 8) & 9 (22 2.55 8) \\
PiStrict & 8 (27 1.52 3) & 12 (40 1.62 05) & 96 (275 1.68 5) & 17 (51 1.80 5) \\
NewPiStrict & 5 (18 1.50 3) & 9 (30 1.70 05) & 57 (154 1.81 5) &11 (32 2.00 5)  \\
ImpPiStrict & 4 (17 1.35 3) & 8 (31 1.48 05) & 44 (153 1.48 5) & 9 (32 1.72 5) \\ \hline
SeqPiStrict & 4 (18 1.33 2) & 8 (42 1.21 02) & 44 (184 1.32 3) & 9 (47 1.23 2) \\ \hline
NewLazy & 5 (20 1.60 5) & 19 (38 2.71 10) & 80 (301 1.55 5) & 8 (30 1.70 5) \\
PiLazy & 7 (23 1.52 5) & 20 (41 2.20 07) & 94 (306 1.46 5) & 13 (42 1.52 5) \\
NewPiLazy & 4 (14 1.57 5) & 17 (32 2.41 07) & 52 (180 1.48 5) & 7 (24 1.58 5) \\ \hline
\end {tabular}
\end{center}
\end{document}
}
