%%% 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{Syntax and Semantics of Pi in the Sky Calculus}
\author{
        {\it John Glauert, Zurab Khasidashvili, Lone Leth, and Bent Thomsen} \\
       }
%\reportref{Draft}
\date{Version 4}

\newenvironment{observation}{\noindent{\bf Observation: }}{}
\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
% Pi Sky
%\input{PiSkyMacros}
% Pi Sky
\newcommand{\PPin}[2]{?{#1} \cdot {#2}}
\newcommand{\PPoutP}[2]{{#1}\,!\,{#2}}
\newcommand{\PPout}[3]{\PPoutP{#1}{#2} \cdot {#3}}
\newcommand{\PPnew}[3]{{\nu}\,{#1} \cdot {#2} \cdot {#3}}
\newcommand{\PPmatch}[4]{[{#1} = {#2}]\,{#3}\,:\,{#4}}
\newcommand{\PPdef}[2]{{#1} = {#2}}
\newcommand{\PPstop}[0]{\bf stop}
\newcommand{\PPname}[2]{{#1}:\,{#2}}
\newcommand{\PPpar}[2]{{#1}\,\|\,{#2}}
\newcommand{\PPres}[2]{{#2} \backslash {#1}}
\newcommand{\PPsub}[2]{{#1}\{{#2}\}}
\newcommand{\PPdefn}[2]{{#1} & = & {#2}}
%\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{\agtdefn}[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{\nonmatch}[3]{{#1}\neq{#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{\Prule}[4]{{#1} & ? & {#2} \; : \; (\,{#3}\,)\;\cdot\;{#4}}
\newcommand{\PruleSpawn}[3]{\Prule{#1}{#2}{#3}{#1}}
\newcommand{\Ppar}[2]{{#1}\,|\,{#2}}
\newcommand{\Pcall}[2]{{#1}\,!\,{#2}}
\newcommand{\Pdef}[2]{{#1}:\,{#2}}
% Translation representation
\newcommand{\PPwhere}[2]{where & & {#1} \; = \; {#2}}
\newcommand{\PPand}[2]{and & & {#1} \; = \; {#2}}
\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}{$\pi^\pi$--Calculus}
\newcommand{\PPc}{$\pi^\pi$--calculus}
\newcommand{\TPPC}{Term--$\pi^\pi$--Calculus}
\newcommand{\TPPc}{term--$\pi^\pi$--calculus}
\newcommand{\RA}{{\em return-address\/} channel}
% Source representation
\newcommand{\Labs}[2]{\lambda{#1}.\,{#2}}
\newcommand{\Lapp}[2]{{#1}\,{#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}

In this version I am providing more information about the \TPPC. I have 
yet to show formally how this calculus relates to the OGR notation, but 
I do reformulate the \F\ translation in \TPPc in an extra section. The 
rest of the information is as version 3.

\section{Syntax}

We assume a set $N$ of {\em names} ranged over by $n$, $m$, etc. and a 
disjoint set $X$ of
{\em variables} ranged over by $x$, $y$, $z$ etc. A set $\Sigma$ of 
{\em symbols} raged over by $F$, $G$, etc. each with an associated 
{\em arity} ($\geq 0$) giving the number of arguments it should take. 
These are combined in 
the set of {\em terms}, $T$ ranged over by $t$:
\begin{eqnarray*}
T & ::= & n \mid x \mid F(t_1,\dots,t_n)\:, \:\: where \: arity(F) = n
\end{eqnarray*}

$S$, the class of process {\em scripts}, 
is given by the following syntax:
\begin{eqnarray*}
S & ::= & \PPin{x}{S} \mid \PPout{t}{t'}{S} \mid \PPnew{n}{S}{S'} 
\mid \PPmatch{t}{t'}{S}{S'}
\mid A(t_1,\ldots,t_n) \mid \PPstop
\end{eqnarray*}
Also a set of recursive {\em agent} definitions is assumed: 
$\PPdef{A(x_1,\ldots,x_k)}{S}$. 

The intuition is that $S$ is the sequential body of a process.
$S$ can be input $\PPin{x}{S}$ where $x$ binds over $S$
or output $\PPout{t}{t'}{S}$ meaning send $t'$ to $t$ and behave as $S$.
The send will be asynchronous as in the asynchronous \Pc.
$S$ can also spawn a new process $\PPnew{n}{S}{S'}$ where $S$ 
is the body of the new
process. Its name will be $n$ which may be shared 
between the new process
and its creator (which will behave as $S'$).
The match construct $\PPmatch{t}{t'}{S}{S'}$ behaves as $S$ if $t$ 
and $t'$ can be unified, otherwise as $S'$. Free variables in $t$ 
and $t'$ are bound in $S$ by a successful match.

\begin{observation}
There will need to be some rules about the patterns in matches: 
free variables introduced must not be repeated; all free variables 
must be bound to terms containing no variables (hence a match 
cannot unify two variables).
\end {observation}

Recursive processes are dealt with through agent definitions.
Given a definition $\PPdef{A(x_1,\ldots,x_k)}{S}$, the script 
$A(t_1,\ldots,t_k)$ behaves as $\PPsub{S}{t_1/x_1,\ldots,t_k/x_k}$.

Parallel {\em processes} form the set $P$ defined by the following syntax:
\begin{eqnarray*}
P & ::= & \PPname{n}{S} \mid \PPpar{P}{P'} \mid \PPoutP{n}{t} 
\mid \PPres{n}{P}
\end{eqnarray*}
The term $t$ in $\PPoutP{n}{t}$ is closed, meaning that it contains 
only names and symbols.

$\PPname{n}{S}$ is a named process (the idea is similar to 
locations in some versions of  CCS).
$\PPpar{P}{P'}$ is parallel processes. It is assumed that $P$ and $P'$ 
in $\PPoutP{n}{t}$ are linear
wrt $\PPname{n}{S}$ subcomponents. This just means that named 
processes are unique.
$\PPoutP{n}{t}$ is a message $t$ on its way to process $n$ 
and $\PPres{n}{P}$ is restriction.

Free names, variables and substitution, with renaming to avoid name capture, 
are defined in an obvious way. This should be done but is left for now.

\section{Semantics}

There is an assumption that while scripts can contain
variables, during reduction communications contain only names and closed 
terms.
There are therefore some contextual constraints left vague at this point.
A sort discipline seems necessary to ensure that if a script contains 
$\PPout{t}{t'}{S}$ then either $t$ is a name, or it is a variable that 
will be bound to a name before the communication is released.

The operational semantics below encapsulates some of the assumptions by 
assuming that various terms are instantiated to names before the rules apply.
Suggestions welcomed.

The following structural rules define structural congruence of \PPc\ processes:
\begin{eqnarray*}
\PPres{n'}{\PPres{n}{P}} & \equiv & \PPres{n}{\PPres{n'}{P}} \\
\PPres{n}{P} & \equiv & P\:, \hspace{1cm} n \not\in fn(P) \\
\PPpar{\PPres{n}{P}}{P'} & \equiv & \PPres{n}{(\PPpar{P}{P'})}\:, 
\hspace{1cm} n \not\in fn(P') \\
\PPpar{(\PPpar{P}{P'})}{P''} & \equiv & \PPpar{P}{(\PPpar{P'}{P''})} \\
\PPpar{P}{P'} & \equiv & \PPpar{P'}{P} \\
\PPpar{\PPname{n}{\PPstop}}{P} & \equiv & P \\
\PPname{n}{A(t_1,\ldots,t_k)} & \equiv & \PPname{n}{\PPsub{S}{t_1/x_1,\ldots,t_k/x_k}}\:,
\hspace{0.5cm} where \:\: \PPdef{A(x_1,\ldots,x_k)}{S}
\end{eqnarray*}

The operational semantics is given as a set of reduction rules 
on processes $P$:
\begin{eqnarray*}
\PPname{n}{\PPout{n'}{t}{S}} & \rightarrow & 
\PPpar{\PPname{n}{S}}{\PPoutP{n'}{t}} \\
\PPpar{\PPname{n}{\PPin{x}{S}}}{\PPoutP{n}{t}} & \rightarrow & 
\PPname{n}{\PPsub{S}{t/x}} \\
\PPname{n}{\PPnew{n'}{S}{S'}} & \rightarrow &
\PPres{n'}{(\PPpar{\PPname{n'}{S}}{\PPname{n}{S'}})} \\
\PPname{n}{\PPmatch{t}{t'}{S}{S'}} & \rightarrow & 
\PPname{n}{\sigma(S)}\:, 
\hspace{1cm} \exists \sigma \: : \: \sigma(t) = \sigma(t') \\
\PPname{n}{\PPmatch{t}{t'}{S}{S'}} & \rightarrow & 
\PPname{n}{S'}\:, 
\hspace{1cm} \forall \sigma \: : \: \sigma(t) \neq \sigma(t')
\end{eqnarray*}
Here $\sigma$ is a mapping from variables to closed terms.

The first rule releases a message from process $n$ to 
process $n'$ with the contents $t$.
The second rule shows how a message is received by process $n$
and the third rule describes the creation of a new process $n'$.
The final reduction rules handle the match construct.

The following rules extend the reduction relation to contexts:
\begin{eqnarray*}
P \rightarrow P' & \Rightarrow & \PPres{n}{P} \rightarrow \PPres{n}{P'} \\
P \rightarrow P' & \Rightarrow & \PPpar{P}{Q} \rightarrow \PPpar{P'}{Q} \\
Q \equiv P, \; P \rightarrow P', \; P' \equiv Q' & \Rightarrow & Q \rightarrow Q'
\end{eqnarray*}

\begin{observation}
We have not discussed the initial configuration of a process 
network in this calculus, but I assume it will be something 
like $\PPres{n}{(\PPname{n}{S})}$ for some script $S$.
\end{observation}

\section{Translation of \PPc\ into the \Pc}

This suddenly becomes more difficult! The new \PPc\ has the ability 
to send arbitrary terms around. I could easily develop a \Pc\ with 
terms which would translate as easily as before. The notation \Pc\ 
with terms is what I used to use when doing translations of the \Lc\ 
to \Pc\ way back. Perhaps that is a way to go: show that \Pc\ can 
simulate \Pc\ with terms (the reverse is trivial).

\section{Translation of \Pc\ into the \PPc}

A proposed translation of the asynchronous \Pc\ is provided. 
It is assumed that the synchronous calculus can be simulated 
adequately by the asynchronous calculus.

The translation is based on the use of a process  
to implement a \Pc\ channel. This time, much simpler definitions can be used:
\begin{eqnarray*}
\PPdefn{Chan(q)}{\PPin{x}{\PPmatch{x}{Get(n)}{ChanGet(n,q)}
{\PPmatch{x}{Put(v)}{ChanPut(v,q)}{stop}}}} \\
\PPdefn{ChanGet(n,q)}{\PPmatch{q}{OQ(v,r)}{\PPout{n}{v}{Chan(r)}}
{Chan(IQ(n,q))}} \\
\PPdefn{ChanPut(v,q)}{\PPmatch{q}{IQ(n,r)}{\PPout{n}{v}{Chan(r)}}
{Chan(OQ(v,q))}}
\end{eqnarray*}
The definitions $ChanGet$ and $ChanPut$ are added for clarity; a 
single recursive definition could have been used.

A \PPc\ channel process maintains a queue of data values, provided 
by $Put$ messages or a queue of requests, provided by $Get$ messages 
which contain the names of \PPc\ processes to receive data values. 
Initially, a \Pc\ channel $n$ will be represented by a process with 
script $Chan$ holding an empty queue represented by the symbol $EQ$:
\begin{eqnarray*}
\PPname{n}{Chan(EQ)}
\end{eqnarray*}
Scripts for sending and receiving on channel $n$ by a \PPc\ process 
$m$ would be as follows:
\begin{eqnarray*}
\outacta{n}{v} & \equiv & \PPname{m}{\PPout{n}{Put(v)}{\PPstop}} \\
\inpact{n}{x}{P} & \equiv & \PPname{m}{\PPout{n}{Get(m)}{\PPin{x}{P}}}
\end{eqnarray*}

Exercises for the reader:
\begin{itemize}
\item Generalise the definition above and translation scheme below 
to support normal synchronous \Pc.
\end{itemize}

\begin{observation}
There is a close link between this notation and the style I adopted 
for the implementation notation, which I call 
{\em Object Graph Rewriting} (OGR). 
The equivalent would have been:
\begin{eqnarray*}
\Prule {Chan(OQ(v,r))} {Get(n)} {\Pcall {n} {v}} {Chan(r)} \\
\PruleChange {Chan(q)} {Get(n)} {Chan(IQ(n,q))} \\
\Prule {Chan(IQ(n,r))} {Put(v)} {\Pcall {n} {v}} {Chan(r)} \\
\PruleChange {Chan(q)} {Put(v)} {Chan(OQ(v,q))}
\end{eqnarray*}
A concept of rule priority is assumed. Slightly more rules are 
required if we do not assume priorities:
\begin{eqnarray*}
\Prule {Chan(OQ(v,r))} {Get(n)} {\Pcall {n} {v}} {Chan(r)} \\
\PruleChange {Chan(EQ)} {Get(n)} {Chan(IQ(n,EQ))} \\
\PruleChange {Chan(IQ(m,r))} {Get(n)} {Chan(IQ(n,IQ(m,r)))} \\
\Prule {Chan(IQ(n,r))} {Put(v)} {\Pcall {n} {v}} {Chan(r)} \\
\PruleChange {Chan(EQ)} {Put(v)} {Chan(OQ(v,EQ))} \\
\PruleChange {Chan(OQ(w,r))} {Put(v)} {Chan(OQ(v,OQ(w,r)))}
\end{eqnarray*}
An alternative, very much in the style of the Facile CHAM and as 
presented to the Aarchen Implementation Workshop is to maintain two queues, 
at least one of which is always empty. 
A new channel has state of the form $Chan(EQ,EQ)$:
\begin{eqnarray*}
\PruleChange {Chan(q,EQ)} {In(r)} {Chan(IQ(r,q),EQ)} \\
\PruleChange {Chan(EQ,q)} {Out(v)} {Chan(EQ,OQ(v,q))} \\
\Prule {Chan(EQ,OQ(v,q))} {In(r)} {\Pcall {r} {v}} {Chan(EQ,q)} \\
\Prule {Chan(IQ(r,q),EQ)} {Out(v)} {\Pcall {r} {v}} {Chan(q,EQ)}
\end{eqnarray*}
It seems a fairly simple matter to cast OGR as a derived syntax for \PPc\ with 
terms. (Hence my suggestion of going this way).
\end{observation}

We give a possible translation from asynchronous \Pc\ to \PPc.
Note that the \Pc\ to \PPc\ translation only used asynchronous 
sends. The translation uses a function $r$ with auxiliary 
function $t$ which does the real work. The function $t$ 
carries the name of a \PPc\ process associated with the
translated network. This is needed when simulating \Pc\ 
communication since the channel processes need the name 
of the receiving \PPc\ process. 
\begin{eqnarray*}
r\sembrac{N} & = & \PPres{m}{(\PPname{m}{t\sembrac{N}_m})}\;, \:\:m \not\in fn(N) \\
\\
t\sembrac{\inpact{n}{n'}{N}}_m & = & \PPout{n}{Get(m)}{\PPin{n'}{t\sembrac{N}_m}} \\
t\sembrac{\outacta{n}{n'}}_m & = & \PPout{n}{Put(n')}{\PPstop} \\
t\sembrac{\restrict{n}{N}}_m & = & \PPnew{n}{Chan(EQ)}{t\sembrac{N}_{m}} \\
t\sembrac{\parprocs{N}{N'}}_m & = & \PPnew{m'}{t\sembrac{N}_{m'}}
{t\sembrac{N'}_m}\;, \:\:m' \not\in fn(\parprocs{N}{N'}) \\
t\sembrac{\match{n}{n'}{N}}_m & = & 
\PPmatch{n}{n'}{t\sembrac{N}_m}{\PPstop} \\
t\sembrac{\nonmatch{n}{n'}{N}}_m & = & 
\PPmatch{n}{n'}{\PPstop}{t\sembrac{N}_m} \\
t\sembrac{\agtuse{A}{n_1,\ldots,n_k}}_m & = & \agtuse{A}{n_1,\ldots,n_k} \\
t\sembrac{\inaction}_m & = & stop
\end{eqnarray*}
For symmetry it would be possible to create new processes for each process
in $(\parprocs{N}{N'})$ rather than keep one thread in the old process.

A further function $f$ handles
agent definitions:
\begin{eqnarray*}
f\sembrac{\agtdef{A}{n_1,\ldots,n_k}{N}} & = & 
\PPnew{m}{t\sembrac{N}_m}{\PPstop}\;, \:\:m \not\in fn(N)
\end{eqnarray*}

\begin{observation}
As before, I am afraid I have not checked any of it too well and a test 
using a simple example is necessary.

I have given some thought to term--passing \Pc\ which I don't think is 
too hard to formalise as a derived syntax from \Pc. More later -- but 
maybe not for a little while.
\end{observation}

\section{Translation of the \F\ 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.

\subsection{Source Language Syntax}
The language is the \Lc\ with constants and pairing. The trivial
value and pairing operator could have been considered as normal constants.
\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 features of \F\ are encoded in our source language as special constants 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$.

The function $channel$ takes a trivial value and returns a new 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, the scripts of processes, is provided by using delay closures,
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.

\subsection{Translation of the Source Language into OGR}
This translation was presented in a paper at the Aachen Implementation 
Workshop.
The model for channels is different from the Aachen presentation and 
closer to the
style described in the last section.

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 {\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 {c}{u} {\Pcall {u}{Unit(c)}} \\
\transdef {\Ltriv}{u} {\Pcall {u} {Triv}} \\
\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(EQ)}} }\\
\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$ are:
\begin{eqnarray*}
\Prule {Chan(OQ(oq,v,s))} {In(r)} {\Ppar {\Pcall {r} {v}} {\Pcall {s}
{Triv}}} {Chan(oq)} \\
\PruleChange {Chan(q)} {In(r)} {Chan(IQ(q,r))} \\
\Prule {Chan(IQ(iq,r))} {Out(v,s)} {\Ppar {\Pcall {r} {v}} {\Pcall {s}
{Triv}}} {Chan(iq)} \\
\PruleChange {Chan(q)} {Out(v,s)} {Chan(OQ(q,v,s))}
\end{eqnarray*}
When a process representing a new channel is created, the initial state 
has an empty
queue: $\Pdef {c} {Chan(EQ)}$ as seen above.

The form of channel used here handles synchronous communication by 
recording both a data value and the sender of the data. It differs 
from the asynchronous channel model described in the last section.

\subsection{Translation of the Source Language into \TPPC}
Here I give the same rules in the \TPPc--style. Most of the OGR rules 
leave the
{\em process state} unchanged. In \TPPc\ we must make the replication 
explicit.
\begin{eqnarray*}
\transdef {x}{u} {\PPout {u} {Unit(x)} {\PPstop}} \\
\transdef {\Labs{x}{e}}{u} {\PPnew {y} {Y(fv(\Labs{x}{e}))} ({\PPout {u} 
{Unit(y)} {\PPstop}})} \\
\PPwhere {Y(fv(\Labs{x}{e}))} {\PPin{v}{\PPnew{w}{(\PPmatch{v}{Doub(b,x)} 
{\transexp{e}{b}} {\PPstop})}{Y(fv(\Labs{x}{e}))}}} \\
\transdef {\Lapp{e}{e'}}{u} {\PPnew {a} {A(u,fv(e'))} {\transexp{e}{a}}} \\
\PPwhere {A(u,fv(e'))} {\PPin{v}{\PPnew{w}{(\PPmatch{v}{Unit(y)} {\PPnew{b} 
{B(u,y)} {\transexp{e}{b}}} {\PPstop})}{A(u,fv(e'))}}} \\
\PPand {B(u,y)} {\PPin{v} {\PPnew{w} {(\PPmatch{v}{Unit(z)} {\PPout {y}
{Doub(u,z)} {\PPstop}} {\PPstop})}{B(u,y)}}} \\
\transdef {c}{u} {\PPout {u} {Unit(c)} {\PPstop}} \\
\transdef {\Ltriv}{u} {\PPout {u} {Triv} {\PPstop}} \\
\transdef {\Lpair{e}{e'}}{u} {\PPnew {a} {A(u,fv(e'))} {\transexp{e}{a}}} \\
\PPwhere {A(u,fv(e'))} {\PPin{v}{\PPnew{w}{(\PPmatch{v}{Unit(y)} 
{\PPnew{b} {B(u,y)} {\transexp{e}{b}}} {\PPstop})}{A(u,fv(e'))}}} \\
\PPand {B(u,y)} {\PPin{v} {\PPnew{w} {(\PPmatch{v}{Unit(z)} {\PPout {u}
{Doub(y,z)} {\PPstop}} {\PPstop})}{B(u,y)}}}
\end{eqnarray*}

The translation of the various constant functions for arithmetic and the
operators of \F\ is as follows:
\begin{eqnarray*}
\transdef {succ}{u} {\PPnew {f} {Succ} ({\PPout {u} {Unit(f)} {\PPstop}})} \\
\PPwhere {Succ} {\PPin{v}{\PPmatch{v}{Doub(b,x)} {\PPout{b}{Unit(x+1)}
{Succ}} {\PPstop}}} \\
\transdef {mul}{u} {\PPnew {f} {Mul} ({\PPout {u} {Unit(f)} {\PPstop}})} \\
\PPwhere {Mul} {\PPin{v}{\PPmatch{v}{Doub(b,Pair(x,y))} {\PPout{b}
{Unit(x*y)}{Mul}} {\PPstop}}} \\
\transdef {channel}{u} {\PPnew {f} {Channel} ({\PPout {u} {Unit(f)} 
{\PPstop}})} \\
\PPwhere {Channel} {\PPin{v}{\PPmatch{v}{Doub(b,Triv)} {NewChan(b)}
{\PPstop}}} \\
\PPand {NewChan(b)} {\PPnew{c} {Chan(EQ)} {\PPout{b}{Unit(c)}{Channel}}} \\
\transdef {send}{u} {\PPnew {f} {Send} ({\PPout {u} {Unit(f)} {\PPstop}})} \\
\PPwhere {Send} {\PPin{v}{\PPmatch{v}{Doub(b,Pair(c,v))} {\PPout{c}
{Out(v,s)}{Send}} {\PPstop}}} \\
\transdef {receive}{u} {\PPnew {f} {Receive} ({\PPout {u} {Unit(f)} 
{\PPstop}})} \\
\PPwhere {Receive} {\PPin{v}{\PPmatch{v}{Doub(b,c)} {\PPout{c}{In(b)}
{Receive}} {\PPstop}}} \\
\transdef {spawn}{u} {\PPnew {f} {Spawn} ({\PPout {u} {Unit(f)} 
{\PPstop}})} \\
\PPwhere {Spawn} {\PPin{v}{\PPmatch{v}{Doub(b,p)} {DoSpawn(b,p)} 
{\PPstop}}} \\
\PPand {DoSpawn(b,p)} {\PPout{b}{Unit(Triv)} {\PPnew{s}{Sink}{\PPout{p}
{Doub(Triv,s)}{Spawn}}}} \\
\PPand {Sink} {\PPin{v} {\PPstop}}
\end{eqnarray*}
The rules for $Chan$ are:
\begin{eqnarray*}
\PPdefn{Chan(q)}{\PPin{x}{\PPmatch{x}{In(r)}{ChanGet(q,r)}
{\PPmatch{x}{Out(v,s)}{ChanPut(q,v,s)}{stop}}}} \\
\PPdefn{ChanGet(q,r)}{\PPmatch{q}{OQ(oq,v,s)}{\PPout{r}{v}{\PPout{s}
{Triv}{Chan(oq)}}}{Chan(IQ(q,r))}} \\
\PPdefn{ChanPut(q,v,s)}{\PPmatch{q}{IQ(iq,r)}{\PPout{r}{v}{\PPout{s}
{Triv}{Chan(iq)}}}{Chan(OQ(q,v,s))}}
\end{eqnarray*}

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