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

%\newcommand{\comment}[1]{} % Comment out text. JRWG
\newcommand{\comment}[1]{\{\{{\sf #1}\}\}} % Highlight text. JRWG

\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{\PPmatches}[3]{{#1},\,{#2}\,:\,{#3}}
\newcommand{\PPabs}[2]{\lambda{#1}\,{#2}}
\newcommand{\PPdef}[2]{{#1} = {#2}}
\newcommand{\PPstop}[0]{Stop}
\newcommand{\PPempty}[0]{()}
\newcommand{\PPname}[2]{{#1}:\,{#2}}
\newcommand{\PPpar}[2]{{#1}\,\|\,{#2}}
\newcommand{\PPres}[2]{\nu{#1}\,{#2}}
\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}[4]{{#1}={#2} \cdot {#3} \; : \; {#4}}
\newcommand{\inaction}{0}
\newcommand{\pair}[2]{{#1}\,{#2}}
\newcommand{\triv}{}
%\input{john-proc-macros}
% New Process notation
\newcommand{\Ppar}[2]{{#1},\;{#2}}
\newcommand{\Pcall}[2]{{#1}\,!\,{#2}}
\newcommand{\Pdef}[2]{{#1}:{#2}}
\newcommand{\Prule}[5]{\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}} & \rightarrow & \Ppar{\Pdef{#1}{#5}}{#4}}
\newcommand{\PruleChange}[4]{\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}} & \rightarrow & \Pdef{#1}{#4}}
\newcommand{\PruleSpawn}[4]{\Prule{#1}{#2}{#3}{#4}{#2}}
% Translation representation
\newcommand{\transwhere}[4]{& & {\makebox[1.5cm][l]{where}}
\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}}  \rightarrow  \Ppar{\Pdef{#1}{#2}}{#4}}
\newcommand{\transand}[4]{& & {\makebox[1.5cm][l]{and}}
\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}}  \rightarrow  \Ppar{\Pdef{#1}{#2}}{#4}}
\newcommand{\PPwhere}[2]{where & & {#1} \; = \; {#2}}
\newcommand{\PPand}[2]{and & & {#1} \; = \; {#2}}
\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{\TPC}{Term--$\pi$--Calculus}
\newcommand{\TPc}{term--$\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{\OGRe}{OGRe}
\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{History}

This version is denoted {\em Version G\/} rather then {\em Version 7\/} to reflect the file name I am using. The document works with the formulation of \PPc\ introduced under the name \TPPc\ in {\em Version 6\/} which aims to have a more uniform syntax using a much simplified syntactic class for {\em scripts}. However, the central role of agent definitions is softened by the introduction of {\em abstractions} over process names.

This document is very much an outline, with detail and introduction to be filled in.

\section{Introduction}

Awaits material giving proper motivation and a gentle introduction to the world of processes and messages we are considering.

The paper gives a definition of the syntax and semantics of \PPc. We show that the notation is powerful enough to simulate the \Pc, giving an encoding of \Pc terms in the \PPc. We also (will) prove that the encoding is correct. This encoding represents the names of the \Pc, which can be though of as unbuffered communication channels, as \PPc\ processes which act as mailboxes.

We (will) go on to show that any \PPc\ system may be simulated using the \Pc.

It has been demonstrated that the \Lc\ can be modelled using the \Pc. Clearly, the \PPc\ can model the \Lc\ through simulation of the corresponding \Pc. However, a more direct translation is also presented and (will be) shown to be correct.

We (will) also give a translation of the \PPc\ into Object Graph Rewriting (\OGRe).

The \Lc\ can be modelled in \OGRe\ via the translation of the equivalent \PPc\ term. We (will) also give a more direct translation.

\section{\PPC\ 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*}

$P$, the class of process, and $S$, the class of process {\em scripts}, are defined in terms of each other.

$S$ is given by the following syntax:
\begin{eqnarray*}
S & ::= & \PPin{x}{S} \mid \PPmatch{x}{t}{S}{S'} \mid \PPabs{n}{P} \mid A(t_1,\ldots,t_n)
\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.
An input--guarded script takes the form $\PPin{x}{S}$ where $x$ binds over $S$.
The match construct $\PPmatch{x}{t}{S}{S'}$ tests to see if the term 
bound to $x$ matches the term $t$. The term contains one or more 
symbols, and may contain variables but no bound names. The 
construct behaves as $S$ if the term bound to $x$ matches $t$. 
If the match fails it behaves as $S'$. Variables in $t$ 
and $t'$ are bound in $S$ by a successful match.

Abstractions of the form $\PPabs{n}{P}$ denote scripts which can release the process network defined by P. This construct can be used to provide process spawning and to create messages.

Recursive scripts are dealt with through agent definitions. I am tempted to say that all free names in the body of the definition should appear in the head, but as long as capture of free names is prevented during substitution, I think it would be possible for free names to appear. These free names would identify processes existing in the original process configuration.

Parallel {\em processes} form the class $P$ defined by the following syntax:
\begin{eqnarray*}
P & ::= & \PPname{n}{S} \mid \PPoutP{n}{t} 
\mid \PPres{n}{P} \mid \PPpar{P}{P'} \mid \PPempty
\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).
$\PPoutP{n}{t}$ is a message $t$ on its way to process $n$ 
and $\PPres{n}{P}$ is restriction.
$\PPpar{P}{P'}$ denotes parallel composition of processes, and $\PPempty$ is the empty composition. 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.

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

\section{\PPC\ 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 an agent definition contains 
$\PPoutP{t}{t'}$ then either $t$ is a name, or it is a variable that 
will be bound to a name when the definition is expanded.

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{P}{\PPempty} & \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*}
\PPpar{\PPname{n}{\PPin{x}{S}}}{\PPoutP{n}{t}} & \rightarrow & 
\PPname{n}{\PPsub{S}{t/x}} \\
\PPname{n}{\PPmatch{x}{t}{S}{S'}} & \rightarrow & 
\PPname{n}{\sigma(S)}\:, 
\hspace{1cm} \exists \sigma \: : \: x = \sigma(t) \\
\PPname{n}{\PPmatch{x}{t}{S}{S'}} & \rightarrow & 
\PPname{n}{S'}\:, 
\hspace{1cm} \forall \sigma \: : \: x \neq \sigma(t) \\
\PPname{n}{\PPabs{m}{P}} & \rightarrow & {\PPsub{P}{n/m}}
\end{eqnarray*}
Here $\sigma$ is a mapping from variables to closed terms.

The first rule shows how a message is received by process $n$.
The second and third reduction rules handle the match construct.
The final rule applies an abstraction and may involve process spawning and message creation.

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}
An alternative would be to consider application of a name to an abstraction to be a part of the structural equivalence relation rather than a reduction. It seems more natural to me that process spawning and message creation should be accompanied by a reduction.
\end{observation}

\begin{observation}
We have not discussed the initial configuration of a process 
network in this calculus. If we disallow free names in agent definitions, then, without loss of generality, 
it could take the form $\PPres{n}{(\PPname{n}{A})}$ for some agent $A$ of arity $0$.
\end{observation}

To spawn a message $t'$ directed to process $t$ and continue with 
a script $S$ we can use an abstraction
$\PPabs{m}{(\PPpar{\PPoutP{t}{t'}}{\PPname{m}{S}})}$. 

To spawn a new process running script $S$, and continue with script $S'$
we can use an abstraction $\PPabs{m}{\PPres{n}{(\PPpar{\PPname{n}{S}}{\PPname{m}{S'}})}}$.

More complex process networks and numbers of messages may be created using such abstractions. Abstractions also allow a process to discover its identity. The script $S$ in the following abstraction finds $n$ bound to its process name: $\PPabs{n}{(\PPname{n}{S})}$.

To terminate a process we can invoke a definition $Stop$ where $\PPdef{Stop}{\PPabs{n}{\PPempty}}$. An agent $Stop$ with this definition is assumed to exist in the rest of the paper.

\section{Simulation of \Pc\ by \PPc}

A proposed translation of the \Pc\ is provided. We assume that agent 
definitions take the place of replication in the \Pc.

The translation is based on the use of a process  
to implement a \Pc\ name (communication channel).
A \PPc\ channel process maintains either a queue of requests,
which are provided by $Get$ messages, or a queue of
data values and synchronisation addresses, which are provided 
by $Put$ messages. 
$Get$ messages contain the names of \PPc\ processes to receive data values. 
$Put$ messages contain a value to be sent and the name of a \PPc\ process to receive a synchronisation message when the communication completes.

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

\begin{eqnarray*}
\PPdefn{Chan(q)}{\PPin{x}{\PPmatch{x}{Get(n)}{ChanGet(n,q)}
{\PPmatch{x}{Put(v,s)}{ChanPut(v,s,q)}{Stop}}}} \\
\PPdefn{ChanGet(n,q)}{\PPmatch{q}{OQ(v,s,r)}{Reply(n,v,s,r)}
{Chan(IQ(n,q))}} \\
\PPdefn{ChanPut(v,s,q)}{\PPmatch{q}{IQ(n,r)}{Reply(n,v,s,r)}
{Chan(OQ(v,s,q))}} \\
\PPdefn{Reply(n,v,s,r)}{\PPabs{m}{(\PPpar{\PPoutP{n}{v}}{\PPpar{\PPoutP{s}{Sync}}{\PPname{m}{Chan(r)}}})}}
\end{eqnarray*}
The definitions $ChanGet$ and $ChanPut$ are added for clarity; a 
single recursive definition could have been used.

We give a possible translation from asynchronous \Pc\ to \PPc.
Note that the \Pc\ to \TPPc\ translation only used asynchronous 
sends. The translation uses a function $r$, mapping \Pc\ terms to processes,
with auxiliary 
function $t$ which maps \Pc\ terms to scripts. A further function $f$ maps \Pc\ agent defintions to \PPc\ definitions.

In the following, names $m$ and $m'$ are not in $fn(N)$ or $fn(N')$: 
\begin{eqnarray*}
r\sembrac{N} & = & \PPres{m}{(\PPname{m}{t\sembrac{N}})} \\
\\
t\sembrac{\inpact{n}{n'}{N}} & = &
    \PPabs{m}{(\PPpar{\PPoutP{n}{Get(m)}}{\PPname{m}{\PPin{n'}{t\sembrac{N}}}})} \\
t\sembrac{\outact{n}{n'}{N}} & = &
    \PPabs{m}{(\PPpar{\PPoutP{n}{Put(n',m)}}{\PPname{m}{\PPin{m'}{t\sembrac{N}}}})} \\
t\sembrac{\restrict{n}{N}} & = &
    \PPabs{m}{(\PPpar{\PPname{n}{Chan(EQ)}}{\PPname{m}{t\sembrac{N}}})} \\
t\sembrac{\parprocs{N}{N'}} & = &
    \PPabs{m}{\PPres{m'}{(\PPpar{\PPname{m}{t\sembrac{N}}}{\PPname{m'}{t\sembrac{N'}}})}} \\
t\sembrac{\agtuse{A}{n_1,\ldots,n_k}} & = & A(n_1,\ldots,n_k) \\
t\sembrac{\inaction} & = & \PPstop \\
\\
f\sembrac{\agtdef{A}{n_1,\ldots,n_k}{N}} & = &
    \PPdef{A(n_1,\ldots,n_k)}{t\sembrac{N}}
\end{eqnarray*}

For symmetry we could have generated a script which creates a new \PPc\ process for each process
in $(\parprocs{N}{N'})$. In the translation given, we keep one thread in the old \PPc\ process.

For most purposes an asynchronous form of the \Pc\ is adequate. To simulate the asynchronous \Pc\ we can simplify the definition of the channel processes and change the translation of output actions:

\begin{eqnarray*}
\PPdefn{AChan(q)}{\PPin{x}{\PPmatch{x}{AGet(n)}{AChanGet(n,q)}
{\PPmatch{x}{APut(v)}{AChanPut(v,q)}{Stop}}}} \\
\PPdefn{AChanGet(n,q)}{\PPmatch{q}{OQ(v,r)}{AReply(n,v,r)}
{Chan(IQ(n,q))}} \\
\PPdefn{AChanPut(v,q)}{\PPmatch{q}{IQ(n,r)}{AReply(n,v,r)}
{Chan(OQ(v,q))}} \\
\PPdefn{AReply(n,v,r)}{\PPabs{m}{(\PPpar{\PPoutP{n}{v}}{\PPname{m}{AChan(r)}})}} \\
\\
t\sembrac{\inpact{n}{n'}{N}} & = &
    \PPabs{m}{(\PPpar{\PPoutP{n}{AGet(m)}}{\PPname{m}{\PPin{n'}{t\sembrac{N}}}})} \\
t\sembrac{\outacta{n}{n'}} & = &
    \PPabs{m}{\PPoutP{n}{APut(n')}} \\
t\sembrac{\restrict{n}{N}} & = &
    \PPabs{m}{(\PPpar{\PPname{n}{AChan(EQ)}}{\PPname{m}{t\sembrac{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.
\end{observation}

\section{Simulation of \Lc\ by \PPc}

It has been demonstrated that the \Lc\ can be modelled using the \Pc. Clearly, the \PPc\ can model the \Lc\ through simulation of the corresponding \Pc. However, a more direct translation is also presented and (will be) shown to be correct.

\section{Simulation of \PPc\ by \OGRe}

We (will) also give a translation of the \PPc\ into Object Graph Rewriting (\OGRe).

\section{Simulation of \Lc\ by \OGRe}

The \Lc\ can be modelled in \OGRe\ via the translation of the equivalent \PPc\ term. We (will) also give a more direct translation.

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