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

%\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{\PPdef}[3]{{#1}:{#2} = {#3}}
\newcommand{\PPstop}[0]{\bf stop}
\newcommand{\PPempty}[0]{()}
\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}[4]{{#1}={#2} \cdot {#3} \; : \; {#4}}
\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{\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{\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}

This version proposes an alternative formulation of \TPPc\ which aims to have a more uniform syntax. We still have a much simplified syntactic class for {\em scripts}.

\section{Syntax for \TPPC}

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 \PPmatch{x}{t}{S}{S'} \mid A(t_1,\ldots,t_n)
\end{eqnarray*}
Also a set of recursive {\em agent} definitions is assumed: 
$\PPdef{n}{A(x_1,\ldots,x_k)}{P}$. 

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.

Recursive processes 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 avoided by substitution, I think it would be possible for free names to appear. Agent definitions also support spawning of new processes and termination of the current process.

Parallel {\em processes} form the set $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{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 & {\PPsub{P}{n/m,t_1/x_1,\ldots,t_k/x_k}}\:,
\hspace{0.5cm} where \:\: \PPdef{m}{A(x_1,\ldots,x_k)}{P}
\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)
\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}{A})}$ for some agent $A$.
\end{observation}

The new formulation removes several forms of process script which appeared in Version 5 and modifies the nature of agent definitions. The original was:
\begin{eqnarray*}
S & ::= & \PPin{x}{S} \mid \PPout{t}{t'}{S} \mid \PPnew{n}{S}{S'} 
\mid \PPmatch{x}{t}{S}{S'}
\mid A(t_1,\ldots,t_n) \mid \PPstop
\end{eqnarray*}
with agent definitions of the form: 
$A(x_1,\ldots,x_k) = S$. 

There are new way of expressing each of the missing forms. Each of them uses an agent definition which takes suitable arguments to capture the free names of the scripts involved.

$\PPout{t}{t'}{S}$ would become a use of an agent $A$ where $\PPdef{m}{A}{(\PPpar{\PPoutP{t}{t'}}{\PPname{m}{S}})}$. 

$\PPnew{n}{S}{S'}$ would become a use of an agent $A$ where $\PPdef{m}{A}{\PPres{n}{(\PPpar{\PPname{n}{S}}{\PPname{m}{S'}})}}$.

$\PPstop$ would become a use of an agent $Stop$ where $\PPdef{m}{Stop}{\PPempty}$.

The new formulation is somewhat simpler, which must be a good thing. It is also slightly more powerful. The new formulation of agent definitions allows spawning of a complete process network including one process which keeps the name of the creator process. The $\nu$ construct had some restrictions. For example, consider how the script for the following agent might be coded in the original style. Agents $B$, $C$ and $D$ are aware of the identities of $m$, $n$, and $o$:
\begin{eqnarray*}
\PPdef{m}{A}{\PPres{o}{\PPres{n}{(\PPpar{\PPpar{\PPname{m}{B(m,n,o)}}{\PPname{n}{C(m,n,o)}}}
{\PPname{o}{D(m,n,o)}})}}}
\end{eqnarray*}
The problem is that $\nu$ has to create processes one at a time, so that one of $n$ and $o$, say $n$, is created before the other exists and I believe that communication would be required to inform $n$ of the identity of $o$.

The translations need to be reworked in the new style. For the moment, that is an exercise for the reader.

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