9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # A calculus of mobile processes, parts

A Calculus of Mobile Processes, Part I

Robin Milner, University of Edinburgh, Scotland Joachim Parrow, Swedish Institute of Computer Science, Kista, Sweden David Walker, University of Technology, Sydney, Australia June 1989 (Revised September 1990)

1

Running title: Calculus of Mobile Processes, Part I

Address for proofs: Robin Milner, Computer Science Department, University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, UK

Abstract: We present the -calculus, a calculus of communicating systems in which one can naturally express processes which have changing structure. Not only may the component agents of a system be arbitrarily linked, but a communication between neighbours may carry information which changes that linkage. The calculus is an extension of the process algebra CCS, following work by Engberg and Nielsen who added mobility to CCS while preserving its algebraic properties. The -calculus gains simplicity by removing all distinction between variables and constants; communication links are identi ed by names, and computation is represented purely as the communication of names across links. After an illustrated description of how the -calculus generalises conventional process algebras in treating mobility, several examples exploiting mobility are given in some detail. The important examples are the encoding into the calculus of higher-order functions (the -calculus and combinatory algebra), the transmission of processes as values, and the representation of data structures as processes. The paper continues by presenting the algebraic theory of strong bisimilarity and strong equivalence, including a new notion of equivalence indexed by distinctions { i.e. assumptions of inequality among names. These theories are based upon a semantics in terms of a labelled transition system and a notion of strong bisimulation, both of which are expounded in detail in a companion paper. We also report brie y on work-in-progress based upon the corresponding notion of weak bisimulation, in which internal actions cannot be observed.

Special symbols: Since this copy is mathematically type-set, only a few of the less obvious symbols are listed below.

=

:

0 ; S S0 S1 S2 K K0 K1 I I0 I1

s0

. ' ' < > = .

: : : t : : : cons A C0 : : : SGE ]

Greek letters Various relation symbols Boldface zero Empty set Boldface symbols for Combinators Various constant names Boldface names of axioms etc Double square brackets

1 Introduction

We present a calculus of communicating systems in which one can naturally express processes which have changing structure. Not only may the component agents of a system be arbitrarily linked, but a communication between neighbours may carry information which changes that linkage. The most mathematically developed models of concurrency can at best express this mobility { as we shall call it { indirectly. Examples are: Petri nets 14], CSP 7], ACP 3], CCS 9]. On the other hand there are models which express mobility directly but which still require, in our view, a mathematical analysis of their basic concepts such as we provide in this paper. A well-known model of this kind, which has had considerable success in applications, is the Actors model of Hewitt 5]. In such models, mobility is often achieved by allowing processes to be passed as values in communication; we shall instead achieve it by allowing references to processes, i.e. links, to be communicated. This presents an interesting contrast with recent attempts to combine the ideas of -calculus and process calculi by admitting processes as values; examples are by Gerard Boudol 4], Flemming Nielson 12] and Bent Thomsen 16]. The calculus given here is based upon the approach of U e Engberg and Mogens Nielsen 6], who successfully extended CCS to include mobility while preserving its algebraic properties. In the concluding section we describe in more detail what we have added to that work; roughly speaking, we retain (we hope) its essence, but reduce its complexity and strengthen its elementary theory. We shall introduce the calculus by means of a sequence of examples, which are clearly of practical signi cance and which fall naturally into the formalism. Let us begin with a very simple example; we present it at rst in the notation of CCS, and we shall use informally a kind of diagram, which we call a ow graph, to represent the linkage between (or among) agents. We suppose that an agent P wishes to send the value 5 to an agent R, along a link named a, and that R is willing to receive any value along that link. Then the appropriate ow graph is as follows:

P

a

r

S S

S S S

R

We may have, for example, P a5:P 0 and R a(x):R0 . The pre x a(x) binds the variable x in R0; in general, both here and later, we use parentheses to indicate the binding occurrence of a variable. The system depicted in the ow graph is 5

a

r

represented by the expression (a5:P 0 j a(x):R0 )na The post xed operator na is called a restriction, and indicates that the link a is private to P and R. Let us now suppose instead that P wishes to delegate to a new agent, Q, the task of transmitting 5 to R. We therefore suppose that P is connected to Q initially by a link b:

P

ab

rr

S

rb Q

S S S S

R

We now let P ba:b5:P 0; it sends along b both the link a and the value 5 to be transmitted along a. We also let Q b(y):b(z):yz:0; it receives a link and a value upon b, then transmits the value along the link and terminates. Note that the name a is not in the expression Q; Q possesses no link to R initially. The whole system is now (ba:b5:P 0 j b(y):b(z):yz:0 j a(x):R0 )nanb After two communications, both along b, it then becomes (P 0 j a5:0 j a(x):R0 )nanb Thus, if a does not appear in P 0, we may draw the new con guration of the system as follows, indicating that P 's a-link has moved to Q, and Q has become Q0 a5:0:

a

r

P0 b

r

R

This formalism, in which link names appear as parameters in communication, goes beyond CCS. It may seem that with the addition of variables over link names, as well as over ordinary data values, the calculus would become over-rich 6

a

r

rbraQ

0

in primitives. But we shall avoid this prodigality. In fact we shall remove all distinction among link names, variables and ordinary data values; we shall call them all names. There will be just two essential classes of entity: names and agents. Restriction and input-pre x become name-binding operators of di erent nature; restriction localises the scope of a name, while input-pre x is similar to abstraction in the -calculus (being a place-holder for a name which may be received as input). To emphasize the name-binding property of restriction we shall write (x)P in place of P nx; with this syntax, the above example becomes (a)(b)(ba:b5:P 0 j b(y):b(z):yz:0 j a(x):R0 ) Note that a; b; x; y; 5 are all just names. It will appear as though we reduce all concurrent computation to something like a cocktail party, in which the only purpose of communication is to transmit (or to receive) a name which will admit further communications. Surprisingly, this meagre basis is enough to encode computation over an arbitrary data types, if we consider a data type to be a set of data structures { values recursively built from a given nite set of constructors. We tentatively call our new calculus the -calculus, since it aims for universality (at an elementary level) for concurrent computation, just as the -calculus is universal for functional computation. In a companion paper 11] we treat the semantics of the -calculus in depth. The present paper is devoted to a sequence of motivating examples, followed by a statement of the important algebraic properties. In more detail, the remainder of the paper proceeds as follows. In Section 2 we de ne the constructions of the calculus with some auxiliary notions; we then discuss its salient di erences from CCS. In Section 3 we look at some basic examples of the calculus; these are simple nite processes which indicate how scope and mobility are closely interdependent notions. In Section 4, we introduce some convenient abbreviations, which allow us to treat more realistic examples. In particular, we carefully compare the passing of names as parameters with the passing of processes as parameters; we also show how to encode data structures as processes. This section should indicate, particularly to those familiar with process algebras, that the addition of names-as-parameters to CCS provides great modelling strength and transforms the nature of these algebras. Some of the examples in Section 4 are quite substantial; the reader may safely skip some or all of them on a rst reading, and proceed to Section 5 without loss of continuity. In Section 5 we present the equational theory of bisimilarity, as it is de ned and derived in the companion paper 11]. Although this equational theory is strikingly simple, one feature is noteworthy, and needs careful treatment; it is that bisimilarity is not preserved in general by instantiation of names. Our solution appears to be quite tractable; it is to adopt a relativized equality, which is preserved only by those instantiations which maintain the distinction between 7

certain pairs of names. We derive some convenient laws for this relativized equality. The section also records the fact that the equational theory of weak equality, in which the internal actions of a system are ignored as far as possible, is a direct generalization from that in CCS.

8

We presuppose an in nite set N of names, and let u; v; w; x; y; z range over names. We also presuppose a set K of agent identi ers, each with an arity { an integer 0. We let A; B; C; : : : range over agent identi ers. We now let P; Q; R; : : : range over the agents or process expressions, which are of six kinds as follows: 1. A summation Pi2I Pi, where the index set I is nite. This agent behaves like one or other of the Pi. We write 0 for the empty summation, and call it inaction; this is the agent which can do nothing. Henceforward, in de ning the calculus, we con ne ourselves just to 0 and binary summation, written P1 + P2. 2. A pre x form yx:P , y(x):P or :P . `yx:' is called a negative pre x. y may be thought of as an output port of an agent which contains it; yx:P outputs the name x at port y and then behaves like P . `y(x):' is called a positive pre x. A name y may be thought of as an input port of an agent; y(x):P inputs an arbitrary name z at port y and then behaves like P fz=xg (see the de nition of substitution below). The name x is bound by the positive pre x `y(x):'. (Note that a negative pre x does not bind a name.) ` :' is called a silent pre x. :P performs the silent action and then behaves like P . 3. A composition P1 j P2. This agent consists of P1 and P2 acting in parallel. The components may act independently; also, an output action of P1 (resp. P2) at any output port x may synchronize with an input action of P2 (resp. P1) at x, to create a silent ( ) action of the composite agent P1 j P2 . 4. A restriction (x)P . This agent behaves like P except that actions at ports x and x are prohibited (but communication between components of P along the link x are not prohibited, since they have become actions as explained above). 5. A match x = y]P . This agent behaves like P if the names x and y are identical, and otherwise like 0. 6. A de ned agent A(y1; : : : ; yn). 9

2 The calculus

For any agent identi er A (with arity n) used thus, there must be a unique de ning equation A(x1 ; : : : ; xn)def P , where the names x1 ; : : : ; xn are distinct = and are the only names which may occur free in P . Then A(y1; : : : ; yn) behaves like P fy1=x1; : : : ; yn=xng (see below for the de nition of substitution). De ning equations provide recursion, since P may contain any agent identi er, even A itself. The syntax of agents may be summarized as follows:

P ::= 0 j P1 + P2 j yx:P j y(x):P j :P j P1 j P2 j (x)P j x = y]P j A(y1; : : : ; yn)

When our attention is con ned to nite agents, i.e. agents with nite behaviour, the agent identi ers and their de nitions can be omitted, thus removing recursion. The -calculus without the match form is also interesting. Although matching makes it easy to encode computation with data structures, it turns out to be unnecessary for this purpose, as we shall see in Section 4, Example 7. We include the match form partly for clarity, and partly for the pleasant form of expansion law which it provides (rule E0 in Section 5). A few further de nitions will be needed. The free names fn(P ) of P are just those names which occur in P not bound either by a positive pre x or by a restriction. We write fn(P1; P2; : : :) for fn(P1) fn(P2) . As in the -calculus we shall not distinguish between agents which are alpha-convertible, i.e. which di er only by a change of bound names. We shall write P Q if P and Q are alpha-convertible. e We shall sometimes write x for the vector fx1 ; : : : ; xng of names, where n is understood from context. ee We write P fy1=x1 ; : : : ; yn=xng, or P fyi=xig1 i n, or P fy=xg, for the simultaneous substitution of yi for all free occurrences of xi (for 1 i n) in P , with change of bound names if necessary to prevent any of the new names yi from becoming bound in P . 10

In the pre xes `yx:' and `y(x):' we say that y is the subject, and x is the object or parameter. It is the names occurring free in subject position which determine the (current) communication capabilities of an agent. We adopt the following precedence among the syntactic forms: 9 Restriction > = Pre x > > Composition > Summation Match ; Thus, (x)P j :Q + R means (((x)P ) j ( :Q)) + R. We now discuss some of the more important features of the calculus, as a preparation for the examples in the following two sections. 1. Apart from the presence of parallel composition, the outstanding di erence between the -calculus and the -calculus is that names may be instantiated only to names, not to agents (i.e. expressions). This distinction will be understood better through our examples. We explain informally here why we have chosen this course. An agent enacts a process, which changes state through its history; parallel composition admits communication among a family of such processes each with independent state. Such a communication is typically formed by the synchronization of a negative pre x `yx:' with a positive pre x `y(z):'. As an example, suppose the sending agent is P yx:P 0, and the receiving agent is Q y(z):Q0; then Q may acquire from P access { via x { to an already existing agent R (see our rst example below). One may choose to model this by passing R itself as a parameter, rather than just passing an x-link as a parameter, but we choose not to do so for several reasons. First, to pass R as a parameter to Q may result in replication of R, due to repeated occurrence of the formal parameter z within Q0 ; we do not wish the replication of agents with state to be a side-e ect of communication in the -calculus. Second, to pass R as a parameter gives Q access to the whole of R; we are concerned to model the case where a received name x provides only partial access to another agent. (For example, R may communicate with still other neighbours via names not known to Q.) Third, the transmission of access links is a very common phenomenon in computation, even in purely sequential computation, which has hitherto had no adequate theoretical basis; we must examine primitives which may provide such a basis in as lean a framework as possible. 2. The free names of an agent represent its current knowledge of, or linkage to, other agents. If several agents { say P , Q and R { all contain x free, we shall portray this linkage or shared knowledge by a multi-arc in the ow graph of P j Q j R, as follows: 11

P

HH H H

r

rR

x

rQ

Further, if the shared name x is restricted we shall write it internally to the components; so the ow graph of (x)(P j Q j R) is

P

xH

r

HH H

R

The free names fn(P ) correspond roughly to what is called in CCS the sort of P . But there are di erences. First, a sort in CCS contains both names and co-names such as b; if fa; bg is the sort of a CCS agent P , it means that P may input on the link a and output on the link b, but not vice versa. For the present calculus, we do not yet wish to adopt this re nement. Second, in CCS a sort cannot grow throughout the history of an agent; however, the free names fn(P ) can grow throughout P 's subsequent history, since P can receive names in communication. Third, a free occurrence of x in subject position in P indicates that P may communicate along the link x, while a free occurrence in object position merely indicates that P may pass x as a parameter; it is only the former type of occurrence which corresponds closely to CCS sort, since CCS did not admit the latter type. This subject{object distinction is not captured by fn(P ). In later development the distinction will no doubt become increasingly important, in order to understand the potential mobility among the agents of a system. 3. In CCS there is no risk of confusing the binding of an ordinary data variable x, in a positive pre x form a(x):P , with the restriction of a port-name a as in Qna. This is because port-names are distinct from data variables in CCS. Here, the two are identi ed. (More accurately, we shall see that primitive values are represented as names, while compound values { e.g. trees { are represented as processes.) To emphasize this identi cation, we have adopted the pre x notation (x)Q for restriction, in place of the post x 12

x

r

rxQ

notation Qnx. Nonetheless, we must carefully distinguish between the two forms of binding, y(x):P and (x)Q. In y(x):P , x is a place-holder for any name which may be received on the link y, and this may even be a name already free in P ; thus the variable bound by a positive pre x is susceptible to arbitrary instantiation. In (x)Q, x represents a name which is private to Q, and which moreover can never be identi ed with any other name in Q. The di erent treatment of these bindings lies at the heart of the -calculus. In this paper we do not present the basic semantics of the calculus; this is done in our companion paper 11], in the same style as in CCS, namely as a labelled transition system de ned by structural inference rules. In that paper the notions of strong bisimulation and strong equivalence are also de ned; the latter is a congruence relation, so it may be understood as (strong) semantic equality. Here, we shall rely somewhat upon analogy with the transitions of CCS agents. In particular, we shall assume simple transitions such as ( + yx:P + )j( + y(z):Q + ) ! P j Qfx=z g and simple equations such as (y)(yx:P j y(z):Q) =

:(y)(P j Qfx=z g)

in which = means strong equivalence. But not all transitions will be analogous to CCS; the reader will nd the essence of mobility in Example 3 in the next section, where we see that the e ect of certain transitions is to change the scope of a restriction.

13

3 Basic examples

The examples in this section are almost entirely concerned with di erent patterns of occurrence of the two forms of name-binding, positive pre x and restriction, and their behaviour in the presence of communication. This is the basic anatomy of the -calculus.

Example 1: Link passing

P

S S

rr

y

S

rQ

?!

P0

r

y

S S

x

rR

rR

x

r rQ

00

The agent P has a link x to R, and wishes to pass x along its link y to Q. Q is willing to receive it. Thus P may be yx:P 0 and Q may be y(z):Q0; in this case, the transition is yx:P 0 j y(z):Q0 j R ! P 0 j Q0 fx=zg j R (1) 00 0 x So Q in the diagram is Q f =zg. The diagram illustrates the case in which x 2 fn(Q), meaning that Q possesses no x link before the transition. But the = transition is the same if x 2 fn(Q); there is no reason that Q should not receive a link which it already possesses. (Compare Examples 2 and 3, though, in which one or other of the x links is private.) The diagram also illustrates the case in which x 2 fn(P 0), meaning that P 0 has no x-link after the transition, but again = this condition does not a ect the transition. The situation is not much di erent when the link y between P and Q is private. In this case the proper ow graphs are

P

y

S S

rr

ry Q

P0 y

r

S

S S

x

rR

?!

rR

x

r yr Q

00

The privacy of the y-link is represented by a restriction, so the transition is now (2) (y)(yx:P 0 j y(z):Q0 ) j R ! (y)(P 0 j Q0 fx=zg) j R 14

In fact we shall be able to prove the equation

(y)(yx:P 0 j y(z):Q0) = :(y)(P 0 j Q0fx=zg)

(3)

Example 2: Scope intrusion

.. . . . . . .scope of x . ... .. y . Q .... .. x P ... .. ... S S .. ... ... S S ... Sx S ... S S . ... S ... Sx .... R ... S .. ... . . . . . . . ...

rr

r

r r

P0

r

r

?!

.. . . . . . .scope of x .. .. 00 .... y . Q .. x0 .... .. ... S .. ... S ... x .... S ... S ... ... S ... x0 .... R ... S 0 .. .. . . . . . . . ..

r

rr r

0

r

As in Example 1, P has a link x to R, and wishes to pass x along its link y to Q. Q is willing to receive it, but already possesses a private link x to S ; the latter must be renamed to avoid confusion. We describe this informally by saying that P (or the link-passing action) intrudes the scope of the private link x between Q and S . Taking P to be yx:P 0 and Q to be y(z):Q0 as in Example 1, the transition is So Q00 and S 0 in the diagram are Q0 fx0=xgfx=z g and S fx0=xg respectively, where x0 is a new name. This phenomenon is analogous to the avoidance of the capture of bound variables in the -calculus. The transition rules will be such that, as in the -calculus, alpha-conversion (i.e. change of bound variables) is enforced in such cases. For the present example, the transition rules will ensure that the transition (4) is the same, up to alpha-conversion of the result, as we would obtain if we applied the alpha-equivalence (x)(Q j S ) = (x0)(Qfx0=xg j S fx0=xg) (5) beforehand, thus avoiding the intrusion. (Also note that, as we state in Section 5 below, alpha-equivalence implies strong equivalence of agents.)

yx:P 0 j R j (x)(y(z):Q0 j S ) ! P 0 j R j (x0 )(Q0fx0=xgfx=zg j S fx0=xg)

(4)

Example 3: Scope extrusion

15

.. . . . . . .scope of x . ... .. . .. P .... y Q .. x ... .. ... S ... S ... ... S .. ... S .. S ... . ... x ... ... R ... . . . . . . . ..

rr

r

r

?!

.. . . . . . . . ... scope..of. x. . . . .. . . .. ... y .... 00 .. .. P 0 Q . .. x .... .... x ... HH . .. .. H ... H .. . ... ... ... . ... ... ... x ..... ... R ... .......

rr

r

rr

As in Example 1, P has a link x to R, but we now suppose that this link is private. However, P wishes to pass x along its link y to Q. Q is willing to receive it, and possesses no x-link. This situation is exactly that of a program P , with a local variable modelled by a storage register R, passing R to a procedure Q which takes its parameter by reference, not by value. So, taking P to be yx:P 0 and Q to be y(z):Q0 , as in Example 1, the transition is (x)(yx:P 0 j R) j y(z):Q0 ! (x)(P 0 j R j Q0fx=z g) (6) So Q00 in the diagram is Q0 fx=zg, as it was in Example 1. The di erence here is in the privacy of P 's x-link to R, represented by the restriction (x). When this link is exported to Q the scope of the restriction is extended; we say that P (or the link-passing action) extrudes the scope of the private x-link. Now, in contrast with Example 1, the situation is di erent if Q possesses a public x-link before the transition, i.e. if x 2 fn(Q). Then we have to change the private link name in order to preserve its distinction from the public link. .. . . . . . .scope of x . ... .. . .. P .... y Q0 .. x ... .. ... S S ... S S ... S x ... S .. ... S .. S ... . ... x ... ... R ... . . . . . . . ..

rr

r

r r

?!

.. . . . . . . . ... scope..of. x. . . . .. . . .. 00 .. y ... 00 .. .. P 0 ... ... Q .. .. x . . x0 ... HH ... .. S . H ... . H .S ... ..S x . ... ... . ... x00 ..... ... ... R .... .......

rr

r

rr r

0

Now the transition becomes (x)(yx:P 0 j R) j y(z):Q0 ! (x0 )(P 0fx0=xg j Rfx0=xg j Q0 fx0=zg) So P 00 in the diagram is P 0fx0=xg, Q00 is Q0 fx0=z g, and R0 is Rfx0=xg. 16

(7)

Reverting to the case x 2 fn(Q), let us now suppose also that x 2 fn(P 0), i.e. = = 0 P possesses no private x-link after the transition: .. . . . . . .scope of x . ... .. . .. P .... y Q .. x ... .. ... S ... S ... ... S .. ... S .. S ... . ... x ... ... R ... . . . . . . . ..

rr

r

P0

r

r

?!

x .. . . . . . . . ... y ..... Q00 .. x .... ... . . ... .. . . . ... .... . .. ... . .. x .. R ..... . .. . . . . . . . ...

scope of

r

rr

The transition is exactly as in (6), but we can transform the result. There is a general law (x)(P1 j P2) = P1 j (x)P2 if x 2 fn(P1) = (8) which we can apply to the result of (6): (x)(P 0 j R j Q0 fx=z g) = P 0 j (x)(R j Q0fx=z g) (9) This is what justi es the preceding diagram. We may describe this as a migration of scope, a special case of extrusion; the scope of the restriction (x) has migrated from P to Q. The reader may like to consider a combination of Examples 2 and 3, in which both intrusion and extrusion occur. pair (u; v) of names to one of two agents Q and R. Consider the following attempt at de ning the three agents: xu:xv:P 0 P Q x(y):x(z):Q0 R x(y):x(z):R0 A di culty arises, with these de nitions, in the behaviour of the composite agent QjP jR. It may perform the following pair of transitions, which represents the possibility that Q receives u and R receives v, instead of one or other of them receiving the whole pair as intended: QjP jR x(y):x(z):Q0 j xu:xv:P 0 j x(y):x(z):R0 ! x(z):Q0 fu=yg j xv:P 0 j x(y):x(z):R0 ! x(z):Q0 fu=yg j P 0 j x(z):R0 fv=yg 17

Example 4: Molecular actions Suppose that an agent P wishes to pass a

If this possibility is to be avoided, we need a way in which the pair (u; v) of names can somehow be transmitted in a single atomic action. Private names are the key to the solution. Instead of passing the elements u and v directly, we arrange that P passes to Q (or to R) the private name of a small process whose only task is to deliver u and then v:

P Q R

(w)(xw:P 0 j wu:wv:0) x(w):w(y):w(z):Q0 x(w):w(y):w(z):R0

where w 2 fn(P 0; Q0; R0). Now, QjP jR has two alternative transitions: =

QjP jR ! (w)(w(y):w(z):Q0 j P 0 j wu:wv:0) j R = : :(Q0 fu=ygfv=zg j P 0 j R)

and

QjP jR ! Q j (w)(P 0 j wu:wv:0 j w(y):w(z):R0) = : :(Q j P 0 j R0fu=ygfv=zg)

(We have slightly simpli ed these transitions, taking advantage of the associativity of j.) The two transitions represent the transmission of the pair to Q and to R respectively; no mixture is possible. We may think of the atomic action xw, together with the actions of the process wu:wv:0 which it makes accessible, as together forming a molecular action. (It is vital to this idea that w, which bonds the molecule, is indeed a private name.) This device is very powerful, extending far beyond this illustration with pairs. As we shall see in Example 7, it yields a uniform encoding of data structures as processes.

18

4 Further examples

In this section we shall explore some more concrete examples; they are on a small scale, but deal with real applications in computing. First, we de ne some abbreviations. 1. Sometimes a communication needs to carry no parameter. To model this we presuppose a special name, say , which is never bound; then we write

x:P in place of x :P x:P in place of x(y):P

(y not free in P )

2. We shall often omit `:0' in an agent, and write for example

xy in place of xy:0

3. We shall often wish to allow input names to determine the course of computation. Thus, we naturally write

x(v):( v = y1]P1 + v = y2]P2 + )

where usually the names yi will be distinct. Assuming that v does not occur free in any Pi, we shall abbreviate this to

x : y1 ) P1; y2 ) P2; : : :]

or { schematically {

x : yi ) Pi]i2I Exec(x) def x(y):y =

(10)

Example 5: An Executor Let us de ne

Exec(x) may be called an executor. It receives, on link x, a link which it calls y; it then activates that link. We can think of y as the trigger of a process which Exec(x) has been called upon to run. Now for any process P , we should (up to a few initial communications) obtain the same behaviour in each of the following cases: (a) We run P directly; (b) We pre x a trigger z to P , and pass z along the link x to the executor Exec(x). (We assume x; z 2 fn(P ).) Here is the agent which, in the presence of Exec(x), should = behave like P : (z)(xz j z:P ) (11) (Later we shall nd that a construction like this can be regarded as passing the process P itself as a value along the link x, but that the passing of links as values

19

has other applications too.) Here then is the agent which should be equivalent to P : (x)((z)(xz j z:P ) j Exec(x)) (12) To see this, rst apply equation (8) to obtain (x)(z)(xz j z:P j x(y):y) Now this, by a suitably generalized expansion law, becomes :(x)(z)(0 j z:P j z ) which in turn becomes : :(x)(z)(0 j P j 0) which, since x and z were chosen not free in P , is equal to : :P executor had no work to do except to activate (the link to) P , and the sender had no work to do except to transmit (the link to) P (and then to retain P awaiting activation). If the parenthetical parts of the preceding sentence are included, the sentence accurately describes Example 5; if they are omitted, then it describes the passing of a process as a parameter. Though these two situations are not { at least not obviously { the same, the e ect of process-passing can in many cases be achieved by link-passing. Passing processes as parameters is not represented directly in the -calculus. In a direct representation we would write, instead of (12), something like (x)(xP:0 j x(p):p) (13) where p is a variable over processes, and P is a process expression (i.e. an agent). This notation is close to that of Thomsen 16], for example (see our later discussion of his work). We have seen that, in this simple case, (12) indeed has the e ect which would be intended for (13). Let us pursue this direct representation of process-passing further, to draw attention to an important issue of scope. To develop (13) a little, suppose that the sender, after sending P , wishes to run Q; suppose also that the executor, after receiving P , wishes to run it in parallel with R. In an extended language, permitting (13), we would write (x)(xP:Q j x(p):(p j R)) (14) where we assume that x 2 fn(P; Q; R). A suitably generalized expansion law = would equate this to :(Q j (P j R)) (15) 20

Example 6: Passing processes as parameters In the previous example, the

This allows communication to occur both between P and it rst `neighbour', Q, and also between P and its second `neighbour', R. To develop the example further, we now suppose that before transmission a private link w exists between P and Q; this privacy may be represented as a restriction (w) applied to the sender: (x)((w)(xP:Q) j x(p):(p j R)) (16) Now there are two alternatives for how the transmission of P should treat the private link w; the choice is signi cant even when w 2 fn(R), and even more = signi cant when w 2 fn(R). In the rst alternative, the generalized expansion law would equate (16) with

:((w)Q j (P j R)) (17) This shows that the private link w between P and Q is broken by the communication. To put it di erently, in the expression (w)(xP:Q), the restriction (w) binds w in Q but not in P (and thus the private link does not in fact exist!). Moreover, if w 2 fn(R), then w represents a link between P and R. In this approach, the passing of processes as parameters amounts to passing the text of the process as a parameter, which is similar to the treatment of function parameters in LISP as originally de ned by McCarthy. This has often been called `dynamic binding'; the free variables in (the text of) a function parameter are interpreted in the receiving environment. Thomsen 16] has adopted dynamic binding in his Calculus of Higher-order Communicating Systems (CHOCS), and has found that many important computational phenomena can thereby be modelled satisfactorily. However, we intend to adopt static binding. The second alternative is that, by a form of scope extrusion (see Example 3), the generalized expansion law equates (16) to (18) :(w0)(Qfw0=wg j (P fw0=wg j R)) where w0 has been chosen not free in P , Q or R. This alternative preserves the w-link between P and Q, and preserves its distinction from any w-link possessed by R. Now let us return to the way we represent the passing of a process parameter in the -calculus, and we shall see that the e ect of (18) is obtained. In place of (16) we write (x)((z)(w)(xz:(z:P j Q)) j x(y):y:R) (19) (where y; z 2 fn(R)) which, by expansion, will be equal to = (20) :(z)((w)(z:P j Q) j z:R) (The restriction (x) is dropped since x 2 fn(P; Q; R).) Now, by a change of = 0 bound name w to w 2 fn(R), followed by (8) in reverse to extend the scope of =

21

the restriction (w0), we obtain

:(z)(w0)(z:P fw0=wg j Qfw0=wg j z:R) : :(w0)(P fw0=wg j Qfw0=wg j R)

(21) (22)

which, by expansion and then discard of the restriction (z), becomes This, but for an extra action, is identical with (18). It may therefore seem that link-passing has all the power of process-passing. This is indeed true, in the presence of recursion; indeed, in a private communication Bent Thomsen has given a translation of a static-binding variant of his CHOCS calculus 16] into the -calculus. In one sense link-passing has greater power, since the link which is passed need not only be the trigger of a process; one may pass { to many di erent recipients perhaps { the power to interact in di erent ways with an existing process. In another sense, the power of link-passing is less; for it does not by itself give the ability to copy a process, as in x(p):(p j p). In particular, the -calculus without recursion cannot provide the power of general recursion, as the -calculus does via the paradoxical combinator Y. We take the view that it is natural to provide recursion explicitly. we can simply designate n names { denoted by v1 ; : : : ; vn { as constants. (The role of constant names in the theory is dealt with in Section 5.) Clearly the match operator { in its derived form for convenience { can be used to control computation. Consider the case V = ft; f g, the truth values. We set t = t and f = f. Then a process for simply copying a truth value from one link to another is

Copy(y; z) def y : t ) z t; f ) z f] =

Example 7: Values and data structures If the only values with which we wish to compute are drawn from a nite set, say V = fv1; : : : ; vng, then

(23)

(A simpler de nition might be Copy(y; z)def y(x):zx, but we are starting a series = of de nitions which all compute by case-analysis upon the constant or data constructor which is input.) Further, a process And(x; y; z), which produces at z the logical conjunction of the truth values received at x and y, may be de ned as follows:

And(x; y; z) def x : t ) Copy(y; z); f ) z f] =

(24)

Now, since we are representing a n-ary boolean function by an agent with n + 1 link parameters, it is reasonable to extend this to the case n = 0. We think of the = agents True (x)def x t and False (x)def x f as pointed values, with x playing the role = of pointer. We may then represent application of a function by composition of 22

agents, followed by restriction of the pointer. It is then easy to prove the simple equations which justify the above encoding, such as the following: (x)(True(x) j Copy(x; y)) = :True(y) (x)(y)(True(x) j False(y) j And(x; y; z)) = : :False(z) The matter is di erent if we wish to compute over an in nite set, for example over the natural numbers Nat. We could choose an in nite family of constants fn : n 2 Natg, but we cannot write the successor function (for example) as an agent in the form

Succ(x; y) def x : n ) y n +1]n2Nat = because this is an in nite sum, and we want the terms of our calculus to be nite. To illustrate an alternative method, we shall use the data type of list structures, built from a nullary operator `nil' (the empty list) and a binary operator `cons'. Any list structure L, say `cons(cons(nil,nil),nil)', is represented by a pointed value L] (x); this is an agent which will emit L piecemeal along the link x. L] is de ned as follows, in terms of constant names cons (for `cons') and nil (for `nil'):

nil]](x) def x nil = (25) def cons(L1 ; L2 )]](x) = (y)(z)(x cons:xy:xz j L1 ] (y) j L2 ] (z)) (26) In the presence of L] (x), an agent which possesses or receives the link x thereby possesses or receives the power to explore the list structure L piecemeal, by following pointers. In the case that an agent P privately holds the name x of a list structure L, as in the system (x)(P j L] (x)), the transfer of L by P to another agent is therefore a molecular action as de ned in Example 4. Note particularly that the constituent actions of this molecule may themselves be molecular, since L may have non-trivial sub-structures. We shall now introduce a few further abbreviations to make the following examples more legible. First we de ne some composite pre xes: xy1 yn means xy1: :xyn (27) x(y1) (yn) means x(y1 ): :x(yn) (28) Thus, if L = cons(cons(nil,nil),nil), then we have L] (x) = (y)(z)(x consyz j (v)(w)(y consvw j v nil j w nil) j z nil) Second, we de ne a more re ned form of matching clause: x : : : : ; v(y1) (yn) ) P; : : :] means x : : : : ; v ) x(y1 ) (yn)P; : : :] (29) 23

Thus, when v is received on link x, the names subsequently received on x are bound to y1; : : : ; yn. As an example, let us de ne an agent Equal(x; y; b) which outputs t on b if x and y point to equal structures, f otherwise:

Equal(x; y; b) def x : nil ) Null(y; b); cons(x1 )(x2 ) ) = Consequal(x1 ; x2 ; y; b)] Null(y; b) def y : nil ) True(b); cons ) False(b)] = Consequal(x1 ; x2; y; b) def y : nil ) False(b); cons(y1)(y2) ) = (b1 )(b2 )(Equal(x1 ; y1; b1 ) j Equal(x2; y2; b2 ) j And(b1 ; b2 ; b))]

(30) (31)

(32)

We hope these simple examples provide convincing evidence for what we shall show rigorously in a later paper, namely that our bare calculus of names is enough to encode a richer calculus in which values of many kinds may be communicated, and in which value computations may be freely mixed with communications. The analogous encoding for CCS 9] relies upon in nite summation; instead, we exploit the power which private links provide to represent complex values as structured agents. One or two points about the above encoding deserve mention: Our pointed values are nite processes; they are ephemeral, in the sense that they may only be analysed once. But other encodings are possible which give permanence to values. The encoding has only needed a nite number of constant names: t, f, cons and nil. But there are encodings which need no constant names whatever. The trick is to use matching to distinguish private names; for example:

True(x) def (u)(v)(xuvu) = def False(x) = (u)(v)(xuvv)

The reader may enjoy re-de ning And(x; y; z) to work with these forms. We shall now justify the claim made in the introduction that the match form is unnecessary for encoding computation over data types. The control which it provides can, in fact, be achieved by other means. Consider the following agent P , which inputs a truth value (in the encoding we have just presented) on link x, and enters either P1 or P2 according to the value:

x(u)(v)(w):( w = u]P1 + w = v]P2)

24

Now let us change the encoding of truth values very slightly:

True(x) def (u)(v)(xuv:u) = def False(x) = (u)(v)(xuv:v)

Then the agent P can be correspondingly changed to

x(u)(v):(u:P1 + v:P2)

Clearly, both this encoding and the previous one can be extended to deal with any nite set of value constructors or constants. The attentive reader will have noticed that, in allowing constants to occur free in the equations which de ne agent identi ers, we have violated the condition on de ning equations imposed in Section 2. We justify this violation at the end of Section 5; it is merely part of a conventional treatment of constants. built from combinators by a binary operation called application. We let M , N and P range over terms, and we shall consider only the three most basic combinators S, K and I. The syntax of terms is therefore

Example 8: Combinator graph reduction In combinatory logic, terms are

M

::= S j K j I j (MN )

Application associates to the left, so the term SK(MN )S means (((SK)(MN ))S). Terms may be reduced by the following rules:

SMNP ?! MP (NP ) KMN ?! M IM ?! M

A combinator graph is a graph which represents a term. For every application in the term it contains a node labelled @, with a left and a right child; every other node is labelled by a combinator and has no children. Thus, for the term S(KM )(KM )N , either of two graphs shown in Figure 1 will do: The rst graph represents sharing of two occurrences of the subterm KM . Combinator graph reduction models term reduction, except that it takes advantage of sharing. It is an important implementation technique for functional programming languages, and computers are being designed to support it by hardware { see for example Goguen et al 8]. It will therefore also be important to model the performance of this hardware in a formal calculus, to verify its performance. This presents a tough challenge to the calculus, which must describe not only the mobile structure of the (virtual) processes among themselves, but also their changing allocation to (real) processors. We believe that the -calculus 25

@ @ @

A A A A

@

A

N

OR @

A A

@

A

@

N

@

A A

@ @

S

@

A A

S

@ K

A A

M

K

M

K

M

Figure 1: Two combinator graphs for the term S(KM )(KM )N contains the right primitives to meet this challenge. We have given a hint in Example 5 (the Executor) of how allocation to processors may be modelled; the changing virtual structure is combinator graph reduction, to which we now turn. First, we give the graph reduction rules; see Figure 2. They use auxiliary combinators S1 , S2 , K1 and I1 in addition to S, K and I (which we shall now call S0 , K0 and I0 ). There is exactly one rule for each combinator, allowing reduction when it occurs as a left child. Note how sharing is introduced by the rule for S2 . Note also that the auxiliary combinators S1 ; S2; : : : appear in the graphs not at the leaves, but as operators of arity one or two. We shall now illustrate how the term reduction

(1) (2) (3) S(KM )(KM )N ?! KMN (KMN ) ?! M (KMN ) ?! MM

is modelled by graph reduction. We give the graph reduction in Figure 3. Notice that several steps of graph reduction correspond to a single step of term reduction; we show this by numbering the arrows. The redex { i.e. the subgraph to be reduced { at each stage is indicated by ringing its @ node. One should note that, just as the subgraph for (KM ) has two parents, so any other node in the graph may have another parent not shown in the diagram (if the whole is a subgraph of a larger system); such nodes, even if they become disconnected during this particular reduction, cannot be discarded altogether. (In passing, note that we have not succeeded in eliminating I1 entirely; a more sophisticated set of rules can achieve this.) We can now proceed to model the combinator graphs as ( ow graphs of) composite agents. Each combinator Si, Ki or Ii is modelled by an agent with i+1 parameters; the rst i parameters are links to its children, and the last a link to its parent(s). Each combinator repeatedly utters a message, which contains its own identity (a constant name such as s0 ) and the names of its children. Here are 26

@

S0

A A

M

?!

@

S1

A A

@

M

S1

A A

A A

N

?!

S2

M

A A

N

M

@

A A

S2

M

@

A A

A A

P

?!

M

@

Q

Q

@

N

N

@

A Q A Q Q

P

K0

A A

M

?!

K1

A A

M

K1

A A

A A

N

?!

I1

A A

M

M

@

A A

@

I0

A A

M

?!

I1

A A

M

I1

A A

N

?!

@

M

A A

N

M

Figure 2: Rules for combinator graph reduction

27

@ @ @

A A A A

N

?!

(1)

@ @

A A

N

?!

(1)

@

A

S2

@

A A

A

N

?!

(1)

@

A

@ @

A

S1

@

A A A A

@ ? ? @ ? @ A A

@

N

S0

@

A A

K0

M

@

M

K0

M

K0

M

@

K0

A A

?!

(2)

@

K1

@ ? ? @ ? @

@

?!

(2)

I1 K

A A

N

A A

M

? B? ? 1 BB JB J JB B B

@

?!

(2)

@

A A ? ? ?

@

?!

(3)

@

A A

I1

N

K1

N

M

M

A A

M

Figure 3: Graph reduction for the term S(KM )(KM )N

28

the de nitions for the three S combinators (the others are completely analogous):

S0(p) def (w)(pw:(w s0 j S0 (p))) = S1(x; p) def (w)(pw:(w s1x j S1(x; p))) = S2(x; y; p) def (w)(pw:(w s2xy j S2 (x; y; p))) = The message sent by S1, for example, consists of the pointed value ws1:wx, formed into a molecular action whose pointer is the private link w. S1 restores itself

after the message, and its next message will have a new private link. The use of molecular actions ensures that di erent parents do not read parts of the same message. All that remains is to de ne the application agent @(x; y; p). It communicates only with its left child, and only when this is a combinator. Each clause of the match, in the de nition, corresponds to one of the seven graph reduction rules. @(x; y; p) def x(w): w : s0 ) S1(y; p); = s1 (x1 ) ) S2 (x1 ; y; p); s2 (x1 )(x2 ) ) (p1 )(p2 )(@(x1 ; y; p1) j @(x2; y; p2) j @(p1; p2; p)); k0 ) K1 (y; p); k1 (x1 ) ) I1 (x1 ; p); i0 ) I1 (y; p); i1 (x1 ) ) @(x1 ; y; p) ] With these de nitions, the reader can show, without too much di culty, that (for example) the graph reduction rule for S2 is captured by the equation (p0 )(S2(x; y; p0) j @(p0; z; p)) j M (x) j N (y) j P (z) = : : : :((p1 )(p2 )(@(x; z; p1 )j@(y; z; p2)j@(p1; p2; p)) j M (x) j N (y) j P (z)) Finally the reader may like to check that one can avoid using both constants (s0; s1 ; : : :) and the match form in modelling combinator graphs, using alternative encoding as suggested at the end of Example 7.

Example 9: The -calculus

The encoding of combinator graph reduction (Example 8) has already shown that higher-order functions can be `handled', in some sense, in the -calculus. This can be thought of as an encoding of the -calculus, since there are natural translations of -calculus into combinator algebra; but the encoding is rather indirect. Here we give a much more direct encoding, one in which reduction sequences in the two calculi correspond closely. 29

It will also show that, to gain the full power of -calculus, only a very limited use of recursion is needed { no more than just to achieve replication of an agent. More precisely, what we shall encode is a particular reduction strategy for -calculus: lazy reduction 1]. Theorems which justify this encoding, and also an encoding of call-by-value reduction, appear in a separate paper 10]. First, recall the syntax of -calculus; its terms M; N; : : : 2 have the syntax M ::= x j ( xM ) j (MN ) where x ranges over an in nite set V of variables. We often omit the parentheses around the composite forms, when there is no ambiguity, taking application (MN ) to be left-associative. For convenience we assume that V is a subset of N , with N ? V in nite, and for this example we take x; y; z to range over V while u; v; w range over N ? V . Then the lazy reduction relation ?! over is the smallest relation such that ( xM )N ?! M fN=xg If M ?! M 0 then MN ?! M 0 N This reduction strategy is completely deterministic. Any term M can be written M0 M1 Mm (m 0), where M0 is not an application. Then M ?! M 0 for some M 0 if and only if m 1 and M0 is xN , and then M 0 is N fM1=xgM2 Mm . So for each M there is at most one irreducible term M 0 such that M ?! M 0 , and moreover M 0 is either of the form xN or of the form xN1 Nn (n 0). We shall rst encode the linear -calculus, in which no sub-term of a term may contain more than one free occurrence of x, for any variable x. The paradoxical combinator Y is thereby excluded; indeed, every reduction sequence terminates in the linear -calculus. Correspondingly, we nd that we need not call upon recursion for the encoding in the -calculus. We shall translate each -term M into a map M ] from names to agents. To understand the agent M ] u, where u is any name (2 N ? V ), we may think of u pointing to the argument sequence appropriate for a particular occurrence of M . More precisely, if M eventually reduces to a -abstraction xM 0 , then the corresponding derivative of M ] u will receive along the link u two names: a pointer to M 's rst argument, and a pointer to the rest of its argument sequence. Thus u represents a list, just as lists are represented in Example 7. Here is the full de nition of the encoding function ] : xM ] u def u(x)(v): M ] v = (33) def x] u = xu (34) (35) MN ] u def (v)( M ] v j (x)vxu:x(w): N ] w) = (x not free in N ) Note that the variable x occurs free in the translation of the -term x; hence in equation (33) x will normally occur free in M ] v. 30

The double guarding of N ] in equation (35) is the essence of lazy reduction. The rst guard, the pre x vxu, will be activated only when M has reduced to the form xM 0 and is ready for its argument; the second guard x(w) will be activated only when M 0 calls N via the name x; only then may the reduction on N commence. It is illuminating to see how the encoding of a particular example behaves. Consider ( xx)N ; rst, we have

xx] v

So, assuming x not free in N : ( xx)N ] u = = = =

v(x)(w):xw

(v)( xx] v j (x)vxu:x(w): N ] w) (v)(v(x)(w):xw j (x)vxu:x(w): N ] w) :(v)(x)(v(w):xw j vu:x(w): N ] w) : :(v)(x)(xu j x(w): N ] w) : : :(v)(x)(0 j N ] u) : : : N] u

More generally, it is easy to show that ( xM )N ] u

M fN=xg] u

(36)

where is the weak bisimilarity discussed brie y in Section 5. Moreover the (unique) derivation sequences of both sides are closely related. (They do not keep precisely in step; the left-hand side takes more steps, because it simulates the substitution of N for x in M by making the (only!) occurrence of x in M send its argument list to N .) The proof of (36) relies strongly on the linearity of M ; if M contains x twice then each occurrence of x will attempt to send an argument list to N , and this will fail because the agent x(w): N ] w (which represents the `procedure' N ] receiving an arbitrary argument list w along x) is consumed by the rst call. In the translation of the full -calculus, then, what is needed is replication. Let us therefore de ne, for any action-pre x , the form

tinguished solution of the agent equation X = E . (We could have used such constructions throughout, instead of using agent identi ers and providing them with 31

xX ( :(P j X )) Here we have used the xed-point construction xXE , which stands for a disP def =

de ning equations; apart from one or two niceties the two approaches amount to the same.) Thus, we have

P =

:(P j

P)

which indicates that each `call' { i.e. each occurrence of the action { generates a new copy of P . Note that this equation holds even when is a bound action such as x(w). This replicator, as we shall call it, can now be used to make the only change needed in our translation to accommodate the full -calculus, namely to replace equation (35) by

MN ] u def (v)( M ] v j (x)vxu:(x(w) N ] w)) = (x not free in N )

(37)

Now N may be called more than once from M ; each call generates a new replica of N and provides it with a di erent argument list in place of w. Moreover, with the help of some lemmas about replicators, equation (36) can still be proven, and the close correspondence between the reduction sequence of any M in the -calculus and the derivation of its encoding M ] is maintained. Earlier we referred to Bent Thomsen's translation of the static-binding variant of his CHOCS calculus 16] into the -calculus; in this translation, he independently found that replication is the only use of recursion required. Abramsky 1] de nes a notion of applicative simulation, < , for the lazy calculus, and analyses its model theory and proof theory in depth. He actually called it applicative bi-simulation, but we prefer to reserve this term for the induced equivalence < \ > , which we shall denote by = . It is therefore natural to ask the relationship between M ] u N ] u and M = N . It turns out that for closed terms M ] u N ] u implies M = N But the converse is false; an example of Ong 13] can be adapted to show this. Intuitively, the reason is that applicative bisimulation only considers the behaviour of a term M when applied to arguments which are -terms, while the process M ] u inhabits the more unruly environment of arbitrary processes. Before leaving the -calculus we should remark that we have only encoded faithfully one of its reduction strategies, albeit an important one. Much work remains to be done to broaden the connection between the two calculi.

32

5 Algebraic theory

In our companion paper 11] we give a de nition of strong bisimulation between agents,: and a corresponding equivalence relation of strong bisimilarity. We shall use P Q to mean that P and Q are strongly bisimilar. Before giving the equational theory of this relation, we point out a subtlety which was of no great concern in CCS, but is important here { namely that strong bisimilarity is not preserved by substitution for free names. For this reason, we shall sometimes refer to strong bisimilarity as strong ground equivalence. For example, let x and y be distinct names and consider the equation

xjy

:

x:y + y:x

(38) (39)

This holds in our theory, but the substitution of x for y falsi es it; we have

x j x 6 : x:x + x:x

but on the other hand

x j x : x:x + x:x + (40) This is the price we pay for not distinguishing constants from variables. Later, however, we shall introduce strong (non-ground) equivalence ; it will be simply de ned as strong bisimilarity under all substitutions. This relation is preserved by substitution, and moreover we shall nd the following (more general) equation true: x:P j y:Q x:(P j y:Q) + y:(x:P j Q) + x = y] :(P j Q)

(41)

Our equational axioms will use a kind of head normal form. In order to de ne this form we shall need a new abbreviation:

x(y):P means (y)xy:P if x and y are distinct

(42)

This special case of restriction may be thought of as the simultaneous creation and transmission of a new private name; it is a name which cannot have been `used before' because it only occurs within P , which only becomes active after the transmission. The importance of this form is that, as our equational theory shows, every use of restriction can be reduced (up to bisimilarity) to this special case. We now have four kinds of pre x, and we shall allow ; ; : : : to range over them. The syntax of pre xes is ::=

j x(y) j xy j x(y)

33

where, of course, the rst three are primitive forms and the last is derived.

De nition 1

An agent P is in head normal form if it is a sum of pre xes: X 2 P i :Pi

i

We shall now give an equational theory for strong bisimilarity. It will turn out that this theory is :complete over nite agents, but incomplete over all agents (necessarily since is not recursively enumerable). We shall state the rules using the standard equality symbol = , rather than the symbol : ; the reason for this is that, both in this paper and in later work, we shall wish to consider the validity of a rule when = is interpreted by other equivalence relations. For example, Proposition 4 below asserts that several { but not all { of the rules are valid when = stands for strong equivalence, . The reader may wonder why we rst axiomatize : , rather than , even though the latter is preserved by all substitutions (i.e. is a congruence) and is therefore a more natural candidate for the `equality' of agents. In fact, in Proposition 9 below we do axiomatize , but that second axiomatization, as we shall see, depends upon the present one. We omit the standard rules for an equivalence relation, taking them as given. On the other hand = will not always stand for a congruence relation; in fact the congruence rule C0 asserts that = is preserved by all operators except the positive pre x, while C1 asserts a weaker property for positive pre x.

5.1 Strong bisimilarity

Alpha-conversion A From P Q infer P = Q Congruence C0 From P = Q infer

C1 From P fz=yg = Qfz=yg, for all names z 2 fn(P; Q) fyg, infer

x(y):P = x(y):Q

:P = :Q xy:P = xy:Q P + R=Q + R P j R=Q j R (x)P = (x)Q x = y]P = x = y]Q

Summation

S0 S1 S2 S3

P + 0=P P + P =P P + Q=Q + P P + (Q + R) = (P + Q) + R

34

Restriction

R0 R1 R2 R3 R4

(x)P = P if x 2 fn(P ) = (x)(y)P = (y)(x)P (x)(P + Q) = (x)P + (x)Q (x) :P = :(x)P if x is not in (x) :P = 0 if x is the subject of if x and y are distinct

Match

M0 x = y]P = 0 M1 x = x]P = P

Expansion E Assume P = Pi i :Pi and Q = Pj j :Qj , where no i (resp. j ) binds a name

free in Q (resp. P ); then infer X X P jQ = j :(P j Qj ) + i :(Pi j Q) +

i j

X

i

comp

:Rij

j

where the relation i comp j ( i complements j ) holds in four cases: 1. i is xu and j is x(v); then Rij is Pi j Qj fu=vg. 2. i is x(u) and j is x(v); then Rij is (w)(Pifw=ug j Qj fw=vg), where w is not free in (u)Pi or in (v)Qj . 3. i is x(v) and j is xu; then Rij is Pifu=vg j Qj . 4. i is x(v) and j is x(u); then Rij is (w)(Pifw=vg j Qj fw=ug), where w is not free in (v)Pi or in (u)Qj .

Identi er ee e = e I From A(x) def P infer A(y) = P fy=xg

We shall call this axiomatic theory SGE (for Strong Ground Equivalence); if P = Q can be proved in SGE we write SGE ` P = Q or just ` P = Q if no ambiguity arises. Note some important points: 1. The last clause of rule C0, namely From P = Q infer x = y]P = x = y]Q is redundant in the presence of M0 and M1, since any case of it can be deduced from them. But C0 will be needed when = is interpreted as , since M0 is invalid in that interpretation. 35

2. Rule C1 cannot be strengthened to From P = Q infer x(y):P = x(y):Q as we can see by considering equation 38 above; we have in fact z(y):(x j y) 6 : z(y):(x:y + y:x) because y is a place-holder for any received name, and the received name may be x. Thus the hypothesis of rule C1 must account for all substitutions; for this purpose, however, only nitely many of them need to be veri ed. 3. By means of C0, M0 and M1 all occurrences of a match operator which are not within an input-pre x form can be eliminated from an agent. However, y = z] cannot be removed from the input-pre x form x(y): y = z]P . (See also the previous point.) 4. In rule R3 note that includes in its range the derived pre x z (y). 5. In rule E, cases 2 and 4 are crucial; they represent the communication of a new private name, resulting in a restriction (w) which embraces both sender and receiver in its scope. The: following results are all proved in the companion paper 11], for the de nition of which is given there.

Proposition 1 (Soundness)

interpreted as strong bisimilarity,

:

All the laws of SGE are valid when = is . 2

A natural constraint upon de ned agents is the following:

De nition 2 An agent identi er B is weakly guarded in P if every occurrence

The following now shows the importance of head normal form:

of B in P is within a pre x form. The agent identi er A is weakly-guardedly de ned if every agent identi er is weakly guarded in the right-hand side of the de nition of A. 2

If every agent identi er is weakly-guardedly de ned then, for any agent P , there is a head normal form H such that SGE ` P = H Proof An easy case-analysis upon the structure of P . 2 From this, it is a not hard to show that SGE is complete for strong bisimilarity of nite agents. 36

Proposition 2

Proposition 3 (Completeness for nite agents) and Q, if P : Q then SGE ` P = Q. Proof Given in the companion paper 11].

For all nite agents P

2

5.2 Strong equivalence

De nition 3

The de nition of strong equivalence is now straightforward. A substitution is a function from N to N . We use to stand for a substitution, and post x substitutions in application. fyi=xig1 i n denotes the substitution for which xi = yi, 1 i n, and otherwise x = x. 2

P and Q are strongly equivalent, written P for all substitutions .

De nition 4

Q, if P

:

Q

Now, when the equality symbol = is interpreted as strong equivalence , all the laws of SGE hold except for rules M0 and E. The failure of M0 is clear; equations (38) and (39) indicate why E fails. On the other hand, a stronger form of rule C1 is valid: C10 From P = Q infer x(y):P = x(y):Q It may also be shown that recursive de nition preserves (though not : ) in an appropriate sense; thus strong equivalence is truly a congruence relation. Matching can be employed to yield a new form E0 of the expansion law which is valid for :

E0 Assume P = Pi i:Pi and Q = Pj j :Qj , where no

name free in Q (resp. P ); then infer

i

(resp. j ) binds a

P jQ =

X

i

i :(Pi

j Q) +

X

j

j :(P

j Qj ) +

i

X opp

j

xi = yj ] :Rij

where the relation i opp j ( i opposes j ) holds in four cases: 1. i is xi u and j is yj (v); then Rij is Pi j Qj fu=vg. 2. i is xi (u) and j is yj (v); then Rij is (w)(Pifw=ug j Qj fw=vg), where w is not free in (u)Pi or in (v)Qj . 3. i is xi (v) and j is yj u; then Rij is Pifu=vg j Qj . 4. i is xi (v) and j is yj (u); then Rij is (w)(Pifw=vg j Qj fw=ug), where w is not free in (v)Pi or in (u)Qj . We summarize these facts as follows: 37

Proposition 4 (Soundness)

The laws of SGE ? fC1; M0; Eg fC10 ; E0g are valid when = is interpreted as strong equivalence, . 2 This system is not complete for over nite agents. It may be possible to make it so by adding reasonable laws for matching, but we have not yet succeeded in this. An alternative and perhaps simpler way to axiomatise strong equivalence is given in Proposition 9 below. In Proposition 5 we give further useful laws of strong equivalence; they are important in the sense that, in exploring alternatives for the semantic de nition, we have found them { particularly the last two { a stringent test. It is no exaggeration to say that, without these laws, we would not feel justi ed in proposing the calculus.

Proposition 5 1. P j 0 P 2. P j Q Q j P 3. P j (Q j R) (P j Q) j R 4. (x)(P j Q) P j (x)Q if x 2 fn(P ) = Proof In the companion paper 11].

2

5.3 Recursion

We record here the properties which we would expect of recursive de nitions, by analogy with CCS 9]. First, if we transform the right-hand sides of de nitions, respecting , then the agent de ned is the same up to . Second, if two agents satisfy the same (recursive) equation, then they are the same up to ,: provided the equation satis es a standard condition. Both properties fail for , strong bisimilarity. In order to state these results, we need a few preliminaries. We assume a set of schematic identi ers, each having a nonnegative arity. In the following, X and Xi will range over schematic identi ers. An agent expression is like an agent, but may contain schematic identi ers in the same way as identi ers; in this section E; F will range over agent expressions.

e Let X have arity n, let x = x1 ; : : : ; xn be distinct names, and e assume that fn(P ) fx1; : : : ; xng. The replacement of X (x) by P in E , written ee e):= P g, means the result of replacing each subterm X (y) in E by P fy=xg. e E fX (x This extends in the obvious way to simultaneous replacement of several schematic e e identi ers, E fX1(x1 ):= P1; : : : ; Xm(xm ):= Pm g. 2

De nition 5

38

As an example, xy:X (x; x) + (y)X (x; y) fX (u; w):= uw:0g xy:xx:0 + (y)xy:0 In what follows, we assume the indexing set I to be either f1; : : : ; mg for some f m 1, or else !. We write X for a sequence X1; X2; : : : indexed by I ; similarly f, etc. We use i; j to range over I . When a sequence X of schematic identi ers f P e is implied by context, each with an associated name sequence xi , then it is cone e venient to write E fX1 (x1):= P1 ; : : : ; Xm(xm ):= Pmg simply as E (P1; P2; : : :), or f). If each Pi is Ai (xi ), we also write E (A1 ; A2 ; : : :) or E (A ). f e as E (P It is natural to de ne strong equivalence between agent expressions as equivalence under all replacements of schematic identi ers by agents:

De nition 6

Let E and F be two agent expressions containing only the e schematic identi ers Xi, each with associated name sequence xi. Then E F means that E (f) F (f) P P e for all f such that fn(Pi) xi for each i. P 2

We can now state our rst result, that recursive de nition preserves strong equivalence:

f Assume that E and f are agent expressions containing only F e the schematic identi ers Xi, each with associated name sequence xi . Assume f and B are identi ers such that for each i the arities of Ai , Bi and Xi are f that A equal. Assume that for all i: Ei Fi def f e Ai(xi ) = Ei(A ) f e Bi(xi ) def Fi(B ) = e e Then Ai(xi ) Bi (xi) for all i. 2

Proposition 6

If A is weakly guarded in E then intuitively, from the de nition Adef E , we can = unfold the behaviour of A uniquely. The next result makes this precise in the general case:

Proposition 7

f Assume that E are agent expressions containing only the e schematic identi ers Xi, each with associated name sequence xi , and that each Xi is weakly guarded in each Ej . Assume that f and f are agents such that P Q e e fn(Pi) xi and fn(Qi) xi for each i. Assume that for all i: Pi Ei (f) P f Qi E i (Q )

39

Then Pi

Qi for all i.

2

5.4 Distinctions

Having looked at the theories of both strong bisimilarity and strong equivalence, we now address the task of combining them into one. We shall let D range over distinctions. A substitution respects a distinction D if, for all (x; y) 2 D, x 6= y . 2

De nition 7 A distinction is a symmetric irre exive relation between names.

D

De nition 8 P and Q are strongly D-equivalent, written P

for all substitutions respecting D.

Q, if P

:

Q 2

Now it is quite natural to record, for certain pairs of agents, the distinction under which they are equivalent; D need involve only the names which are free in the agents. As a simple example, equation (38) can be strengthened to

xjy

fx;yg

x:y + y:x

(43)

Here we have used a natural abbreviation, allowing ourselves to write a set A N when we mean the distinction A A ? IdN , which keeps all members of A distinct from each other. (It may turn out that we only need distinctions of this simpler form, but we have not been able to assure ourselves of this.) Clearly, then, we have the two extreme cases

:

=

N

and

=

;

There are two useful operations upon distinctions. First, we de ne

Dnx def D ? (fxg N N fxg) =

This removes any constraint in D upon the substitution for x. Also, for any set A N of names, we de ne

DjA def D \ (A A) =

Proposition 8

by distinctions: 1. If D D0 then P D Q implies P 2. x = y]P fx;yg 0 3. If P D Q then (x)P Dnx (x)Q

The following properties hold for strong equivalence indexed

D

0

Q

40

4. If P 5. If P

Dnx

Q then y(x):P D y(x):Q D Q and A = fn(P; Q) then P

D jA

Q

2

Prop 8.1 needs little comment. Prop 8.2 is the proper strengthening of rule M0 in SGE. It also combines pleasantly with the modi ed expansion law E0; by using it, we can remove summands from an expansion provided we strengthen the distinction. As a very simple example, note rst that equation (41): x:P j y:Q ; x:(P jy:Q) + y:(x:P jQ) + x = y] :(P jQ) is an instance of E0; then using Prop 8.2 we can deduce x:P j y:Q fx;yg x:(P jy:Q) + y:(x:P jQ) (44) Props 8.3 and 8.4 neatly contrast the two kinds of name-binding. 8.3 indicates that since a restriction (x) itself preserves x distinct from other variables, there is no need to enforce the distinction by other means. On the other hand, 8.4 indicates the obligation, in proving equality of positive pre x forms, to allow the bound variable to range over all names. Note that, using 8.3, we can deduce from (44) that (x)(x:P j y:Q) ; (x)(x:(P jy:Q) + y:(x:P jQ)) This is a full equivalence, and compared with (41) it does not require the x = y] term because the restriction (x) enforces the distinction between x and y. (In passing, note that this expression simpli es further to y:(x)(x:P jQ) by R2, R3 and R4.) In contrast, using Prop 8.4 with D = ;, we deduce from (41) (45) z(y)(x:P j y:Q) ; z(y)(x:(P jy:Q) + y:(x:P jQ) + x = y] :(P jQ)) and the match cannot be discarded. Prop 8.5 merely asserts that, in an equation P D Q, only the free names in P and Q have any relevance in D. While Proposition 8 provides useful working laws, we do not need it to obtain a complete axiomatization of strong equivalence indexed by distinctions. This can trivially be done by adding the following law: D From P = Q , for all respecting D, infer P =D Q (A more re ned formulation of rule D actually con nes the hypothesis to nitely many distinct .)

Proposition 9

SGE fDg is sound, and complete over nite agents, when = and =D are interpreted as : and D respectively. Proof Directly from De nition 8. 2.

41

We now turn brie y to weak bisimilarity. Analogously with CCS, there is a notion of weak bisimilarity . , also called weak ground equivalence, which ignores the silent actions; it will be treated in a subsequent paper. As in CCS, this equivalence is not preserved by summation; also, like : , it is not preserved by positive pre x (since it is not preserved by substitution). These two defects can be remedied either separately or together; we thus arrive at three further equivalences, the third of which is a congruence:

5.5 Weak bisimilarity and equivalence

De nition 9

. 1. The agents P and Q are (weakly) ground-equal, written P ' Q, if P + . Q + R for all agents R. R 2. The agents P and Q are (weakly) equivalent, written P Q, if P . Q for all substitutions . . 3. The agents P and Q are (weakly) equal, written P ' Q, if P ' Q for all substitutions . 2

(Of course the last two may also be distinction-indexed, by constraining .) We shall not pursue these now, but merely point out that the laws of CCS are valid for weak ground equality. The laws are as follows:

Pre x

P0 : :P = :P P1 P + :P = :P P2 :(P + :Q) + :Q = :(P + :Q)

2

. Proposition 10 SGE fP0; P1; P2g is sound, when = is interpreted as ' .

We conjecture that this axiomatization is also complete for nite agents, but the details remain to be checked. We nish with a brief discussion of constants. In our examples in Section 4 we introduced constant names, and we now need to see how they are best handled. The key property of constants, in the general understanding of the term, is that they `stand for themselves'. In our context, this means simply that they are never instantiated. In particular, we therefore take the liberty { as in (23,24) for example { not to include them among the parameters of an agent identi er 42

5.6 Constants

A which uses them in its de nition. They could be so included, to meet the condition imposed on de ning equations in Section 2; then one would simply include them also in the parameter list of every use of A in agent expressions. More important is that, since constants will never be instantiated, they never run the risk of being identi ed with one another. Thus, while working in the theory, one may prove equations among agents which use certain constant names, e say v = fv1; : : : ; vng, and one may take advantage of their `constanthood' by e e e proving equations indexed by the distinction D = v (or, more explicitly, v v ? IdN ). In this working, one may by convention choose to omit the index D from equations. Later, one may wish to abstract from the particular choice of constant names. But this is the essence of Proposition 8.3 (or its analogue for '); from e any D-indexed equation P = D Q, with D = v, one can infer

e e (v)P = ; (v)Q

Thus the calculus re ects the idea that the di erence between constants and variables should not be sharply drawn.

43

6 Conclusion

An algebraic process calculus with mobility has been long in maturing. In 1979, before CCS was published, one of us (Milner) discussed with Mogens Nielsen at Aarhus the possibility of including such a notion at the outset, but we failed to see how to do it. It was not until the paper by Engberg and Nielsen 6] that the possibility was established; their semantic rules represent our starting point. In two ways it has been fortunate that the various process algebras { for example CSP 7], ACP 3] and CCS 9] { did not include mobility: First, they were thereby simpler, and yet presented many problems which were better tackled in a simpler setting; second, the situations in which mobility is needed have become more sharply de ned, and therefore the need more sharply felt, through experimental use of these algebras. There have been a number of formalisms which allow mobility, but have not developed its algebraic theory. The rst was Hewitt's Actor formalism. Hewitt's ideas on the changing con guration among actors were developed in the early 1970s; a semantic treatment is given by Clinger in his PhD thesis 5]. More recently, Kennaway and Sleep invented their LNET and DyNe formalisms specifically to describe parallel graph reduction processes, such as we present in Section 4, in the context of a project to design a parallel processor 15]. Also Astesiano and Zucca 2] have extended CCS to include parametric channels. Engberg and Nielsen 6] did not publish their report, and it has not received due attention, probably because its treatment of constants, variables and names is somewhat di cult. Many features of the -calculus are due to them, in particular: the replacement of CCS relabelling by syntactic substitution (crucial for formulation of the semantic rules); the semantic treatment of scope extrusion; the extension of the de nition of bisimulation to account for name parameters; the de nition of strong bisimilarity (which they call simply \strong equivalence"); and the soundness of most algebraic laws. We made many failed attempts to depart from their formulation. Our contribution has been: to remove all discrimination among constant names, variable names and values, yielding a more basic calculus; to discriminate between ground and non-ground equivalence (needed to replace the constant-variable discrimination); to strengthen the algebraic laws { in particular the expansion law { in order to achieve complete equational theories; to encode value-computations in the calculus in a tractable way (with the help of a new match construct); and to provide rather simple encodings of functional calculi { the -calculus and combinatory algebra.

44

References

1] Abramsky, S., The Lazy Lambda Calculus, to appear in Declarative Programming, ed. D. Turner, Addison Wesley, 1988. 2] Astesiano, E. and Zucca, E., Parametric channels via Label Expressions in CCS, Journal of Theor. Comp. Science, Vol 33, pp45{64, 1984. 3] Bergstra, J.A. and Klop, J-W., Algebra of Communicating Processes with Abstraction, Journal of Theor. Comp. Science, Vol 33, pp77{121, 1985. 4] Boudol, G., Towards a Lambda-Calculus for Concurrent and Communicating Systems, INRIA Sophia-Antipolis, private communication, 1988. 5] Clinger, W.D., Foundations of Actor Semantics, AI-TR-633, MIT Arti cial Intelligence Laboratory, 1981. 6] Engberg, U. and Nielsen, M., A Calculus of Communicating Systems with Label-passing, Report DAIMI PB{208, Computer Science Department, University of Aarhus, 1986. 7] Hoare, C.A.R., Communicating Sequential Processes, Prentice Hall, 1985. 8] Leinwand, S., Goguen, J.A. and Winkler, T., Cell and Ensemble Architecture for the Rewrite Rule Machine, Proc. International Conference on Fifth Generation Computing Systems, ICOT, pp869{878, 1988. 9] Milner, R., Communication and Concurrency, Prentice Hall, 1989. 10] Milner, R., Functions as Processes, Research Report 1154, INRIA, 1990. Also in abbreviated form in Proc. ICALP '90. 11] Milner, R., Parrow, J.G. and Walker, D.J., A Calculus of Mobile Processes, Part II, Report ECS-LFCS-89-86, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University, 1989. 12] Nielson, F., The Typed -calculus with First-class Processes, Report IDTR:1988-43, Inst. for Datateknik, Tekniske Hojskole, Lyngby, Denmark, 1988. 13] Ong, C-H.L., Fully Abstract Models of the Lazy Lambda Calculus, Proc 29th Symposium on Foundations of Computer Science, pp368{376, 1988. 14] Reisig, W., Petri Nets, EATCS Monographs on Theoretical Computer Science, ed. W.Brauer, G.Rozenberg, A.Salomaa, Springer Verlag, 1983. 45

15] Sleep, M.R. and Kennaway, J.R., The Zero Assignment Parallel Processor (ZAPP) Project, in The Distributed Computing Systems Programme, ed. D.A.Duce, Peter Peregrinus Ltd., pp250{269, 1984. 16] Thomsen, B., A Calculus of Higher-order Communicating Systems, Proc POPL Conference, 1989.

46

赞助商链接

- Seamless mobile computing on fixed infrastructure
- 可信计算的安全防护机制及其在高可信网络中的应用
- CH4 二元关系和函数 1 二元关系的基本概念
- PI演算观察等价的推理系统
- 我国可信计算研究与发展
- A calculus of mobile agents
- Stochastic calculus of variations for general L'evy processes and its applications to jump-
- Local -Calculus At Work Mobile Objects As Mobile Processes
- A Calculus of Distributed and Parallel Processes - An Approach Using Linear Logic and Algeb
- A typed calculus of synchronous processes
- A Short Introduction to Diffusion Processes and Ito Calculus
- Combinatory representation of mobile processes
- Mobile Calculus Semantics of Concurrent
- Common Sense of a Mobile Robot and the Consistency of Event Calculus
- THE LAYOUT AND MAIN PARTS OF AUTOMOBILE

更多相关文章：
更多相关标签：