Syntax and Semantics of Pi in the Sky Calculus

John Glauert, Zurab Khasidashvili, Lone Leth, and Bent Thomsen

Version L. 1st December 1995

1 Changes

Version L integrates some thoughts on replication from a separate document by moving away from a π–calculus with agent definitions to one with a restricted form of replication. There is discussion of the varieties of π–calculus in use in the literature.

There is a significant change from unconditional input with a separate conditional construct to the use of conditional input. The previous forms are still available, but seen as syntactic sugar. Certain processes are made very much simpler as a result.

The history of earlier versions is in the final section.

2 Introduction

Awaits material giving proper motivation and a gentle introduction to the world of processes and messages we are considering.

The paper gives a definition of the syntax and semantics of π^{π}–calculus. We show that the notation is powerful enough to simulate the π–calculus, giving an encoding of π–calculus terms in the π^{π}–calculus. We also (will) prove that the encoding is correct. This encoding represents the names of the π–calculus, which can be though of as unbuffered communication channels, as π^{π}–calculus processes which act as mailboxes.

We (will) go on to show that any π^{π}–calculus system may be simulated using the π–calculus.

It has been demonstrated that the λ–calculus can be modelled using the π–calculus. Clearly, the π^{π}–calculus can model the λ–calculus through simulation of the corresponding π–calculus. However, a more direct translation is also presented and (will be) shown to be correct.

We (will) also give a translation of the π^{π}–calculus into Object Graph Rewriting (OGRe). OGRe is described in “Parallel Implementation through Object Graph Rewriting” by John Glauert.

The λ–calculus can be modelled in OGRe via the translation of the equivalent π^{π}–calculus term. We (will) also give a more direct translation.

3 π^{π}–Calculus Syntax

We assume a set N of names ranged over by n, m, etc. A set Σ of symbols ranged over by F, G, etc. each with an associated arity (≥ 0) giving the number of arguments it should take. These are combined in the set of terms, T ranged over by t:

T ::= n | F (t_{1}, …, t_{n}) , where arity(F) = n

P, the class of process, and S, the class of process scripts, are defined in terms of each other.

3.1 π^{π}–Calculus Processes

Parallel Processes form the class P defined by the following syntax:

P ::= n : S | n!t | νn P | P ∥ P′ | ()

n : S is a named process (the idea is similar to locations in some versions of CCS) running a script S. n!t is a message t on its way to process n. These two forms make up a π^{π}–calculus network and all computation involves the interaction of named processes and messages.

νn P denotes restriction of the name n to P. P may contain a process with name n, but the name n is bound by the restriction and is not confused with any other use of the same name in the surrounding context.

P ∥ P′ denotes parallel composition of processes, and () is the empty composition. It is assumed that P and P′ in n!t are linear wrt n : S subcomponents. This just means that named processes are unique. Rules to ensure this are given below.

3.2 π^{π}–Calculus Scripts

Process Scripts, S are given by the following syntax:

S ::= ∑_{i}?t_{i} · S_{i} | λn P | A(t_{1}, …, t_{n})

Also a set of recursive agent definitions is assumed: A(n_{1}, …, n_{k}) = S.

The intuition is that S is the sequential body of a process. An input–guarded script takes the form ∑_{i}?t_{i} · S_{i}. If a message is directed to the process and matches at least one of the patterns t_{i} then the process continues with the script given by the corresponding S_{i}. Variables in t_{i} bind over S_{i}. If more than one pattern matches, the first is taken.

Abstractions of the form λn P allow a process to generate new processes. The parent process continues to exist if there is a process named n within P. That process takes on the name of the parent and other processes in P are spawned in parallel. We will illustrate the power of the construct with some examples:

To spawn a message t directed to process n and continue with a script S we can use an abstraction λm (n!t ∥ m : S).

To spawn a new process running script S′, and continue with script S we can use an abstraction λm νn (n : S′ ∥ m : S).

More complex process networks involving numbers of messages may be created in a similar way. Abstractions also allow a process to discover its identity. The script S in the following abstraction finds n bound to its process name: λn (n : S).

To terminate a process we can invoke a definition Stop where Stop = λn (). An agent Stop with this definition is assumed to exist in the rest of the paper.

Recursive scripts are dealt with through agent definitions. { I am tempted to say that all free names in the body of the definition should appear in the head, but as long as capture of free names is prevented during substitution, I think it would be possible for free names to appear. These free names would identify processes existing in the original process configuration. } In previous versions we permitted the match construct in scripts:

[n = t : S]; S′

which tests to see if the term bound to n matches the term t. The term contains one or more symbols, and may introduce variables. The construct behaves as S if the term bound to n matches t. Names in n are bound in S by a successful match. If the match fails it behaves as S′.

This is seen as syntactic sugar in the present version. For each such match we assume a new symbol P att. Then

[n = t : S]; S′ ≡ λm (m!P att(n) ∥ m : (?P att(t) · S + ?P att(x) · S′))

where m, and x do not occur in S or S′. This script sends to itself a message which will match the first case if n is an instance of t and the second case otherwise. No other message sent to this process will use the symbol P att.

3.3 π^{π}–Calculus Syntactic Constraints

It is necessary to define concepts of free and bound names in π^{π}–calculus. We will also describe some static constraints to be obeyed by well–formed processes and scripts.

Free names of processes are given by fn(P). dn(P) identifies defining names – free names which name processes in P.

Free names of scripts are given by fn(S). Names in a term, t, are denoted by fn(t). No free names in scripts or terms are defining names.

fn(n : S) = fn(S) ∪ {n}
dn(n : S) = {n}
fn(n!t) = fn(t) ∪ {n}
dn(n!t) = {}
fn(νn P) = fn(P) \ {n}
dn(νn P) = dn(P) \ {n}
fn(P ∥ P′) = fn(P) ∪ fn(P′)
dn(P ∥ P′) = dn(P) ∪ dn(P′)
fn(()) = {}
dn(()) = {}
fn(∑_{i}?t_{i} · Si) = ⋃_{i} fn(S_{i}) \ fn(t_{i})
fn(λn P) = fn(P) \ {n}
fn(A(t_{1}, …, t_{k})) = fn(t_{1}) ∪ … ∪ fn(t_{k})

To ensure that named processes have distinct names, we need to add the constraint that dn(P)∩ dn(P′) = {} in P ∥ P′. We also want to make sure that every new process created by use of an abstraction in a script is bound by some restriction. In λn P, we require that dn(P) ⊆ {n}. Hence the only possible free named process is n which is bound in the abstraction.

For parametric definitions A(n_{1}, …, n_{k}) = S we require that fn(S) ⊆ {n_{1}, …, n_{k}}.

Note that the consequence is that no free name in a script is a defining name. Hence, such a name cannot be bound by input or matching.

One rather operational choice would be to ensure that every potential message has a process to go to. This would mean that a process could not just die by using a script like Stop. We would need a new form of script for a terminated process, say Dead, and a structural equivalence rule to garbage collect processes when the form νn (n : Dead) arises.

We would need extra constraints to say that whenever there is a restriction νn P, n ∈ dn(P). The constraint for an abstraction, λn P, would be strengthened to read dn(P) = {n}.

4 π^{π}–Calculus Semantics

A sort discipline seems necessary to ensure that if an agent definition contains n!t′ then n will be bound to a defined name when the definition is expanded.

The following structural rules define structural congruence of π^{π}–calculus processes:

νn′ νn P ≡ νn νn′ P
νn P ≡ νm P {m/n} ,  m ∉ fn(P)
νn P ∥ P′ ≡ νn (P ∥ P′) ,  n ∉ fn(P′)
νn () ≡ ()
(P ∥ P′) ∥ P′′ ≡ P ∥ (P′ ∥ P′′)
P ∥ P′ ≡ P′ ∥ P
P ∥ () ≡ P
n : A(t_{1}, …, t_{k}) ≡ n : S{t_{1}/n_{1}, …, t_{k}/n_{k}} , where A(n_{1}, …, n_{k}) = S
n : λm P ≡ P {n/m} ,  dn(P) ⊆ {m}

The final rule applies an abstraction and may involve process spawning and message creation.

The reduction semantics is given by a single reduction rule on processes P:

n!t ∥ n : ∑_{i}?t_{i} · S_{i} → n : σ_{j}(S_{j}) ,  ∃j ≤ i, σ_{j} : t = σ_{j}(t_{j}) ∧ ∀k < j, σ : t ≠ σ(t_{k})

σ is a mapping from names to terms. A message is received by process n if it has a script ready for input with a pattern matching the message. Since patterns might overlap, the earliest pattern will be chosen.

The following rules extend the reduction relation to contexts:

P → P′ ⇒ νn P → νn P′
P → P′ ⇒ P ∥ Q → P′ ∥ Q
Q ≡ P, P → P′, P′ ≡ Q′ ⇒ Q → Q′

We have not discussed the initial configuration of a process network in this calculus. If we disallow free names in agent definitions, then, without loss of generality, it could take the form νn (n : A) for some agent A of arity 0.

5 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 use such a syntax for the π–calculus, though we will consider polyadic communication and synchronous communication. Both of these extensions can be seen as syntactic sugar, but can also be simulated directly in the π^{π}–calculus.

N ::= x(y⃗) · N | ! x(y⃗) · N | \overline{x} v⃗ · 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.

6 Simulation of π–calculus by π^{π}–calculus

A proposed translation of the π–calculus is provided. The translation is based on the use of a π^{π}–calculus process to implement a π–calculus name (communication channel). A π^{π}– calculus channel process coordinates requests for input and output actions using the name. Input requests are provided by Get messages which carry the identity of the process to receive data. Output requests are provided by AP ut messages which carry data values.

Chan = ?Get(n) ·?AP ut(v) · λl (n!v ∥ l : Chan)

Originally, a Chan process will only take a Get message. Outstanding AP ut messages are only accepted once a Get has been seen. A data message is sent and the script is repeated.

This form supports asynchronous communication. Synchronous communication requires that the sending process is blocked until the communication completes. This is achieved by making the translation of the output guarded process wait for a synchronisation signal Sync when the communication is closed. We use P ut messages in place of AP ut and add the identity of a process to receive the synchronisation message.

Chan = ?Get(n) ·?P ut(v, s) · λl (n!v ∥ s!Sync ∥ l : Chan)

In the translation below, we support both styles, at the cost of a slightly more sophisticated definition of Chan:

Chan = ?Get(n) · (?AP ut(v) · λl (n!v ∥ l : Chan) + ?P ut(v, s) · λl (n!v ∥ s!Sync ∥ l : Chan))

In the following we only handle monadic communication. Jeong Ho has extensions to handle the polyadic form. The function t maps π–calculus processes to π^{π}–calculus processes:

t[[x(y) · N]] = νm (x!Get(m) ∥ m : ?y · λm′ t[[N]])
t[[! x(y) · N]] = νm (m : A(x, n⃗))
where  A(x, n⃗) = λm (x!Get(m) ∥ m : ?y · λm′ (m′ : A(x, n⃗) ∥ t[[N]]))

n⃗ =^{△} (fn(N) \ {x, y})

t[[\overline{x} v · N]] = νm (x!P ut(v, m) ∥ m : ?Sync · λm′ t[[N]])
t[[\overline{x} v]] = x!AP ut(v)
t[[(ν x) (N)]] = νx (x : Chan ∥ t[[N]])
t[[N | N′]] = t[[N]] ∥ t[[N′]]
t[[0]] = ()

The names in the π–calculus are represented by π^{π}–calculus processes which start by running the script Chan. It is the restriction construct which causes the channel processes to be introduced. If a π–calculus term with a free name is translated, no corresponding channel process is produced. Hence we need to consider carefully how a π–calculus term is simulated by the π^{π}–calculus.

I suggest a possible framework. How do we investigate the properties of a π–calculus term, P? In general, we might perform an experiment by placing P in parallel with some probe, represented by Q, and observe the behaviour of the combined system. Without loss of generality, we can restrict free names of the combination:

(ν a⃗) (P | Q) where a⃗ = fn(P | Q)

Hence we would be considering the translation of closed π–calculus terms. If such terms are encoded, suitable π^{π}–calculus channel processes will always be generated.

This may be adequate if we are only interested in whether systems converge or not. However, if we consider a labelled transition system for π^{π}–calculus we will only observe τ events from such systems.

A different approach is simply to add π^{π}–calculus processes of the form n : Chan for each name n ∈ fn(P) in parallel with the translation of π–calculus term P.

7 A Restricted Subcalculus of π–Calculus

In some very restricted circumstances we do not need to use the translation based on special π^{π}–calculus channel processes. In these circumstances we can be sure that for each name, at most one π–calculus process in a parallel composition of processes 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 a process cannot 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.

Every symbol, A, used in parametric definitions has an arity, where 0 ≤ arity(A). In the restricted calculus we will also associate an input arity, 0 ≤ inarity(A) ≤ arity(A), which identifies the parameters which can carry names used for input.

We will define a function dn(N) over π–calculus processes. This will be similar in effect to the function defined for π^{π}–calculus and 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 · N) = dn(N)
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 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.

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.

8 Simulation of λ–calculus by π^{π}–calculus

It has been demonstrated that the λ–calculus can be modelled using the π–calculus. Clearly, the π^{π}–calculus can model the λ–calculus through simulation of the corresponding π–calculus. However, a more direct translation is also presented and (will be) shown to be correct.

9 Simulation of π–calculus by OGRe

We give a translation of the π–calculus into Object Graph Rewriting (OGRe). The translation below is based on the use of an OGRe process to implement a π–calculus name (communication channel).

9.1 OGRe Channel Processes

OGRe may be used to implement a channel process which receives either requests for input, provided by Get messages, or data values, with optional synchronisation addresses, provided by AP ut and P ut messages. Get messages contain the names of OGRe processes to receive data values. AP ut messages contain a value to be sent. In addition to a value to be sent, P ut messages also contain the name of an OGRe process to receive a synchronisation message when the communication completes.

Initially, a π–calculus channel n will be represented by a process with state Chan:

n : Chan

c : Chan, c! Get(r) → c : RChan(r)
c : RChan(r), c! AP ut(v) → c : Chan, r! Data(v)
c : RChan(r), c! P ut(v, s) → c : Chan, r! Data(v), s! Sync

In the translation of a π–calculus term, an input action is simulated by a Get message which carries the identity of an OGRe process which will simulate the term following the action. This process will wait for a Data message carrying the value from the corresponding output action when a communication is closed.

An output-guarded action is simulated by a P ut message to the OGRe channel process corresponding to the subject of the action. The P ut message carries the value offered and the identity of an OGRe process which will simulate the π–calculus term following the action. This process will wait for a Sync message indicating that the communication has been closed and the value passed to the corresponding input action.

Asynchronous output is simulated using an AP ut message which requires no synchronisation.

9.2 Simulation of π–calculus

The function q maps π–calculus processes to OGRe processes. The parameter m is the name of the OGRe process corresponding to the translated π–calculus process:

q[[x(y) · N]]_{m} = A(n⃗), x! Get(m)
where m : A(n⃗), m! Data(y) → q[[N]]_{m}

n⃗ =^{△} (fn(N) \ {y})

q[[! x(y) · N]]_{m} = A(x, n⃗), x! Get(m)
where m : A(x, n⃗), m! Data(y) → m : A(x, n⃗), x! Get(m), m′ : q[[N]]_{m′}

n⃗ =^{△} (fn(N) \ {x, y})

q[[\overline{x} v · N]]_{m} = B(n⃗), x! P ut(v, m)

where m : B(n⃗), m! Sync → m : q[[N]]_{m}

n⃗ =^{△} fn(N)

q[[\overline{x} v]]_{m} = Dead, x! AP ut(v)
q[[(ν x) (N)]]_{m} = q[[N]]_{m}, x : Chan
q[[N | N′]]_{m} = q[[N]]_{m}, m′ : q[[N′]]_{m′}
q[[0]]_{m} = Dead

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.

The names in the π–calculus are represented by OGRe processes of the form Chan. It is the restriction construct which causes the channel processes to be introduced. When a π–calculus term with a bound name is translated by the scheme q, a channel process is produced by the translation of the binding restriction.

To account for names which are free in the whole translated term, we add an OGRe process of the form n : Chan for each name n ∈ fn(P) in parallel with the translation of P. The translation of a π–calculus term P is m : q[[P]]_{m} where m ∉ fn(P).

The following example shows translation of the term R = (x(y) · P | \overline{x} v · Q) where fn(P) = \{y\} and fn(Q) = {}:

m : q[[x(y) · P | \overline{x} v · Q]]_{m} = m : q[[x(y) · P]]_{m}, m′ : q[[\overline{x} v · Q]]_{m′}
= m : A, x! Get(m), m′ : q[[\overline{x} v · Q]]_{m′}
where m : A, m! Data(y) → m : q[[P]]_{m}
= m : A, x! Get(m), m′ : B, x! P ut(v, m′)
where m : A, m! Data(y) → m : q[[P]]_{m}
and  m′ : B, m′! Sync → m′ : q[[Q]]_{m′}

Since x is free in R we also add the OGRe process x : Chan. Assuming the definitions of A and B as defined above, the network may then evolve as follows:

m : A, x! Get(m), m′ : B, x! P ut(v, m′), x : Chan
→ m : A, m′ : B, x! P ut(v, m′), x : RChan(m)
→ m : A, m′ : B, x : Chan, m! Data(v), m′! Sync
→ m : q[[P {v/y}]]_{m}, m′ : B, x : Chan, m′! Sync
→ m : q[[P {v/y}]]_{m}, m′ : q[[Q]]_{m′}, x : Chan

Since, by the assumptions we made about free names, x does not appear free in P or Q, the channel process x : Chan can never receive further messages and can be garbage collected. The resulting network is the same as m : q[[P {v/y} | Q]]_{m}. (P {v/y} | Q) is, of course, the result of a communication step in the original term (x(y) · P | \overline{x} v · Q). Since π–calculus names are preserved in the translation it will be seen that we were justified in identifying q[[P]]_{m}{v/y} with q[[P {v/y}]]_{m}.

10 Simulation of π^{π}–calculus by OGRe

We (will) also give a translation of the π^{π}–calculus into Object Graph Rewriting (OGRe).

11 Simulation of λ–calculus by OGRe

The λ–calculus can be modelled in OGRe via the translation of the equivalent π^{π}–calculus term. We (will) also give a more direct translation.

12 History

Version K introduced a translation of π–calculus into OGRe. Since we have a translation of π–calculus to π^{π}–calculus, the original aim was to provide a mapping to OGRe by developing a mapping from π^{π}–calculus to OGRe. This proved less straightforward than expected, while a direct mapping to OGRe presented few problems.

It remains to add a mapping from OGRe to π^{π}–calculus which should compose with the π– calculus to OGRe mapping to provide an alternative, but obviously equivalent, π–calculus to π^{π}–calculus mapping.

The document also omits a proper definition of OGRe which will be provided separately.

Version J added a little more explanation to Version I. It also introduced a running example showing how replication is modelled by a parametric definition and how such a definition can satisfy the constraints of the sub–calculus. Davide Sangiorgi seems to use parametric definitions in his thesis. We will restrict ourselves to the main use of replication which is always guarded by an input action.

Version I changed the reduction relation. If we are to use barbed-bisimulation related the reduction semantics, then the reduction relation should only capture the observable events. I think that means just communication, for now.

Version I introduced some definitions of free and bound names and also some static constraints to be obeyed by well-formed processes. I am not entirely happy with this and would value proposals for improvement! One major change is to try to live without a separate class of variables in terms. There is a bit more explanation of the process and script classes.

An extra section is added, defining a sub–calculus of the π–calculus which may be helpful in defining a more direct translation to π^{π}–calculus. If it could be shown that all π–calculus can be simulated in the sub–calculus, then an even simpler translation should be possible, since the sub–calculus is intended to capture the essential properties of π^{π}–calculus.

Version H contained minor corrections and a new formulation of the translation of the π– calculus which maps to π^{π}–calculus processes rather than scripts.

Version G works with the formulation of π^{π}–calculus introduced under the name term–π^{π}– calculus in Version 6 which aims to have a more uniform syntax using a much simplified syntactic class for scripts. However, the central role of agent definitions is softened by the introduction of abstractions over process names.

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)