A Calculus for Concurrent Processes with Constraints ^{∗}

Juan Francisco DIAZ FRIAS ^{†} Camilo RUEDA ^{‡} Frank D. VALENCIA POSSO ^{§}

August 29, 1997

Abstract

The π-calculus is a formal model of concurrent computation based on the notion of naming. It has an important role to play in the search for more abstract theories of concurrent and communicating systems. In this paper we extend the π-calculus with constraints by adding the notion of constraint agent to the standard π-calculus concept of agent. We call this extension the π^{+}-calculus. We also extend the notion of barbed bisimulation to define behavioral equivalence in the π^{+}-calculus and then we use the extended notion to characterize some equivalent behaviors derived ¿from constraint agents. This paper also includes interesting uses of the extended calculus showing the transparent interaction of constraints and communicating processes.

Keywords: Concurrent Programming, Constraint Programming, π-calculus, π^{+}-calculus, Formal Calculi, Mobile Processes.

1 Introduction

Research on multiparadigm languages has known increasing interest in the last years. The integration of what appears to be fundamentally different notions of programming has come up as a real need in some domains. One salient example is the realm of computer supported musical composition. Composers define complex hierarchical structures representing multiple musical dimensions which are to evolve according to either (or both) predetermined trajectories or to satisfaction of a set of compositional rules supplying partial structural information. Both Object-Oriented and Constraint programming paradigms easily come to mind as relevant for devising music composition tools capable of effectively handling such interactions.

Constraint Programming paradigm is a simple and powerful model of computation obtained by internalizing the notion of computation as deduction over (first-order) systems of partial information. The basic move in this paradigm is to replace the notion of store-as-valuation central to von Neumann computing with the notion that the store is a constraint, that is, pieces of partial information about the values that variables can take [Sar93]. The traditional notions of “read” and “write” are replaced by the notions of ask and tell. An ask operation (instead of read) is executed to check whether or not the store entails a given constraint (i.e., whether every valuation permitted by the store is permitted by the constraint). A tell operation (instead of write) is executed to add a given constraint to store. A tell operation does not change the value of a variable, but may rule out certain values that were previously possible. In this sense the store is monotonically refined by using tell operations. Thus, in Constraint Programming, computation progresses by accumulating constraints in the store, and by checking whether the store entails constraints.

∗This work is supported in part by grant 1251-14-041-95 from Colciencias-BID.

†Associate Professor, Computer Science Department, Faculty of Engineering, Universidad del Valle, Colombia.

Member of AVISPA team and GEDI team. E-mail: jdiaz@borabora.univalle.edu.co.

‡Associate Professor, Faculty of Engineering, Pontificia Universidad Javeriana Cali, Colombia. Chief of AVISPA team and member of GEDI team. E-mail: crueda@atlas.ujavcali.edu.co.

§Instructor of Programm Verification, Faculty of Engineering, Pontificia Universidad Javeriana Cali, Colombia. Member of AVISPA team. E-mail: fvalenci@atlas.ujavcali.edu.co.

The need to establish a firm base for the integration of programming models has led to the design of formal calculi for a variety of paradigms. One approach in this direction is to devise a calculus for a particular paradigm and then show how to simulate the others in the calculus [NM95]. A more direct approach is to include the notions of the integrated paradigms in a new calculus [Vas94]. In our quest for the foundations of a computer music language we favor the strategy of relying on minimal orthogonal extensions to calculi that have already found an established place in the programming language community. We have chosen as our point of departure the π-calculus [MPW92, Mil91], a well known, elegant and simple model of concurrent computation.

Having concurrency in the calculus appeals to us because it is at the heart of the musical craft and also because we believe it is fundamental to both Object-Oriented and Constraint Programming. Indeed, several tell and/or ask operations can be executed simultaneously using blocking ask as mechanism of synchronization, that is, blocking (agents executing) ask operations until there exists enough information to entail them.

To our knowledge there has been no attempt to encode first-order constraints into the π-calculus nor to orthogonally extend the π-calculus to include them. The κ-calculus [Smo94b] considers only equational constraints, whereas [VP96] shows that equational constraints can be encoded into the π-calculus.

In this paper we define the π^{+}-calculus, an orthogonal extension of the (polyadic) π-calculus. In the π^{+}-calculus the notion of constraint agent interacting with a store is added to the standard π-calculus concept of agent. In this way communication between processes can be parametric in a constraint system. Constraint agents perform the basic Ask and Tell operations of Concurrent Constraint Programming (CCP) languages, thus adding to the π-calculus processes synchronization via blocking ask. The semantics of the extension is defined operationally in a similar way as the one given for the cc-model in [Sar93]. We illustrate the definition of recursive processes in the π^{+}-calculus and discuss the representation of cells providing a notion of state compatible with concurrency and constraints.

We also extend the concept of barbed bisimulation [MS92] to define behavioral equivalence and to characterize equivalent behaviors derived from constraint agents.

In sections 2, 3, and 4 we present the syntax and semantics of the π^{+}-calculus and discuss some examples. The proposed syntax adds constraint agents to the standard π-calculus agents.

In section 5 we define a notion of behavioral equivalence for our calculus, in a similar way as it was done for the π-calculus [MPW92, Mil91]. Finally, section 6 shows conclusions and section 7 presents future work.

2 Syntax

The syntax of the π^{+}-Calculus is given in Table 1. There are only two kinds of entities in the πcalculus: Channels and Agents (or Processes). The π^{+}-calculus adds Constraint agents and agents declaring variables to the standard π-calculus agents. In the π-calculus, names denote channels. The π^{+}-calculus also allows variables and primitive values to be channels.

Normal Processes:

M, N ::= π.P Agent under prefix

| M + N  Summation

| O Inaction or null process

Constraint agents: R  ::= !ϕ.P  Tell agent
| ?ϕ.P  Ask agent

Agents (or processes)

P, Q

::= (υa)P

New name a in P

| (υx)P New variable x in P

| P | Q  Composition
| N  Normal process
| ∗P  Replicated agent
| R  Constraint agent
Channels C  ::= a  Name
| v  Value
| x  Variable
Prefixes: π  ::= C?[x_{1} … x_{n}] Reading prefix
| C![C_{1} … C_{n}] Writing prefix

Table 1: π^{+}-calculus syntax

In what follows, we describe the agents informally. In an agent π.P the prefix π represents an atomic action, the first action performed by π.P and P represents the continuation of π.P. When π is a writing prefix C![C_{1} … C_{n}], π.P means “send C_{1}, …, C_{n} along channel C and then activate P ”. When π is a reading prefix C?[x_{1} … x_{n}], π.P means “receive the arguments, say x_{1}, …, x_{n}, along channel C, use them in P and then activate P ”. In both cases C is called the subject of π.

The summation form M + N represents a process able to take part in one -but only one - of two alternatives for communication. The choice of one alternative precludes the other. The null process 0 is the process doing nothing.

Constraint agents are new kind of agents whose behavior depends on a global store. A store contains information given by constraints. The Tell agent !ϕ.P means “Add ϕ to the store and then activate P.” The Ask agent ?ϕ.P means “Activate P if constraint ϕ is a logical consequence of the information in the store”

The agent (υa)P restricts the use of the name a to P. Another way to describe this is that (υa)P declares a new unique name a, distinct from all external names, for use in P. Similarly, (υx)P (new agent) declares a new variable x, distinct from all external variables in P.

The agent P | Q means that P and Q are concurrently active, so they can act independently (and possibly communicate). ∗P “Bang P ” means P | P …( as many copies as you wish ). The operator ∗ is called replication. A common instance of replication is ∗π.P; a resource which can only be replicated when a requester communicates via π.

Usually, agents of the form π.O are written π. We also omit the .O in the constraint agents !ϕ.O and ?ϕ.O

In the next section, we describe formally the behavior of agents.

3 Operational Semantics

3.1 Constraint System

The π^{+}-calculus is parametrized in a Constraint System. For our purposes it will suffice to found the notion of constraint system on first-order Predicate Logic, as it was done in [Smo94b, Smo94a]

1. A Constraint System consists of [Smo94b, Smo94a]:

• A signature Σ ( a set of functions, constants and predicate symbols with equality) including a distinguished infinite set, N , of constants called names denoted as a, b, …, u. Other constants, called values, are written v_{1}, v_{2}, ….

• A consistent theory Δ (a set of sentences over Σ having a model) satisfying two conditions:

1. Δ ⊧ ¬(a = b) for every two distinct names a, b.

2. Δ ⊧ ϕ ↔ ψ for every two sentences ϕ, ψ over Σ such that ψ can be obtained ¿from ϕ by permutation of names.

Often Δ will be given as the set of all sentences valid in a certain structure (e.g. the structure of finite trees, integers, or rational numbers). Given a constraint system, symbols ϕ, ψ, … denote first-order formulae in Σ, henceforth called constraints. We say that ϕ entails ψ in Δ, written ϕ ⊧_{Δ} ψ, iff ϕ → ψ is true in all models of Δ. We say that ϕ is equivalent to ψ in Δ, written ϕ ⊧|_{Δ}ψ, iff ϕ ⊧_{Δ} ψ and ψ ⊧_{Δ} ϕ. We say that ϕ is satisfiable in Δ iff ϕ |̸=⊥ . We use ⊥ for the constraint that is always false and ⊤ for the constraint that is always true.

As usual, we will use infinitely many x, y, … ∈ V to denote logical variables, designating some fixed but unknown element in the domain under consideration. The sets fv(ϕ) ⊂ V and bv(ϕ) ⊂ V denote the sets of free an bound variables in ϕ, respectively. Finally, fn(ϕ) ⊂ N is the set of names appearing in ϕ.

1There exist more general and foundationally less heavy alternatives for setting up the notion of a constraint system (e.g [Sar93]); however, by taking Predicative Logic as the starting point, we can build on well-established intuitions, notions and notations, and proceed quickly to the issues we want to bring across.

As we said before, constraint agents act relative to a store. A store is defined in terms of the underlined constraint system:

Definition 3.1 (Store) A store S = ϕ_{1} ∧ ϕ_{2} ∧ … ∧ ϕ_{r} (with r ≥ 0) is a constraint in Σ. When r = 0, S is said to be the empty store (i.e., S = ⊤). When S ⊧_{Δ}⊥, S is said to be the unsatisfiable store.

The operational semantics of the π^{+}-calculus will be defined in terms of a equivalence relation, ≡_{π^{+}}, on configurations describing computation states and a one-step reduction relation, ⟶ describing transitions on these configurations. A configuration is a tuple ⟨P; S⟩ consisting of an agent P and a store S.

3.2 Structural Congruence and equivalence on configurations

We identify first the binding operators in the π^{+}-calculus: The binding operator for names is (υa)P which declares a new name a in P. There are two binding operators for variables: (υx)P which binds x in P and C?[x_{1} … x_{n}].P which declares formal parameters x_{1}, …, x_{n} in P. So we can define free names fn(P), bound names bn(P), free variables fv(P), bound variables bn(P) of a process P in the usual way. In a similar way as [Mil91] we define structural congruence for the π^{+}-calculus.

Definition 3.2 (Structural Congruence) Let structural congruence, ≡, be the smallest congruence relation over agents which satisfies the following axioms:

• Agents are identical if they only differ by a change of bound variables or bound names.

• (N P/ ≡, +, O) and (A/ ≡, |, O) are symmetric monoids, where N P and A are the set of normal processes and agents respectively.

• ∗P ≡ P | ∗ P.

• (υa)O ≡ O, (υx)O ≡ O, (υ > a)(υb)P ≡ (υb)(υa)P, (υx)(υy)P ≡ (υy)(υx)P, (υa)(υx)P ≡ (υx)(υa)P.

• If a ∉ fn(P) then (υa)(P | Q) ≡ P | (υ > a)Q.

• If x ∉ fv(P) then (υx)(P | Q) ≡ P | (υx)Q.

• If ϕ ⊧|_{Δ}ψ and P ≡ Q then !ϕ.P ≡!ψ.Q and ?ϕ.P ≡?ψ.Q

Definition 3.3 (π^{+}-equivalence relation on configurations) We will say that < P_{1}; S_{1} > is π^{+}-equivalent to < P_{2}; S_{2} >, written < P_{1}; S_{1} >≡_{π^{+}}< P_{2}; S_{2} >, if P_{1} ≡ P_{2}, S_{1} ⊧|_{Δ}S_{2}, fn(S_{1}) = fn(S_{2}) and fv(S_{1}) = fv(S_{2}). ≡_{π^{+}} is said to be the π^{+}-equivalence relation on configurations.

The behavior of an agent P is defined by transitions from an initial configuration ⟨P; ⊤⟩ . A transition, ⟨P; S⟩ ⟶ ⟨P′; S′⟩ , means that ⟨P; S⟩ can be transformed into ⟨P′; S′⟩ by a single computational step. For simplicity, we assume that all variables and names are declared in the initial configuration i.e., fv(P) = fn(P) = ∅. We define transitions on configurations next.

3.3 Reduction relation

The reduction relation ,⟶, over configurations is the least relation satisfying the following rules:

COMM: \frac{S⊧_{Δ}C=C′}{⟨((M + C?[x_{1}...x_{n}].Q) | (N+C′![C_{1}...C_{n}].P));S⟩⟶⟨(Q\{C_{1},...,C_{n}/x_{1},...,x_{n}\} | P);S⟩}

COMM describes the communication between two normal processes C?[x_{1} … x_{n}].Q and C′![C_{1} … C_{n}].P appearing in a summation, which are sending and receiving along the same channel. We decide from the store whether they are using the same channel. In this sense we can say that the store controls the communication in the π^{+}-calculus. Agent Q {C_{1}, …, C_{n}/x_{1}, …, x_{n}} is obtained by replacing, in parallel, every free occurrence of x_{1}, …, x_{n} by C_{1}, …, C_{n}, respectively. Notice that the remaining normal processes, M and N, are discarded, since at most one component of a summation is allowed to execute.

The rules ASK and TELL describe the interaction between constraint agents and the store.

TELL: ⟨!ϕ.P; S⟩ ⟶ ⟨P; S ∧ ϕ⟩

ASK: \frac{S⊧_{Δ}ϕ}{⟨?ϕ.P;S⟩⟶⟨P;S⟩} , \frac{S⊧_{Δ}¬ϕ}{⟨?ϕ.P;S⟩⟶⟨O;S⟩}

TELL is the way of adding information to the store. It says that !ϕ.P adds the constraint ϕ to store S and then activates its continuation P. Such augmentation of the store is the major mechanism in CCP languages for an agent to influence other agents in the system [Sar93]. For example, agent !(x = a).P tells agent x![C_{1} … C_{n}].Q that its communication channel is now fixed to a.

ASK is the way of obtaining information from the store. It says that P can be activated if the current store S entails ϕ, or discarded when S entails ¬ϕ. For instance, agent ?(x = a∨x = b).x![C_{1} … C_{n}].P is able to send C_{1} … C_{n} along a channel x, just in case x is either channel a or channel b.

An Ask agent that cannot be reduced in the current store S is said to be suspended by S. An agent suspended by S might be reduced in some augmentation of S. In the previous example ?(x = a ∨ x = b).x![C_{1} … C_{n}].P is suspended by the empty store, but if a Tell agent adds x = a to this store, it can be reduced.

PAR: \frac{⟨P;S⟩⟶⟨P′;S′⟩}{⟨Q | P;S⟩⟶>⟨Q | P′;S′⟩}

DEC-V: \frac{x∉fv(S)  ⟨P;S≫\{x\}⟩⟶⟨P′;S′⟩}{⟨(υx)P;S⟩⟶⟨P′;S′⟩} , DEC-N: \frac{a∉fn(S)  ⟨P;S≫\{a\}⟩⟶⟨P′;S′⟩}{⟨(υa)P;S⟩⟶⟨P′;S′⟩}

PAR says that reduction can occur underneath composition. DEC-V is the way of introducing new variables. By S ≫ {C_{1}, …, C_{n}} we mean the store S ∧ C_{1} = C_{1} ∧ … ∧ C_{n} = C_{n}, which is obviously equivalent to S. Thus, we add variable x ∉ fv(S) to the store by S ≫ {x} ensuring that x will not be used in following declarations. In the case that x ∈ fv(S) we can rename x with a new variable z ∉ fv(S)∪fv(P) by using the first item of Definition 3.2 (i.e. (υx)P ≡ (υz)P {z/x} if z ∉ fv(P)). DEC-N is defined in a similar way.

Rule EQUIV simple says that π^{+}-equivalent configurations have the same reductions.

EQUIV: \frac{⟨P_{1};S_{1}⟩≡_{π+}⟨P′_{1};S′_{1}⟩  ⟨P_{2};S_{2}⟩≡_{π+}⟨P′_{2};S′_{2}⟩  ⟨P_{1};S_{1}⟩⟶⟨P_{2};S_{2}⟩}{⟨P′_{1};S′_{1}⟩⟶⟨P′_{2};S′_{2}⟩}

It is easy to see that the π-calculus is a special case of the π^{+}-calculus parametrized in a minimal constraint system (i.e. a constraint system including only names in the domain under consideration), without resorting to constraint agents.

In what follows, ⟹ will denote the reflexive and transitive closure of ⟶. Finally, we will say that ⟨P′; S′⟩ is a derivative of ⟨P; S⟩ iff ⟨P; S⟩ ⟹ ⟨P′; S′⟩ .

Runtime failure. In the cc-model [Sar93], the invariant property of the store is that it is satisfiable. This can be done in the π^{+}-Calculus by performing a transition from ⟨!ϕ.P; S⟩ iff S ∧ϕ is satisfiable, otherwise reducing to a distinguished configuration called fail, which denotes a runtime failure. This runtime failure is propagated thereafter in the usual way. For the sake of simplicity we do not consider runtime failures, but we can add these rules orthogonally, as in [Tur95], without affecting any of our results.

Potentiality of reduction. Whenever we augment the store, we may increase the potentiality of reduction, that is, the number of possible transitions from a configuration. The following proposition states that any agent P′ obtained from a configuration ⟨P; S_{1}⟩ can be obtained from a configuration ⟨P; S_{2}⟩, S_{2} being an augmentation of S_{1}.

Proposition 3.4 If S_{2} ⊧_{Δ} S_{1} and ⟨P_{1}; S_{1}⟩ ⟶ ⟨P_{2}; S′_{1}⟩ then ⟨P_{1}; S_{2}⟩ ⟶ ⟨P_{2}; S′_{2}⟩ and S′_{2} ⊧_{Δ} S′_{1}.

Proof: Straightforward from rules TELL, COMM and ASK:

1. Transitions using ASK or COMM: Since S_{2} ⊧_{Δ} S_{1}, for any constraint ϕ such that S_{1} ⊧_{Δ} ϕ we have S_{2} ⊧_{Δ} ϕ. Thus, any P_{2} obtained by using ASK or COMM in ⟨P_{1}; S_{2}⟩ can be obtained by using the same rule for ⟨P_{1}; S_{2}⟩ . Neither ASK nor COMM modify the store, therefore S′_{2} ⊧_{Δ} S′_{1}.

2. Transitions using TELL: TELL does not consider the store as premise, but it modifies it. In this case P_{1} ≡!ϕ.Q. For the transition ⟨!ϕ.Q; S_{1}⟩ ⟶ ⟨Q; S_{1} ∧ ϕ⟩ we have ⟨!ϕ.Q; S_{2}⟩ ⟶ ⟨Q; S_{2} ∧ ϕ⟩. Thus, S′_{2} ⊧_{Δ} S′_{1}.

3. Transitions using EQUIV: If ⟨P_{1}; S_{1}⟩ ≡_{π^{+}} ⟨P_{3}; S_{3}⟩ and ⟨P_{3}; S_{3}⟩ ⟶ ⟨P′_{3}; S′_{3}⟩ , where ⟨P′_{3}; S′_{3}⟩ ≡_{π^{+}} ⟨P_{2}; S′_{1}⟩ , then from 3.3 we have S_{2} ⊧_{Δ} S_{3} and P_{1} ≡ P_{3}. The desired result is obtained by applying inductively items 1,2,3,4,5.

4. Transitions using DEC-V or DEC-N: In this case P_{1} ≡_{π^{+}} (υx)Q. Suppose first that x ∉ fv(S_{2}). If x ∉ fv(S_{1}) we have S_{2} ≫ {x} ⊧_{Δ} S_{1} ≫ {x}. If x ∈ fv(S_{1}), then using 3.2 (i.e. (υx)Q ≡ (υz)Q{z/x} if z ∉ fv(Q), x was replaced in P_{1} by a new variable, z, such that z ∉ fv(S_{1}). For any z we have S_{2} ≫ {x} ⊧_{Δ} S_{1} ≫ {z}. Similarly, if x ∈ fv(S_{2}) it is easy to see that for any y, S_{2} ≫ {y} ⊧_{Δ} S_{1} and for any z, S_{2} ≫ {x} ⊧_{Δ} S_{1} ≫ {z}. Thus, the desired result is obtained by applying inductively items 1,2,3,4,5.

5. Transitions using PAR: PAR does not consider the store (directly) as a premise, therefore the desired result is obtained by applying inductively items 1,2,3,4,5.

In the following example we will describe the behavior of an agent to clarify our semantics.

Example 3.5 Agent P_{1} sends along channel r the greater of two numbers x and y, which is then used by Q. Let Δ be the set of all sentences valid in the rational numbers.

P_{1} ≡ (υx)P_{2}; P_{2} ≡ (υy)P_{3}; P_{3} ≡ (υr)P_{4}; P_{4} ≡ (r?[z].Q | ?(x > y).r![x] | ?¬(x > y).r![y] | !(x = y + 1)), i.e., P_{1} ≡ (υx)(υy)(υr)(r?[z].Q | ?(x > y).r![x] | ?¬(x > y).r![y] | !(x = y + 1)).

Since the variable declarations are different, by DEC-V, the derivatives of ⟨P_{1}; ⊤⟩ are the derivatives of ⟨P_{2}; ⊤ ≫ {x}⟩ , whose derivatives are the derivatives of ⟨P_{2}; ⊤ ≫ {x, y}⟩ . By DEC-N (remember that r denotes a name) the derivatives of ⟨P_{2}; ⊤ ≫ {x, y}⟩ are the derivatives of ⟨P_{4}; ⊤ ≫ {x, y, r}⟩ if any. The Ask agents in P_{4} are suspended by ⊤ ≫ {x, y, r}, and there is no other agent sending along channel r, so we can only reduce ⟨P_{4}; ⊤ ≫ {x, y, r}⟩ by applying TELL combined with PAR and EQUIV. Thus,

⟨P_{4}; ⊤ ≫ {x, y, r}⟩ ⟶ ⟨(r?[z].Q | ?(x > y).r![x] | ?¬(x > y).r![y] | 0); ⊤ ≫ {x, y, r} ∧ x = y + 1⟩ .

Now using ASK combined with PAR and EQUIV, ⟶ ⟨(r?[z].Q | r![x] | ?¬(x > y).r![y] | 0); ⊤ ≫ {x, y, r} ∧ x = y + 1⟩ .

We can eliminate the null process by using ≡_{π^{+}}, ≡_{π^{+}} ⟨(r?[z].Q | r![x] | ?¬(x > y).r![y]); ⊤ ≫ {x, y, r} ∧ x = y + 1⟩ .

Using ASK combined with PAR, ⟶ ⟨(r?[z].Q | r![x] | 0); ⊤ ≫ {x, y, r} ∧ x = y + 1⟩ .

Using ≡_{π^{+}} we can rewrite the processes so they can have the correct format for COMM, and eliminate the null process,

≡_{π^{+}} ⟨((r?[z].Q + 0) | (r![x] + 0)); ⊤ ≫ {x, y, r} ∧ x = y + 1⟩ .

Finally, applying COMM and ≡_{π^{+}}, ⟶ ⟨(Q{x/z} | 0); ⊤ ≫ {x, y, r} ∧ x = y + 1⟩ . ≡_{π^{+}} ⟨Q{x/z}; ⊤ ≫ {x, y, r} ∧ x = y + 1⟩

Thus, ⟨P_{1}; ⊤⟩ ⟶ ⟨Q{x/z}; ⊤ ≫ {x, y, r} ∧ x = y + 1⟩ .

Names and Variables. In the π-calculus there is no difference between names and variables [Smo94b]. Names, conveniently used, provides a unique reference to concurrent objects and can also be used for data encapsulation as in [Tur95]. In the π^{+}-calculus Names and Variables are considered different because of the presence of constraints.

We first give an example to illustrate the difference. Let P_{1} ≡ (υx)(υy)(?¬(x = y).Q) and P_{2} ≡ (υa)(υb)(?¬(a = b).Q) and let Δ be the set of sentences valid in the natural numbers. It is easy to see that ⟨P_{2}; ⊤⟩ ⟶ ⟨Q; ⊤ ≫ {a, b}⟩ . However, since ?¬(x = y).Q is suspended by ⊤ ≫ {x, y}, there is no reduction for ⟨P_{1}; ⊤⟩ .

Finally, we take from [Smo94b] a proposition which states that names are different from any other value that can be uniquely described by a formula:

Proposition 3.6 . Let ϕ be a constraint such fv(ϕ) = {x}, and such that ϕ determines x, that is, Δ ⊧ ∃!xϕ. Then Δ ⊧ ¬ϕ{a/x} for every name a not occurring in ϕ.

Proof: The proof is based on conditions (1) and (2) of the underlined constraint system. See [Smo94b].

4 Using the π^{+}-calculus

4.1 Recursive process definitions

We often wish to define process recursively. For instance suppose you want to define the addition of the natural numbers x, y, returning the result along channel z. This can be done as follows (consider a constraint system providing equations, inequations, natural numbers and the succesor function):

D_{1}(x, y, z) =^{def} (?y > 0.(υx_{1})(υy_{1})(!(x_{1} = succ(x)) | !(succ(y_{1}) = y) | D_{1}(x_{1}, y_{1}, z))) | ?y = 0.z![x].

Recursively-defined processes have the form D(x_{1}, …, x_{n}) =^{def} P, where P may contain occurrences of D (perhaps with different arguments), fv(P) ⊆ {x_{1}, …, x_{n}} and fn(P) = ∅. When no confusion arises we write D (without arguments) instead of D(x_{1}, …, x_{n}) =^{def} P.

However ”definition-making” is not a primitive, since it can be easily encoded using replication as in [Milner, 91] and [Turner, 95]. The idea is to replace each definition D(x_{1}, …, x_{n}) =^{def} P (i.e. D) by the process ∗d_{1}?[x_{1} … x_{n}].P (where d is a new channel) and every call D(C_{1}, …, C_{n}) by the process d![C_{1} … C_{n}]. We give an example to clarify this idea.

Example 4.1 Let Q = (υr)(υx)(D_{1} | D_{1}(x, 1, r) | !(x = 5) | r?[z].Q_{1}) be a context including the process definition of the previous example, D_{1}, and a call to it. Intuitively, we expect that ⟨Q; ⊤⟩ ⟹ ⟨D_{1} | Q_{1}{x_{1}/z}; … ∧ x = 5 ∧ x_{1} = succ(x) ∧ …⟩ .

In the translation, D_{1} is replaced by an agent P, where P ≡ ∗d_{1}?[xyz].(?y > 0.((υx_{1})(υy_{1})(!(x_{1} = succ(x)) | !(succ(y_{1}) = y) | d_{1}![x_{1}y_{1}z])) | ?y = 0.z![x]).

Context Q is replaced by agent Q′, where Q′ ≡ (υd_{1})(υr)(υx)(P | d_{1}![x1r] | !(x = 5) | r?[z].Q_{1}).

Finally, note that ⟨Q′; ⊤⟩ ⟹ ⟨P | Q_{1}{x_{1}/z}; ⊤ ≫ {d_{1}, r, x_{1}, y_{1}} ∧ x = 5 ∧ x_{1} = succ(x) ∧ succ(y_{1}) = y⟩ .

4.2 Encoding Cells

Cells are useful for modelling mutable data structures. They are syntactical entities in the concurrent constraint calculi ρ and γ [Smo94b]. A cell a : C can be thought of as a location a whose current contents is C. In the π^{+}-calculus, cells can be encoded as follows:

Definition 4.2 (Cell generator) The  cell  generator  agent  is  defined  as:

D_{2}(x, y) =^{def} x?[x_{1}x_{2}].(x_{1}![y].D_{2}(x, y) + x_{2}?[z].D_{2}(x, z)). A cell a : C is obtained by an invocation to the cell generator; i.e. [[a : C]] =^{def} D_{2} | D_{2}(a, C).

A cell containing the value 5 in location a is [[a : 5]] , a cell containing a value greater than 10 in location b is (υx)([[b : x]] | !(x > 10)) . The contents of the cell can be read along a channel x_{1} or updated by sending a new value along a channel x_{2}. The summation operator in the cell generator ensures that read and update request cannot be executed concurrently. Thus, when an update request has been accepted, all subsequent read requests will be answered with the updated contents of the cell.

For instance the agent [[a : 5]] | (υr)(υu)(a![ru].r?[z].Q) reads the contents of the cell [[a : 5]] along channel r, which is then used by Q. Note that:

⟨[[a : 5]] | (υr)(υu)(a![ru].r?[z].Q; ⊤⟩ ⟹ ⟨D_{2} | (r![5].D_{2}(a, 5) + u?[z].D_{2}(a, z)) | r?[z].Q; ⊤ ≫ {r, u}⟩
⟹ ⟨D_{2} | D_{2}(a, 5) | Q{5/z}; ⊤ ≫ {r, u}⟩
≡_{π^{+}} ⟨[[a : 5]] | Q{5/z}; ⊤ ≫ {r, u}⟩

The process [[a : 5]] | (υr)(υu)(a![ru].u![4]) updates (decreases) the contents of the cell [[a : 5]] by using channel u. Note that:

⟨[[a : 5]] | (υr)(υu)(a![ru].u![4]; ⊤⟩ ⟹ ⟨D_{2} | (r![5].D_{2}(a, 5) + u?[z].D_{2}(a, z)) | u![4]; ⊤ ≫ {r, u}⟩
⟹ ⟨D_{2} | D_{2}(a, 4) | 0; ⊤ ≫ {r, u}⟩
≡_{π^{+}} ⟨[[a : 4]] ; ⊤ ≫ {r, u}⟩

A common operation in cells, written ayC, is called Exchange. It records the current contents of the cell in a variable y and replaces it by C. Obviously Exchange can be implemented in three steps: reading the contents of the cell, recording this contents in y by using a Tell agent, and finally updating the contents with C. The definition of exchange is:

D_{3}(x, y, z) =^{def} (υr)(υu)(x![ru].r?[z_{0}].!(y = z_{0}).x![ru].u![z])

Thus, exchange operation [[ayC]] is defined as:

[[ayC]] =^{def} D_{3} | D_{3}(a, y, C)

For instance the agent P ≡ ([[a : 5]] | (υx) [[ax4]]) transforms [[a : 5]] into [[a : 4]] and records its old contents in a new variable x. Note that:

⟨P; ⊤⟩ ⟹ ⟨D_{2} | D_{3} | (r![5].D_{2}(a, 5) + u?[z].D_{2}(a, z)) | r?[z].!(x = z).a![ru].u![4]; ⊤ ≫ {x, r, u}⟩
⟹ ⟨D_{2} | D_{3} | D_{2}(a, 5) | !(x = 5).a![ru].u![4]; ⊤ ≫ {x, r, u}⟩
⟹ ⟨D_{2} | D_{3} | D_{2}(a, 5) | a![ru].u![4]; ⊤ ≫ {x, r, u} ∧ x = 5⟩
⟹ ⟨D_{2} | D_{3} | D_{2}(a, 4); ⊤ ≫ {x, r, u} ∧ x = 5⟩
≡_{π^{+}} ⟨D_{3} | [[a : 4]] ; ⊤ ≫ {x, r, u} ∧ x = 5⟩

5 Behavioral equivalence

In the π-calculus, barbed bisimulation [MS92] equates agents that can match each other’s interaction and can communicate on the same channels at each step. For each channel C, the latter is expressed by means of an observation predicate ↓_{C} detecting the possibility of performing a communication with the external environment along C. We take from [Mil91] the notions of unguardness and observability and modify them by parametrizing in a store (the store controls the communication in the π^{+}-calculus, anyhow).

Definition 5.1 (Observability in the π^{+}-calculus) An agent P occurs unguarded in Q iff it has some occurrence in Q which is not under a prefix or within a constraint agent. An agent Q is observable at C in a store S, written Q ↓_{C}^{S}, iff some π.P′ occurs unguarded in Q and S ⊧_{Δ} C = C′, where C′ is the subject of π and it is not bound by a binding operator (υx) or (υa). More precisely, given a channel C:

\begin{matrix}O ↓̸_{C}^{S} . & (υa)P ↓_{C}^{S} iff P ↓_{C}^{S} and S ⊧_{Δ} C ≠ a. \\ !ϕ.P ↓̸_{C}^{S} . & (υx)P ↓_{C}^{S} iff P ↓_{C}^{S} and S ⊧_{Δ} C ≠ x. \\ ?ϕ.P ↓̸_{C}^{S} . & (P | Q) ↓_{C}^{S} iff P ↓_{C}^{S} or Q ↓_{C}^{S} . \\ C′![x_{1} … x_{n}].P ↓_{C}^{S} iff S ⊧_{Δ} C = C′. & > (P + Q) ↓_{C}^{S} iff P ↓_{C}^{S} or Q ↓_{C}^{S} . \\ C′?[x_{1} … x_{n}].P ↓_{C}^{S} iff S ⊧_{Δ} C = C′. & ∗P ↓_{C}^{S} iff P ↓_{C} . \end{matrix}

Definition 5.2 (Strong π^{+}- reduction equivalence) (Strong) π^{+}- reduction equivalence (or π^{+}-barbed bisimulation), ˙∼_{π^{+}}, is the largest equivalence relation R over configurations such that (⟨P_{1}; S_{1}⟩, ⟨P_{2}; S_{2}⟩) ∈ R implies:

1. If ⟨P_{1}; S_{1}⟩ ⟶ ⟨P′_{1}; S′_{1}⟩ then ⟨P_{2}; S_{2}⟩ ⟶ ⟨P′_{2}; S′_{2}⟩ for some ⟨P′_{2}; S′_{2}⟩ such that (⟨P′_{1}; S′_{1}⟩ , ⟨P′_{2}; S′_{2}⟩) ∈ R.

2. For each channel C if P_{1} ↓_{C}^{S_{1}} then P_{2} ↓_{C}^{S_{2}}

In other words, the first condition says that any transition from P_{1} in a store S_{1} can be simulated by a transition from P_{2} in a store S_{2} (and vice versa), such that derivatives ⟨P′_{1}; S′_{1}⟩ and ⟨P′_{2}; S′_{2}⟩ remain in the simulation. Note that in the second condition we do not require S_{1} and S_{2} to be equivalent, but we just require they allow communication with the external environment along the same channels.

However, π^{+}- reduction equivalence is not preserved by agent constructions. For example ⟨x?[z] | y?[z]; S⟩ ˙∼_{π^{+}} ⟨x?[z] + y?[z]; S⟩, but communicating the agents along x with x![r], we have ⟨x?[z] | y?[z] | x![r]; S⟩ ˙≁_{π^{+}}⟨(x?[z] + y?[z]) | x![r]; S⟩. This motivates the definition appearing below:

Definition 5.3 (Strong π^{+}-context reduction equivalence) We will say that P_{1} in a store S_{1} is (strong) π^{+}- context reduction equivalent to P_{2} in a store S_{2}, written, ⟨P_{1}; S_{1}⟩ ∼_{π^{+}} ⟨P_{2}; S_{2}⟩ , iff for any agent context C[.], ⟨C[P_{1}]; S_{1}⟩ ˙∼_{π^{+}} ⟨C[P_{2}]; S_{2}⟩. An agent context C[.] is an agent term with a single hole, such that placing an agent in the hole yields a well-formed process. ∼_{π^{+}} is said to be the (strong) π^{+}- context reduction equivalence relation.

The weak version of the equivalences, where a reduction from a configuration can be simulated by several reductions from the other, is obtained in the standard way: Let ⇓_{C}^{S} be ⟹↓_{C}^{S}, the composition of the two relations. Weak π^{+}- reduction equivalence, written ˙≈_{π^{+}}, is defined by replacing in Definition 5.2 the reduction ⟨P_{2}; S_{2}⟩ ⟶ ⟨P′_{2}; S′_{2}⟩ with ⟨P_{2}; S_{2}⟩ ⟹ ⟨P′_{2}; S′_{2}⟩ and P_{2} ↓_{C}^{S_{2}} with P_{2} ⇓_{C}^{S_{2}}. Weak π^{+}- context reduction equivalence, written ≈_{π^{+}}, is defined by replacing in Definition 5.3 ˙∼_{π^{+}} with ˙≈_{π^{+}}.

The standard congruence theorems (congruence of bisimulation wrt. parallel composition, substitution, etc.) can be shown in a similar way as it was done in the π-calculus [MPW92, Mil91]. In what follows we only show some equivalent behaviors derived from constraint agents.

The following proposition shows an obvious result: There is no need to replicate a Tell agent:

Lemma 5.4 For any Q, ⟨Q | ∗!ϕ.P; S⟩ ˙≈_{π^{+}} ⟨Q | !ϕ. ∗ P; S⟩

Proof:

• First Condition: There is only two kinds of transitions from each configuration: (a) ⟨Q | ∗!ϕ.P; S⟩ ⟶ ⟨Q | P | ∗!ϕ.P; S ∧ ϕ⟩ and ⟨Q | !ϕ. ∗ P; S⟩ ⟶ ⟨Q | P | ∗ P; S ∧ ϕ⟩ , and (b) ⟨Q | ∗!ϕ.P; S⟩ ⟶ ⟨Q′ | ∗!ϕ.P; S′⟩ and ⟨Q | !ϕ. ∗ P; S⟩ ⟶ ⟨Q′ | !ϕ. ∗ P; S′⟩. The derivatives in (b) are particular cases of the antecedent configurations in (a), so we will consider case (a). Then we should show that there exists a weak bisimulation including (⟨Q | P | ∗!ϕ.P; S ∧ ϕ⟩ , ⟨Q | P | !ϕ. ∗ P; S ∧ ϕ⟩). We give next a sketch of the proof: There are only two kinds of reductions: By considering copies of P and their interactions with the current Q in both configurations and their derivatives, and by using TELL with !ϕ.P in ⟨P | ∗!ϕ.P; S ∧ ϕ⟩ and its derivatives. In the first case we can obtain infinitely many copies of P that can interact with Q. Thus, if P allows reductions in the current store or it can interact with the current Q, any derivative from a configuration by considering this case can be (weak) simulated by the other. In the second case, since the current store includes ϕ, this kind of reduction has no effect. More precisely, for any reduction, ⟨Q | P | ∗!ϕ.P; S ∧ ϕ⟩ ⟹ ⟨Q′ | P | ∗!ϕ.P; S′ ∧ ϕ⟩ (where Q′ is the result of considering the first case) there exists a reduction ⟨Q | P | ∗ P; S ∧ ϕ⟩ ⟹ ⟨Q′ | P | ∗ P; S′ ∧ ϕ⟩ and vice versa. Thus, by Definition 5.1 the observability condition is held, i.e., for each C, (Q′ | P | ∗!ϕ.P) ↓_{C}^{S′∧ϕ} iff (Q′ | P | ∗ P) ↓_{C}^{S′∧ϕ} .

• Second condition: From Definition 5.1, for each C, (Q | ∗!ϕ.P) ↓_{C}^{S} iff (Q | !ϕ. ∗ P) ↓_{C}^{S} .

Theorem 5.5 ⟨∗!ϕ.P; S⟩ ≈_{π^{+}} ⟨!ϕ. ∗ P; S⟩

Proof: To show that ⟨P_{1}; S⟩ ≈_{π^{+}} ⟨P_{2}; S⟩ we only need consider contexts C[.], where both P_{1} and P_{2} can act, that is, with P_{1} and P_{2} occurring unguarded in C[P_{1}] and C[P_{2}], respectively . Since ∗!ϕ.P and !ϕ. ∗ P are not normal processes, these contexts has the form (υC^{i})(Q | (υC′^{j}) . ) for any Q (here C^{k} denote a sequence of variables and/or names, possibly empty, C_{1} … C_{k}, and (υC^{k}) denotes (υC_{1}) … (υC_{k})). Thus, assuming that there is no need of renaming, from DEC-V (or DEC-N) we should show that ⟨Q | ∗!ϕ.P; S ≫ {C_{1}, …, C_{i}, C′_{1}, …, C′_{j}}⟩ ˙≈_{π^{+}} ⟨Q | !ϕ. ∗ P; S ≫ {C_{1}, …, C_{i}, C′_{1}, …, C′_{j}}⟩. The proof follows from the lemma 5.4

As we said before, in the cc-model a computation fails if a Tell agent attempts to add an inconsistent information to the store. In this sense two agents rendering the store unsatisfiable, and able to use its inconsistent information (i.e. they can use the inconsistent store to be observed at external channels) should be equivalent. In the π^{+}-calculus these agents will be weak reduction equivalent:

Theorem 5.6 Lets suppose ⟨P_{1}; S_{1}⟩ ⟹ ⟨P_{1}′; S_{1}′⟩ and ⟨P_{2}; S_{2}⟩ ⟹ ⟨P_{2}′; S_{2}′⟩ where S_{1}′ and S_{2}′ are unsatisfiable stores and each P_{i}′ (with i ∈ {1, 2}) includes at least one unguarded agent. Then ⟨P_{1}; S_{1}⟩ ˙≈_{π^{+}}⟨P_{2}; S_{2}⟩.

Proof: It is straightforward from Definition 5.1. Both configurations can reduce (in zero o more steps) to a configuration having an unsatisfiable store with an agent including an unguarded agent. From Definition 5.1 this agent is observable at any channel, so it can simulate (weakly) any derivative from the other.

In the previous section we gave an example of the behavior of P_{1} ≡ (υx)(υy)(?¬(x = y).Q) and P_{2} ≡ (υa)(υb)(?¬(a = b).Q) to illustrate the difference between names and variables. Assuming that Q is observable at some channel, the difference is preserved by our behavioral equivalence, that is, ⟨P_{1}; ⊤⟩ ˙≁_{π^{+}} ⟨P_{2}; ⊤⟩ .

6 Conclusions

We defined the π^{+}-calculus, an orthogonal extension of the π-calculus to handle constraints. We did this by adding variables and allowing agents to interact through constraints with a global store.

The π^{+}-calculus is parametrized in a constraint system and thus independent of a particular domain for constraints. We defined the operational semantic through an equivalence relation and a reduction relation on configurations of an agent and a store. We showed how the reduction relation essentially mimics that of the π-calculus but also that the π^{+} is able to express the more general notion of potentiality of reduction by the presence of ASK and TELL rules interacting with the store. We described examples showing the transparent interaction of constraints and communicating processes, including the possibility to define mutable data.

We extended to the π^{+}-calculus the notion of observability of an agent and defined equivalence of configurations under context reductions. These allowed us to prove that there is no need to replicate Tell agent and that configurations having different agents communicating through inconsistent stores are weak reduction equivalent, thus confirming the usual behavior in CCP of Tell agents attempting to add inconsistent information to the store.

7 Future Work

We propose three main directions for future work on this topic:

• Among the most successful work in parallel object-oriented programming languages is that on the POOL family of languages [Ame89]. [Wal95] provides a semantics for a member of this family, via a phrase by phrase translation into the π-calculus. In particular, an object is represented as an agent whose algebraic structure reflects the internal structure of the object, and whose pattern of interaction captures the way in which the object may interact with others. The variables (which represent attributes), are translated into cells in the π-calculus, which are similar to those of the π^{+}-calculus, but without constraints. We believe that an extension of that language integrating OO, Concurrent and Constraints paradigms can be constructed successfully by using the π^{+}-calculus.

• The Turner’s abstract machine [Tur95] is an efficient implementation of the π-calculus used in the programming language PICT [PT96]. Because of the orthogonality of our extension, it is feasible to think in an extension of this abstract machine for the π^{+}-calculus and also an extension of PICT to consider first-order constraints.

• We will analyze the possibility of incorporating in our calculus the type system for the πcalculus presented in [Tur95]. Moreover, we want to extend our calculus to consider objects (with classes) as a basic entity in a similar way as in [Vas94].

References

[Ame89] P. America. Issues in the design of a parallel object-oriented language. Formal Aspects of Computing, 1989.

[Mil80] Robin Milner. A calculus of communicating systems. Lecture Notes in Computer Science, LNCS 92, 1980.

[Mil91] Robin Milner. The polyadic π-calculus: a tutorial. Technical Report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, UK, October 1991. Also in Logic and Algebra of Specification, ed. F. L. Bauer, W. Brauer and H. Schwichtenberg, Springer-Verlag, 1993.

[Mil92] Robin Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119–141, 1992.

[MNS97] Martin Müller, Joachim Niehren, and Gert Smolka. Typed Concurrent Programming with Logic Variables. Technical report, Programming Systems Lab, Universität des Saarlandes, 1997. Submitted.

[MPW92] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, Parts I and II. Journal of Information and Computation, 100:1–77, September 1992.

[MS92] Robin Milner and Davide Sangiorgi. Barbed bisimulation. In W. Kuich, editor, Proc. of 19th International Colloquium on Automata, Languages and Programming (ICALP ’92), volume 623 of Lecture Notes in Computer Science, pages 685–695. Springer-Verlag, 1992.

[Nie96] Joachim Niehren. Functional computation as concurrent computation. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM Press, January 1996. to appear.

[NM95] Joachim Niehren and Martin Müller. Constraints for Free in Concurrent Computation. In Kanchana Kanchanasut and Jean-Jacques Lévy, editors, Asian Computing Science Conference, Lecture Notes in Computer Science, vol. 1023, pages 171–186, Pathumthani, Thailand, December 11–13 1995. Springer-Verlag.

[Pie96] Benjamin C. Pierce. Programming in the pi-calculus: An experiment in programming language design. Tutorial notes on the Pict language. Available electronically, 1996.

[PRT93] Benjamin C. Pierce, Didier Rémy, and David N. Turner. A typed higher-order programming language based on the pi-calculus. In Workshop on Type Theory and its Application to Computer Systems, Kyoto University, July 1993.

[PT94a] Benjamin C. Pierce and David N. Turner. Concurrent objects in a process calculus. In Theory and Practice of Parallel Programming (TPPP), Sendai, Japan, November 1994.

[PT94b] Benjamin C. Pierce and David N. Turner. Pict user manual. Forthcoming report. Available electronically, 1994.

[PT96] Benjamin C. Pierce and David N. Turner. Pict: A programming language based on the pi-calculus. Technical report in preparation; available electronically, 1996.

[Sar93] Vijay A. Saraswat. Concurrent Constraint Programming. The MIT Press, Cambridge, MA, 1993.

[Smo94a] Gert Smolka. A calculus for higher-order concurrent constraint programming with deep guards. Research Report RR-94-03, Deutsches Forschungszentrum für Künstliche Intelligenz, Stuhlsatzenhausweg 3, D-66123 Saarbrücken, Germany, February 1994.

[Smo94b] Gert Smolka. A foundation for higher-order concurrent constraint programming. In Jean-Pierre Jouannaud, editor, 1st International Conference on Constraints in Computational Logics, Lecture Notes in Computer Science, vol. 845, pages 50–72, München, Germany, 7–9 September 1994. Springer-Verlag.

[Tur95] David N. Turner. The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, UK, 1995.

[Vas94] Vasco T. Vasconcelos. Typed concurrent objects. In M. Tokoro and R. Pareschi, editors, Proc. of 8th European Conference on Object-Oriented Programming (ECOOP’94), volume 821 of Lecture Notes in Computer Science, pages 100–117. Springer-Verlag, 1994.

[VDR97] Frank VALENCIA, Juan Francisco DIAZ, and Camilo RUEDA. The π^{+}-calculus. Technical Report No.2, AVISPA Team, 1997.

[VP96] Björn Victor and Joachim Parrow. Constraint as processes. In Proc. of CONCUR’96, volume 1119 of Lecture Notes in Computer Science, pages 389–405. Springer-Verlag, 1996.

[Wal91] David Walker. π-calculus semantics of object-oriented programming languages. In Takayasu Ito and Albert Meyer, editors, Theoretical Aspects of Computer Software, volume 526 of Lecture Notes in Computer Science, pages 532–547. Springer-Verlag, 1991. Available as Report ECS-LFCS-90-122, University of Edinburgh.

[Wal95] David Walker. Objects in the π-calculus. Journal of Information and Computation, 116(2):253–271, 1995.