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

\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}\}}
%\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{\inaction}{0}
\newcommand{\pair}[2]{{#1}\,{#2}}
\newcommand{\triv}{}
%\input{john-proc-macros}
% New Process notation
\newcommand{\PruleChange}[3]{{#1}\;?\;{#2} & := & {#3}}
\newcommand{\PruleSpawn}[3]{{#1}\;?\;{#2} & \rightarrow & (\,{#3}\,)}
\newcommand{\Prule}[4]{{#1}\;?\;{#2} & \rightarrow & (\,{#3}\,)\;:=\;{#4}}
\newcommand{\Ppar}[2]{{#1}\,|\,{#2}}
\newcommand{\Pcall}[2]{{#1}\,!\,{#2}}
\newcommand{\Pdef}[2]{{#1}:\,{#2}}
% Translation representation
\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{\RA}{{\em return-address\/} channel}
% Translation representation
\newcommand{\transexp}[2]{\sembrac{#1}_{#2}}
\newcommand{\transdef}[3]{\transexp{#1}{#2} & = & {#3}}
% End of macros
\begin{document}
\maketitle

\section{Introduction}

This is an attempt to ``formalise'' the \PPc. It is based on the 
original notes
from Lone and Bent with more detail added and me observations made.
Mostly I have just turned the email into \LaTeX\ which is no great 
contribution.

There is some doubt about whether it is useful to distinguish names 
and variables. I think the existing treatment is muddled, but I 
have left the distinction there until we decide whether it makes sense.

\section{Syntax}

We assume a set $N$ of names ranged over by $n$, $m$, etc. and a 
disjoint set $X$ of
variables ranged over by $x$, $y$, $z$ etc.
Also a set of recursive agent definitions is assumed: 
$\PPdef{A(x_1,\ldots,x_k)}{S}$. $S$, the class of {\em process scripts}, 
is given by the following syntax:

\begin{eqnarray*}
S & ::= & \PPin{x}{S} \mid \PPout{n}{n'}{S} \mid \PPnew{x}{S}{S'} 
\mid A(x_1,\ldots,x_n) \mid \PPstop
\end{eqnarray*}

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{n}{n'}{S}$ meaning send $n'$ to $n$ and behave as $S$.
The send will be asynchronous as in the asynchronous \Pc.
$S$ can also spawn a new process $\PPnew{x}{S}{S'}$ where $S$ 
is the body of the new
process. Its name will be bound to $x$ which may be shared 
between the new process
and its creator (which will behave as $S'$).
Recursive processes are dealt with through agent definitions
and $A(n_1,\ldots,n_k)$ behaves as $\PPsub{S}{n_1/x_1,\ldots,n_k/x_k}$ 
if $A(x_1,\ldots,x_k) = S$

Parallel processes are defined by the following syntax:

\begin{eqnarray*}
P & ::= & \PPname{n}{S} \mid \PPpar{P}{P'} \mid \PPoutP{n}{n'} 
\mid \PPres{n}{P}
\end{eqnarray*}

$\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}{n'}$ are linear
wrt $\PPname{n}{S}$ subcomponents. This just means that named 
processes are unique.
$\PPoutP{n}{n'}$ is a message $n'$ on its way to process $n$ 
and $\PPres{n}{P}$ is restriction.
Free names, variables and substitution are defined as usual.

\section{Semantics}

The operational semantics is given as a set of reduction rules 
on processes $P$:
\begin{eqnarray*}
\PPname{n}{\PPout{n'}{n''}{S}} & \rightarrow & 
\PPpar{\PPname{n}{S}}{\PPoutP{n'}{n''}} \\
\PPpar{\PPname{n}{\PPin{x}{S}}}{\PPoutP{n}{n'}} & \rightarrow & 
\PPname{n}{\PPsub{S}{n'/x}} \\
\PPname{n}{\PPnew{x}{S}{S'}} & \rightarrow &
\PPres{n'}{(\PPpar{\PPname{n}{\PPsub{S'}{n'/x}}}
{\PPname{n'}{\PPsub{S}{n'/x}}})}\:,
\hspace{1cm} n' \not\in fn(\PPname{n}{\PPnew{x}{S}{S'}}) \\
\end{eqnarray*}

The first rule ``releases'' a message from process $n$ to 
process $n'$ with the 
contents $n''$.
The second rule shows how a message is received by process $n$
and the third rule describes the creation of a new process $n'$

A simpler version of the last rule is possible if variables 
and names form one class:
\begin{eqnarray*}
\PPname{n}{\PPnew{x}{S}{S'}} & \rightarrow &
\PPres{x}{(\PPpar{\PPname{x}{S}}{\PPname{n}{S'}})} \\
\end{eqnarray*}

These rules may be applied modulo the following structural rules:
\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 \\
\end{eqnarray*}

\begin{observation}
The final cleanup rule for processes might be extended to clean up 
messages as well. I believe we could do this by first eliminating 
messages destined for a stopped process, and then removing the 
process once no further messages could possibly be sent to it. 
This is achieved by these congruence rules:
\begin{eqnarray*}
\PPpar{\PPoutP{n}{n''}}{\PPname{n}{\PPstop}} & \equiv & 
{\PPname{n}{\PPstop}} \\
\PPpar{\PPres{n}{(\PPname{n}{\PPstop})}}{P} & \equiv & P \\
\end{eqnarray*}
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$. I think 
it should be clear that there will never be any free names in 
the resulting network.
\end{observation}

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

This is given as two translation functions:

$s\sembrac{S}_n$ where $S$ is a process script and $n$ is a name, and 
$p\sembrac{P}$ where $P$ is a parallel process.
\begin{eqnarray*}
s\sembrac{\PPin{x}{S}}_n & = & \inpact{n}{x}{s\sembrac{S}} \\
s\sembrac{\PPout{n'}{n''}{S}}_n & = & 
\parprocs{\outact{n'}{n''}{\inaction}}{s\sembrac{S}_n} \\
s\sembrac{\PPnew{x}{S}{S'}}_n & = &
\restrict{n'}{\parprocs{s\sembrac{\PPsub{S}{n'/x}}_{n'}}
{s\sembrac{\PPsub{S'}{n'/x}}_n}}\:,
\hspace{1cm} n' \not\in fn(\PPnew{x}{S}{S'}) \\
s\sembrac{A(x_1,\ldots,x_k)}_n & = & A(x_1,\ldots,x_k) 
\hspace{1cm} where \hspace{1cm} A(x_1,\ldots,x_k) = s\sembrac{S}_n \\
s\sembrac{stop}_n & = & nil \\
\\
p\sembrac{\PPname{n}{S}} & = & s\sembrac{S}_n \\
p\sembrac{\PPpar{P}{P'}} & = & \parprocs{p\sembrac{P}}{p\sembrac{P'}} \\
p\sembrac{\PPoutP{n}{n'}} & = & \outact{n}{n'}{\inaction} \\
p\sembrac{\PPres{n}{P}} & = & \restrict{n}{p\sembrac{P}} \\
\end{eqnarray*}

Again, a simpler translation is possible if variables and 
names form one class:
\begin{eqnarray*}
s\sembrac{\PPnew{x}{S}{S'}}_n & = &
\restrict{x}{\parprocs{s\sembrac{S}_{x}}{s\sembrac{S'}_n}}\\
\end{eqnarray*}


It seems rather straightforward to prove the following 
(modulo structural equivalence):
\begin{eqnarray*}
P \rightarrow P' & \Rightarrow & p[P] \rightarrow p[P']
\end{eqnarray*}

For stronger results we should define a notion of equivalence, e.g. barbed
bisimulation could be defined as:

$P \sim Q$ iff
\begin{itemize}
\item $P \rightarrow P'$ then $Q \rightarrow Q'$ and $P' \sim Q'$
\item the reverse
\item $P \uparrow$ iff $Q \uparrow$
\end{itemize}
where $\uparrow$ ({\em commit}) is defined as 
$C[\PPoutP{n}{n'}] \uparrow\ \PPoutP{n}{}$ 
and $C[\PPname{n}{\PPin{x}{S}}] \uparrow\ \PPin{n}{}$
and $C$ is a one hole context of processes.

\begin{observation}
The original said $c?$ rather than $n?$. I assume the latter was meant.
\end{observation}

With this we could prove
\begin{eqnarray*}
P \sim Q & \Rightarrow & p\sembrac{P} \approx p\sembrac{Q}
\end{eqnarray*}
where $\approx$ is barbed bisimulation on the \Pc.

\section{Derived syntax}

The above calculus may be viewed as an assembly language for point to point
asynchronous communication.
We may want to introduce a notion of sending and receiving pairs.
It is not obivous that this can be encoded (as it is the case for the
\Pc).
With pairs we should be able to encode the derived syntax that John has been
using for the encoding of lambda calculus and Facile, but some work is needed
on this. If it works out fine we will get indirectly an encoding of 
the \Pc\ into the \PPc\ since the \Pc\ is a 
subcalculus of Facile and Facile translates into the derived syntax. It may
be interesting to do this directly for comparison.
We may also want to go straight for an operational semantics for the derived 
syntax.

The route through Facile for this translation is
a bit contorted. It may be better and quite interesting to do it directly.
We may want to add a comparison/match operator to \PPc.

The new rule would be something like:
\begin{eqnarray*}
S & ::= & \PPmatch{x}{y}{S}{S'}
\end{eqnarray*}

With semantics:
\begin{eqnarray*}
\PPname{n}{\PPmatch{n}{n}{S}{S'}} & \rightarrow & 
\PPname{n}{S} \\
\PPname{n}{\PPmatch{n}{n'}{S}{S'}} & \rightarrow & 
\PPname{n}{S'}\:, \hspace{1cm} n \neq n'
\end{eqnarray*}
\begin{observation}
This is not as suggested before - it is a reduction. Maybe it is a bad idea to make it a reduction, and perhaps the structural congruence could be used. I am not sure of the implications.

\newcommand{\PPmatchO}[3]{[{#1} = {#2}]\,{#3}}
I think it needs to be two--armed. It may be possible to make it one--armed with semantics:
\begin{eqnarray*}
\PPname{n}{\PPmatchO{n}{n}{S}} & \rightarrow & 
\PPname{n}{S} \\
\PPname{n}{\PPmatchO{n}{n'}{S}} & \rightarrow & 
\PPname{n}{\PPstop}\:, \hspace{1cm} n \neq n'
\end{eqnarray*}

However, I cannot see how to use this at present as you still need the concept of an action to take if the match fails.
\end {observation}

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