%%% Start of LaTeX Document %%%
\documentclass[11pt,a4paper]{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{Pi Calculus and OGRe}
\author{
        {\it John Glauert} \\
       }
%\reportref{Draft}
\date{Version A. 5th January 2001}

\input{procmacros}

\begin{document}
\maketitle

\section{Introduction}

This note provides information on a subset of \Pc\ and its possible encoding in \OGRe.
The \Pc\ subset is sufficient for modelling the \Lc\ and, by some additional reasoning,
it can be implemented in functional \OGRe, which is \OGRe\ that uses no agents that can
change their state once created.

\section{Review of \Pc}

The \Pc\ appears in various syntactic forms. The presentation of semantics has also
evolved.

The monadic form in \cite{MPW} provides very general choice, a matching construct, and
parametric definitions. The simpler, more restricted, form in \cite{FunAsProcs} uses
replication and omits choice and matching. It is sufficiently powerful to model the
\Lc, however.

The Polyadic \Pc\ in \cite{PolyPi} has guarded choice and replication. Milner shows
that conditional computation may be modelled without a match operation and that
parametric definitions can be (weakly) simulated by replication. Polyadic communication
can be seen as syntactic sugar based on monadic communication.

Meanwhile Honda an Tokoro \cite{HandT} and Boudol \cite{Boudol} (and Glauert
\cite{Parle92}) show that the asynchronous calculus, in which processes are not guarded
by output actions, has all the required power, and may be used to simulate the
synchronous calculus in almost all respects.

There is increasing use of a simplified calculus which is called the \emph{\MAPC}. This
has no choice or match construct. Communication is asynchronous and a restricted form
of input-guarded replication is used.

We will restrict attention to such a syntax for the \Pc.
\begin{eqnarray*}
N & ::= & \inpact{x}{y}{N} \mid \; \guardedrep{A}{x}{y}{N}
	\mid \outacta{x}{v}
	\mid \restrict{x}{N} \mid \parprocs{N}{N'} \mid \inaction
\end{eqnarray*}
All features of the full \Pc\ can be simulated by the \MAPc, except perhaps the general
choice construct which does not seem to be of interest to anyone. For example, we can
provide something like the general case of replication. In
the following, $x \not\in fn(P)$:
\begin{eqnarray*}
Q = \restrict{x}{\parprocs{\outacta{x}{}}
		{\guardedrep{X}{x}{}{(\parprocs{P}{\outacta{x}{}})}}} &
	\approx & \replicate{X}{P}
\end{eqnarray*}
$Q$ becomes, by a $\tau$ step,
\begin{eqnarray*}
& & \restrict{x}{\parprocs{P}{\parprocs{\outacta{x}{}}
{\guardedrep{X}{x}{}{(\parprocs{P}{\outacta{x}{}})}}}} \\
& \cong & \parprocs{P}{\restrict{x}{\parprocs{\outacta{x}{}}
{\guardedrep{X}{x}{}{(\parprocs{P}{\outacta{x}{}})}}}} \\
& = & \parprocs{P}{Q}
\end{eqnarray*}
So it seems that $Q$ is weakly bisimilar to $\replicate{X}{P}$ using
standard \Pc\ semantics.

For our translation to \OGRe\ it is possible to relax the restriction to asynchronous
communication and it is possible to support polyadic communication. However, since
these features do not affect the computational power, we omit them here.

The semantics will be assumed to be standard for \Pc, although since replication is
always input guarded we can can remove
structural equivalence rules for replication and provide two
forms of communication:
\begin{eqnarray*}
\parprocs{\outact{x}{v}{P}}{\inpact{x}{y}{Q}} &
	\rightarrow & \parprocs{P}{\subs{Q}{v}{y}} \\
\parprocs{\outact{x}{v}{P}}{\guardedrep{X}{x}
	{y}{Q}} & \rightarrow & \parprocs
		{\parprocs{P}{\subs{Q}{v}{y}}}
		{\guardedrep{X}{x}{y}{Q}}
\end{eqnarray*}

We will use a normal definition of free names given by the function $fn(N)$ over
processes:
\begin{eqnarray*}
fn(\inpact{x}{y}{N}) & = & \{x\} \cup (fn(N) \setminus \{y\}) \\
fn(\guardedrep{A}{x}{y}{N}) & = & \{x\} \cup (fn(N) \setminus \{y\}) \\
fn(\restrict{x}{N}) & = & fn(N) \setminus \{x\} \\
fn(\outacta{x}{v}) & = & \{x,v\} \\
fn(\parprocs{N}{N'}) & = & fn(N) \cup fn(N') \\
fn(\inaction) & = & \{\}
\end{eqnarray*}

\section{A Restricted Subcalculus of \MAPC}

Some \Pc\ processes have the property that for each name, at most one
\Pc\ process in a parallel composition will have an
input prefix for that name at a given time. It will be seen that
this imposes severe restrictions on the possible forms of \Pc\
process, but these restrictions are obeyed by networks generated
by some simulations of the \Lc.

A first observation is that such a process should not receive input on any
name it has received as input -- unless we are to trace the behaviour
of all processes which might send output on a given name. Secondly,
in a parallel composition only one process in the composition can
take input on a given name.

We will define a function $dn(N)$ over \Pc\ processes which will
be used to constrain the form of \Pc\ processes we allow:
\begin{eqnarray*}
dn(\inpact{x}{y}{N}) & = & \{x\} \\
dn(\guardedrep{A}{x}{y}{N}) & = & \{x\} \\
dn(\restrict{x}{N}) & = & dn(N) \setminus \{x\} \\
dn(\outacta{x}{v}) & = & \{\} \\
dn(\parprocs{N}{N'}) & = & dn(N) \cup dn(N') \\
dn(\inaction) & = & \{\}
\end{eqnarray*}

We then add some constraints that must be obeyed. Firstly,
in $(\parprocs{N}{N'})$, we require that $dn(N) \cap dn(N') = \{\}$.
Hence no free name may be used for input in both $N$ and $N'$.

Secondly, in $\inpact{n}{n'}{N}$, we require that $n \neq n'$
and that $dn(N) \subseteq \{n\}$. Otherwise, after performing input,
the property required for a parallel composition might be violated.
A consequence is that if $N$ contains a parallel composition,
all names used for input must be restricted, except for $n$. The requirement that $n
\neq n'$ can be ensured by alpha conversion of the process to
$\inpact{n}{n''}{\subs{N}{n''}{n'}}$ where $n'' \not\in fn(\inpact{n}{n'}{N})$.

For similar reasons, in $\guardedrep{A}{x}{y}{N}$ we require that $dn(N) =
\{\}$. Unravelling a replication only happens following an input action, in which case
we have $(\parprocs{\PPsub{N}{v/y}}{\guardedrep{A}{x}{y}{N}})$, where $v$ is
the value received. In the new network the replication can receive on $x$ so we require
that $\PPsub{N}{v/y}$ cannot.

Finally, we will also consider a further, and possibly surprising, restriction which is
to allow input \emph{only} in replication. Only one transition rule represents
communication, but it always involves replication.

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

It is possible to produce a translation of the \Pc\ into Object Graph Rewriting
(\OGRe).
Such a translation may use of an \OGRe\ process  
to implement a \Pc\ name  which is seen as a communication channel or mailbox.
However, for the resticted subset introduced above, \Pc\ names are closely connected
with unique processes that use them in input actions. Hence we can associate those
names with the names of \OGRe\ processes that recive input directly rather than via a
mailbox.

The translation below assumes, without loss of generality, that in the whole process to
be translated, every restriction relates to different names and that no name free in
the whole process is restricted. Hence if the process is $N$ then for every pair of
distinct processes of the form $\restrict{x}{M}$ and $\restrict{x'}{M'}$ in $N$, $x
\neq x'$ and $x \not\in fn(N)$. This property can be ensured by alpha conversion. Note
that this property is not necessrily preserved when transitions take place, but the
scoping rules in the \OGRe\ model will preserve the scoping rules of restriction in the
\Pc\ process.

The function $q$ maps \Pc\ processes to \OGRe\ processes:
\begin{eqnarray*}
q\sembrac{\inpact{x}{y}{N}} & \defeq &
	\Pdef{x}{A(\vec{z})} \\
	\transwhere{x}{A(\vec{z})}{Data(y)}{q\sembrac{N}} \\
	\anddef{where}{\vec{z} \defeq fn(N) \setminus \{y\}} \\
	\anddef{if}{dn(N) = \{x\}} \\
q\sembrac{\inpact{x}{y}{N}} & \defeq &
	\Pdef{x}{A(\vec{z})} \\
	\transwhere{x}{A(\vec{z})}{Data(y)}{\Ppar{\Pdef{x}{Dead}}{q\sembrac{N}}} \\
	\anddef{where}{\vec{z} \defeq fn(N) \setminus \{y\}} \\
	\anddef{if}{dn(N) = \{\}} \\
q\sembrac{\guardedrep{A}{x}{y}{N}} & \defeq &
	\Pdef{x}{A(\vec{z})} \\
	\transwhere{x}{A(\vec{z})}{Data(y)}{\Ppar{\Pdef{x}{A(\vec{z})}}{q\sembrac{N}}} \\
	\anddef{where}{\vec{z} \defeq fn(N) \setminus \{y\}} \\
q\sembrac{\outacta{x}{v}} & \defeq &
	\Pcall{x}{Data(v)} \\
q\sembrac{\restrict{x}{N}} & \defeq &
    q\sembrac{N} \\
	\anddef{if}{x \in dn(N)} \\
q\sembrac{\restrict{x}{N}} & \defeq &
    \Ppar{\Pdef{x}{Dead}}{q\sembrac{N}} \\
	\anddef{if}{x \not\in dn(N)} \\
q\sembrac{\parprocs{N}{N'}} & \defeq &
    \Ppar{q\sembrac{N}}{q\sembrac{N'}} \\
q\sembrac{\inaction} & \defeq &
\end{eqnarray*}

An \OGRe\ agent with agent term symbol $Dead$ will ignore any further
messages. This models a \Pc\ process in which output actions on a name find no process
which has an input action for the name. The two rules for $\inpact{x}{y}{N}$
distinguish the case where $N$ continues to take input on $x$ and where it does not.

Each time an input action or replication is encoded, a new \OGRe\ rule is introduced
with a new agent term symbol denoted by $A$ in the definitions above.

Where a restriction $\restrict{x}{N}$ applies to an identifier $x$ that is not used for
input actions in $N$, we create an agent whose name may be passed around, but will not
respond to output actions.

The constraints on the restricted subset ensure that in parallel compositions and in
other \OGRe\ expressions, all definitions are linear.

When translating a complete \Pc\ process we must account for names that are free in the
process. We assume that restrictions are added so that the whole process has no free
names and then translate using the function $p$ below:
\begin{eqnarray*}
p\sembrac{N} & \defeq &
	\Ppar{\Pdef{x}{Start}}{\Pcall{x}{POMTrigger}} \rightarrow
		\Ppar{\Pdef{x}{Start}}{q\sembrac{N}}
\end{eqnarray*}

where $fn(N) = \{\}$ and $x$ does not occur in $N$. The result is a set of \OGRe\ rules
that are executed in the normal way by creating an initial expression of the form
$\Ppar{\Pdef{x}{Start}}{\Pcall{x}{POMTrigger}}$.

To perform experiments, a \Pc\ process can be placed in parallel with output actions
and processes guarded by input actions, as long as the constraints of the \Pc\ subset
are observed. The \OGRe\ implementation of any additional processes can monitor
interactions with the process under test

The following example shows translation of the process
$R = (\parprocs{\inpact{x}{y}{P}}{\outacta{x}{v}})$ where 
$fn(P) = \{y\}$. Note that $dn(R) = \{x\}$. We add restrictions for $x$ and $v$ which are
free names so we translate $\restrictand{x}{\restrict{v}{R}}$:
\begin{eqnarray*}
& & p\sembrac{\restrictand{x}{\restrict{v}{\parprocs{\inpact{x}{y}{P}}{\outacta{x}{v}}}}} ; \\
& \defeq & \Ppar{\Pdef{x}{Start}}{\Pcall{x}{POMTrigger}} \rightarrow
	\Ppar{\Pdef{x}{Start}}{q\sembrac{\restrictand{x}{\restrict{v}
	{\parprocs{\inpact{x}{y}{P}}{\outacta{x}{v}}}}}} ; \\
& \defeq & \Ppar{\Pdef{x}{Start}}{\Pcall{x}{POMTrigger}} \rightarrow
	\Ppar{\Pdef{x}{Start}}{q\sembrac{\restrict{v}
	{\parprocs{\inpact{x}{y}{P}}{\outacta{x}{v}}}}} ; \\
& \defeq & \Ppar{\Pdef{x}{Start}}{\Pcall{x}{POMTrigger}} \rightarrow
	\Ppar{\Pdef{x}{Start}}{\Ppar{\Pdef{v}{Dead}}{q\sembrac{
	\parprocs{\inpact{x}{y}{P}}{\outacta{x}{v}}}}} ; \\
& \defeq & \Ppar{\Pdef{x}{Start}}{\Pcall{x}{POMTrigger}} \rightarrow
	\Ppar{\Pdef{x}{Start}}{\Ppar{\Pdef{v}{Dead}}{\Ppar{q\sembrac{
	\inpact{x}{y}{P}}}{q\sembrac{
	\outacta{x}{v}}}}} ; \\
& \defeq & \Ppar{\Pdef{x}{Start}}{\Pcall{x}{POMTrigger}} \rightarrow
	\Ppar{\Pdef{x}{Start}}{\Ppar{\Pdef{v}{Dead}}{\Ppar{\Pdef{x}{A}}{q\sembrac{
	\outacta{x}{v}}}}} ; \\
& & \Ppar{\Pdef{x}{A}}{\Pcall{x}{Data(y)}} \rightarrow 
	\Ppar{\Pdef{x}{Dead}}{q\sembrac{P}} ; \\
& \defeq & \Ppar{\Pdef{x}{Start}}{\Pcall{x}{POMTrigger}} \rightarrow
	\Ppar{\Pdef{x}{Start}}{\Ppar{\Pdef{v}{Dead}}{\Ppar{\Pdef{x}{A}}{\Pcall{x}{Data(v)}}}} ; \\
& & \Ppar{\Pdef{x}{A}}{\Pcall{x}{Data(y)}} \rightarrow 
	\Ppar{\Pdef{x}{Dead}}{q\sembrac{P}} ;
\end{eqnarray*}

We note that the only type of process that can introduce mutable agents in the \OGRe\ code
is an input guarded process (not an inpiut guarded replication). We can produce entirely
functional \OGRe\ rules if such processes are excluded. This makes for an even more restricted
subset, though in cases where input on a given name can be accepted only once, then replication
can replace standard input.

Consider a process $\restrict{x}{\parprocs{\outacta{x}{v}}{\inpact{x}{y}{P}}}$
where $x \neq v$ and $x \not\in fn(P)$. Then once an interaction has occurred we have
$\restrict{x}{\subs{P}{v}{y}}$ which is equivalent to $\subs{P}{v}{y}$ since $x$ is not free in
$\subs{P}{v}{y}$. 
If replication, $\restrict{x}{\parprocs{\outacta{x}{v}}{\guardedrep{A}{x}{y}{P}}}$, is
used instead, interaction yields
$\restrict{x}{\parprocs{\subs{P}{v}{y}}{\guardedrep{A}{x}{y}{P}}}$. This is equivalent
to $\parprocs{\subs{P}{v}{y}}{\restrict{x}{\guardedrep{A}{x}{y}{P}}}$ in which
$\restrict{x}{\guardedrep{A}{x}{y}{P}}$ can take no further part.
In general, if it can be proven that at most one output action could ever arise for a particular
name, then replication can be used in place of standard guarded input without changing the
observable behaviour of the process.

\begin{thebibliography}{MPW89}

\bibitem[{Boudol}]{Boudol}
G. Boudol

\bibitem[{Gla92}]{Parle92}
J.R.W. Glauert:
{\em Asynchronous Mobile Processes
and Graph Rewriting}, 
Proc PARLE'92. LNCS 605. June 1992. (1992) 

\bibitem[{HoTo91}]{HandT}
K. Honda \& M. Tokoro:
{\em An object calculus for asynchronous communication}.
Proc.\ ECOOP'91, Geneva, July 1991.

\bibitem[{Mil90}]{FunAsProcs}
R. Milner: 
{\em Functions as Processes},
Automata, Languages, and Programming. Springer LNCS 443. (1990)
Also: Technical Report INRIA Sophia Antipolis, June 1989. 

\bibitem[{Mil91}]{PolyPi}
R. Milner: 
{\em The \PPC: A Tutorial},
Technical Report ECS-LFCS-91-180, Edinburgh University, October 1991. (1991)

\bibitem[{MPW89}]{MPW}
R. Milner, J. Parrow, \& D. Walker: 
{\em A Calculus of Mobile Processes}, Parts I and II,
Technical Report ECS-LFCS-89-85, Edinburgh University, June 1989. (1989)

\end{thebibliography}

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