Pi Calculus and OGRe

John Glauert

Version A. 5th January 2001

1 Introduction

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

2 Review of π–calculus

The π–calculus appears in various syntactic forms. The presentation of semantics has also evolved.

The monadic form in [MPW89] provides very general choice, a matching construct, and parametric definitions. The simpler, more restricted, form in [Mil90] uses replication and omits choice and matching. It is sufficiently powerful to model the λ–calculus, however.

The Polyadic π–calculus in [Mil91] has guarded choice and replication. Milner shows that conditional computation may be modelled without a match operation and that parametric definitions can be (weakly) simulated by replication. Polyadic communication can be seen as syntactic sugar based on monadic communication.

Meanwhile Honda an Tokoro [HoTo91] and Boudol [Boudol] (and Glauert [Gla92]) show that the asynchronous calculus, in which processes are not guarded by output actions, has all the required power, and may be used to simulate the synchronous calculus in almost all respects.

There is increasing use of a simplified calculus which is called the Mini Asynchronous π– Calculus. This has no choice or match construct. Communication is asynchronous and a restricted form of input-guarded replication is used.

We will restrict attention to such a syntax for the π–calculus.

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

All features of the full π–calculus can be simulated by the mini asynchronous π–calculus, except perhaps the general choice construct which does not seem to be of interest to anyone. For example, we can provide something like the general case of replication. In the following, x ∉ 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.

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

The semantics wil be assumed to be standard for π–calculus, although since replication is always input guarded we can can remove structural equivalence rules for replication and provide 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 will use a normal definition of free names given by the function fn(N) over processes:

fn(x(y) · N) = {x} ∪ (fn(N) \ {y})
fn(! x(y) · N) = {x} ∪ (fn(N) \ {y})
fn((ν x) (N)) = fn(N) \ {x}
fn(\overline{x} v) = \{x, v\}
fn(N | N′) = fn(N) ∪ fn(N′)
fn(0) = {}

3 A Restricted Subcalculus of Mini Asynchronous π–Calculus

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

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

We will define a function dn(N) over π–calculus processes which will be used to constrain the form of π–calculus processes we allow:

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

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

Secondly, in n(n′) · N, we require that n ≠ n′ and that dn(N) ⊆ {n}. Otherwise, after performing input, the property required for a parallel composition might be violated. A consequence is that if N contains a parallel composition, all names used for input must be restricted, except for n. The requirement that n ≠ n′ can be ensured by alpha conversion of the process to n(n′′) · N{n′′/n′} where n′′ ∉ fn(n(n′) · N).

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

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

4 Simulation of π–calculus by OGRe

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

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

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

q[[x(y) · N]] =^{△} x : A(z⃗)
with x : A(z⃗), x! Data(y) → q[[N]]
where z⃗ =^{△} fn(N) \ {y}
if  dn(N) = {x}
q[[x(y) · N]] =^{△} x : A(z⃗)
with x : A(z⃗), x! Data(y) → x : Dead, q[[N]]
where z⃗ =^{△} fn(N) \ {y}
if  dn(N) = {}
q[[! x(y) · N]] =^{△} x : A(z⃗)
with x : A(z⃗), x! Data(y) → x : A(z⃗), q[[N]]
where z⃗ =^{△} fn(N) \ {y}
q[[\overline{x} v]] =^{△} x! Data(v)
q[[(ν x) (N)]] =^{△} q[[N]]
if  x ∈ dn(N)
q[[(ν x) (N)]] =^{△} x : Dead, q[[N]]
if  x ∉ dn(N)
q[[N | N′]] =^{△} q[[N]], q[[N′]]
q[[0]] =^{△}

An OGRe agent with agent term symbol Dead will ignore any further messages. This models a π–calculus process in which output actions on a name find no process which has an input action for the name. The two rules for x(y) · N distinguish the case where N continues to take input on x and where it does not.

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

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

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

When translating a complete π–calculus process we must account for names that are free in the process. We assume that restrictions are added so that the whole process has no free names and then translate using the function p below:

p[[N]] =^{△} x : Start, x! P OMT rigger → x : Start, q[[N]]

where fn(N) = {} and x does not occur in N. The result is a set of OGRe rules that are executed in the normal way by creating an initial expression of the form x : Start, x! P OMT rigger.

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

The following example shows translation of the process R = (x(y) · P | \overline{x} v) where fn(P) = \{y\}. Note that dn(R) = {x}. We add restrictions for x and v which are free names so we translate (ν x) ((ν v) (R)):

p[[(ν x) ((ν v) (x(y) · P | \overline{x} v))]];
=^{△} x : Start, x! P OMT rigger → x : Start, q[[(ν x) ((ν v) (x(y) · P | \overline{x} v))]];
=^{△} x : Start, x! P OMT rigger → x : Start, q[[(ν v) (x(y) · P | \overline{x} v)]];
=^{△} x : Start, x! P OMT rigger → x : Start, v : Dead, q[[x(y) · P | \overline{x} v]];
=^{△} x : Start, x! P OMT rigger → x : Start, v : Dead, q[[x(y) · P]], q[[\overline{x} v]];
=^{△} x : Start, x! P OMT rigger → x : Start, v : Dead, x : A, q[[\overline{x} v]];
x : A, x! Data(y) → x : Dead, q[[P]];
=^{△} x : Start, x! P OMT rigger → x : Start, v : Dead, x : A, x! Data(v);
x : A, x! Data(y) → x : Dead, q[[P]];

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

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

References

[Boudol] G. Boudol

[Gla92] J.R.W. Glauert: Asynchronous Mobile Processes and Graph Rewriting, Proc PARLE’92. LNCS 605. June 1992. (1992)

[HoTo91] K. Honda & M. Tokoro: An object calculus for asynchronous communication. Proc. ECOOP’91, Geneva, July 1991.

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

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

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