%\documentstyle[a4,11pt]{article}
\documentstyle[11pt]{article}

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

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

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

\title{{\Large\bf  Full Facile Translation Scheme}}
\author{
        {\it J. Glauert}\\
%        {\it J. Glauert\thanks{Partially supported by ESPRIT BRA 3074: Semagraph}}\\
%	School of Information Systems\\
%	University of East Anglia\\
%	Norwich NR4 7TJ, UK\\
        \and
        {\it L. Leth} \and {\it B. Thomsen}\\
%        {\it L. Leth and B. Thomsen}\\
%        European Computer-Industry Research Centre\\
%        Arabellastrasse 17\\
%        D-8000 Munich 81, Germany
	}
%\date{DRAFT}
%\date{Semagraph '91}

%Environments
\newtheorem{defi}{Definition}[subsection]
\newtheorem{thm}{Theorem}[subsection]
\newtheorem{lemma}{Lemma}[subsection]
\newtheorem{prop}{Proposition}[subsection]
\newtheorem{cor}{Corollary}[subsection]
\newtheorem{ex}{Example}[subsection]
%%%%%%%%%%%%%%%%%%%%%%%

\newtheorem{fact}{Fact}[section]
\newtheorem{lemmaa}[fact]{Lemma}
\newtheorem{thmm}[fact]{Theorem}
\newtheorem{corr}[fact]{Corollary}
\newtheorem{notation}[fact]{Notation}
\newtheorem{propp}[fact]{Proposition}
\newtheorem{exx}[fact]{Example}
\newtheorem{defii}[fact]{Definition}

\newenvironment{definition}{\begin{defii}\rm}{\null\hfill $\Box$ \end{defii}}
\newenvironment{example}{\begin{exx}\rm}{\end{exx}}

\newenvironment{proof}{\vspace{3 mm}{\noindent \bf Proof}\rm}{\null\hfill
$\Box$\\ \vspace{3 mm}}
%%%%%%%%%%%%%%%%


%\newenvironment{proof}{{\bf Proof.}}{\hfill $\Box$}
%\newenvironment{framedfigure}[1]{\begin{figure}
%			   		\mbox{}\hrulefill\mbox{}\\\\}
%						%text
%					{\mbox{}		\\\\
%					\mbox{}\hrulefill\mbox{}
%				\end{figure}}
%%%%%%%%%%%%%%%%%%%%%

\newcommand{\myline}{\mbox{}\\\mbox{}\hrulefill\mbox{}\\\\}
\newcommand{\qed}{\hfill $\Box$}
\newcommand{\fed}[1]{{\bf #1}}
\newcommand{\ov}[1]{\overline{#1}}
\newcommand{\compf}{\overline{\vspace{12pt}}}
\newcommand{\un}[1]{\underline{#1}}
\newcommand{\mynot}[1]{\,\,\,\not{\!\!\!#1}}
\newcommand{\cat}[1]{{\bf #1}}

%Arrows
\newcommand{\ioi}{\;\;\Leftrightarrow\;\;}
\newcommand{\ra}{\longrightarrow}
\newcommand{\inta}{\succ\!\rightarrow}
\newcommand{\finta}{\succ\!\rightarrow\hspace{-.35cm}\rightarrow}
\newcommand{\notinta}{\inta\hspace{-5mm}\not\hspace{5mm}}
\newcommand{\con}{\downarrow}
\newcommand{\wcon}{\Downarrow}
\newcommand{\dvr}{\uparrow}
\newcommand{\wdvr}{\Uparrow}
\newcommand{\wra}{\Longrightarrow}
\newcommand{\der}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\fder}[1]{\stackrel{\!#1}
	{\longrightarrow\hspace{-.6cm}\longrightarrow}}
\newcommand{\wder}[1]{\stackrel{#1}{\Longrightarrow}}
\newcommand{\fun}{\longrightarrow}
\newcommand{\parfun}{\rightharpoonup}
%%%%%%%%%%%%%%%%%%%


% Denotations, Angles, Box and Diamond

\newcommand{\den}[1]{[\![#1]\!]}
\newcommand{\fden}[1]{[\![\!|#1|\!]\!]}
\newcommand{\ran}{\rangle}
\newcommand{\lan}{\langle}
\newcommand{\diam}[1]{\lan #1 \ran}
\newcommand{\ddiam}[1]{\lan\cdot #1\cdot\ran}
\newcommand{\bbox}[1]{[ #1 ]}
\newcommand{\dbox}[1]{[\cdot #1\cdot]}


%Preorder,equivalence and other relations

\newcommand{\equidef}{\stackrel{``def''}{=\!\!=}}
\newcommand{\preorder}[1]{\raisebox{-.6ex}{\raisebox{.95ex}
				{$#1$}$\!\!\!\!\!\scriptscriptstyle \sim$}}
\newcommand{\Mord}{\;\presim_M\;}
%\newcommand{\Meq}{{\;\preorder{-}}_M\;}
\newcommand{\eq}{\mathrel{%\lower.2ex
             \hbox{${\stackrel{-}{\scriptscriptstyle \sim}}$}}}
\newcommand{\Meq}{\eq_M} 
\newcommand{\presim}{\mathrel{\lower.2ex
             \hbox{${\stackrel{\sqsubset}{\scriptscriptstyle \sim}}$}}}
\newcommand{\altpreord}{\mathrel{\lower.2ex
             \hbox{${\stackrel{\sqsubset}{\scriptscriptstyle \approx}}$}}}
\newcommand{\wpresim}{\mathrel{\lower.2ex
          \hbox{${\stackrel{\sqsubset}{\scriptscriptstyle \approx}}$}}}
\newcommand{\lt}{\sqsubseteq}
\newcommand{\must}{\;\un{must}\; }
\newcommand{\mustnot}{\;\un{m\!\!\!\not u st}\; }
\newcommand{\prleq}{\sqsubseteq_E}

%Simple symbols

\newcommand{\ac}{{\cal A}}
\newcommand{\cB}{{\cal B}}
%\newcommand{\cu}{{\cal u}}
\newcommand{\si}{\sigma}
\newcommand{\ff}{f\!f}
\newcommand{\tr}{t\!\!t}
\newcommand{\f}[1]{f_{in}^{#1}\uplus f_{out}^{#1}}


%Big sums, unions, etc.

\newcommand{\osum}{\sum\!\!\!\!\!\!\circ\,\,\,}%internal sum
\newcommand{\osumdis}{\sum\!\!\!\!\!\!\circ\,\,\,\,\,}%internal sum displayed
\newcommand{\oss}{\sum\!\!\!\!\!\!\circ\,\,\,\,\,}%the same as osumdis
\newcommand{\udot}{\cup\!\!\!\!\!\,\!\,\cdot\,\,\,}
\newcommand{\Lor}[1]{\bigcup_{#1}}
\newcommand{\Land}[1]{\bigcap_{#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%Structure of formulas

\newcommand{\casedef}[4]% case definition
	{\left\{ \begin{array}{ll}
		#1 & #2 \\
		#3 & #4
		\end{array}\right.}




\newcommand{\mafrac}[2]{\begin{array}{c}
				{#1}	\\
				\hline{#2}\\
			\end{array}

			}
\newcommand{\ITE}[3]
		{\;If\; #1 \;\begin{array}[t]{l}
				Then\; #2 \\
				Else\; #3
			      \end{array}
		   }
\newtheorem{theorem}{Theorem}[section]
\newtheorem{nlemma}{Lemma}[section]
\newtheorem{ndefinition}[theorem]{Definition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{nnotation}[theorem]{Notation}
\newtheorem{nexample}[theorem]{Example}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{conjecture}[theorem]{Conjecture}
\newcounter{LLN}
\newcommand{\beginit} {
                         \begin{list}{\hfill{\rm \arabic{LLN}.}
}{\usecounter{LLN}
                         \setlength{\leftmargin}{\leftmarginii}
                         \setlength{\itemsep}{\smallskipamount}}}

\newcommand{\nonconsys}{nondeterministic and concurrent systems}
\newcommand{\lcal}{$\lambda$--Calculus}
\newcommand{\pcal}{$\pi$--Calculus}
\newcommand{\ahob}{applicative higher order bisimulation}
\newcommand{\ahos}{applicative higher order simulation}
%\newcommand{\presim}{\stackrel{\scriptscriptstyle\sqsubset}
%                     {\scriptscriptstyle\sim}}
%\newcommand{\wpresim}{\stackrel{\scriptscriptstyle\sqsubset}
%                     {\scriptscriptstyle\approx}}
\newcommand{\Pbrac}[1]{\{\!\mid #1 \mid\!\}}
\newcommand{\para}{\|}
\newcommand{\PPr}{\mbox{\sl Pr}}
\newcommand{\CPr}{\mbox{\sl CPr}}
\newcommand{\RPr}{\mbox{\sl RPr}}
\newcommand{\FPr}{\mbox{\sl FPr}}
\newcommand{\CFPr}{\mbox{\sl CFPr}}
\newcommand{\Prminus}{\mbox{\sl Pr}^-}
\newcommand{\CPrminus}{\mbox{\sl CPr}^-}
\newcommand{\Id}{\mbox{\sl Id}}
\newcommand{\CR}{\mbox{\sl CR}}
\newcommand{\ACR}{\mbox{\sl ACR}}
\newcommand{\ACRS}{\mbox{\sl ACR}^{\ast}}
\newcommand{\CRS}{\mbox{\sl CR}^{\ast}}
\newcommand{\WCR}{\mbox{\sl WCR}}
\newcommand{\IWCR}{\mbox{\sl IWCR}}
\newcommand{\IWCRS}{\mbox{\sl IWCR}^{\ast}}
\newcommand{\WCRminus}{\mbox{\sl WCR}^-}
\newcommand{\WCRminusS}{\mbox{\sl WCR}^{-\ast}}
\newcommand{\SPEC}{\mbox{\sl SPEC}}
\newcommand{\IMP}{\mbox{\sl IMP}}
\newcommand{\Names}{\mbox{\sl Names}}
\newcommand{\Act}{\mbox{\sl Act}}
\newcommand{\Actminus}{\mbox{\sl Act}^-}
\newcommand{\CAct}{\mbox{\sl CAct}}
\newcommand{\FAct}{\mbox{\sl FAct}}
\newcommand{\CFAct}{\mbox{\sl CFAct}}
\newcommand{\Actdownarrow}{\mbox{\sl Ev}}
\newcommand{\CHOCS}{\mbox{\sl CHOCS}}
%\newcommand{\cat}[1]{{\bf #1}}
\newcommand{\Slim}[1]{\mbox{\sl #1}}
\newcommand{\slim}[1]{\;\mbox{\sl #1}\;}
\newcommand{\ol}[1]{\overline{#1}}
\newcommand{\pbefore}{\;\mbox{$before$}\;}
\newcommand{\bresult}{\;\mbox{\tt result}\;}
\newcommand{\presult}{\;\mbox{$result$}\;}
\newcommand{\displace}{\leftarrow\!\!\!\mid}
\newcommand{\rec}{{\tt rec}}
\newcommand{\recpx}{\rec\,x.\tau.(p\backslash a)}
\newcommand{\subrecpx}[1]{#1[\recpx/x]}
\newcommand{\ypx}{Y_x[p]}
\newcommand{\subypx}[1]{#1[\ypx/x]}
\newcommand{\Rres}{R^{\backslash}}
\newcommand{\Rsim}{\sim\! R\!\sim}
\newcommand{\Rhat}{\widehat{\Rsim}}
\newcommand{\HAT}[1]{\widehat{#1}}
\newcommand{\HATHAT}[1]{\widehat{\widehat{#1}}}
\newcommand{\TILDE}[1]{\widetilde{#1}}
\newcommand{\bvar}{\mbox{\tt var}\;}
\newcommand{\bobj}{\mbox{\tt obj}\;}
\newcommand{\bmethod}{\mbox{\tt method}\;}
\newcommand{\bclass}{\mbox{\tt class}\;}
\newcommand{\binherits}{\mbox{\tt inherits}\;}
\newcommand{\bbody}{\mbox{\tt body}\;}
\newcommand{\bcreate}{\mbox{\tt create}\;}
\newcommand{\bstart}{\mbox{\tt start}\;}
\newcommand{\emptysort}{\mbox{\tt \O}\;}
\newcommand{\emptyrho}{\rho_{\emptysort}}
\newcommand{\bproc}{\mbox{\tt proc}\;}
\newcommand{\is}{\;\mbox{\tt is}\;}
\newcommand{\bif}{\mbox{\tt if}\;}
\newcommand{\bthen}{\;\mbox{\tt then}\;}
\newcommand{\belse}{\;\mbox{\tt else}\;}
\newcommand{\pif}{\mbox{$if$}\;}
\newcommand{\pthen}{\;\mbox{$then$}\;}
\newcommand{\pelse}{\;\mbox{$else$}\;}
\newcommand{\bwhile}{\mbox{\tt while}\;}
\newcommand{\bdo}{\;\mbox{\tt do}\;}
\newcommand{\bpar}{\;\mbox{\tt par}\;}
\newcommand{\ppar}{\;\mbox{$par$}\;}
\newcommand{\binput}{\mbox{\tt input}\;}
\newcommand{\boutput}{\mbox{\tt output}\;}
\newcommand{\bskip}{\mbox{\tt skip}\;}
\newcommand{\bbegin}{\mbox{\tt begin}\;}
\newcommand{\bend}{\;\mbox{\tt end}}
\newcommand{\bcall}{\mbox{\tt call}\;}
\newcommand{\bvalue}{\mbox{\tt value}\;}
\newcommand{\bref}{\mbox{\tt ref}\;}
\newcommand{\sembrac}[1]{[\![ #1 ]\!]}
\newcommand{\setof}[2]{\{ #1 \: : \: #2 \}}
\newcommand{\Psetof}[2]{\Pbrac{ #1 \: | \: #2 }}
\newcommand{\arrow}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\warrow}[1]{\stackrel{#1}{\Longrightarrow}}
\newcommand{\trans}[3]{#1 \arrow{#2} #3}
\newcommand{\wtrans}[3]{#1 \warrow{#2} #3}
\newcommand{\skil}{\ \raisebox{-4.5pt}{\rule{1pt}{5mm}} \ }
\newcommand{\nonarrow}[1]{\stackrel{#1}{\not\rightarrow}}
\newcommand{\wnonarrow}[1]{\stackrel{#1}{\not\Longrightarrow}}
\newcommand{\bigL}{{\cal L}}
\newcommand{\bigb}{{\cal B}}
\newcommand{\bighb}{{\cal H\!\!B}}
\newcommand{\bigwhb}{{\cal W\!\!H\!\!B}}
\newcommand{\bigwhpb}{{\cal W\!\!H\!\!P\!\!B}}
\newcommand{\bigawhb}{{\cal A\!W\!\!H\!\!B}}
\newcommand{\bigiwhb}{{\cal I\!W\!\!H\!\!B}}
\newcommand{\bigahb}{{\cal A\!\!H\!\!B}}
\newcommand{\bigp}{{\cal P}}
\newcommand{\bigpminus}{{\cal P}^-}
\newcommand{\bigcp}{{\cal C\!\!P}}
\newcommand{\bigfp}{{\cal F\!\!P}}
\newcommand{\bigfcp}{{\cal F\!\!C\!\!P}}
\newcommand{\bigcpminus}{{\cal C\!\!P}^-}
\newcommand{\bighpb}{{\cal H\!\!P\!\!B}}
\newcommand{\bis}{bisimulation}
\newcommand{\SGamma}{{\scriptstyle \Gamma}}
\newcommand{\SPhi}{{\scriptstyle \Phi}}
\newcommand{\infer}[3]
           {\vspace{.2cm}
            \hbox{${\displaystyle {\frac {#1}{#2}}\hspace{.5cm}{#3}}$}
            \vspace{.2cm}}
\newcommand{\SFP}{{\bf SFP}}
\newcommand{\LLC}{Lazy--$\lambda$--Calculus}
\newcommand{\OOP}{object oriented programming}
\newcommand{\OOOP}{Object oriented programming}
\newcommand{\OOL}{object oriented programming language}
\newcommand{\Lazytrans}{\underline{\ }\!\Downarrow\!\underline{\ }}
\newcommand{\bigAB}{{\cal A\!\!B}}
\newcommand{\lapprox}{\approx_{\lambda}}
\newcommand{\lvapprox}{\approx_{\lambda v}}
\newcommand{\res}[1]{\backslash #1}
\newcommand{\lsub}[2]{\{#1/#2\}}
\newcommand{\ren}[2]{[#1\mapsto #2]}
\newcommand{\simdot}{\stackrel{\cdot}{\sim}}
\newcommand{\ahbsim}{\stackrel{:}{\sim}}
\newcommand{\ahbapprox}{\stackrel{:}{\approx}}
\newcommand{\tausim}{\ahbsim_{\tau}}
\newcommand{\tausub}[2]{[#1/#2]_{\tau}}
\newcommand{\Cp}[2]{\rec\, X.#1.(#2\mid X)}
\newcommand{\trig}[2]{#1\Rightarrow#2}
\newcommand{\loc}[1]{\lfloor #1}
\newcommand{\tausubqx}{\tausub{q}{x}}
\newcommand{\lsubbx}{\{b/x\}}
\newcommand{\lsubcx}{\{c/x\}}
\newcommand{\Cpbq}{(\trig{b}{\sembrac{q}})}
\newcommand{\Cpcq}{(\trig{c}{\sembrac{q}})}
%===========================================================================
%	END OF PROOF BOX
%
%
%  The complexity of the macro necessary to get a little box on the
%  right-hand-side at the end of a proof is amazing.  It really does
%  have to be this long!  Otherwise you're liable to get it at the
%  beginning of the next line, or even on the next page.
%
%\def\sqr#1#2{{\vcenter{\vbox{\hrule height.#2pt
     %\hbox{\vrule width.#2pt height#1pt \kern#1pt
           %\vrule width.#2pt}
     %\hrule height.#2pt}}}}
%\def\square{\mathchoice\sqr34\sqr34\sqr{2.1}3\sqr{1.5}3}
\def\pushright#1{{%        set up
   \parfillskip=0pt            % so \par doesnt push \square to left
   \widowpenalty=10000         % so we dont break the page before \square
   \displaywidowpenalty=10000  % ditto
   \finalhyphendemerits=0      % TeXbook exercise 14.32
  %
  %                 horizontal
   \leavevmode                 % \nobreak means lines not pages
   \unskip                     % remove previous space or glue
   \nobreak                    % don't break lines
   \hfil                       % ragged right if we spill over
   \penalty50                  % discouragement to do so
   \hskip.2em                  % ensure some space
   \null                       % anchor following \hfill
   \hfill                      % push \square to right
   {#1}                        % the end-of-proof mark (or whatever)
  %
  %                   vertical
   \par}}                      % build paragraph

% prefer proofs with statements, also space after
%\def\qed{\pushright{$\square$}\penalty-700 \smallskip}
\def\qed{\pushright{$\Box$}\penalty-700 \smallskip}

%===========================================================================
\newcommand{\BExp}{\mbox{\sl BExp}}
\newcommand{\Ev}{\mbox{\sl Ev}}
\newcommand{\Val}{\mbox{\sl Val}}
\newcommand{\PVar}{\mbox{\sl PVar}}
\newcommand{\DVar}{\mbox{\sl DVar}}
\newcommand{\Exp}{\mbox{\sl Exp}}
\newcommand{\Chan}{\mbox{\sl Chan}}
\newcommand{\FCPr}{\mbox{\sl FCPr}}
\newcommand{\eab}{strong extensional applicative prebisimulation}
%\newcommand{\presim}{\mathrel{\lower.2ex
%             \hbox{${\stackrel{\sqsubset}{\scriptscriptstyle \sim}}$}}}
%\newcommand{\wpresim}{\mathrel{\lower.2ex
 %         \hbox{${\stackrel{\sqsubset}{\scriptscriptstyle \approx}}$}}}
\begin{document}
\maketitle
\section{Small Process Notation}
We use  a process notation  similar to the  $\pi$--calculus of Milner,
Parrow, and  Walker,  but are also   interested  in the restriction of
Honda and Tokoro in which asynchronous communication models are derived by
insisting that output actions are followed by inaction ({\em tail sends}).

The syntax for the process notation is as follows:
\begin{eqnarray*}
p & ::= & ()\,|\,c?c.p\,|\,c!c.p\,|\,p|p\,|\,p\res{c}\,|\,{\bf rec}\,X.p\,|\,X\,|\,c=c.p \\
\end{eqnarray*}

\section{Translating Core Facile}
We consider sequential schemes where the function is to be evaluated
before the argument, so that side effects will be deterministic (in
some sense).

The syntax for core Facile is as follows:
\begin{eqnarray*}
e & ::= & x | {\lambda}x.e | e\,e | c | {\bf channel} | e!e | e? | {\bf code}(be) | {\bf spawn}(be) \\
be & ::= & {\bf terminate}\,|\,{\bf activate}\,e\,|\,be || be
\end{eqnarray*}

The translation is:
\begin{eqnarray*}
\sembrac{ x }_u & = & u!x.() \\
\sembrac{ {\lambda}x.e }_u & = & ( u!y.()\,|\,{\bf rec}\,X.\,y?(x,b).\,(\,\sembrac{e}_b\,|\,X)\,)\res{y} \\
\sembrac{ e\,e' }_u & = & (\,\sembrac{e}_a\,|\,a?y.\,(\,\sembrac{e'}_b\,|\,b?z.\,y!(z,u).()\,)\res{b}\,)\res{a} \\
\sembrac{ c }_u & = & u!c.() \\
\sembrac{ {\bf channel} }_u & = &( u!c.() )\res{c} \\
\sembrac{ e!e' }_u & = & (\,\sembrac{e}_a\,|\,a?y.\,(\,\sembrac{e'}_b\,|\,b?z.\,z!(y,u).()\,)\res{b}\,)\res{a} \\
\sembrac{ e? }_u & = & (\,\sembrac{e}_a\,|\,a?y.\,y?(x,z).\,(u!x.()\,|\,z!{\bf triv}.())\,)\res{a} \\
\sembrac{ {\bf code}(be) }_u & = & ( u!y.()\,|\,{\bf rec}\,X.\,y?x.\,(\,\sembrac{be}\,|\,X)\,)\res{y} \\
\sembrac{ {\bf spawn}(be) }_u & = & ( u!{\bf triv}.()\,|\,\sembrac{be} ) \\
\\
\sembrac{ {\bf terminate} } & = & () \\
\sembrac{ {\bf activate}\, e } & = & ( \sembrac{e}_u\,|\,u?y.\,y!{\bf triv}.() )\res{u} \\
\sembrac{ be || be' } & = & ( \sembrac{be}\,|\,\sembrac{be'} ) \\
\end{eqnarray*}
In the rule for {\bf code}, the channel $x$ must not be free in $be$;
it is used just to trigger the behaviour expression in {\bf activate}.
{\bf spawn} can be implemented as a derived operator if required. See
Magic Note 21.

\section{Translating Scalar Values, Tuples, and Tupled Application}
We will enhance the pure $\lambda$--calculus component  of Facile with
constants, including  scalar data values  and their  operators. Binary
operations in ML are represented by unary  operations taking a pair of
values.

Tupled application requires us to develop a translation for tuples as
values and a translation of a function taking a tuple of arguments.
Pairs will be used for illustration, but it should be clear how the
process would generalise. The rule for application does not change. A
type system would know the size of messages on the channels handled by
the application:
\begin{eqnarray*}
\sembrac{ (e, e') }_u & = & (\,\sembrac{e}_a\,|\,a?m.\,(\,\sembrac{e'}_b\,|\,b?n.\,u!(m,n).()\,)\res{b}\,)\res{a} \\
\sembrac{ e\,e' }_u & = & (\,\sembrac{e}_a\,|\,a?y.\,(\,\sembrac{e'}_b\,|\,b?z.\,y!(z,u).()\,)\res{b}\,)\res{a} \\
\sembrac{ {\bf fn}\,(x,x') => e }_u & = & ( u!y.()\,|\,{\bf rec}\,X.\,y?((x,x'),b).\,(\,\sembrac{e}_b\,|\,X)\,)\res{y}
\end{eqnarray*}

We can show how the arithmetic operators are handled. A binary
operator like $mult$, 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*}
\sembrac{ succ }_u & = & (\,u!y.()\,|\,{\bf rec}\,X.\,y?(x,b).\,(\,b!(x+1).()\,|\,X\,)\,)\res{y} \\
\sembrac{ mult }_u & = & (\,u!y.()\,|\,{\bf rec}\,X.\,y?((n,m),b).\,(\,b!(n*m).()\,|\,X\,)\,)\res{y}
\end{eqnarray*}
Application of these functions to an argument involves a couple more
communications than the restricted forms produced for earlier
translations, but it should be simple to optimise the translation when
the function is a known constant.  These forms of $succ$ and $mult$
are compatible with the style of ML and can be used freely.

Rather than using the approach in the last section, we may encode
sending and receiving of messages using functions similar to those in
the current Facile implementation. For sending, 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 Facile
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*}
\sembrac{ send }_u & = & (\,u!y.()\,|\,{\bf rec}\,X.\,y?((c,v),b).\,(\,c!(v,b).()\,|\,X)\,)\res{y} \\
\sembrac{ receive }_u & = & ( u!y.()\,|\,{\bf rec}\,X.\,y?(c,b).\,c?(v,z).\,(\,b!v.()\,|\,z!{\bf triv}.()\,|\,X)\,)\res{y} \\
\end{eqnarray*}

For each of these constant functions it would be possible to assign a 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. Hence the translation might be:
\begin{eqnarray*}
\sembrac{ send }_u & = & u!send.()
\end{eqnarray*}
anda program using $send$ would be evaluated in a context:
\begin{eqnarray*}
(\,\sembrac{ P }_u\,|\,{\bf rec}\,X.\,send?((c,v),b).\,(\,c!(v,b).()\,|\,X)\,)\res{send}\res{u}
\end{eqnarray*}

In ML, tuples are considered as forms of records, with integers as
field names.  However, we will consider tuples more primitive than
records, with field names mapping to offsets in a tuple.

\section{Translating Data Structures and Pattern Matching}
The language shown so far is strict. We will need to support some form of
conditional computation and laziness. It will be seen that
this can be achieved as a bi-product of considering datatypes in the
style of ML.

As in ML, we can use a pattern-matching form of function definition as
the basis for conditional computation. We will assume that patterns
have been flattened so that they are no more than one level deep. This
will leave us with three cases to consider:
\begin{itemize}
\item A single choice with a pattern which is a singleton or tuple of bound variable names.
\item A number of constant patterns.
\item A number of patterns for datatype elements.
\end{itemize}
The first case has been considered above. The last two cases may have
a default value in the form of a bound variable name as well.

\subsection{Pattern Matching with Constant Patterns}
When testing constant patterns in a function match, we need
some sort of process-level testing construct as in the
$\pi$--calculus. The proposed form of process is $(c=c'.p)$ where $c$
and $c'$ would be scalar data values. For default cases we might use
some more general form of predicate, but it would be no more than a
simple logical combination of constant tests. The semantics will be
that the behaviour is the same as inaction if the test fails,
otherwise it is the behaviour of the process following the test.

The translation of constant values is as before. Our example will be
an {\em if-the-else} test:
\begin{eqnarray*}
\sembrac{ {\bf fn}\,false => e \,|\, true => e'}_u & = & ( u!y.() | {\bf rec}\,X.y?(x,b).(x={\bf false}.\sembrac{e}_b | x={\bf true}.\sembrac{e'}_b | X)\,)\res{y}
\end{eqnarray*}
$x$ must not occur free in $e$ or $e'$.  The different tests are
intended to be mutually exclusive, so on pragmatic grounds we might
wish to introduce a form which would suggest sequential application of
tests, or use of a jump table, with provision for a default case.

\subsection{Pattern Matching with Datatype Elements}
Datatypes  can be  handled  in  a number of  ways. Our example will be
lists. Rules are needed for building datatype  values and for matching
on the   tag, extracting the  appropriate value  from  a   $Cons$, for
example.

Similar ideas are found in the $\pi$--calculus papers, but I think the
approaches described here are different in minor ways. It is not
necessary to use the test construct for these datatypes, but as the
test is required elsewhere, we will use it in some of our schemes.

The first version encodes a data value as a list of channels, one for
each component of the datatype, and outputs the value on the
appropriate channel for the particular component:
\begin{eqnarray*}
\sembrac{ {\bf Nil} }_u & = & (\,u!(n,c).()\,|\,n!{\bf triv}.()\,)\res{n}\res{c} \\
\sembrac{ {\bf Cons}\,e }_u & = & (\,\sembrac{e}_a\,|\,a?m.\,(\,u!(n,c).()\,|\,c!m.()\,)\res{n}\res{c}\,)\res{a} \\
\sembrac{ {\bf fn}\,{\bf Nil}=>e \,|\, {\bf Cons}\,(h,t)=>e'}_u & = & ( u!y.() | {\bf rec}\,X.y?((n,c),b).(n?z.\sembrac{e}_b | c?(h,t).\sembrac{e'}_b | X)\,)\res{y}
\end{eqnarray*}
$n$ and $z$ must not occur free in $e$. $c$ must not occur free in
$e'$.  I think some extra recursion may be required in the rules for
$Cons$ and $Nil$ in case it was necessary to receive the untagged
value more than once. The recursion would be rather nasty as it would
have to be true replication or be triggered by a synchronous
communication.

Default rules would be a messy as the default code would need to be
replicated. Worse, if the default rule wanted to use the matched
value, each default case would have to rebuild the appropriate tagged
value. This does not seem very practical.

A varient of this  approach would be for the function code to send a list of
channels to the data value. The data value is sent back on the
appropriate channel:
\begin{eqnarray*}
\sembrac{ {\bf Nil} }_u & = & (\,u!y.()\,|\,y?(n,c).n!{\bf triv}.()\,)\res{y} \\
\sembrac{ {\bf Cons}\,e }_u & = & (\,\sembrac{e}_a\,|\,a?m.\,(\,u!y.()\,|\,y?(n,c).c!m.()\,)\res{y}\,)\res{a} \\
\sembrac{ {\bf fn}\,{\bf Nil}=>e \,|\, {\bf Cons}\,(h,t)=>e'}_u & = & ( u!y.() | {\bf rec}\,X.\,y?(z,b). \\
& & \:\: (\,z!(n,c).() | n?x.\sembrac{e}_b | c?(h,t).\sembrac{e'}_b | X)\res{n}\res{c}\,)\res{y}
\end{eqnarray*}
$n$ and $x$ must not occur free in $e$. $c$ must not occur free in $e'$.

In the general case, handling of defaults is no better than before,
but we could simplify the handling of default cases if the value
matched was never used: repeated names could be used in the list of
channels sent to the data value.  As an example, consider a datatype
with constructors $North$, $South$, $East$, and $West$. Let us say
that only $East$ is selected:
\begin{eqnarray*}
\sembrac{ {\bf fn}\,{\bf East}\,(v) => c \,|\, x => d}_u & = & ( u!y.() | {\bf rec}\,X.y?(z,b). \\
& & \:\: (\, z!(x,x,e,x).()\,|\, e?v.\sembrac{c}_b\,|\,x?w.\sembrac{d}_b\,|\,X)\res{x}\,)\res{y}
\end{eqnarray*}
$e$ must not occur free in $c$. $x$ and $w$  must not occur free in $d$.

A different style of encoding uses the match construct and represents
a data value by a numeric tag and a channel for receiving the untagged
value. This has the benefit that the representation of a datatype
value does not depend on the number of elements in the datatype:
\begin{eqnarray*}
\sembrac{ {\bf Nil} }_u & = & (\,u!({\bf 0},n).()\,)\res{n} \\
\sembrac{ {\bf Cons}\,e }_u & = & (\,\sembrac{e}_a\,|\,a?m.\,(\,u!({\bf 1},c).()\,|\,c!m.()\,)\res{c}\,)\res{a} \\
\sembrac{ {\bf fn}\,{\bf Nil}=>e \,|\, {\bf Cons}\,(h,t)=>e'}_u & = & ( u!y.() | {\bf rec}\,X.\,y?((g,z),b). \\
& & \:\: (\,g=0.\sembrac{e}_b | g=1.z?(h,t).\sembrac{e'}_b | X) )\res{y}
\end{eqnarray*}
$g$ and $z$ must not appear free in $e$ or $e'$. There is no need for $Nil$ to
send a value since the expression in the match will never use it.

Default handling is easier as the pair $(g,z)$ is the standard
representation of a datatype value:
\begin{eqnarray*}
\sembrac{ {\bf fn}\,{\bf East}\,(v) => c \,|\, x => d}_u & = & ( u!y.() | {\bf rec}\,X.\,y?((g,z),b). \\
& & \:\: (\,g=2.\,z?v.\sembrac{c}_b\,|\,g<>2.\,\sembrac{d}_b\,|\,X\,)\,)\res{y}
\end{eqnarray*}
$g$ and $z$ must not be free in $c$ or $d$. We also need to substitute
$(g,z)$ for $x$ in $d$.

As before, a varient of this scheme can be produced in which the
untagged value is only sent on demand. The value can be retrieved
multiple times without difficulty if recursion is added to the scheme
for encoding a datatype.  In this final scheme, a datatype value is
represented by a pair. The first component is an integer tag, and the
second is the name of a channel by which the untagged value may be
requested:
\begin{eqnarray*}
\sembrac{ {\bf Nil} }_u & = & (\,u!({\bf 0},n).()\,)\res{n} \\
\sembrac{ {\bf Cons}\,e }_u & = & (\,\sembrac{e}_a\,|\,a?m.\,(\,u!({\bf 1},c).()\,|\,{\bf rec}\,X.\,c?b.(b!m.()\,|\,X)\,)\res{c}\,)\res{a} \\
\sembrac{ {\bf fn}\,{\bf Nil}=>e \,|\, {\bf Cons}\,(h,t)=>e'}_u & = & ( u!y.() | {\bf rec}\,X.\,y?((g,z),b). \\
& & \:\: (\,g=0.\sembrac{e}_b | g=1.(z!c.() | c?(h,t).\sembrac{e'}_b)\res{c} | X) )\res{y}
\end{eqnarray*}
$g$ must not appear free in $e$ or $e'$.

\section{Translating the Process Notation to Facile}
The following translation converts the process notation constructs to Facile:
\begin{eqnarray*}
\sembrac{ () } & = & {\bf terminate} \\
\sembrac{ a?x.\,p } & = & {\bf activate}\,({\lambda}x. {\bf code}(\sembrac{p})\,a? \\
\sembrac{ a!b.\,p } & = & {\bf activate}\,({\lambda}x. {\bf code}(\sembrac{p})\,a!b \\
\sembrac{ p\,|\,p' } & = & \sembrac{p}\,||\,\sembrac{p'} \\
\sembrac{ p\,\res{x} } & = & {\bf activate}\,({\lambda}x. {\bf code}(\sembrac{p})\,)\,{\bf channel} \\
\sembrac{ {\bf rec}\,X.\,p } & = & {\bf activate}\,Y\,({\lambda}X. {\bf code}(\sembrac{p})\,) \\
\sembrac{ X } & = & X \\
\end{eqnarray*}
For the output rule, $x$ must not be free in $p$. $Y$ is the recursion
construct used in the Facile papers.

We still need a rule for the match construct, but this rule would rely on
additional features of Facile. The match is not required in the translation of
Pure Facile.

\end{document}
}
