%%% Start of LaTeX Document %%%

%\documentstyle[a4,11pt]{article}
\documentclass[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=0.3in
\textheight=9.5in              % A4 paper is 11.7in high

\pagestyle{plain}
\setlength{\parindent}{0cm}
\setlength{\parskip}{\medskipamount}
\setlength{\itemsep}{\smallskipamount}

\title{A $\nu$--Notation for Process Calculi}

\author{{\it Jeong-Ho Lee} \\
				\\
	School of Information Systems \\
	University of East Anglia \\
	Norwich NR4 7TJ, UK \\
	Tel: +44 603 593213 \\
	Fax: +44 603 507720 \\
	{\em jhl@sys.uea.ac.uk}}

\date{July, 1994}

%% New macros %%
% Calculus representation %
\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}{polyadic $\pi$--calculus}
\newcommand{\PPC}{Polyadic $\pi$--Calculus}
\newcommand{\mynote}{$\nu$--notation}
\newcommand{\Mynote}{$\nu$--Notation}

% Translation representation %
\newcommand{\transexp}[2]{\sembrac{#1}_{#2}}
\newcommand{\sembrac}[1]{[\![ #1 ]\!]}
\newcommand{\infer}[3]
           {\vspace{.2cm}
            \hbox{${\displaystyle {\frac {#1}{#2}}\hspace{.5cm}{#3}}$}
            \vspace{.2cm}}

% Jeong-Ho's macro %
\newcommand{\prefix}{\sum_{i\in I}\nu_i.}
\newcommand{\sumofp}{\sum_{i\in I}P_i}
\newcommand{\sumofnup}{\sum_{i\in I}\nu_i.\,P_i}
\newcommand{\productofp}{\prod_{i\in I}P_i}
\newcommand{\binsum}[2]{{#1}\,+\,{#2}}
\newcommand{\intsum}[2]{{#1}\,\oplus\,{#2}}
\newcommand{\extsum}[2]{{#1}\,\,\frame{+}\,\,{#2}}
\newcommand{\comsum}[2]{{#1}\,[]\,{#2}}
\newcommand{\compo}[2]{{#1}\,|\,{#2}}
\newcommand{\res}[2]{({\nu}\,{#1})\,{#2}}
\newcommand{\rep}[1]{*{#1}}
\newcommand{\paradef}[3]{{#1}\,({\vec{#2}})\,\stackrel{\rm def}{=}\,{#3}}
\newcommand{\substi}[3]{{#1}\,\{{#2}/{#3}\}}
\newcommand{\simulsubsti}[3]{{#1}\,\{{\vec{#2}}/{\vec{#3}}\}}
\newcommand{\match}[3]{[{#1}\,=\,{#2}]\,{#3}}
\newcommand{\inact}{{\bf 0}}
\newcommand{\ident}[2]{{#1}\,({#2}_{1}, \ldots, {#2}_{n})}
\newcommand{\inputact}[2]{{#1}?{#2}}
\newcommand{\outputact}[2]{{#1}!{#2}}
\newcommand{\intransition}[2]{{#1}\;\rightarrow\;{#2}}
\newcommand{\labeltransition}[3]{{#1}\;\stackrel{#2}{\rightarrow}\;{#3}}
\newcommand{\membrane}[1]{\{\!|\,{#1}\,|\!\}}

%% endofmacro %%

\begin{document}

\maketitle

\begin{abstract}
This paper addresses the need for notational unification across different theories of communicating and concurrent systems. We present a \mynote, an unified notation for various process calculi. Using the \mynote\ we show that we can redefine the syntax and semantics for each process calculus, such as CCS \cite{CCS}, TCCS (for Testing CCS) \cite{TCCS}, the \Pc\ \cite{Pi}, \cite{FunAsProcs}, LCCS (for Label passing CCS) \cite{Leth91}, and the \ppc\ \cite{PolyPi}, in order to achieve notational unification on process calculi. 
\end{abstract}

\section{Introduction}

Since Milner developed CCS \cite{CCS}, many theories of communicating and concurrent systems have been developed, for example, CCS \cite{CCS}, CSP \cite{CSP}, ECCS \cite{ECCS}, TCCS \cite{TCCS}, CHOCS \cite{CHOCS}, \cite{Chocs}, the Cham (for \Cham) \cite{CHAM}, the \Pc\ \cite{Pi}, \cite{FunAsProcs}, LCCS \cite{Leth91}, the \ppc\ \cite{PolyPi}, the object--calculus \cite{HoT91}, and so on have been designed. Each of theories of these process calculi, however, has its own notations to represent its syntax and operational semantics. Even same author uses different notations to develop improved and more theoretically well founded versions of his calculi. We think that such many notations could cause confusions to understand these theories, even though they are interpreted almost same concepts.
 
In order to avoid such confusions this paper addresses the need for notational unification across different theories of communicating and concurrent systems. We present a \mynote, an unified notation, which will be used to redefine the syntax and the operational semantics for process calculi. We show that the \mynote\ can be used to redefine the syntax and semantics for every process calculus in order to achieve notational unification on process calculi. Although the \mynote\ is presented by the form of syntax and semantics, it is not another kind of process calculus, but a new notation to unify all different notations. Because this paper is an experiment, we restrict ourselves to redefining syntax and semantics of CCS, TCCS, the \Pc, LCCS, and the \ppc\ only. We, however, believe that the \mynote\ has capability to recast all notations for process calculi. 

This paper's layout is as follows: Section 2 defines the syntax and semantics of the \mynote. Section 3 gives a short overview of the concepts of each process calculus, and then presents the syntax and operational semantics for each calculus with its own notation. The operational semantics will be given as a set of reduction rules on processes, but some of them may be given with the structural congruence relation over terms to simplify the form of the reduction rules. We then reproduce the syntax and semantics for each process calculus using our \mynote. Section 4 investigates whether our notation could express all process calculi and what should be considered to get more transparency among the different approaches. Finally we conclude our experiment on notations of process calculi in Section 5.  

\section{A \Mynote}

We present a \mynote, an {\em unified notation} for process calculi, based mainly upon the \Pc\ \cite{Pi}. In the following subsections, we define the syntax and operational semantics for arbitrary process calculi. Important entities and agent constructions of process calculi, which are used to express syntax and semantics for each process calculus, are defined in Appendix A and Appendix B, respectively.

\subsection{\Mynote\ for Syntax}

We let ${\cal N}$ be an infinite set of {\em names}, ranged over by $x, y, z, \ldots$, and let $\overline{\cal N}$ be an infinite set of {\em co--names}, ranged over by $\overline{x}, \overline{y}, \overline{z}, \ldots$. We also let $\vec{\cal N}$ be an infinite set of {\em name vectors}, ranged over by ${\vec x}, {\vec y}, {\vec z}, \ldots$, and let $\cal A$ be a set of {\em agent identifiers}, ranged over by $A, B, C, \ldots$. Then the set of {\em processes} ${\cal P}$, ranged over by $P, Q, \ldots$, is given by the following syntax:

\begin{eqnarray*}
P & ::= & \prefix\,P\;|\;\sumofp\;|\;(\compo{P}{Q})\;|\;\rep{P}\;|\;\res{x}{P}\;|\;P\,[f]\;|\;\match{x}{y}{P}\;|\;A\,(\vec x)
\end{eqnarray*}
\begin{tabbing}
xxxxxxxx\= \kill
where \\
       \>$\prefix\;::=\;y(x).\;|\;\overline{y}x.\;|\;y(\vec x)\;|\;\overline{y}{\vec x}.\;|\;\tau.$ \\
\\
       \>$\sumofp\; ::=\;\inact\;|\;P\,+\,Q\;|\;\intsum{P}{Q}\;|\;\extsum{P}{Q}$
\\
\end{tabbing}
\begin{tabbing}
xxxxxxxxxxxxxxxxxxx\= \kill
$P ::= y(x).\,P$	\> The monadic input agent $y(x).\,P$ receives a name $z$ at port $y$ and then \\
		\> behaves like $\substi{P}{z}{x}$. \\
\\
$P ::= \overline{y}x.\,P$	\> The monadic output agent $\overline{y}x.\,P$ sends the name $x$ at port $\overline{y}$ and then \\
		\> behaves like $P$. \\
\\
$P ::= y(\vec x).\,P$	\> The polyadic input agent $y(\vec x).\,P$ receives a name vector $z$ at port $y$ and \\
		\> then behaves like $\substi{P}{\vec z}{\vec x}$.\\
\\
$P ::= \overline{y}{\vec x}.\,P$ \> The polyadic output agent $\overline{y}{\vec x}.\,P$ sends the name vector $\vec x$ at port $\overline{y}$ and \\
		\>then behaves like $P$. \\
\\
$P ::= \tau.\,P$	\> The silent agent $\tau.\,P$ performs the silent action and then behaves like $P$. \\
\\
$P ::= \inact$		\> The inaction agent $\inact$ performs nothing. \\
\\
$P ::= \binsum{P}{Q}$	\> The binary choice agent $\binsum{P}{Q}$ behaves like $P$ or $Q$, but  not both. \\
			\> This choice includes both internal choice and external choice.\\
\\
$P ::= \intsum{P}{Q}$	\> The internal choice agent $\intsum{P}{Q}$ non-deterministically chooses a \\
			\> component.\\
\\
$P ::= \extsum{P}{Q}$	\> The external choice agent $\extsum{P}{Q}$ performs internal actions freely and \\
			\> also communicates to the environment.\\
\\
$P ::= \compo{P}{Q}$	\> The parallel composition agent $\compo{P}{Q}$ may act independently, but may \\
		\> also communicate. \\
\\
$P ::= \rep{P}$	\> The replication agent $\rep{P}$ stands for $P\;|\;P\;|\;\ldots$, as many concurrent \\
		\> instances of $P$ as you please.\\
\\
$P ::= \res{x}{P}$	\> The restriction agent $\res{x}{P}$ behaves like $P$ but actions are prohibited \\
		\> at port $x$ and $\overline{x}$. \\
\\
$P ::= P\,[f]$	\> The relabelling agent $P[f]$ renames the ports of the agent $P$ and then \\
		\> behaves like $P$.\\
\\
$P ::= \match{x}{y}{P}$	\> The matching agent $\match{x}{y}{P}$ behaves like $P$ if $x = y$, otherwise like $\inact$.\\
\\ 
$P ::= A\,(\vec x)$	\> The defined agent $A\,(\vec x)$ is a constant, and gives a meaning of agent $P$ \\
		\> such that $A\,(\vec x)\;\stackrel{\rm def}{=}\;P$. 
\end{tabbing}

Note that parentheses used in the input prefix and the restriction indicate the binding occurrence of a variable. Hence in the \mynote\ there are two binding operators: the input prefix $y(x)$ and the restriction $(\nu x)$.
 
\subsection{\Mynote\ for Semantics}

Our semantics of the \mynote\ for process calculi is given as a set inference rules on processes in Plotkin's structural operational semantics style \cite{OperSem}, together with the structural congruence to simplify the form of the reduction rules. For our semantics for process calculi, we, therefore, define the structural congruence relation $\equiv$ over $\cal P$ and the reduction rules in the subsequent sections. 

\subsubsection{Structural Congruence}

We let $fn(P)$ be the {\em free names} of a process $P$, and $bn(P)$ the {\em bound names} of a process $P$. We also let $n(P)$ be the {\em names} of a process $P$, where $n(P) \stackrel{\rm def}{=} fn(P) \cup bn(P)$.

The {\em structural congruence relation} $\equiv$ is the smallest congruence relation over set of processes ${\cal P}$ satisfying the following properties:

\begin{tabbing}
xxxxxxxx\=xxxx\= \kill
	\>1.\>$P\;\equiv\;Q$ if $P$ is $\alpha$--convertible to $Q$. \\
\\
	\>2.\>$({\cal P}/\equiv,\,|,\,\inact)$ is a symmetric monoid. \\
\\
	\>3.\>$({\cal P}/\equiv,\,+,\,\inact)$ is a symmetric monoid. \\
\\
	\>4.\>$({\cal P}/\equiv,\,\oplus,\,\inact)$ is a symmetric monoid. \\
\\
	\>5.\>$({\cal P}/\equiv,\,\frame{+},\,\inact)$ is a symmetric monoid. \\
\\
	\>6.\>$\rep{P}\;\equiv\;\compo{P}{\rep{P}}$. \\
\\
	\>7.\>$\res{x}{\inact}\;\equiv\;\inact,\;\;\;(\nu\,x)(\nu\,y)P\;\equiv\;(\nu\,y)(\nu\,x)P$. \\
\\
	\>8.\>If $x\;\not\in\;fn(P)$ then $(\nu\,x)(\compo{P}{Q})\;\equiv\;\compo{P}{(\nu\,x)Q}$.\\
\\
	\>9.\>If $\vec x\;\neq\;\vec y$ then $(\nu\,\vec y){\vec x}.P\;\equiv\;{\vec x}.(\nu\,\vec y)P$ \\
\\
	\>10.\>$(\nu\,\vec x)(\nu\,\vec y)P\;\equiv\;(\nu\,\vec y)(\nu\,\vec x)P,\;\;\;(\nu\,\vec x)(\nu\,\vec x)P\;\equiv\;(\nu\,\vec x)P$ 
\end{tabbing}

\subsubsection{Reduction Rules}

The rules are associated with Communication, Parallel Composition, Binary Summation, Internal Summation, External Summation, Restriction, Relabelling, Matching, Conditional, Agent Identification, and Structural Congruence are indicated by COMM, PAR, BINSUM, INTSUM, EXTSUM, RES, REL, MATCH, IDENT and STRUCT, respectively. The {\em reduction relation} $\rightarrow$ over processes is the least relation satisfying the following rules: 

\begin{tabbing}
xxxxxxxxxxxxxxx\=\kill
$COMM_1:$\>$\intransition{y(x).\,P\;|\;\overline{y}z.\,Q}{\substi{P}{z}{x}\;|\;Q}$ \\
\\
$COMM_2:$\>$\intransition{(\cdots\,+\,y(\vec x).\,P)\;|\;(\cdots\,+\,\res{\vec w}(\overline{y}{\vec z}.\,Q))}{\res{\vec w}{(P\{{\vec z}/{\vec x}\}\;|\;Q)}}$ \\
\\
$PAR:$\>$\infer{\intransition{P}{P'}}{\intransition{\compo{P}{Q}}{\compo{P'}{Q}}}{}$\\
\\
$BINSUM$:\>$\infer{\intransition{P}{P'}}{\intransition{\binsum{P}{Q}}{\binsum{P'}{Q}}}{}$\\
\\
$INTSUM$:\>${\intransition{\intsum{P}{Q}}{P} }$\\
\\
$EXTSUM$:\>$\infer{\intransition{P}{P'}}{\intransition{\extsum{P}{Q}}{\extsum{P'}{Q}}}{}$\\
\\
$RES:$\>$\infer{\intransition{P}{P'}}{\intransition{\res{x}{P}}{\res{x}{P'}}}{}$ \\
\\
$REL:$\>$\infer{\intransition{P}{P'}}{\intransition{P[f]}{P'[f]}}{}$\\
\\
$MATCH:$\>$\infer{\intransition{P}{P'}}{\intransition{\match{x}{x}{P}}{P'}}{}$\\
\\
$IDENT:$\>$\infer{\intransition{\simulsubsti{P}{x}{y}}{P'}}{\intransition{A(\vec{x})}{P'}}{\paradef{A}{y}{P}}$\\
\\
$CLOSE:$\>$\infer{\labeltransition{P}{\overline{y}(x)}{P'}\;\;\;{\labeltransition{Q}{y(z)}{Q'}}}{\labeltransition{\compo{P}{Q}}{\tau}{(\nu\,x)(\compo{P'}{Q'})}}{}$\\
\\
$OPEN:$\>$\infer{\labeltransition{P}{\overline{y}x}{P'}}{\labeltransition{(\nu\,x)\,P}{\overline{y}(z)}{\substi{P'}{z}{x}}}{x\,\neq\,y,\;\;z\,\not\in\,fn((\nu\,x)\,P')}$ 
\\
\\
$STRUCT:$\>$\infer{Q\;\equiv\;P\;\;\intransition{P}{P'}\;\;P'\;\equiv\;Q'}{\intransition{Q}{Q'}}{}$ 
\end{tabbing}

Note that the reduction rules involving the binary operator $|$, $\oplus$, and $\frame{+}$ additionally have symmetric forms.

\section{Redefining the Syntax and Semantics for Each Process Calculus}

In the following subsections, we give a short overview of the concepts of each process calculus, and we present the syntax and operational semantics for each calculus with its own notation. The operational semantics will be given as a set of reduction rules on processes, but some of them may be given with the structural congruence relation over terms to simplify the form of the reduction rules. We reproduce the syntax and semantics for each process calculus using our \mynote.

\subsection{CCS}

The Calculus of Communicating Systems (CCS) \cite{CCS} was developed by Milner as a means of analysing the behaviours of complex concurrent systems. The behaviour of a system is what is observable, and to observe a concurrent system is to communicate with it. 

Builds a general mathematical model.

Provides with practice in representing real systems by the terms or expressions of the model and skill in manupulating these terms in order to analyse the behaviour of the systems. The essencial idea of CCS is the very observation equivalence between processes, whereas CSP \cite{CSP} designed aroud the primitive of indivisible interaction.

CCS \cite{CCS} lacks the notion of bisimulation, a kind of invariant holding between a pair of dynamic systems, and the technique is to prove two systems equivalent bgy establishing such an invariant. In \cite{CC}, however, the notion of bisimulation and the proof technique are added to overcome a serious shortcoming in the formulation of observation equivalence.

The limitation of CCS: it can describe regular systems whereas systems with an arbitrary and dynamic structure are not describable within the language. At best it can express indirectly. 

\subsubsection{Syntax and Semantics of CCS}

Presuppose an infinite set ${\cal N}$ of {\em names}, and let $x, y, z, \ldots$ range over names. Presuppose also a set ${\cal A}$ of {agent constants}, and let $A, B, C, \ldots$ range over agent constants. Let ${\cal P}$ be a set of {\em agents}, and let $P, Q, \ldots$ range over agents. Then the syntax of CCS is defined as follows:
  
\begin{eqnarray*}
P & ::= & y(x).\,P\;|\;\overline{y}e.\,P\;|\;\tau.\,P\;|\;\sumofp\;|\;(\compo{P}{Q})\;|\;P\setminus\alpha\;|\;P\,[f]\;|\;{\tt if}\; b \;{\tt then}\; P\;|\;\ident{A}{x}
\end{eqnarray*}

The input agent $y(x).\,P$ receives a value $z$ assigned to $x$ at port $y$ and then behaves like $\substi{P}{z}{x}$. The output agent $\overline{y}e.\,P$ sends the name $e$ at port $\overline{y}$ and then behaves like $P$., where $e$ is a value expression. The silent agent $\tau.\,P$ performs the silent action and then behaves like $P$. If $I = \emptyset$ then the summation agent $\sumofp = \inact$ which means it can do nothing. If $I= \{\,1, 2\,\}$ then $\sumofp = \binsum{P}{Q}$ which behaves like $P$ or $Q$, but not both. The parallel composition agent $\compo{P}{Q}$ may act independently, but may also communicate. The restriction agent $P\setminus\alpha$ behaves like $P$ but actions are prohibited with respect to $\alpha$ and $\overline{\alpha}$. The relabelling agent $P[f]$ renames the ports of the agent $P$ and then behaves like $P$. The conditional agent ${\tt if}\; b \;{\tt then}\; P$ is a conditional expression. The defined agent $\ident{A}{x}$ is a constant, and gives a meaning of agent $P$ such that $\ident{A}{x}\;\stackrel{\rm def}{=}\;P$. 

The operational semantics for CCS is given by a set of inference rules. The rules are associated with Prefix, Summation, Composition, Restriction, Relabelling and Constants are indicated by PRE, SUM, COM, RES, REL, and CON, respectively. The reduction relation $\rightarrow$ is the smallest relation satisfying the following rules: 

\begin{tabbing}
xxxxxxxxxx\=xxxxxxx\=xxxxxxx\=xxxxxxx\=xxxxxxx\=xxxxxxx\=xxxxxxxxxx\=\kill
$PRE:$\>$\infer{}{\labeltransition{\alpha.\,P}{\alpha}{P}}{}$\>\>\>\>\>$SUM_j:$\>  $\infer{\labeltransition{P_{j}}{\alpha}{P'_{j}}}{\labeltransition{\sumofp}{\alpha}{P'_{j}}}{}$ \\
\\
$COM_1:$\>  $\infer{\labeltransition{P}{\alpha}{P'}}{\labeltransition{\compo{P}{Q}}{\alpha}{\compo{P'}{Q}}}{}$\>\>\>\>\>$COM_2:$\>  $\infer{\labeltransition{Q}{\alpha}{Q'}}{\labeltransition{\compo{P}{Q}}{\alpha}{\compo{P}{Q'}}}{}$ \\
\\
$COM_3:$\>  $\infer{{\labeltransition{P}{l}{P'}}\;\;\;{\labeltransition{Q}{\overline{l}}{Q'}}}{\labeltransition{\compo{P}{Q}}{\tau}{\compo{P'}{Q'}}}{}$  \\
\\
$RES:$\>$\infer{\labeltransition{P}{\alpha}{P'}}{\labeltransition{P\setminus L}{\alpha}{P'\setminus L}}{(\,\alpha,\,\overline{\alpha}\;\not\in\;L\,)}$\>\>\>\>\>$REL:$\>$\infer{\labeltransition{P}{\alpha}{P'}}{\labeltransition{P[f]}{f(\alpha)}{P'[f]}}{}$ \\
\\
$CON:$\>$\infer{\labeltransition{P}{\alpha}{P'}}{\labeltransition{A}{\alpha}{P'}}{(\,A\;\stackrel{\rm def}{=}\;P\,)}$\\
\end{tabbing}

\subsubsection{Redefined CCS}

We present the redefined syntax and semantics of CCS using the \mynote.  The redefined syntax of CCS is:

\begin{eqnarray*}
P & ::= & \prefix\,P\;|\;\sumofp\;|\;(\compo{P}{Q})\;|\;\res{x}{P}\;|\;\match{x}{y}{P}\;|\;A\,(\vec x)
\end{eqnarray*}
\begin{tabbing}
xxxxxxxx\= \kill
where \\
	\>$\prefix\;::=\;y(x).\;|\;\overline{y}x.\;|\;\tau.$ \\
\\
	\>$\sumofp\;::=\;\inact\;|\;\binsum{P}{Q}$.
\end{tabbing}

Note that in CCS, the restriction is expressed by $P\setminus\,x$, whereas in \mynote\ it is represented by $\res{x}{P}$, which restricts the use of a new unique name $x$, distict from all external names, to $P$. 

The redefined operational semantics for CCS is presented as follows:

\begin{tabbing}
xxxxxxxxxxxxxxx\=\kill
$COMM:$\>$\intransition{y(x).\,P\;|\;\overline{y}z.\,Q}{\substi{P}{z}{x}\;|\;Q}$ \\
\\
$PAR:$\>$\infer{\intransition{P}{P'}}{\intransition{\compo{P}{Q}}{\compo{P'}{Q}}}{}$\\
\\
$BINSUM$:\>$\infer{\intransition{P}{P'}}{\intransition{\binsum{P}{Q}}{\binsum{P'}{Q}}}{}$\\
\\
$RES:$\>$\infer{\intransition{P}{P'}}{\intransition{\res{x}{P}}{\res{x}{P'}}}{}$ \\
\\
$REL:$\>$\infer{\intransition{P}{P'}}{\intransition{P[f]}{P'[f]}}{}$\\
\\
$IDENT:$\>$\infer{\intransition{\simulsubsti{P}{x}{y}}{P'}}{\intransition{A(\vec{x})}{P'}}{\paradef{A}{y}{P}}$\\
\\
$STRUCT:$\>$\infer{Q\;\equiv\;P\;\;\intransition{P}{P'}\;\;P'\;\equiv\;Q'}{\intransition{Q}{Q'}}{}$ 
\end{tabbing}

\subsection{TCCS}

In \cite{TCCS}, De Nicola and Hennesy show that the semantic equivalences used in \cite{CCS} are not preserved by $+$, i.e. they are not congruences. They also show that the choice operator $+$ represents a mixture of different forms of internal and external nondeterminism, and that the behaviour of processes that include $\tau$ actions is hard to describe. They argue that if they are internal and invisible, there should be no need for $\tau$ to represent internal actions in the process calculi. Thus they suggest that the choice operator $+$ and the combinator $\tau$ is replaced with $[]$ and $\oplus$, representing external and internal nondeterminism repectively. The operational semantics of the resulting calculus, TCCS, is simpler and the definition of testing preorders is much cleaner.

\subsubsection{Syntax and Semantics of TCCS}

The syntax of TCCS is: 

\begin{eqnarray*}
p & ::= & \inact\;|\;\alpha .\,p\;|\;(\compo{p}{q})\;|\;p\setminus a\;|\;p\,[\phi]\;|\;p\,\oplus\,q\;|\;p\,[]\,q\;|\;{\tt fix_{i}}({\vec x}\,=\,{\vec p})
\end{eqnarray*}

$\inact$ is an inaction. $\alpha.\,p$ performs action $\alpha$ and then behaves like $p$. $(\compo{p}{q})$ is a parallel composition. $p\setminus a$ is a restriction. $p\,[\phi]$ is a relabelling, in which the relabelling operator $[]$ takes an agent $p$ and a relabelling function $\phi$ and produces a new agent $p\,[\phi]$ which behaves like $p$ except that all its visible actions are relabelled by $\phi$. $p\,\oplus\,q$ is an internal choice in which the decision is made internally and it cannot be influenced by the user. $p\,[]\,q$ is an external choice in which the agents $p$ and $q$ can freely perform internal actions and can also propose communications to the environment. The choice is made only when such a communication is performed. ${\tt fix_{i}}({\vec x}\,=\,{\vec p})$ is a fixpoint operation. 

The rules are associated with Prefix, Internal Choice, External Choice, Composition, Restriction, Relabelling and Fixpoint operation are indicated by PRE, INTSUM, EXTSUM, COM, RES, REL, and FIX, respectively. The semantics for the TCCS is:

\begin{tabbing}
xxxxxxxxxxxx\=xxxxxx\=xxxxx\=xxxxx\=xxxxx\=xxxxx\=xxxxxxxxxxxx\=\kill
$PRE:$\>$\labeltransition{\alpha.\,p}{\alpha}{p}$\\
\\
$INTSUM_1:$\>$\intransition{\intsum{p}{q}}{p}$\>\>\>\>\>$INTSUM_2:$\>$\intransition{\intsum{p}{q}}{q}$ \\
\\
$EXTSUM_1:$\>$\infer{\intransition{p}{p'}}{{\intransition{p\;[]\;q}{p'\;[]\;q}}}{}$\>\>\>\>\>$EXTSUM_2:$\>$\infer{\labeltransition{p}{\alpha}{p'}}{{\labeltransition{p\;[]\;q}{\alpha}{p'}}}{}$ \\
\\
$COM_1:$\>$\infer{\intransition{p}{p'}}{{\intransition{\compo{p}{q}}{\compo{p'}{q}}}}{}$\>\>\>\>\>$COM_2:$\>$\infer{\labeltransition{p}{\alpha}{p'}}{{\labeltransition{\compo{p}{q}}{\alpha}{\compo{p'}{q}}}}{}$ \\
\\
$COM_3:$\>$\infer{{\labeltransition{p}{\alpha}{p'}}\;\;\;{\labeltransition{q}{\overline{\alpha}}{q'}}}{\intransition{\compo{p}{q}}{\compo{p'}{q'}}}{}$  \\
\\
$RES_1:$\>$\infer{\intransition{p}{p'}}{\intransition{p\setminus a}{p'\setminus a}}{}$\>\>\>\>\>$RES_2:$\>$\infer{\labeltransition{p}{\alpha}{p'}}{\labeltransition{p\setminus a}{\alpha}{p'\setminus a}}{\alpha\;\not\in\;\{\,a, \overline{a}\,\}}$ \\
\\
$REL_1:$\>$\infer{\intransition{p}{p'}}{\intransition{p\,[\phi]}{p'\,[\phi]}}{}$\>\>\>\>\>$REL_2:$\>$\infer{\labeltransition{p}{\alpha}{p'}}{\labeltransition{p\,[\phi]}{\phi(\alpha)}{p'\,[\phi]}}{}$ \\
\\
$FIX:$\>$\intransition{{\tt fix}_i({\vec x}\;=\;{\vec p})}{p_i\,[{\tt f{\vec i}x}({\vec x}\,=\,{\vec p})\,/\,{\vec x}]}$ 
\end{tabbing}

\subsubsection{Redefined TCCS}

The redefined syntax of TCCS is: 

\begin{eqnarray*}
P & ::= & \prefix\,P\;|\;\sumofp\;|\;(\compo{P}{Q})\;|\;\res{a}{P}\;|\;\rep{P}\;|\;P[f]
\end{eqnarray*}
\begin{tabbing}
xxxxxxxx\= \kill
where \\
	\>$\sumofp\;::=\;\inact\;|\;\intsum{P}{Q}\;|\;\extsum{P}{Q}$.
\end{tabbing}

The redefined semantics for TCCS is:

\begin{tabbing}
xxxxxxxxxxxx\=\kill
$COMM:$\>$\intransition{y(x).\,P\;|\;\overline{y}z.\,Q}{\substi{P}{z}{x}\;|\;Q}$ \\
\\
$PAR:$\>$\infer{\intransition{P}{P'}}{\intransition{\compo{P}{Q}}{\compo{P'}{Q}}}{}$\\
\\
$INTSUM$:\>${\intransition{\intsum{P}{Q}}{P'} }$\\
\\
$EXTSUM$:\>$\infer{\intransition{P}{P'}}{\intransition{\extsum{P}{Q}}{\extsum{P'}{Q}}}{}$\\
\\
$RES:$\>$\infer{\intransition{P}{P'}}{\intransition{\res{x}{P}}{\res{x}{P'}}}{}$ \\
\\
$REL:$\>$\infer{\intransition{P}{P'}}{\intransition{P[f]}{P'[f]}}{}$\\
\\
$STRUCT:$\>$\infer{Q\;\equiv\;P\;\;\intransition{P}{P'}\;\;P'\;\equiv\;Q'}{\intransition{Q}{Q'}}{}$ 
\end{tabbing}

\subsection{TCCS Cham}

\Cham\ \cite{CHAM}, which originated in the $\Gamma$ language of Ban\^{a}tre and Le Metayer \cite{Gamma}, is designed to model asynchronous concurrent computations. By means of handling the operational semantics of various process calculi and concurrent \lc, Berry and Boudol show that Cham has the power of classical process calculi and behaves as concurrent generalisations of the \lc.
In \cite{CHAM}, they handle the subset of CCS, such as CCS$^-$ and TCCS \cite{TCCS}, and a concurrent \lc, $\gamma$--calculus \cite{gamma}. In this paper we only consider the syntax and operational semantics of the TCCS Cham, in which the TCCS calculus is modelled by Cham. First, we define the syntax and operational semantics of the TCCS, and then deal with the TCCS Cham.

\subsubsection{Syntax and Semantics of TCCS Cham}

The syntax of the TCCS Cham is:

{\em Agents:}
\begin{eqnarray*}
p & ::= & \inact\;|\;\alpha .\,p\;|\;(\compo{p}{q})\;|\;p\setminus a\;|\;p\,[\phi]\;|\;p\,\oplus\,q\;|\;p\,[\!]\,q\;|\;{\tt fix_{i}}({\vec x}\,=\,{\vec p})
\end{eqnarray*}

{\em Molecules:}
\begin{eqnarray*}
m & ::= & P\;|\;\alpha .\,m\;|\;\res{a}{m}\;|\;m\,[f]\;|\;S\;|\;m\,\triangleleft\,S\;|\;<\,m, m\,>\;|\;l:<\,m, m\,>\;|\;r:<\,m, m\,>
\end{eqnarray*}

Rules for the TCCS Cham contructed according to the operational semantics for TCCS are shown as follows:

\begin{tabbing}
xxxxxxxxxxxxxxxxxxxxxx\= \kill
parallel:	      	\>$\compo{p}{q}\;\rightleftharpoons\;p, q$ \\
\\
reaction:	      	\>$a.m, \overline{a}.n\;\rightarrow\;m, n$ \\
\\
restriction membranes: 	\>$m\setminus a\;\rightleftharpoons\;\membrane{m}\setminus a$ \\
\\
restriction ion: 	\>$(\alpha.m)\setminus a\;\rightleftharpoons\;\alpha.(m\setminus a)\;\;\;{\tt if}\;\alpha\;\not\in\;\{\,a, \overline{a}\,\}$ \\
\\
relabelling membranes: \>$m\,[\phi]\;\rightleftharpoons\;{\membrane{m}}\,[\phi]$ \\
\\
relabelling ion: \>$(\alpha.m)\,[\phi]\;\rightleftharpoons\;\phi(\alpha).(m\,[\phi])$ \\
\\
$\oplus$--left:		\>$\intsum{p}{q}\;\rightarrow\;p$ \\
\\
$\oplus$--right:		\>$\intsum{p}{q}\;\rightarrow\;q$ \\
\\
$[\!]$--expansion:	\>$p\,[\!]\,q\;\rightleftharpoons\;<\,\membrane{p}, \membrane{q}\,>$ \\
\\
left $[\!]$--ion:	\>$<\,\membrane{\alpha.m}, S\,>\;\rightharpoonup\;\alpha.l\,:\,<\,m, S\,>$ \\
\\
right $[\!]$--ion:	\>$<\,S, \membrane{\alpha.m}\,>\;\rightharpoonup\;\alpha.r\,:\,<\,S, m\,>$ \\
\\
left projection:	\>$l\,:\,<\,m, m'\,>\;\rightharpoonup\;m$ \\
\\
right projection:	\>$r\,:\,<\,m, m'\,>\;\rightharpoonup\;m'$ \\
\\
fixpoint:		\>${\tt fix}_i(\vec{x}\,=\,\vec{p})\;\rightharpoonup\;p_i[{\tt f\vec{i}x}(\vec{x}\,=\,\vec{p})\setminus\vec{x}]$ \\
\\
inaction cleanup:	\>$\inact\;\rightharpoonup$ \\
\\
restriction cleanup:	\>$\membrane{}\setminus a\;\rightharpoonup$ \\
\\
relabelling cleanup:	\>$\membrane{}\,[\phi]\;\rightharpoonup$ 
\end{tabbing}

\subsubsection{Redefined Syntax and Semantics of TCCS Cham}

The redefined syntax of the TCCS Cham is:

{\em Agents:}
\begin{eqnarray*}
p & ::= & \prefix\,P\;|\;\sumofp\;|\;(\compo{p}{q})\;|\;\res{a}{P}\;|\;\rep{P}\;|\;p\,[\phi]
\end{eqnarray*}
\begin{tabbing}
xxxxxxxx\= \kill
where \\
	\>$\sumofp\;::=\;\inact\;|\;\intsum{P}{Q}\;|\;\extsum{P}{Q}$.
\end{tabbing}

{\em Molecules:}
\begin{eqnarray*}
m & ::= & P\;|\;\alpha .\,m\;|\;\res{a}{m}\;|\;m\,[f]\;|\;S\;|\;m\,\triangleleft\,S\;|\;<\,m, m\,>\;|\;l:<\,m, m\,>\;|\;r:<\,m, m\,>
\end{eqnarray*}

The redefined rules of the TCCS Cham is:

\begin{tabbing}
xxxxxxxxxxxxxxxxxxxxxx\= \kill
parallel:	      	\>$\compo{P}{Q}\;\rightleftharpoons\;P, Q$ \\
\\
reaction:	      	\>$a.m, \overline{a}.n\;\rightarrow\;m, n$ \\
\\
restriction membranes:\>$\res{a}{m};\rightleftharpoons\;\res{a}{\membrane{m}}$\\
\\
restriction ion: 	\>$\res{a}{(\alpha.m)}\;\rightleftharpoons\;\alpha.(\res{a}{m})\;\;\;{\tt if}\;\alpha\;\not\in\;\{\,a, \overline{a}\,\}$ \\
\\
relabelling membranes: \>$m\,[\phi]\;\rightleftharpoons\;{\membrane{m}}\,[\phi]$ \\
\\
relabelling ion: \>$(\alpha.m)\,[\phi]\;\rightleftharpoons\;\phi(\alpha).(m\,[\phi])$ \\
\\
$\oplus$--left:		\>$\intsum{P}{Q}\;\rightarrow\;P$ \\
\\
$\oplus$--right:		\>$\intsum{P}{Q}\;\rightarrow\;Q$ \\
\\
$[\!]$--expansion:	\>$P\,[\!]\,Q\;\rightleftharpoons\;<\,\membrane{P}, \membrane{Q}\,>$ \\
\\
left $[\!]$--ion:	\>$<\,\membrane{\alpha.m}, S\,>\;\rightharpoonup\;\alpha.l\,:\,<\,m, S\,>$ \\
\\
right $[\!]$--ion:	\>$<\,S, \membrane{\alpha.m}\,>\;\rightharpoonup\;\alpha.r\,:\,<\,S, m\,>$ \\
\\
left projection:	\>$l\,:\,<\,m, m'\,>\;\rightharpoonup\;m$ \\
\\
right projection:	\>$r\,:\,<\,m, m'\,>\;\rightharpoonup\;m'$ \\
\\
fixpoint:		\>$\rep{P}\;\rightharpoonup\;P\;|\;\rep{P}$ \\
\\
inaction cleanup:	\>$\inact\;\rightharpoonup$ \\
\\
restriction cleanup:	\>$\res{a}{\membrane{}}\;\rightharpoonup$ \\
\\
relabelling cleanup:	\>$\membrane{}\,[\phi]\;\rightharpoonup$ 
\end{tabbing}

\subsection{\PC}

The \Pc\ \cite{Pi}, based on ECCS \cite{ECCS} which successfully extends CCS to include mobility without sacrificing its algebraic properties, is a calculus of communicating systems in which processes which have changing sturcture can be naturally expressed. In a system, the component agents may be arbirarily linked, and also a communication between neighbours may carry information which changes that linkage. CCS can express this mobility indirectly. In the \Pc, this mobility, however, is achieved directly by allowing references to processes to be communicated. 

In order for the calculus to be as concise in primitives as possible, all distinction among link names, variables, and ordinary data values, are removed. Thus there are only two essential classes of entity: {\em names} and {\em agents}.
 
\subsubsection{Syntax and Semantics of the \PC}

Suppose $\cal {N}$ be an infinite set of names, and let $x, y, z, \ldots \in \cal{N}$. Suppose also $\cal{A}$ be a set of agent identifiers, and let $A, B, C, \ldots \in \cal{A}$. Now let $\cal{P}$ be a set of processes, and let $P, Q, R, \ldots \in \cal{P}$. Then the syntax of the \Pc\ may be defined as follows:

\begin{eqnarray*}
P & ::= & \inact\;|\;\binsum{P}{Q}\;|\;\overline{y}x.\,P\;|\;y(x).\,P\;|\;\tau .\,P\;|\;(\compo{P}{Q})\;|\;(x)\,P\;|\;\match{x}{y}{P}\;|\;\ident{A}{y}
\end{eqnarray*}

$\inact$ means inaction which can do nothing. $\binsum{P}{Q}$ behaves like $P$ or $Q$, but not both. $\compo{P}{Q}$ may act independently, but may also communicate. $\overline{y}x.\,P$ sends the name $x$ at port $\overline{y}$ and then behaves like $P$. $y(x).\,P$ receives a name $z$ at port $y$ and then behaves like $\substi{P}{z}{x}$. $\tau.\,P$ performs the silent action and then behaves like $P$. $(x)\,P$ behaves like $P$ but actions are prohibited at port $x$ and $\overline{x}$. $\match{x}{y}{P}$ behaves like $P$ if $x = y$, otherwise like $\inact$. For any agent identifier $A$, there must be a unique defining equation $\ident{A}{x}\;\stackrel{\rm def}{=}\;P$, where the names $x_1, ldots, x_n$ are distinct and are the only names which may occur free in P. The $\ident{A}{y}$ behaves like $P\,\{\,y_1/x_1, \ldots, y_n/x_n\,\}$. This syntactic substitution replaces CCS relabelling operation.

Note that in \cite{FunAsProcs}, $\tau.\,P, \match{x}{y}{P}, \binsum{P}{Q}$, and $\ident{A}{y}$ have been omitted, but replication $!P$ is added.

In order to define $P$ in {\em head normal form}, a bound output action is defined as follows:

\begin{tabbing}
xxxxxxxx\= \kill	
	\>$\overline{y}(x).\,P = (x)\overline{y}x.\,P$ if $x\;\neq\;y$.
\end{tabbing}

Therefore there are four kinds of action $\alpha$ in the \Pc\ as follows: 
\begin{itemize}
\item The {\em silent} action $\tau$: $\labeltransition{P}{\tau}{Q}$ means that without interaction with the environment $P$ evolves to $Q$.
\item A {\em free output} action $\overline{y}x$: $\labeltransition{P}{\overline{y}x}{Q}$ means that $P$ sends the name $x$ at port $\overline{y}$.
\item A {\em bound output} action $\overline{y}(x)$: $\labeltransition{P}{\overline{y}(x)}{Q}$ sends a private name bound in $P$ at port $\overline{y}$, and $(x)$ is a reference to where this private name occurs. 
\item An {\em input} action $y(x)$: $\labeltransition{P}{y(x)}{Q}$ receives a name $z$ at port $y$ and then evolves to $\substi{Q}{z}{x}$. 
\end{itemize}
Note that there is no notion about bound output action in CCS. Note also that in CCS an input action contains the actual received value, whereas in the \Pc\ $(y)$ is a reference to the place where the received name occurs.

The operational semantics for the \Pc\ is defined by the reduction rules, in which the rules associated with $\tau$--Action, Input--Action, Output--action, Communication, Parallel Composition, Summation, Restriction, Matching, Agent Identification, Scope Opening, and Scope Closing are indicated by TAU, INPUT, OUTPUT, COMM, PAR, SUM, RES, MATCH, IDENT, OPEN, and CLOSE, respectively. Reduction $\rightarrow$ is the smallest relation satisfying:  

\begin{tabbing}
xxxxxxxxxxxx\= \kill
$TAU:$\>$\infer{}{\labeltransition{P}{\tau}{P}}{}$ \\
\\
$INPUT:$\>$\infer{}{\labeltransition{y(x).\,P}{y(z)}{\substi{P}{z}{x}}}{z\;\not\in\;fn((x)P)}$\\
\\
$OUTPUT:$\>$\infer{}{\labeltransition{\overline{y}x.\,P}{\overline{y}x}{P}}{}$\\
\\
$COMM:$\>$\infer{\labeltransition{P}{\overline{y}x}{P'}\;\;\;{\labeltransition{Q}{y(x)}{Q'}}}{\labeltransition{\compo{P}{Q}}{\tau}{\compo{P'}{\substi{Q'}{x}{Z}}}}{}$\\
\\
$PAR:$\>$\infer{\labeltransition{P}{\alpha}{P'}}{\labeltransition{\compo{P}{Q}}{\alpha}{\compo{P'}{Q}}}{bn(\alpha)\,\cap\,fn(Q)\;=\; \emptyset}$\\
\\
$SUM:$\>$\infer{\labeltransition{P}{\alpha}{P'}}{\labeltransition{\binsum{P}{Q}}{\alpha}{P'}}{}$\\
\\
$RES:$\>$\infer{\labeltransition{P}{\alpha}{P'}}{\labeltransition{(y)\,P}{\alpha}{(y)\,P'}}{y\;\not\in\;n(\alpha)}$\\
\\
$MATCH:$\>$\infer{\labeltransition{P}{\alpha}{P'}}{\labeltransition{\match{x}{x}{P}}{\alpha}{P'}}{}$\\
\\
$IDENT:$\>$\infer{\labeltransition{\simulsubsti{P}{x}{y}}{\alpha}{P'}}{\labeltransition{A(\vec{x})}{\alpha}{P'}}{\paradef{A}{y}{P}}$\\
\\
$CLOSE:$\>$\infer{\labeltransition{P}{\overline{y}(x)}{P'}\;\;\;{\labeltransition{Q}{y(z)}{Q'}}}{\labeltransition{\compo{P}{Q}}{\tau}{(x)(\compo{P'}{Q'})}}{}$\\
\\
$OPEN:$\>$\infer{\labeltransition{P}{\overline{y}x}{P'}}{\labeltransition{(x)\,P}{\overline{y}(z)}{\substi{P'}{z}{x}}}{x\,\neq\,y,\;\;z\,\not\in\,fn((x)\,P')}$ 
\end{tabbing}

However, inspired by Berry and Boudol \cite{CHAM}, Milner \cite{FunAsProcs} defined a structural congruence relation over terms to simplify the form of the reduction rules. Structural congruence  $\equiv$  is the smallest congruence over the set of processes ${\cal P}$ satisfying these equations:

\begin{tabbing}
xxxxxxxx\=xxx\= \kill
	\>1.\>$P\;\equiv\;Q$  whenever $P$ is $\alpha$-convertible to $Q$ \\
\\
	\>2.\>$({\cal P}/\equiv,\,|,\,\inact)$ is a symmetric monoid \\
\\
	\>3.\>$!P\;\equiv\;\compo{P}{!P}$ \\
\\
	\>4.\>$(x){\inact}\;\equiv\;\inact,\;\;\;(x)(y)P\;\equiv\;(y)(x)P$ \\
\\
	\>5.\>$(x)(\compo{P}{Q})\;\equiv\;\compo{P}{(x)Q}\;\;\;x\;\not\in\;fn(P)$
\end{tabbing}

The operational semantics of the \Pc\ in \cite{FunAsProcs} may be summarised as follows: Using the above structural congruence the simplified form of reduction rule is presented. The rules are associated with Communication, Parallel Composition, Restriction, and Structural Congruence are indicated by COMM, PAR, RES, and STRUCT, respectively. Reduction $\rightarrow$ is the smallest relation satisfying:  

\begin{tabbing}
xxxxxxxxxxxx\=\kill
$COMM:$\>$\intransition{y(x).\,P\;|\;\overline{a}y.\,Q}{\substi{P}{y}{x}\;|\;Q}$ \\
\\
$PAR:$\>$\infer{\intransition{P}{P'}}{\intransition{\compo{P}{Q}}{\compo{P'}{Q}}}{}$\\
\\
$RES:$\>$\infer{\intransition{P}{P'}}{\intransition{(y)P}{(y)P'}}{}$ \\
\\
$STRUCT:$\>$\infer{Q\;\equiv\;P\;\;\intransition{P}{P'}\;\;P'\;\equiv\;Q'}{\intransition{Q}{Q'}}{}$ 
\end{tabbing}

\subsubsection{Redefined \PC}

The redefined syntax of the \Pc\ is:

\begin{eqnarray*}
P & ::= & \prefix\,P\;|\;\sumofp\;|\;(\compo{P}{Q})\;|\;\res{x}{P}\;|\;\match{x}{y}{P}\;|\;\ident{A}{y}
\end{eqnarray*}
\begin{tabbing}
xxxxxxxx\= \kill
where \\
	\>$\prefix\;::=\;y(x).\;|\;\overline{y}x.\;|\;\tau.$ \\
\\
	\>$\sumofp\;::=\;\inact\;|\;\binsum{P}{Q}$.
\end{tabbing}

Because the structural congruence has interesting features including the power of simplification, we redefine the operational semantics for the \Pc\ according to the \cite{FunAsProcs} which uses the structural congruence relation to define the operational semantics:

\begin{tabbing}
xxxxxxxxxxxx\=\kill
$COMM:$\>$\intransition{y(x).\,P\;|\;\overline{y}z.\,Q}{\substi{P}{z}{x}\;|\;Q}$ \\
\\
$PAR:$\>$\infer{\intransition{P}{P'}}{\intransition{\compo{P}{Q}}{\compo{P'}{Q}}}{}$\\
\\
$BINSUM:$\>$\infer{\intransition{P}{P'}}{\intransition{\binsum{P}{Q}}{P'}}{}$\\
\\
$RES:$\>$\infer{\intransition{P}{P'}}{\intransition{\res{x}{P}}{\res{x}{P'}}}{}$ \\
\\
$MATCH:$\>$\infer{\intransition{P}{P'}}{\intransition{\match{x}{x}{P}}{P'}}{}$\\
\\
$IDENT:$\>$\infer{\intransition{\simulsubsti{P}{x}{y}}{P'}}{\intransition{A(\vec{x})}{P'}}{\paradef{A}{y}{P}}$\\
\\ 
$CLOSE:$\>$\infer{\labeltransition{P}{\overline{y}(x)}{P'}\;\;\;{\labeltransition{Q}{y(z)}{Q'}}}{\labeltransition{\compo{P}{Q}}{\tau}{(\nu\,x)(\compo{P'}{Q'})}}{}$\\
\\
$OPEN:$\>$\infer{\labeltransition{P}{\overline{y}x}{P'}}{\labeltransition{(\nu\,x)\,P}{\overline{y}(z)}{\substi{P'}{z}{x}}}{x\,\neq\,y,\;\;z\,\not\in\,fn((\nu\,x)\,P')}$ 
\\
\\
$STRUCT:$\>$\infer{Q\;\equiv\;P\;\;\intransition{P}{P'}\;\;P'\;\equiv\;Q'}{\intransition{Q}{Q'}}{}$ 
\end{tabbing}

\subsection{LCCS}

In \cite{Leth91} to tackle the parallel implementation problem, the idea of parallel reduction which performs only small and simple computations is taken. Upon the idea of using  process networks to implement functional languages, Leth developed the process calculus LCCS (for Label passing CCS) for describing the reconfigurable networks of communicating processes in which the only computation is communication and the manipulation of the interconnection structure.  

\subsubsection{Syntax and Semantics of LCCS}

The syntax of LCCS is:

\begin{eqnarray*}
P & ::= & nil\;|\;l?x.\,P\;|\;l!l'.\,P\;|\;\extsum{P}{P'}\;|\;\intsum{P}{P'}\;|\;\compo{P}{P'}\;|\;P\setminus\alpha\;|\;{\tt rec}X.\,P \\
  &     & |\;X\;|\;{\tt if}\;b\;{\tt then}\;P\;{\tt else}\; P' \\
l & ::= & x\;|\;\alpha \\
b & ::= & true\;|\;l = l'\;|\;b\,\wedge\,b'\;|\;\neg b
\end{eqnarray*}
\begin{tabbing}
xxxxxxxx\= \kill
where \\
	\>$x\,\in\,Var; \alpha\,\in\,Labels; X\,\in\,VAR; b\,\in\,BExp$.
\end{tabbing}

$nil$ means the inaction. $l?x.\,P$ receives the name $y$ at port $l$ and then behaves like $\substi{P}{y}{X}$. $l!l'.\,P$ sends the name $l'$ at port $l$ and then behaves like $P$. $\extsum{P}{P'}$ is the external choice between $P$ and $P'$ by communication with a user. $\intsum{P}{P'}$ is the internal choice between $P$ and $P'$ by the system. $\compo{P}{P'}$ may act independently, but they may also communicate. $P\setminus\alpha$ behaves like $P$ but actions are prohibited at port $\alpha$ and $\overline{\alpha}$. ${\tt rec}X.\,P$ is the recursive process $P$. $X$ is a bound variable and can be renamed without any semantic effect. ${\tt if}\;b\;{\tt then}\;P\;{\tt else}\; P'$ is a conditional in which if $b$ is {\em true} then $P$ is activated, otherwise $P'$ is activated.

As the choice problem has been addressed in \cite{TCCS}, to overcome the different interpretations of the binary choice $+$, Leth has used two new distinct operators; external choice $\frame{+}$ and internal choice $\oplus$. LCCS does not include the syntactical construct $\tau.\,P$, but allow $\tau$ to describe internal actions.

The rules are associated with Input, Output, Internal Summation, External Summation, Parallel Composition, Communication, Import, Restriction, Export, Conditional operation, Recursion are indicated by INPUT, OUTPUT, INTSUM, EXTSUM, PAR, COMM, IMPORT, RES, EXPORT, COND, and REC, respectively. The operational semantics of LCCS is: 

\begin{tabbing}
xxxxxxxxxxxx\=\kill
$INPUT:$\>$\labeltransition{\inputact{\alpha}{x}.\,P}{\inputact{\alpha}{x}}{P}$ \\
\\
$OUTPUT:$  \>$\labeltransition{\outputact{\alpha}{\beta}.\,P}{\outputact{\alpha}{\beta}}{P}$ \\
\\
$COMM:$\>$\infer{{\labeltransition{P_{1}}{\inputact{\alpha}{x}}{P'_{1}}}\;\;{\labeltransition{P_{2}}{\outputact{\alpha}{\beta}}{P'_{2}}}}{\labeltransition{\compo{P_{1}}{P_{2}}}{\tau}{\compo{\substi{P'_{1}}{\beta}{x}}{P'_{2}}}}{}$ \\
\\
$PAR:$\>$\infer{\labeltransition{P_{1}}{\Gamma}{P'_{1}}}{\labeltransition{\compo{P_{1}}{P_{2}}}{\Gamma}{\compo{P'_{1}}{P_{2}}}}{}$ \\
\\
$INTSUM_1:$\>$\labeltransition{\intsum{P_{1}}{P_{2}}}{\tau}{P_{1}}$\\
\\
$INTSUM_2:$\>$\labeltransition{\intsum{P_{1}}{P_{2}}}{\tau}{P_{2}}$\\
\\
$EXTSUM_1:$\>$\infer{\labeltransition{P_{1}}{\Gamma}{P'_{1}}}{\labeltransition{\extsum{P_{1}}{P_{2}}}{\Gamma}{P'_{1}}}{\Gamma\,\neq\,\tau}$\\
\\
$EXTSUM_2:$\>$\infer{\labeltransition{P_{1}}{\tau}{P'_{1}}}{\labeltransition{\extsum{P_{1}}{P_{2}}}{\tau}{\extsum{P'_{1}}{P_{2}}}}{}$ \\
\\
$RES:$\>$\infer{\labeltransition{P}{\Gamma}{P'}}{\labeltransition{P\setminus\alpha}{\Gamma}{P'\setminus\alpha}}{{\tt if}\;\alpha\;\not\in\;sort(\Gamma)}$ \\
\\
$COND_1:$\>$\infer{\labeltransition{P_{1}}{\Gamma}{P'_{1}}}{\labeltransition{{\tt if\;true\;then}\;{P_{1}}\;{\tt else}\;{P_{2}}}{\Gamma}{P'_{1}}}{}$\\
\\
$COND_2:$\>$\infer{\labeltransition{P_{1}}{\Gamma}{P'_{1}}}{\labeltransition{{\tt if\;false\;then}\;{P_{1}}\;{\tt else}\;{P_{2}}}{\Gamma}{P'_{2}}}{}$ \\
\\
$REC:$\>$\labeltransition{{\tt rec}X.\,P}{\tau}{P[{\tt rec}X.P/X]}$ \\
\\
$IMPORT:$\>$\infer{{\labeltransition{P_{1}}{\inputact{\alpha}{x}}{P'_{1}}}\;\;{\labeltransition{P_{2}}{\outputact{\alpha}{\setminus\beta}}{P'_{2}}}}{\labeltransition{\compo{P_{1}}{P_{2}}}{\tau}{({\compo{\substi{P'_{1}}{\gamma}{x}}{\substi{P'_{2}}{\gamma}{\beta}}})\setminus\gamma}}{\gamma\;\not\in\;sort(P'_{1})\;\cup\;sort(P'_{2}\setminus\beta)}$ \\
\\
$EXPORT:$\>$\infer{\labeltransition{P}{\outputact{\alpha}{\beta}}{P'}}{\labeltransition{P\setminus\beta}{\outputact{\alpha}{\setminus\beta}}{P'}}{{\tt if}\; \alpha\;\neq\;\beta}$ 
\end{tabbing}
\begin{tabbing}
xxxxxxxx\= \kill
where \\
	\>$\Gamma\;=\;\{\,\inputact{\alpha}{x},\,\outputact{\alpha}{\beta},\,\tau,\,\outputact{\alpha}{\setminus\beta}\,\}$\\
\\
	\>$\alpha,\,\beta\;\in\;{\cal L}\,;\,x\;\in\;Var$.
\end{tabbing}

Notice that $\outputact{\alpha}{\setminus\beta}$ is a bound output action as defined in \cite{Pi}.

Note also that IMPORT and EXPORT rules correspod to the Scope Closing and Scope Opening rules in \cite{Pi}, respectively. In the scope closing rule IMPORT, a bound output action combines with an input action, whereas in the scope opening rule EXPORT, a free output action is transformed to a bound output action removing one restriction operator.

\subsubsection{Redefined LCCS}

The redefined syntax of LCCS is:

\begin{eqnarray*}
P & ::= & \prefix\,P\;|\;\sumofp\;|\;\compo{P}{P'}\;|\;\res{x}{P}\;|\;\rep{P}\;|\;\match{x}{y}{P} 
\end{eqnarray*}
\begin{tabbing}
xxxxxxxx\= \kill
where \\
	\>$\prefix\;::=\;y(x).\;|\;\overline{y}x.$ \\
\\
	\>$\sumofp\;::=\;\inact\;|\;\intsum{P}{P'}\;|\;\extsum{P}{P'}$.
\end{tabbing}

Note that replication replaces recursion without losing its meaning.

The redefined operational semantics of LCCS is: 

\begin{tabbing}
xxxxxxxxxxxx\=\kill
$COMM:$\>$\intransition{y(x).\,P\;|\;\overline{y}z.\,Q}{\substi{P}{z}{x}\;|\;Q}$ \\
\\
$PAR:$\>$\infer{\intransition{P}{P'}}{\intransition{\compo{P}{Q}}{\compo{P'}{Q}}}{}$\\
\\
$INTSUM:$\>$\intransition{\intsum{P}{Q}}{P}$\\
\\
$EXTSUM:$\>$\infer{\intransition{P}{P'}}{\intransition{\extsum{P}{Q}}{\extsum{P'}{Q}}}{}$ \\
\\
$RES:$\>$\infer{\intransition{P}{P'}}{\intransition{\res{x}{P}}{\res{x}{P'}}}{}$ \\
\\
$MATCH:$\>$\infer{\intransition{P}{P'}}{\intransition{\match{x}{x}{P}}{P'}}{}$\\
\\
$CLOSE:$\>$\infer{\labeltransition{P}{\overline{y}(x)}{P'}\;\;\;{\labeltransition{Q}{y(z)}{Q'}}}{\labeltransition{\compo{P}{Q}}{\tau}{(\nu\,x)(\compo{P'}{Q'})}}{}$\\
\\
$OPEN:$\>$\infer{\labeltransition{P}{\overline{y}x}{P'}}{\labeltransition{(\nu\,x)\,P}{\overline{y}(z)}{\substi{P'}{z}{x}}}{x\,\neq\,y,\;\;z\,\not\in\,fn((\nu\,x)\,P')}$ 
\\
\\
$STRUCT:$\>$\infer{Q\;\equiv\;P\;\;\intransition{P}{P'}\;\;P'\;\equiv\;Q'}{\intransition{Q}{Q'}}{}$ 
\end{tabbing}

\subsection{\PPC}

The \ppc\ \cite{PolyPi} is a polyadic version of the \Pc, which is a model of concurrent computation based on the notion of naming. 

\subsubsection{Syntax and Semantics of the \PPC}

We presuppose $\cal N$ be a set of names, and let $\alpha, \beta, \ldots$ ranged over names and co--names. We also presuppose $\vec x, \vec y, \ldots$ be vectors of names, with length $|\vec x|, |\vec y|, \ldots$.

The syntax of the \ppc\ is:

\begin{eqnarray*}
Normal processes:&      & N  ::=  \alpha .\,A\;|\;\inact\;|\;M + N \\
Processes:       &      & P  ::=  N\;|\;(\compo{P}{Q})\;|\;!P\;|\;\res{x}{P}\\
Abstractions:    &      & F  ::=  P\;|\;(\lambda\,x)\,F\;|\;\res{x}{F} \\
Concretions:     &      & C  ::=  P\;|\;[x]\,C\;|\;\res{x}{C} \\
Agents:          &      & A  ::=  F\;|\;C
\end{eqnarray*}

The structural congruence $\equiv$ is the smallest congruence relation over set of processes ${\cal P}$ such that the following rules hold:

\begin{tabbing}
xxxxxxxx\=xxx\= \kill
	\>1.\>Processes are identified if they only differ by a change of bound names \\
\\
	\>2.\>$({\cal N}/\equiv,\,+,\,\inact)$ is a symmetric monoid \\
\\
	\>3.\>$({\cal P}/\equiv,\,|,\,\inact)$ is a symmetric monoid \\
\\
	\>4.\>$!P\;\equiv\;\compo{P}{!P}$ \\
\\
	\>5.\>$\res{x}{\inact}\;\equiv\;\inact,\;\;\;(\nu\,x)(\nu\,y)P\;\equiv\;(\nu\,y)(\nu\,x)P$ \\
\\
	\>6.\>If $x\;\not\in\;fn(P)$ then $(\nu\,x)(\compo{P}{Q})\;\equiv\;\compo{P}{(\nu\,x)Q}$ \\
\\
	\>7.\>$(\nu\,y)(\lambda\,x)F\;\equiv\;(\lambda\,x)(\nu\,y)F\;\;\;(x\;\neq\;y)$ \\
\\
	\>8.\>$(\nu\,y)[x]\,C\;\equiv\;[x](\nu\,y)C\;\;\;(x\;\neq\;y)$ \\
\\
	\>9.\>$(\nu\,x)(\nu\,y)A\;\equiv\;(\nu\,y)(\nu\,x)A,\;\;\;(\nu\,x)(\nu\,x)A\;\equiv\;(\nu\,x)A$ 
\end{tabbing}

The rules are associated with Communication, Parallel Composition, Restriction, Structural Congruence are indicated by COMM, PAR, RES, and STRUCT, respectively. The reduction relation $\rightarrow$ over processes is the least relation satisfying the following rules: 

\begin{tabbing} 
xxxxxxxxxxxx\=xxxxxx\=xxxxxx\=xxxxxx\=xxxxxx\=xxxxxx\=xxxxxxxxxxxx\=xxxxxx\=\kill
$COMM:$\>$\intransition{(\cdots\,+\,x.\,F)\;|\;(\cdots\,+\,\overline{x}.\,C)}{F\/\bullet\/C}$ \\
\\
$PAR:$\>$\infer{\intransition{P}{P'}}{\intransition{\compo{P}{Q}}{\compo{P'}{Q}}}{}$ \\
\\
$RES:$\>$\infer{\intransition{P}{P'}}{\intransition{\res{x}{P}}{\res{x}{P'}}}{}$ \\
\\
$STRUCT:$\>$\infer{Q\;\equiv\;P\;\;\intransition{P}{P'}\;\;P'\;\equiv\;Q'}{\intransition{Q}{Q'}}{}$ 
\end{tabbing}
 
\begin{tabbing}
xxxxxxxx\= \kill
where \\
      	\>standard form of abstraction $F\;\equiv\;(\lambda {\vec x})\,P$ \\
\\
	\>standard form of concretion $C\;\equiv\;(\nu {\vec z})[{\vec y}]\,Q\;\;\;({\vec z}\,\subseteq\,{\vec y})$ \\
\\
	\>pseudo-application $F\/\bullet\/C\;\stackrel{\rm def}{=}\;(\nu{\vec z})(P\{{\vec y}/{\vec x}\}\;|\;Q)$ 
\end{tabbing}

\subsubsection{Redefined \PPC}

The redefined syntax of the \ppc\ is:

\begin{eqnarray*}
P & ::= & \prefix\,P \;|\;\sumofp\;|\;(\compo{P}{Q})\;|\;\rep{P}\;|\;\res{\vec x}{P}
\end{eqnarray*} 
\begin{tabbing}
xxxxxxxx\= \kill
where \\
	\>$\prefix\;::=\;y(x).\;|\;\overline{y}x.\;|\;y(\vec x)\;|\;\overline{y}{\vec x}.$ \\
\\
	\>$\sumofp\;::=\;\inact\;|\;\binsum{P}{Q}$\\
\\
	\>$y(\vec x).P\;\stackrel{\rm def}{=}\;y.(\lambda\,{\vec x})\,P$\\
\\
	\>$\overline{y}{\vec x}.P\;\stackrel{\rm def}{=}\;\overline{y}.[\vec x]\,P$\\
\\
	\>${\vec x} = x_1, x_2, \ldots, x_n$
\end{tabbing}

We now should redefine the structural congruence relation $\equiv$, which is the smallest relation over set of processes $\cal P$ satisfying:

\begin{tabbing}
xxxxxxxx\=xxx\= \kill
	\>1.\>$P\;\equiv\;Q$ if $P$ is $\alpha$--convertible to $Q$. \\
\\
	\>2.\>$({\cal P}/\equiv,\,+,\,\inact)$ is a symmetric monoid. \\
\\
	\>3.\>$({\cal P}/\equiv,\,|,\,\inact)$ is a symmetric monoid. \\
\\
	\>4.\>$\rep{P}\;\equiv\;\compo{P}{\rep{P}}$ \\
\\
	\>5.\>$\res{\vec x}{\inact}\;\equiv\;\inact,\;\;\;(\nu\,\vec x)(\nu\,\vec y)P\;\equiv\;(\nu\,\vec y)(\nu\,\vec x)P$ \\
\\
	\>6.\>If $x\;\not\in\;fn(P)$ then $(\nu\,\vec x)(\compo{P}{Q})\;\equiv\;\compo{P}{(\nu\,\vec x)Q}$ \\
\\
	\>7.\>If $\vec x\;\neq\;\vec y$ then $(\nu\,\vec y){\vec x}.P\;\equiv\;{\vec x}.(\nu\,\vec y)P$ \\
\\
	\>8.\>$(\nu\,\vec x)(\nu\,\vec y)P\;\equiv\;(\nu\,\vec y)(\nu\,\vec x)P,\;\;\;(\nu\,\vec x)(\nu\,\vec x)P\;\equiv\;(\nu\,\vec x)P$ 
\end{tabbing}

Hence the redefined operational semantics for the \ppc\ is:

\begin{tabbing} 
xxxxxxxxxxxx\= \kill
$COMM:$\>$\intransition{(\cdots\,+\,y(\vec x).\,P)\;|\;(\cdots\,+\,\res{\vec w}(\overline{y}{\vec z}.\,Q))}{\res{\vec w}{(P\{{\vec z}/{\vec x}\}\;|\;Q)}}$ \\
\\
$PAR:$\>$\infer{\intransition{P}{P'}}{\intransition{\compo{P}{Q}}{\compo{P'}{Q}}}{}$ \\
\\
$BINSUM:$\>$\infer{\intransition{P}{P'}}{\intransition{\binsum{P}{Q}}{P'}}{}$\\
\\
$RES:$\>$\infer{\intransition{P}{P'}}{\intransition{\res{x}{P}}{\res{x}{P'}}}{}$ \\
\\
$STRUCT:$\>$\infer{Q\;\equiv\;P\;\;\intransition{P}{P'}\;\;P'\;\equiv\;Q'}{\intransition{Q}{Q'}}{}$ 
\end{tabbing}

\section{Conclusions}

We showed that the \mynote\ can express all the process calculi without sacrificing their concepts. We also showed that the \mynote\ can be used to represent any kinds of process calculi, even though we restricted ourselves to redefining syntax and semantics of CCS, TCCS, the \Pc, LCCS, and the \ppc\ only. As we mentioned earlier, this is an experiment. Thus we need more precise notations to handle various process calculi, including asynchronous process calculi such as \cite{Asynch}, \cite{AsynchMobile}, etc.

\begin{thebibliography}{MPW89}

\bibitem[{BLM86}]{Gamma}
J-P. Ban\^{a}tre and D. Le Metayer:
{\em A New Computational Model and Its Discipline of Programming},
Technical Report INRIA Report 566, 1986.

\bibitem[{BeBo90}]{CHAM}
G. Berry and G. Boudol:
{\em The  Chemical Abstract Machine},
Proceedings of POPL '90, p 81-94, ACM, 1990. Also in Theoretical Computer Science, no.96, pp. 217--248, 1992. 

\bibitem[{Bou89}]{gamma}
G. Boudol:
{\em Towards a \LC\ for concurrent and communicating systems},
Proceedings of TAPSOFT '89, LNCS 351, pp. 149--161, Springer-Verlag, 1989.

\bibitem[{DNH87}]{TCCS}
R. De Nicola and M. Hennessy:
{\em CCS without $\tau$'s},
Proceedings of TAPSOFT '87, LNCS 249, pp. 138--152, Springer-Verlag, 1987.

\bibitem[{EnN86}]{ECCS}
U. Engberg and M. Nielsen:
{\em A Calculus of Communicating Systems with Label Passing},
Report Daimi PB-206, Computer Science Department, University of Aarhus, 1986.

\bibitem[{Gla92}]{AsynchMobile}
J. Glauert:
{\em Asynchronous Mobile Processes and Rewriting},
Proceedings of PARLE '92, LNCS 605, pp.63--78, Springer-Verlag, 1992.

\bibitem[{Hoa85}]{CSP}
C.A.R. Hoare:
{\bf Communicating Sequential Processes},
Prentice Hall, 1985.

\bibitem[{HoT91}]{Asynch}
K. Honda and M. Tokoro:
{\em An Object Calculus for Asynchronous Communication},
Proceedings of ECOOP'91, LNCS, pp. , Springer-Verlag, 1991.

\bibitem[{Leth91}]{Leth91}
L. Leth:
{\em Functional Programs as Reconfigurable Networks of Communicating Processes},
Ph.D. Thesis, Imperial College, London, 1991. 

\bibitem[{Mil80}]{CCS}
R. Milner: 
{\em A Calculus of Communicating Systems},
LNCS 92, Springer-Verlag, 1980.

\bibitem[{Mil89}]{CC}
R. Milner:
{\bf Communication and Concurrency},
Prentice Hall, 1989.

\bibitem[{MPW89}]{Pi}
R. Milner, J. Parrow, \& D. Walker:
{\em A Calculus of Mobile Processes}, Parts I and II,
Information and Computation, no. 100, pp. 41--77, 1992. Also in Technical Report ECS-LFCS-89-85(6), Edinburgh University, June 1989.

\bibitem[{Mil90}]{FunAsProcs}
R. Milner: 
{\em Functions as Processes},
Automata, Languages, and Programming. LNCS 443, pp. 167--180, Springer-Verlag, 1990. Also in 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. 

\bibitem[{Plo81}]{OperSem}
G.D. Plotkin:
{\em A Structural Approach to Operational Semantics},
Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

\bibitem[{Tho89}]{CHOCS}
B. Thomsen:
{\em A Calculus of Higher Order Communicating Systems},
Proceedings of POPL 89, pp. 143--154, ACM, 1989.

\bibitem[{Tho90}]{Chocs}
B. Thomsen:
{\em Calculi for Higher Order Communicating Systems},
Ph.D. Thesis, Department of Computing, Imperial College, 1990.

\end{thebibliography}

\newpage
{\Large {\bf Appendices}}

\appendix

\section{Entities}

\begin{tabbing}
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx\= \kill			
processes:		\>$P, Q, \ldots \in {\cal P}$ \\
\\
normal processes:	\>$M, N, \ldots \in {\cal NP}$ \\
\\
names:			\>$x, y, \ldots \in {\cal N}$ \\
\\
co--names:		\>$\overline{x}, \overline{y}, \ldots \in \overline{\cal N}$ \\
\\
name vectors:		\>${\vec x}, {\vec y}, \ldots \in \vec{\cal N}$\\
\\
labels:			\>$l, l', \ldots \in {\cal L}$\\
\\
agent identifiers: 	\>$A, B, \ldots \in {\cal A}$ \\
\\
agent variables:	\>$X, Y, \ldots \in {\cal VAR}$ \\
\\
actions:		\>$\alpha, \beta, \ldots \in Act$ \\
\\
action sequences:	\>$\alpha*, \beta*, \ldots \in Act^{*}$ \\
\\
finite index sets: 	\>$I, J \;\;\; (i, j, \ldots \in I)$ \\
\\
%values: 		\>$u, v, \ldots \in {\cal V}$ \\
%\\	
%value variables:	\>$x, y, \ldots \in Var$ \\
%\\
%value expressions: 	\>$e, e_1, e_2, \ldots \in Exp$ \\
%\\
boolean expressions: 	\>$be, \neg\,be, \ldots \in BExp$ \\
\\
bisimulations: 		\>${\cal S}$ \\
\\
%valences:		\>$\alpha = \{\,a, b, \ldots, \overline{a}, \overline{b}, \ldots\,\}$ \\	
%\\
%molecules: 		\>$m, m' \in {\cal M}$ \\
%\\
%ions:			\>$m = a.\,P$ \\
%\\	
%solutions:	 	\>$S = \{\!|\,P, Q, \ldots\,|\!\}$ \\
%\\
relabelling function:	\>$f, g$ \\
\\
operators: 		\>$op \in Op$ \\
\\
boolean operators: 	\>$bop \in BOp$ \\
\\
free names of a process $P$: 	\>$fn(P)$ \\
\\
bound names of a process $P$: 	\>$bn(P)$ \\
\\
names of a process $P$: \>$n(P) \stackrel{\rm def}{=} fn(P) \cup bn(P)$ 
\end{tabbing}

\newpage
\section{Agent Constructions}

\begin{tabbing}
xxxxxxxx\=xxxxxx\=xxxxxxxxxxxxxxxxxxxxxxxxxx\=xxxxxx\= \kill
Prefix:	\>	\>				\> $\prefix$ \\
	\>where $\nu_{i} ::= y(x)\;|\;\overline{y}x\;|\;\tau$ \\
	\>	\> input prefix:		\>	\> $y(x).$ \\
	\>	\> output prefix:	\>	\> $\overline{y}x.$ \\
	\>	\> silent prefix:		\>	\> $\tau.$ \\
\\
Choice over indexing set: 	\>	\>	\> $\sumofp$ \\
	\> if $I = \emptyset$, then \\
	\>	\> empty choice:		\> 	\> $\inact$ \\
	\> if $I = \{\,1, 2\,\}$, then \\
	\>	\> binary choice:       \>	\> $\binsum{P}{Q}$ \\	
	\>	\> internal choice:	\>	\> $\intsum{P}{Q}$ \\
	\>	\> external choice:	\>	\> $\extsum{P}{Q}$ \\
\\
Composition over indexing set:\> \>		\> $\productofp$ \\
	\> if $I = \emptyset$, then \\
	\>	\> empty composition:		\> 	\> $\inact$ \\
	\> if $I = \{\,1, 2\,\}$, then \\
	\>	\> binary composition:	\>	\> $\compo{P}{Q}$ \\ 
\\
Replication: 	\> 		\>		\> $\rep{P}$ \\
\\
Restriction:	\>		\>		\> $\res{a}{P}$ \\
\\
Relabelling:	\>		\>		\> $P\,[f]$ \\
\\
Parametric agent definition:	\> \>		\> $\paradef{A}{a}{P}$ \\
\\
Simultaneous substitution:	\> \>		\> $\simulsubsti{P}{Y}{X}$ \\
\\
Matching:	\>		\>		\> $\match{a}{b}{P}$ 
\end{tabbing}


\end{document}


%%% End of LaTeX Document %%%
