Replication

John Glauert, and Jeong-Ho Lee

Version A. 13th September 1995

1 Introduction

This document discusses the use of replication in the π–calculus and its translation to OGRe and hence to π^{π}–calculus.

2 Varieties of π–Calculi

The base calculus we will use is for the π–calculus with multiple communications, but without sums, using syntax:

N ::= x(y⃗) · N | \overline{x} v⃗ · N | (ν x) (N) | N | N′ | 0 | ! N

In the discussion on π^{π}–calculus we have assumed that agent definitions take the place of replication:

N ::= x(y⃗) · N | \overline{x} v⃗ · N | (ν x) (N) | N | N′ | 0 | A(y⃗) | N where A(y⃗) = N′

We can provide a crude translation of ! P as:

! P ≡ A(n_{P}) where A(n_{P}) = (P | A(n_{P}))

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 ! x(y⃗) · P. If we use n_{P xy} to stand for fn(P)\{x, y} then we can represent the replication as:

! x(y⃗) · P ≡ A(x, n_{P xy}) where A(x, n_{P xy}) = x(y⃗) · (P | A(x, n_{P xy}))

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 π–calculus, but to restrict replication to the input guarded form:

N ::= x(y⃗) · N | \overline{x} v⃗ · N | (ν x) (N) | N | N′ | 0 | ! x(y⃗) · N

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:

\overline{x} v⃗ · P | x(y⃗) · Q → P | Q\{v⃗/y⃗\}
\overline{x} v⃗ · P |! x(y⃗) · Q → P | Q\{v⃗/y⃗\} |! x(y⃗) · Q

We can provide something like the general case of replication. In the following, x ∉ fn(P):

Q = (ν x) (\overline{x} |! x() · (P | \overline{x})) ≈ ! P

Q becomes, by a τ step,

(ν x) (P | \overline{x} |! x() · (P | \overline{x}))
≅ P | (ν x) (\overline{x} |! x() · (P | \overline{x}))
= P | Q

So it seems that Q is weakly bisimilar to ! P using standard π–calculus semantics.

3 Simulation of π–calculus 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 PiSky Version K for more background.

N ::= x(y⃗) · N | \overline{x} v⃗ · N | (ν x) (N) | N | N′ | 0 | ! x(y⃗) · N

The function q maps π–calculus processes to OGRe processes:

q[[\overline{x} v⃗ · N]] = m : B(n_{N}), n! P ut(V ec_{k}(v⃗), m)
where  m : B(n_{N}), m! Sync → m : Dead, q[[N]]
q[[\overline{x} v⃗]] = n! AP ut(V ec_{k}(v⃗))
q[[x(y⃗) · N]] = m : A(n_{Ny}), x! Get(m)
where  m : A(n_{Ny}), m! Data(V ec_{k}(y⃗)) → m : Dead, q[[N]]
q[[! x(y⃗) · N]] = m : A(x, n_{Nxy}), x! Get(m)
where  m : A(x, n_{Nxy}), m! Data(V ec_{k}(y⃗)) → m : A(x, n_{Nxy}), x! Get(m), q[[N]]
q[[(ν n) (N)]] = n : Chan(EQ), q[[N]]
q[[N | N′]] = q[[N]], q[[N′]]
q[[0]] =

where n_{N} = fn(N), n_{Ny} = fn(N) \ {y_{0} … y_{k}}, and n_{Nxy} = fn(N) \ {x, y_{0} … y_{k}}. V ec_{k} stands for a data constructor of the required arity for the corresponding sequence of input or output values. Hence, for v⃗ = v_{1} … v_{k}, where k ≥ 0, we use V ec_{k}(v_{1}, …, v_{k}).

We have provided rules for asynchronous π–calculus. The translation of guarded replication was also developed by Jeong Ho.

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