A ν–Notation for Process Calculi

Jeong-Ho Lee

School of Information Systems University of East Anglia Norwich NR4 7TJ, UK Tel: +44 603 593213 Fax: +44 603 507720 jhl@sys.uea.ac.uk

July, 1994

Abstract

This paper addresses the need for notational unification across different theories of communicating and concurrent systems. We present a ν–notation, an unified notation for various process calculi. Using the ν–notation we show that we can redefine the syntax and semantics for each process calculus, such as CCS [Mil80], TCCS (for Testing CCS) [DNH87], the π–calculus [MPW89], [Mil90], LCCS (for Label passing CCS) [Leth91], and the polyadic π–calculus [Mil91], in order to achieve notational unification on process calculi.

1 Introduction

Since Milner developed CCS [Mil80], many theories of communicating and concurrent systems have been developed, for example, CCS [Mil80], CSP [Hoa85], ECCS [EnN86], TCCS [DNH87], CHOCS [Tho89], [Tho90], the Cham (for Chemical Abstract Machine) [BeBo90], the π–calculus [MPW89], [Mil90], LCCS [Leth91], the polyadic π–calculus [Mil91], the object–calculus [?], 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 ν–notation, an unified notation, which will be used to redefine the syntax and the operational semantics for process calculi. We show that the ν–notation can be used to redefine the syntax and semantics for every process calculus in order to achieve notational unification on process calculi. Although the ν–notation 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 π–calculus, LCCS, and the polyadic π–calculus only. We, however, believe that the ν–notation 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 ν–notation. 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 ν–notation. 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.

2 A ν–Notation

We present a ν–notation, an unified notation for process calculi, based mainly upon the π– calculus [MPW89]. 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.

2.1 ν–Notation for Syntax

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

P ::= ∑_{i∈I} ν_{i}. P | ∑_{i∈I} P_{i} | (P | Q) | ∗ P | (ν x) P | P [f] | [x = y] P | A (x⃗)

where

∑_{i∈I} ν_{i}. ::= y(x). | \overline{y}x. | y(x⃗) | \overline{y}x⃗. | τ.
∑_{i∈I} P_{i} ::= 0 | P + Q | P ⊕ Q | P + Q

P ::= y(x). P The monadic input agent y(x). P receives a name z at port y and then behaves like 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(x⃗). P The polyadic input agent y(x⃗). P receives a name vector z at port y and then behaves like P {z⃗/x⃗}.

P ::= \overline{y}x⃗. P The polyadic output agent \overline{y}x⃗. P sends the name vector x⃗ at port \overline{y} and then behaves like P.

P ::= τ. P The silent agent τ. P performs the silent action and then behaves like P.

P ::= 0 The inaction agent 0 performs nothing.

P ::= P + Q The binary choice agent P + Q behaves like P or Q, but not both. This choice includes both internal choice and external choice.

P ::= P ⊕ Q The internal choice agent P ⊕ Q non-deterministically chooses a component.

P ::= P + Q The external choice agent P + Q performs internal actions freely and also communicates to the environment.

P ::= P | Q The parallel composition agent P | Q may act independently, but may also communicate.

P ::= ∗P The replication agent ∗P stands for P | P | …, as many concurrent instances of P as you please.

P ::= (ν x) P The restriction agent (ν 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 ::= [x = y] P The matching agent [x = y] P behaves like P if x = y, otherwise like 0.

P ::= A (x⃗) The defined agent A (x⃗) is a constant, and gives a meaning of agent P such that A (x⃗) =^{def} P.

Note that parentheses used in the input prefix and the restriction indicate the binding occurrence of a variable. Hence in the ν–notation there are two binding operators: the input prefix y(x) and the restriction (νx).

2.2 ν–Notation for Semantics

Our semantics of the ν–notation for process calculi is given as a set inference rules on processes in Plotkin’s structural operational semantics style [Plo81], 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 ≡ over P and the reduction rules in the subsequent sections.

2.2.1 Structural Congruence

We let fn(P) be the free names of a process P, and bn(P) the bound names of a process P. We also let n(P) be the names of a process P, where n(P) =^{def} fn(P) ∪ bn(P).

The structural congruence relation ≡ is the smallest congruence relation over set of processes P satisfying the following properties:

1. P ≡ Q if P is α–convertible to Q.

2. (P/ ≡, |, 0) is a symmetric monoid.

3. (P/ ≡, +, 0) is a symmetric monoid.

4. (P/ ≡, ⊕, 0) is a symmetric monoid.

5. (P/ ≡, +, 0) is a symmetric monoid.

6. ∗P ≡ P | ∗P.

7. (ν x) 0 ≡ 0, (ν x)(ν y)P ≡ (ν y)(ν x)P.

8. If x ∉ fn(P) then (ν x)(P | Q) ≡ P | (ν x)Q.

9. If x⃗ ≠ y⃗ then (ν y⃗)x⃗.P ≡ x⃗.(ν y⃗)P

10. (ν x⃗)(ν y⃗)P ≡ (ν y⃗)(ν x⃗)P, (ν x⃗)(ν x⃗)P ≡ (ν x⃗)P

2.2.2 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 reduction relation → over processes is the least relation satisfying the following rules: COMM_{1} : y(x). P | \overline{y}z. Q → P \{z/x\} | Q COMM_{2} : (⋯ + y(x⃗). P) | (⋯ + (ν w⃗) (\overline{y}z⃗. Q)) → (ν w⃗) (P \{z⃗/x⃗\} | Q)

P AR : \frac{P → P′}{P | Q → P′ | Q}

BINSUM: \frac{P → P′}{P + Q → P′ + Q}

INT SUM: P ⊕ Q → P

EXT SUM: \frac{P → P′}{P + Q → P′ + Q}

RES : \frac{P → P′}{(ν x) P → (ν x) P′}

REL : \frac{P → P′}{P [f] → P′[f]}

MAT CH : \frac{P → P′}{[x = x] P → P′}

IDENT : \frac{P \{x⃗/y⃗\} → P′}{A(x⃗) → P′} A (y⃗) =^{def} P

CLOSE : \frac{P →^{\overline{y}(x)} P′ Q →^{y(z)} Q′}{P | Q →^{τ} (ν x)(P′ | Q′)}

OP EN : \frac{P →^{\overline{y}x} P′}{(ν x) P →^{\overline{y}(z)} P′ \{z/x\}} x ≠ y, z ∉ fn((ν x) P′)

ST RUCT : \frac{Q ≡ P P → P′ P′ ≡ Q′}{Q → Q′}

Note that the reduction rules involving the binary operator |, ⊕, and + additionally have symmetric forms.

3 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 ν–notation.

3.1 CCS

The Calculus of Communicating Systems (CCS) [Mil80] 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 [Hoa85] designed aroud the primitive of indivisible interaction.

CCS [Mil80] 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 [Mil89], 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.

3.1.1 Syntax and Semantics of CCS

Presuppose an infinite set N of names, and let x, y, z, … range over names. Presuppose also a set A of agent constants, and let A, B, C, … range over agent constants. Let P be a set of agents, and let P, Q, … range over agents. Then the syntax of CCS is defined as follows:

P ::= y(x). P | \overline{y}e. P | τ. P | ∑_{i∈I} P_{i} | (P | Q) | P \ α | P [f] | if b then P | A (x_{1}, …, x_{n})

The input agent y(x). P receives a value z assigned to x at port y and then behaves like 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 τ. P performs the silent action and then behaves like P. If I = ∅ then the summation agent ∑_{i∈I} P_{i} = 0 which means it can do nothing. If I = { 1, 2 } then ∑_{i∈I} P_{i} = P + Q which behaves like P or Q, but not both. The parallel composition agent P | Q may act independently, but may also communicate. The restriction agent P \ α behaves like P but actions are prohibited with respect to α and \overline{α}. The relabelling agent P [f] renames the ports of the agent P and then behaves like P. The conditional agent if b then P is a conditional expression. The defined agent A (x_{1}, …, x_{n}) is a constant, and gives a meaning of agent P such that A (x_{1}, …, x_{n}) =^{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 → is the smallest relation satisfying the following rules:

P RE :  \overline{α. P →^{α} P}  SUM_{j} : \begin{matrix}P_{j} & →^{α} & P′_{j} \\ ∑_{i∈I} P_{i} & →^{α} & P′_{j} \end{matrix}

COM_{1} : \frac{P →^{α} P′}{P | Q →^{α} P′ | Q} COM_{2} : \frac{Q →^{α} Q′}{P | Q →^{α} P | Q′}

COM_{3} : \begin{matrix}P →^{l} P′ & Q →^{\overline{l}} Q′ \\ P | Q & →^{τ} & P′ | Q′ \end{matrix}

RES :  \frac{P →^{α} P′}{P \ L →^{α} P′ \ L} ( α, \overline{α} ∉ L)  REL :  \frac{P →^{α} P′}{P [f] →^{f(α)} P′[f]}

CON : \frac{P →^{α} P′}{A →^{α} P′} ( A =^{def} P )

3.1.2 Redefined CCS

We present the redefined syntax and semantics of CCS using the ν–notation. The redefined syntax of CCS is:

P ::= ∑_{i∈I} ν_{i}. P | ∑_{i∈I} P_{i} | (P | Q) | (ν x) P | [x = y] P | A (x⃗)

where

∑_{i∈I} ν_{i}. ::= y(x). | \overline{y}x. | τ.
∑_{i∈I} P_{i} ::= 0 | P + Q.

Note that in CCS, the restriction is expressed by P \ x, whereas in ν–notation it is represented by (ν 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:

COMM : y(x). P | \overline{y}z. Q → P \{z/x\} | Q

P AR : \frac{P → P′}{P | Q → P′ | Q}

BINSUM: \frac{P → P′}{P + Q → P′ + Q}

RES : \frac{P → P′}{(ν x) P → (ν x) P′}

REL : \frac{P → P′}{P [f] → P′[f]}

IDENT : \frac{P \{x⃗/y⃗\} → P′}{A(x⃗) → P′} A (y⃗) =^{def} P

ST RUCT : \frac{Q ≡ P P → P′ P′ ≡ Q′}{Q → Q′}

3.2 TCCS

In [DNH87], De Nicola and Hennesy show that the semantic equivalences used in [Mil80] 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 τ actions is hard to describe. They argue that if they are internal and invisible, there should be no need for τ to represent internal actions in the process calculi. Thus they suggest that the choice operator + and the combinator τ is replaced with [] and ⊕, 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.

3.2.1 Syntax and Semantics of TCCS

The syntax of TCCS is:

p ::= 0 | α. p | (p | q) | p \ a | p [ϕ] | p ⊕ q | p [] q | fix_{i}(x⃗ = p⃗)

0 is an inaction. α. p performs action α and then behaves like p. (p | q) is a parallel composition. p \ a is a restriction. p [ϕ] is a relabelling, in which the relabelling operator [] takes an agent p and a relabelling function ϕ and produces a new agent p [ϕ] which behaves like p except that all its visible actions are relabelled by ϕ. p ⊕ 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. fix_{i}(x⃗ = 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:

P RE : α. p →^{α} p

INT SUM_{1} : p ⊕ q → p INT SUM_{2} : p ⊕ q → q

EXT SUM_{1} : \frac{p → p′}{p [] q → p′ [] q} EXT SUM_{2} : \frac{p →^{α} p′}{p [] q →^{α} p′}

COM_{1} :  \frac{p → p′}{p | q → p′ | q}  COM_{2} :  \frac{p →^{α} p′}{p | q →^{α} p′ | q}

COM_{3} : \frac{p →^{α} p′ q →^{\overline{α}} q′}{p | q → p′ | q′}

RES_{1} :  \frac{p → p′}{p \ a → p′ \ a}  RES_{2} :  \frac{p →^{α} p′}{p \ a →^{α} p′ \ a} α ∉ \{ a, \overline{a} \}

REL_{1} :  \frac{p → p′}{p [ϕ] → p′ [ϕ]}  REL_{2} :  \frac{p →^{α} p′}{p [ϕ] →^{ϕ(α)} p′ [ϕ]}

F IX : fix_{i}(x⃗ = p⃗) → p_{i} [fi⃗x(x⃗ = p⃗) / x⃗]

3.2.2 Redefined TCCS

The redefined syntax of TCCS is:

P ::= ∑_{i∈I} ν_{i}. P | ∑_{i∈I} P_{i} | (P | Q) | (ν a) P | ∗ P | P [f]

where

∑_{i∈I} P_{i} ::= 0 | P ⊕ Q | P + Q.

The redefined semantics for TCCS is:

COMM : y(x). P | \overline{y}z. Q → P \{z/x\} | Q

P AR : \frac{P → P′}{P | Q → P′ | Q}

INT SUM: P ⊕ Q → P′

EXT SUM: \frac{P → P′}{P + Q → P′ + Q}

RES : \frac{P → P′}{(ν x) P → (ν x) P′}

REL : \frac{P → P′}{P [f] → P′[f]}

ST RUCT : \frac{Q ≡ P P → P′ P′ ≡ Q′}{Q → Q′}

3.3 TCCS Cham

Chemical Abstract Machine [BeBo90], which originated in the Γ language of Banâtre and Le Metayer [BLM86], is designed to model asynchronous concurrent computations. By means of handling the operational semantics of various process calculi and concurrent λ–calculus, Berry and Boudol show that Cham has the power of classical process calculi and behaves as concurrent generalisations of the λ–calculus. In [BeBo90], they handle the subset of CCS, such as CCS^{−} and TCCS [DNH87], and a concurrent λ–calculus, γ–calculus [Bou89]. 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.

3.3.1 Syntax and Semantics of TCCS Cham

The syntax of the TCCS Cham is:

Agents:

p ::= 0 | α. p | (p | q) | p \ a | p [ϕ] | p ⊕ q | p [] q | fix_{i}(x⃗ = p⃗)

Molecules:

m ::= P | α. m | (ν a) m | m [f] | S | m ◁ S | < m, m > | l :< m, m > | r :< m, m >

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

parallel: p | q ⇀ ↽ p, q

reaction: a.m, \overline{a}.n → m, n

restriction membranes: m \ a ⇀ ↽ {| m |} \ a

restriction ion: (α.m) \ a ⇀ ↽ α.(m \ a) if α ∉ \{ a, \overline{a} \}

relabelling membranes: m [ϕ] ⇀ ↽ {| m |} [ϕ]

relabelling ion: (α.m) [ϕ] ⇀ ↽ ϕ(α).(m [ϕ])

⊕–left: p ⊕ q → p ⊕–right: p ⊕ q → q []–expansion: p [] q ⇀ ↽ < {| p |}, {| q |} > left []–ion: < {| α.m |}, S > ⇀ α.l : < m, S > right []–ion: < S, {| α.m |} > ⇀ α.r : < S, m > left projection: l : < m, m′ > ⇀ m right projection: r : < m, m′ > ⇀ m′ fixpoint: fix_{i}(x⃗ = p⃗) ⇀ p_{i}[fi⃗x(x⃗ = p⃗) \ x⃗] inaction cleanup: 0 ⇀ restriction cleanup: {| |} \ a ⇀ relabelling cleanup: {| |} [ϕ] ⇀ 3.3.2 Redefined Syntax and Semantics of TCCS Cham The redefined syntax of the TCCS Cham is: Agents:

p ::= ∑_{i∈I} ν_{i}. P | ∑_{i∈I} P_{i} | (p | q) | (ν a) P | ∗ P | p [ϕ]

where

∑_{i∈I} P_{i} ::= 0 | P ⊕ Q | P + Q.

Molecules:

m ::= P | α. m | (ν a) m | m [f] | S | m ◁ S | < m, m > | l :< m, m > | r :< m, m >

The redefined rules of the TCCS Cham is: parallel: P | Q ⇀ ↽ P, Q reaction: a.m, \overline{a}.n → m, n restriction membranes: (ν a) m; ⇀ ↽ (ν a) {| m |} restriction ion: (ν a) (α.m) ⇀ ↽ α.((ν a) m) if α ∉ \{ a, \overline{a} \} relabelling membranes: m [ϕ] ⇀ ↽ {| m |} [ϕ] relabelling ion: (α.m) [ϕ] ⇀ ↽ ϕ(α).(m [ϕ])

⊕–left: P ⊕ Q → P

⊕–right: P ⊕ Q → Q

[]–expansion: P [] Q ⇀ ↽ < {| P |}, {| Q |} >

left []–ion: < {| α.m |}, S > ⇀ α.l : < m, S >

right []–ion: < S, {| α.m |} > ⇀ α.r : < S, m >

left projection: l : < m, m′ > ⇀ m

right projection: r : < m, m′ > ⇀ m′

fixpoint: ∗P ⇀ P | ∗ P

inaction cleanup: 0 ⇀

restriction cleanup: (ν a) {| |} ⇀

relabelling cleanup: {| |} [ϕ] ⇀

3.4 π–Calculus

The π–calculus [MPW89], based on ECCS [EnN86] 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 π–calculus, 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: names and agents.

3.4.1 Syntax and Semantics of the π–Calculus

Suppose N be an infinite set of names, and let x, y, z, … ∈ N. Suppose also A be a set of agent identifiers, and let A, B, C, … ∈ A. Now let P be a set of processes, and let P, Q, R, … ∈ P. Then the syntax of the π–calculus may be defined as follows:

P ::= 0 | P + Q | \overline{y}x. P | y(x). P | τ. P | (P | Q) | (x) P | [x = y] P | A (y_{1}, …, y_{n})

0 means inaction which can do nothing. P + Q behaves like P or Q, but not both. 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 P {z/x}. τ. 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}. [x = y] P behaves like P if x = y, otherwise like 0. For any agent identifier A, there must be a unique defining equation A (x_{1}, …, x_{n}) =^{def} P, where the names x_{1}, ldots, x_{n} are distinct and are the only names which may occur free in P. The A (y_{1}, …, y_{n}) behaves like P { y_{1}/x_{1}, …, y_{n}/x_{n} }. This syntactic substitution replaces CCS relabelling operation.

Note that in [Mil90], τ. P, [x = y] P, P + Q, and A (y_{1}, …, y_{n}) have been omitted, but replication !P is added.

In order to define P in head normal form, a bound output action is defined as follows:

\overline{y}(x). P = (x)\overline{y}x. P if x ≠ y.

Therefore there are four kinds of action α in the π–calculus as follows:

• The silent action τ: P →^{τ} Q means that without interaction with the environment P evolves to Q.

• A free output action \overline{y}x: P →^{\overline{y}x} Q means that P sends the name x at port \overline{y}.

• A bound output action \overline{y}(x): 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.

• An input action y(x): P →^{y(x)} Q receives a name z at port y and then evolves to Q {z/x}.

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 π–calculus (y) is a reference to the place where the received name occurs.

The operational semantics for the π–calculus is defined by the reduction rules, in which the rules associated with τ–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 → is the smallest relation satisfying:

T AU : \overline{P →^{τ} P}

INP UT : \overline{y(x). P →^{y(z)} P \{z/x\}} z ∉ fn((x)P)

OUT P UT : \overline{\overline{y}x. P →^{\overline{y}x} P}

COMM : \frac{P →^{\overline{y}x} P′ Q →^{y(x)} Q′}{P | Q →^{τ} P′ | Q′ \{x/Z\}}

P AR : \frac{P →^{α} P′}{P | Q →^{α} P′ | Q} bn(α) ∩ fn(Q) = ∅

SUM : \frac{P →^{α} P′}{P + Q →^{α} P′}

RES : \frac{P →^{α} P′}{(y) P →^{α} (y) P′} y ∉ n(α)

MAT CH : \frac{P →^{α} P′}{[x = x] P →^{α} P′}

IDENT : \begin{matrix}P \{x⃗/y⃗\} & →^{α} & P′ \\ A(x⃗) & →^{α} & P′ \end{matrix} A (y⃗) =^{def} P

CLOSE : \frac{P →^{\overline{y}(x)} P′ Q →^{y(z)} Q′}{P | Q →^{τ} (x)(P′ | Q′)}

OP EN : \frac{P →^{\overline{y}x} P′}{(x) P →^{\overline{y}(z)} P′ \{z/x\}} x ≠ y, z ∉ fn((x) P′)

However, inspired by Berry and Boudol [BeBo90], Milner [Mil90] defined a structural congruence relation over terms to simplify the form of the reduction rules. Structural congruence ≡ is the smallest congruence over the set of processes P satisfying these equations:

1. P ≡ Q whenever P is α-convertible to Q

2. (P/ ≡, |, 0) is a symmetric monoid

3. !P ≡ P |!P

4. (x)0 ≡ 0, (x)(y)P ≡ (y)(x)P

5. (x)(P | Q) ≡ P | (x)Q x ∉ fn(P)

The operational semantics of the π–calculus in [Mil90] 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 → is the smallest relation satisfying:

COMM : y(x). P | \overline{a}y. Q → P \{y/x\} | Q

P AR : \frac{P → P′}{P | Q → P′ | Q}

RES : \frac{P → P′}{(y)P → (y)P′}

ST RUCT : \frac{Q ≡ P P → P′ P′ ≡ Q′}{Q → Q′}

3.4.2 Redefined π–Calculus

The redefined syntax of the π–calculus is:

P ::= ∑_{i∈I} ν_{i}. P | ∑_{i∈I} P_{i} | (P | Q) | (ν x) P | [x = y] P | A (y_{1}, …, y_{n})

where

∑_{i∈I} ν_{i}. ::= y(x). | \overline{y}x. | τ.
∑_{i∈I} P_{i} ::= 0 | P + Q.

Because the structural congruence has interesting features including the power of simplification, we redefine the operational semantics for the π–calculus according to the [Mil90] which uses the structural congruence relation to define the operational semantics:

COMM : y(x). P | \overline{y}z. Q → P \{z/x\} | Q

P AR : \frac{P → P′}{P | Q → P′ | Q}

BINSUM : \frac{P → P′}{P + Q → P′}

RES : \frac{P → P′}{(ν x) P → (ν x) P′}

MAT CH : \frac{P → P′}{[x = x] P → P′}

IDENT : \frac{P \{x⃗/y⃗\} → P′}{A(x⃗) → P′} A (y⃗) =^{def} P

CLOSE : \frac{P →^{\overline{y}(x)} P′ Q →^{y(z)} Q′}{P | Q →^{τ} (ν x)(P′ | Q′)}

OP EN : \frac{P →^{\overline{y}x} P′}{(ν x) P →^{\overline{y}(z)} P′ \{z/x\}} x ≠ y, z ∉ fn((ν x) P′)

ST RUCT : \frac{Q ≡ P P → P′ P′ ≡ Q′}{Q → Q′}

3.5 LCCS

In [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.

3.5.1 Syntax and Semantics of LCCS

The syntax of LCCS is:

P ::= nil | l?x. P | l!l′. P | P + P′ | P ⊕ P′ | P | P′ | P \ α | recX. P

                 | X | if b then P else P′

l ::= x | α
b ::= true | l = l′ | b ∧ b′ | ¬b

where

x ∈ V ar; α ∈ Labels; X ∈ V AR; b ∈ BExp.

nil means the inaction. l?x. P receives the name y at port l and then behaves like P {y/X}. l!l′. P sends the name l′ at port l and then behaves like P. P + P′ is the external choice between P and P′ by communication with a user. P ⊕ P′ is the internal choice between P and P′ by the system. P | P′ may act independently, but they may also communicate. P \ α behaves like P but actions are prohibited at port α and \overline{α}. recX. P is the recursive process P. X is a bound variable and can be renamed without any semantic effect. if b then P else P′ is a conditional in which if b is true then P is activated, otherwise P′ is activated.

As the choice problem has been addressed in [DNH87], to overcome the different interpretations of the binary choice +, Leth has used two new distinct operators; external choice + and internal choice ⊕. LCCS does not include the syntactical construct τ. P, but allow τ 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:

INP UT : α?x. P →^{α?x} P

OUT P UT : α!β. P →^{α!β} P

COMM : \begin{matrix}P_{1} →^{α?x} P′_{1} & P_{2} →^{α!β} P′_{2} \\ P_{1} | P_{2} & →^{τ} & P′_{1} \{β/x\} | P′_{2} \end{matrix}

P AR : \begin{matrix}P_{1} & →^{Γ} & P′_{1} \\ P_{1} | P_{2} & →^{Γ} & P′_{1} | P_{2} \end{matrix}

INT SUM_{1} : P_{1} ⊕ P_{2} →^{τ} P_{1}

INT SUM_{2} : P_{1} ⊕ P_{2} →^{τ} P_{2}

EXT SUM_{1} : \begin{matrix}P_{1} & →^{Γ} & P′_{1} \\ P_{1} + P_{2} & →^{Γ} & P′_{1} \end{matrix} Γ ≠ τ

EXT SUM_{2} : \begin{matrix}P_{1} & →^{τ} & P′_{1} \\ P_{1} + P_{2} & →^{τ} & P′_{1} + P_{2} \end{matrix}

RES : \frac{P →^{Γ} P′}{P \ α →^{Γ} P′ \ α} if α ∉ sort(Γ)

COND_{1} :  P_{1} →^{Γ} P′_{1} ; iftruethen P_{1} else P_{2} →^{Γ} P′_{1}

COND_{2} :  P_{1} →^{Γ} P′_{1} ; iffalsethen P_{1} else P_{2} →^{Γ} P′_{2}

REC : recX. P →^{τ} P [recX.P/X]

IMP ORT : \begin{matrix}P_{1} →^{α?x} P′_{1} & P_{2} →^{α!\β} P′_{2} \\ P_{1} | P_{2} & →^{τ} & (P′_{1} \{γ/x\} | P′_{2} \{γ/β\}) \ γ \end{matrix} γ ∉ sort(P′_{1}) ∪ sort(P′_{2} \ β)

EXP ORT : \frac{P →^{α!β} P′}{P \ β →^{α!\β} P′} if α ≠ β

where

Γ = { α?x, α!β, τ, α!\β }
α, β ∈ L; x ∈ V ar.

Notice that α!\β is a bound output action as defined in [MPW89].

Note also that IMPORT and EXPORT rules correspod to the Scope Closing and Scope Opening rules in [MPW89], 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.

3.5.2 Redefined LCCS

The redefined syntax of LCCS is:

P ::= ∑_{i∈I} ν_{i}. P | ∑_{i∈I} P_{i} | P | P′ | (ν x) P | ∗ P | [x = y] P

where

∑_{i∈I} ν_{i}. ::= y(x). | \overline{y}x.
∑_{i∈I} P_{i} ::= 0 | P ⊕ P′ | P + P′.

Note that replication replaces recursion without losing its meaning.

The redefined operational semantics of LCCS is:

COMM : y(x). P | \overline{y}z. Q → P \{z/x\} | Q

P AR : \frac{P → P′}{P | Q → P′ | Q}

INT SUM : P ⊕ Q → P

EXT SUM : \frac{P → P′}{P + Q → P′ + Q}

RES : \frac{P → P′}{(ν x) P → (ν x) P′}

MAT CH : \frac{P → P′}{[x = x] P → P′}

CLOSE : \frac{P →^{\overline{y}(x)} P′ Q →^{y(z)} Q′}{P | Q →^{τ} (ν x)(P′ | Q′)}

OP EN : \frac{P →^{\overline{y}x} P′}{(ν x) P →^{\overline{y}(z)} P′ \{z/x\}} x ≠ y, z ∉ fn((ν x) P′)

ST RUCT : \frac{Q ≡ P P → P′ P′ ≡ Q′}{Q → Q′}

3.6 Polyadic π–Calculus

The polyadic π–calculus [Mil91] is a polyadic version of the π–calculus, which is a model of concurrent computation based on the notion of naming.

3.6.1 Syntax and Semantics of the Polyadic π–Calculus

We presuppose N be a set of names, and let α, β, … ranged over names and co–names. We also presuppose x⃗, y⃗, … be vectors of names, with length |x⃗|, |y⃗|, . . ..

The syntax of the polyadic π–calculus is:

Normalprocesses : N ::= α. A | 0 | M + N
P rocesses : P ::= N | (P | Q) | !P | (ν x) P
Abstractions : F ::= P | (λ x) F | (ν x) F
Concretions : C ::= P | [x] C | (ν x) C
Agents : A ::= F | C

The structural congruence ≡ is the smallest congruence relation over set of processes P such that the following rules hold:

1. Processes are identified if they only differ by a change of bound names 2. (N / ≡, +, 0) is a symmetric monoid

3. (P/ ≡, |, 0) is a symmetric monoid

4. !P ≡ P |!P

5. (ν x) 0 ≡ 0, (ν x)(ν y)P ≡ (ν y)(ν x)P

6. If x ∉ fn(P) then (ν x)(P | Q) ≡ P | (ν x)Q

7. (ν y)(λ x)F ≡ (λ x)(ν y)F (x ≠ y)

8. (ν y)[x] C ≡ [x](ν y)C (x ≠ y)

9. (ν x)(ν y)A ≡ (ν y)(ν x)A, (ν x)(ν x)A ≡ (ν x)A

The rules are associated with Communication, Parallel Composition, Restriction, Structural Congruence are indicated by COMM, PAR, RES, and STRUCT, respectively. The reduction relation → over processes is the least relation satisfying the following rules: COMM : (⋯ + x. F) | (⋯ + \overline{x}. C) → F • C

P AR : \frac{P → P′}{P | Q → P′ | Q}

RES : \frac{P → P′}{(ν x) P → (ν x) P′}

ST RUCT : \frac{Q ≡ P P → P′ P′ ≡ Q′}{Q → Q′}

where standard form of abstraction F ≡ (λx⃗) P standard form of concretion C ≡ (νz⃗)[y⃗] Q (z⃗ ⊆ y⃗) pseudo-application F • C =^{def} (νz⃗)(P {y⃗/x⃗} | Q)

3.6.2 Redefined Polyadic π–Calculus The redefined syntax of the polyadic π–calculus is:

P ::= ∑_{i∈I} ν_{i}. P | ∑_{i∈I} P_{i} | (P | Q) | ∗ P | (ν x⃗) P

where ∑_{i∈I} ν_{i}. ::= y(x). | \overline{y}x. | y(x⃗) | \overline{y}x⃗.

∑_{i∈I} P_{i} ::= 0 | P + Q

y(x⃗).P =^{def} y.(λ x⃗) P

\overline{y}x⃗.P =^{def} \overline{y}.[x⃗] P

x⃗ = x_{1}, x_{2}, …, x_{n}

We now should redefine the structural congruence relation ≡, which is the smallest relation over set of processes P satisfying:

1. P ≡ Q if P is α–convertible to Q.

2. (P/ ≡, +, 0) is a symmetric monoid.

3. (P/ ≡, |, 0) is a symmetric monoid.

4. ∗P ≡ P | ∗P

5. (ν x⃗) 0 ≡ 0, (ν x⃗)(ν y⃗)P ≡ (ν y⃗)(ν x⃗)P

6. If x ∉ fn(P) then (ν x⃗)(P | Q) ≡ P | (ν x⃗)Q

7. If x⃗ ≠ y⃗ then (ν y⃗)x⃗.P ≡ x⃗.(ν y⃗)P

8. (ν x⃗)(ν y⃗)P ≡ (ν y⃗)(ν x⃗)P, (ν x⃗)(ν x⃗)P ≡ (ν x⃗)P

Hence the redefined operational semantics for the polyadic π–calculus is: COMM : (⋯ + y(x⃗). P) | (⋯ + (ν w⃗) (\overline{y}z⃗. Q)) → (ν w⃗) (P \{z⃗/x⃗\} | Q)

P AR : \frac{P → P′}{P | Q → P′ | Q}

BINSUM : \frac{P → P′}{P + Q → P′}

RES : \frac{P → P′}{(ν x) P → (ν x) P′}

ST RUCT : \frac{Q ≡ P P → P′ P′ ≡ Q′}{Q → Q′}

4 Conclusions

We showed that the ν–notation can express all the process calculi without sacrificing their concepts. We also showed that the ν–notation can be used to represent any kinds of process calculi, even though we restricted ourselves to redefining syntax and semantics of CCS, TCCS, the π–calculus, LCCS, and the polyadic π–calculus 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 [HoT91], [Gla92], etc.

References

[BLM86] J-P. Banâtre and D. Le Metayer: A New Computational Model and Its Discipline of Programming, Technical Report INRIA Report 566, 1986.

[BeBo90] G. Berry and G. Boudol: The Chemical Abstract Machine, Proceedings of POPL ’90, p 81-94, ACM, 1990. Also in Theoretical Computer Science, no.96, pp. 217–248, 1992.

[Bou89] G. Boudol: Towards a λ–Calculus for concurrent and communicating systems, Proceedings of TAPSOFT ’89, LNCS 351, pp. 149–161, Springer-Verlag, 1989.

[DNH87] R. De Nicola and M. Hennessy: CCS without τ’s, Proceedings of TAPSOFT ’87, LNCS 249, pp. 138–152, Springer-Verlag, 1987.

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

[Gla92] J. Glauert: Asynchronous Mobile Processes and Rewriting, Proceedings of PARLE ’92, LNCS 605, pp.63–78, Springer-Verlag, 1992.

[Hoa85] C.A.R. Hoare: Communicating Sequential Processes, Prentice Hall, 1985.

[HoT91] K. Honda and M. Tokoro: An Object Calculus for Asynchronous Communication, Proceedings of ECOOP’91, LNCS, pp. , Springer-Verlag, 1991.

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

[Mil80] R. Milner: A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, 1980.

[Mil89] R. Milner: Communication and Concurrency, Prentice Hall, 1989.

[MPW89] R. Milner, J. Parrow, & D. Walker: 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.

[Mil90] R. Milner: Functions as Processes, Automata, Languages, and Programming. LNCS 443, pp. 167–180, Springer-Verlag, 1990. Also in Technical Report INRIA Sophia Antipolis, June 1989.

[Mil91] R. Milner: The Polyadic π–Calculus: A Tutorial, Technical Report ECS-LFCS-91-180, Edinburgh University, October 1991.

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

[Tho89] B. Thomsen: A Calculus of Higher Order Communicating Systems, Proceedings of POPL 89, pp. 143–154, ACM, 1989.

[Tho90] B. Thomsen: Calculi for Higher Order Communicating Systems, Ph.D. Thesis, Department of Computing, Imperial College, 1990.

Appendices

A Entities

processes: P, Q, … ∈ P normal processes: M, N, … ∈ N P names: x, y, … ∈ N co–names: \overline{x}, \overline{y}, … ∈ \overline{N} name vectors: x⃗, y⃗, … ∈ N⃗ labels: l, l′, … ∈ L agent identifiers: A, B, … ∈ A agent variables: X, Y, … ∈ VAR actions: α, β, … ∈ Act action sequences: α∗, β∗, … ∈ Act^{∗} finite index sets: I, J (i, j, … ∈ I) boolean expressions: be, ¬ be, … ∈ BExp bisimulations: S relabelling function: f, g operators: op ∈ Op boolean operators: bop ∈ BOp free names of a process P: fn(P) bound names of a process P: bn(P) names of a process P: n(P) =^{def} fn(P) ∪ bn(P)

B Agent Constructions

Prefix: ∑_{i∈I} ν_{i}.

where ν_{i} ::= y(x) | \overline{y}x | τ input prefix: y(x). output prefix: \overline{y}x. silent prefix: τ.

Choice over indexing set: ∑_{i∈I} P_{i}

if I = ∅, then

empty choice: 0 if I = { 1, 2 }, then

binary choice: P + Q internal choice: P ⊕ Q external choice: P + Q

Composition over indexing set: ∏_{i∈I} P_{i}

if I = ∅, then

empty composition: 0 if I = { 1, 2 }, then

binary composition: P | Q

Replication: ∗P Restriction: (ν a) P Relabelling: P [f] Parametric agent definition: A (a⃗) =^{def} P Simultaneous substitution: P {Y⃗ /X⃗} Matching: [a = b] P