%%% Start of LaTeX Document %%%
\documentclass[11pt,a4paper]{article}
%\usepackage{times}
%\documentstyle[11pt]{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{Replication}
\author{
        {\it John Glauert, and Jeong-Ho Lee} \\
       }
%\reportref{Draft}
\date{Version A. 13th September 1995}

\newcommand{\suppress}[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{\wheredef}[4]{{#1}\;where\;\agtdef{#2}{#3}{#4}}
\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{\subs}[3]{{#1}\{{#2}/{#3}\}}
\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{\Pinact}{Dead}
\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]{where & &
{\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}} \rightarrow {#4}}}
\newcommand{\transand}[4]{& & {\makebox[1.5cm][l]
	{and}}{\Ppar{\Pdef{#1}{#2}}{\Pcall{#1}{#3}} \rightarrow {#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{Introduction}

This document discusses the use of replication in the \Pc\ and its
translation to \OGRe\ and hence to \PPc.

\section{Varieties of $\pi$--Calculi}

The base calculus we will use is for the \Pc\ with multiple
communications, but without sums, using syntax:
\begin{eqnarray*}
N & ::= & \inpact{x}{\vec{y}}{N} \mid \outact{x}{\vec{v}}{N}
	\mid \restrict{x}{N} \mid \parprocs{N}{N'} \mid \inaction
	\mid \; \replicate{A}{N}
\end{eqnarray*}
In the discussion on \PPc\ we have assumed that agent definitions
take the place of replication:
\begin{eqnarray*}
N & ::= & \inpact{x}{\vec{y}}{N} \mid \outact{x}{\vec{v}}{N}
	\mid \restrict{x}{N} \mid \parprocs{N}{N'} \mid \inaction
	\mid \agtuse{A}{\vec{y}} \mid \wheredef{N}{A}{\vec{y}}{N'}
\end{eqnarray*}
We can provide a crude translation of $\replicate{A}{P}$ as:
\begin{eqnarray*}
\replicate{A}{P} & \equiv &
\wheredef{\agtuse{A}{n_P}}{A}{n_P}{(\parprocs{P}{\agtuse{A}{n_P}})}
\end{eqnarray*}
where $n_P$ stands for $fn(P)$.

For practical purposes we will want communication to trigger
expansion of replications. The usual form in which we will find
replication is $\replicate{X}{\inpact{x}{\vec{y}}{P}}$. If we use $n_{Pxy}$ to
stand
for $fn(P) \setminus \{x,y\}$ then we can represent the replication
as:
\begin{eqnarray*}
\replicate{A}{\inpact{x}{\vec{y}}{P}} & \equiv &
\wheredef{\agtuse{A}{x,n_{Pxy}}}
{A}{x,n_{Pxy}}{\inpact{x}{\vec{y}}(\parprocs{P}{\agtuse{A}{x,n_{Pxy}}})}
\end{eqnarray*}
However, some sort of proof is needed to show that this version is
weakly bisimilar (or even strongly bisimilar) to the crude
translation, using suitable semantics for agents.

An avenue which Jeong Ho and John have explored is to use the base
syntax for \Pc, but to restrict replication to the input guarded
form:
\begin{eqnarray*}
N & ::= & \inpact{x}{\vec{y}}{N} \mid \outact{x}{\vec{v}}{N}
	\mid \restrict{x}{N} \mid \parprocs{N}{N'} \mid \inaction
	\mid \; \replicate{A}{\inpact{x}{\vec{y}}{N}}
\end{eqnarray*}
This form of replication acts like an input guarded process which
spawns a copy of itself when communication occurs. Instead of
structural equivalence rules for replication, we could have two
forms of communication:
\begin{eqnarray*}
\parprocs{\outact{x}{\vec{v}}{P}}{\inpact{x}{\vec{y}}{Q}} &
	\rightarrow & \parprocs{P}{\subs{Q}{\vec{v}}{\vec{y}}} \\
\parprocs{\outact{x}{\vec{v}}{P}}{\replicate{X}{\inpact{x}
	{\vec{y}}{Q}}} & \rightarrow & \parprocs
		{\parprocs{P}{\subs{Q}{\vec{v}}{\vec{y}}}}
		{\replicate{X}{\inpact{x}{\vec{y}}{Q}}}
\end{eqnarray*}

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}{}}
		{\replicate{X}{\inpact{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}{}}
{\replicate{X}{\inpact{x}{}{(\parprocs{P}{\outacta{x}{}})}}}}} \\
& \cong & \parprocs{P}{\restrict{x}{\parprocs{\outacta{x}{}}
{\replicate{Y}{\inpact{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.

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

With these restricted forms or replication, and adding rules for
multiple communications, provided by Jeong Ho, we have a revised
translation scheme. See the more complete note {\em PiSky Version
K\/} for more background.
\begin{eqnarray*}
N & ::= & \inpact{x}{\vec{y}}{N} \mid \outact{x}{\vec{v}}{N}
	\mid \restrict{x}{N} \mid \parprocs{N}{N'} \mid \inaction
	\mid \; \replicate{A}{\inpact{x}{\vec{y}}{N}}
\end{eqnarray*}

The function $q$ maps \Pc\ processes to \OGRe\ processes:
\begin{eqnarray*}
q\sembrac{\outact{x}{\vec{v}}{N}} & = &
	\Ppar{\Pdef{m}{B(n_N)}}{\Pcall{n}{Put(Vec_k(\vec{v}),m)}} \\
	\transwhere{m}{B(n_N)}{Sync}{\Ppar{\Pdef{m}{\Pinact}}
	{q\sembrac{N}}} \\
q\sembrac{\outacta{x}{\vec{v}}} & = &
	\Pcall{n}{APut(Vec_k(\vec{v}))} \\
q\sembrac{\inpact{x}{\vec{y}}{N}} & = &
	\Ppar{\Pdef{m}{A(n_{Ny})}}{\Pcall{x}{Get(m)}} \\
	\transwhere{m}{A(n_{Ny})}{Data(Vec_k(\vec{y}))}
	{\Ppar{\Pdef{m}{\Pinact}}{q\sembrac{N}}} \\
q\sembrac{\replicate{X}{\inpact{x}{\vec{y}}{N}}} & = &
	\Ppar{\Pdef{m}{A(x,n_{Nxy})}}{\Pcall{x}{Get(m)}} \\
	\transwhere{m}{A(x,n_{Nxy})}{Data(Vec_k(\vec{y}))}
	{\Ppar{\Ppar{\Pdef{m}{A(x,n_{Nxy})}}{\Pcall{x}{Get(m)}}}
		{q\sembrac{N}}} \\
q\sembrac{\restrict{n}{N}} & = &
    \Ppar{\Pdef{n}{Chan(EQ)}}{q\sembrac{N}} \\
q\sembrac{\parprocs{N}{N'}} & = &
    \Ppar{q\sembrac{N}}{q\sembrac{N'}} \\
q\sembrac{\inaction} & = &
\end{eqnarray*}
where $n_N = fn(N)$, $n_{Ny} = fn(N) \setminus \{y_0 \ldots y_k\}$,
and $n_{Nxy} = fn(N) \setminus \{x,y_0 \ldots y_k\}$. $Vec_k$ stands
for a data constructor of the required arity for the corresponding
sequence of input or output values. Hence, for $\vec{v} = v_1 \ldots
v_k$,
where $k \geq 0$, we use $Vec_k(v_1, \ldots ,v_k)$.

We have provided rules for asynchronous \Pc. The translation of
guarded replication was also developed by Jeong Ho.

The state $\Pinact$ labels a process which should never receive
any further messages. It remains to be proved that this is the
case for every $\Pinact$ process which arises from evaluating
the \OGRe\ system generated by $q$ from any \Pc\ term.

\end{document}

%%% End of LaTeX Document %%%
