The π-calculus as a theory in linear logic: Preliminary results

23 February 1992

Dale Miller Computer Science Department University of Pennsylvania Philadelphia, PA 19104-6389 USA

dale@cis.upenn.edu

Phone: +1 (215) 898-1593 Fax: +1 (215) 898-0587

Abstract. The agent expressions of the π-calculus can be translated into a theory of linear logic in such a way that the reflective and transitive closure of π-calculus (unlabeled) reduction is identified with “entailedby”. Under this translation, parallel composition is mapped to the multiplicative disjunct (“par”) and restriction is mapped to universal quantification. Prefixing, non-deterministic choice (+), replication (!), and the match guard are all represented using non-logical constants, which are specified using a simple form of axiom, called here a process clause. These process clauses resemble Horn clauses except that they may have multiple conclusions; that is, their heads may be the par of atomic formulas. Such multiple conclusion clauses are used to axiomize communications among agents. Given this translation, it is nature to ask to what extent proof theory can be used to understand the meta-theory of the π-calculus. We present some preliminary results along this line for π_{0}, the “propositional” fragment of the π-calculus, which lacks restriction and value passing (π_{0} is a subset of CCS). Using ideas from proof-theory, we introduce co-agent and show that they can specify some testing equivalences for π_{0}. If negation-as-failure-to-prove is permitted as a co-agent combinator, then testing equivalence based on co-agents yields observational equivalence for π_{0}. This latter result follows from observing that co-agents are isomorphic to formulas in the Hennessy-Milner modal logic.

Contents

1 Introduction 2

2 Translating π-calculus expressions into logic 2

3 Process clauses and process theories 7

4 Reduction in the π-calculus 10

5 An analysis of the propositional fragment 11

6 Conclusions 16 Comments on this draft are welcome. Miller has been funded in part by ONR N00014-88-K-0633, NSF CCR-91-02753, and DARPA N00014-85-K-0018. This paper is available from the Computer Science Department of the University of Pennsylvania as technical report MS-CIS-92-48.

1 Introduction

In this paper we address the question “Can we view a given process calculus as a logic?” This is different (although certainly related) to the question “Can logic be used to characterize a given process calculus?” Such a question would view logic as an auxiliary language to that of the process calculus: for example, the Hennessy-Milner logic has such a relationship to CCS. Our approach here will try to use logic more immediately by asking the question: Are the combinators of the given process calculus logical connectives, and if not, can they be axiomized directly and uniformly in logic. Our logical tools are taken from the sequent calculus, especially the refinement of that subject found in linear logic [5], and from logic programming, particularly the topic of negation-as-failure. We shall investigate to what extent the framework of introduction rules, λ-abstraction in terms and in proofs (also know as eigen-variables), and the central notion of cut-elimination helps in analyzing a process calculus. This work is preliminary: we shall only look at the π-calculus [8, 9, 10] as a particular example of a process calculus. This calculus is, of course, rather rich and presents several interesting challenges.

We shall assume that the reader is familiar with the π-calculus as given in either [7] or [8]. The principle mechanism of the π-calculus is the synchronization of two agents and the sending of a name value from one agent to another. Synchronization is familiar from CCS; value passing is new to the π-calculus. The agent x̄z.P describes an agent that is willing to transmit the value z on the wire x (x and z are names). The agent x(y).Q is willing to receive a value on wire x and formally bind that value to y. The bound variable y in this expression is scoped over Q. Thus, a central computation of the π-calculus is reduction of the parallel composition x̄z.P | x(y).Q to the expression P | Q[z/y]. The agents P and Q[z/y] are now able to continue their interactions with their environment independently.

The π-calculus differs from CCS also in that it has a notion of scope restriction: in the agent expression (x)P, x is bound and invisible to the outside. The scoped value x, however, can be communicated outside its scope, providing a phenomenon known as “scope extrusion.” For example, (z)(x̄z.P | Q) | x(y).R is structurally equivalent to (z)(x̄z.P | Q | x(y).R) (scopes can move freely over agents for which the restricted variable is vacuous, which can be ensured here using α-conversion). This expression can now be reduced to (z)(P | Q | R[z/y]). Now the scope of the restriction (z) is larger since it contains the agent R[z/y] in which z may be free. This mechanism of generating new names (via α-conversion) and sending them outside their scope is an important part of the computational power of the π-calculus.

We shall not study the silent transition τ at all in this paper: it appears difficult to integrate τ into the framework proposed here.

2 Translating π-calculus expressions into logic

I first present one translation and then discuss two major variants to this translation, one of which is used for the rest of the paper.

The first translation requires the logical constants ⊕ (additive disjunction), ℘ (par, multiplicative disjunction), ? (the exponential “why not”), ∀, and ⊥ (the identity for ℘). The translation also require three non-logical constants, given below with their types (assuming that the type of logical expressions is o and that of names is i):

send: i → i → o → o, get: i → (i → o) → o, match: i → i → o → o.

As should be clear from these types, we shall freely make use of higher-order types and λ-calculus to smooth the treatment of bound variables and variable scoping. All those details will be pressed into a simple metalevel that contains the simply typed λ-calculus and quantification at higher-order types.

The first translation is given by the following induction on the structure of agent expressions.

⟨⟨P + Q⟩⟩ = ⟨⟨P⟩⟩ ⊕ ⟨⟨Q⟩⟩ ⟨⟨P | Q⟩⟩ = ⟨⟨P⟩⟩ ℘ ⟨⟨Q⟩⟩
⟨⟨(x)P⟩⟩ = ∀x⟨⟨P⟩⟩ ⟨⟨!P⟩⟩ =?⟨⟨P⟩⟩ ⟨⟨nil⟩⟩ = ⊥
⟨⟨x̄y.P⟩⟩ = sendx y ⟨⟨P⟩⟩ ⟨⟨x(y).P⟩⟩ = getx λy⟨⟨P⟩⟩ ⟨⟨[x = y]P⟩⟩ = matchx y ⟨⟨P⟩⟩

To describe the meaning of the three non-logical constants, we have the following axioms.

∀_{i}x∀_{i}y∀_{o}S∀_{i�o} R [Ry ℘ S −∘getx R ℘ sendx y S]
∀_{i}x∀_{i�o} P [P −∘matchx x P]

Notice that these axioms are higher-order in the sense that they allow quantification over predicate symbols. Such quantification is intended here to be purely syntactic: the type i → o denotes the set of closed, simply typed λ-terms of type i → o and not some abstract domain of functions.

There are at least two major variants to this translation. First, it is trivial to dualize it completely. That is, it is possible to map the “logical” combinators into the dual logical connectives.

⟨⟨P + Q⟩⟩ = ⟨⟨P⟩⟩ & ⟨⟨Q⟩⟩ ⟨⟨P | Q⟩⟩ = ⟨⟨P⟩⟩ ◯ ⟨⟨Q⟩⟩
⟨⟨(x)P⟩⟩ = ∃x⟨⟨P⟩⟩ ⟨⟨!P⟩⟩ = !⟨⟨P⟩⟩ ⟨⟨nil⟩⟩ = 1

In this case, the non-logical axioms would be axiomized with the formulas

∀_{i}x∀_{i}y∀_{o}S∀_{i�o} R [getx R ◯ sendx y S −∘Ry ◯ S]
∀_{i}x∀_{o}P [matchx x P −∘P]

Let us call this the conjunctive translation since it makes use of the multiplicative and additive conjunctions: the first translation should then be called the disjunctive translation for the dual reason.

The formal analysis below is completely dualizable, so there appears to be no formal reason to pick one translation over the other. Intuitively, this seems to be the case because process calculus is fundamentally about reduction, while logic has made a commitment to both reduction (implies/implied-by) and to truth values. Truth values do not naturally map into processes. The disjunctive translation maps reduction to implied-by; the conjunctive translation to implies.

I have the following extra-logical motivations for employing the disjunctive translation. Each of these reasons could be dualized but then they would not appear quite so convincing.

(A) The disjunctive translation makes reduction a “right-hand side” phenomena in sequent proofs. The bottom-up search for cut-free proofs in this translation generally forces succedents to go through reductions. Thus, the activity of searching for proofs can often be seen as agent reduction.

(B) The axiomization of non-logical constants in the disjunctive translation yields very simple “multiple conclusion” clauses. It would be exciting to be able to see such clauses as being a generalization of “single conclusion” clauses such as Horn clauses. Thus, we might be able to see process calculi as being certain kinds of logic programming. Given the above comment, the goal reduction in a logic programming interpreter would match agent reduction. In fact, the axioms used in this paper resemble the clauses used in the logic programming work of Andreoli and Pareschi in [3].

(C) Scope extrusion in the π-calculus is a phenomena that would be wonderful to blame on “classical” rather than “intuitionistic” provability. Proofs involving the disjunctive translation rely on the multiplicative disjunction (℘) and on multiple conclusion sequents. It is easy to see that classical logic supports a kind of scope extrusion and that multiple-conclusion sequents provide a simple analysis of this phenomenon. For example, consider the formula G_{1} ∨ (D ⊃ G_{2}). Intuitionistically, this is provable if and only if either G_{1} is provable or G_{2} is provable from D. That is, D is “scoped” only over the formula G_{2}. Classically, however, this formula is equivalent to (D ⊃ G_{1}) ∨ G_{2} and D ⊃ (G_{1} ∨ G_{2}). Thus the scope of D can move in ways not supported in intuitionistic logic. In particular, p∨(p ⊃ q) is not provable intuitionistically but it is classically. The analysis of the distinction between intuitionistic and classical logics via restrictions to single-conclusion or multiple-conclusion sequents [4] provides an elegant analysis of this scope extrusion issue. Consider the following sequent proof.

{p ⟶ p,q \atop ⟶ p,p ⊃ q} ; ⟶ p ∨ (p ⊃ q)

The occurrence of p in the antecedent has as its scope all the formulas in the succedent: in the intuitionistic case, there can only be one such formula in the succedent and, hence, scope cannot be liberalized in this way. The formula (∀x_{i}.false) ∨ (∃y_{i}.true) is similarly not provable intuitionistically but is provable classically (given that the type i is empty). Here, it is an eigen-variable that escapes its scope. Below is a proof of this sequent.

{x: i ⟶ false,true \atop x: i ⟶ false,∃y_{i}.true} ; ⟶ ∀x_{i}.false,∃y_{i}.true ; ⟶ (∀x_{i}.false) ∨ (∃y_{i}.true)

Scope extrusion in the π-calculus will be explained by exactly this kind of use of eigen-variables. In the conjunctive translation, isomorphic proofs are possible but this time the scope would need to be seen as being on the left and tension between “classical” and “intuitionistic” notions of scope would evaporate.

(D) In order to develop a semantics for π-calculus expressions, we will need to add a notion of a co-agent, one of which will be a constant for truth. In the conjunctive setting, that notion would need to be a constant for false, an unfortunately negative sounding choice.

By the notation Σ;P ⊢ Q we shall mean that Q is provable from P given the signature of constants Σ. We shall present a formal definition for this three-place predicate shortly. Before describing our final translation, we shall note that, given the disjunctive translation described above, the relation Σ;P ⊣⊢Q (defined as Σ;P ⊢ Q and Σ;Q ⊢ P) is an interesting candidate for structural equivalence. Figure 1 provides some examples of this equivalence.

A much more serious aspect of the translation given above is the choice of which combinators should be genuine logical constants and which are axiomatized, non-logical constants. It seems an advantage to make as few of the combinators into logical connectives as possible as long as the remaining combinators can be described uniformly in terms of the logical ones. One reason for this advantage is that reduction steps map rather naturally into right introduction rules of the sequent calculus (this will be clear from the proof of Proposition 5), while the left introduction rules do not generally yield plausible reduction steps. For example, if + is mapped to the logical constant ⊕ and if we wish reduction to be identified with entailed-by,

P  Q  Σ;P ⊢ QΣ;Q ⊢ PΣ;P ⊣⊢Q
P | P  P  no  no  no
P + P  P  yes  yes  yes
(x)P  P[y/x]§  yes  no  no
(x)P^{�}  P  yes^{�} yes  yes^{�}
P |!P  !P  yes  no  no
!P  !P |!P  yes  yes  yes
!P  nil  no  yes  no
P_{1} | (P_{2} | P_{3}) (P_{1} | P_{2}) | P_{3} yes  yes  yes
P_{1} + (P_{2} + P_{3}) (P_{1} + P_{2}) + P_{3} yes  yes  yes
P | nil  P  yes  yes  yes
P | Q  Q | P  yes  yes  yes
P + Q  Q + P  yes  yes  yes
(x)(y)P  (y)(x)P  yes  yes  yes
(x)(P | Q)^{�}  P | (x)Q  yes  yes  yes
(x)(P + Q)^{�}  P + (x)Q no  yes  no
(P_{1} | P_{2}) + (P_{1} | P_{3})P_{1} | (P_{2} + P_{3}) yes  no  no
(P_{1} + P_{2}) | (P_{1} + P_{3})P_{1} + (P_{2} | P_{3}) no  no  no
!P |!Q  !(P + Q)  yes  yes  yes

(†) x is not free in P. (‡) Σ is not empty. (§) y ∈ Σ.

Figure 1: Some logical implications and equivalences assuming that + and ! are logical constants.

\overline{Σ;P −→ P} initial \overline{Σ;nil ⟶}nil-L \frac{Σ;Δ ⟶ Γ}{Σ;Δ ⟶ nil,Γ} nil-R

\frac{Σ;P,Δ_{1} ⟶ Γ_{1} Σ;Q,Δ_{2} ⟶ Γ_{2}}{Σ;P | Q,Δ_{1},Δ_{2} ⟶ Γ_{1},Γ_{2}} | L \frac{Σ;Δ ⟶ P,Q,Γ}{Σ;Δ ⟶ P | Q,Γ} | R

\frac{Σ;P[t/x],Δ ⟶ Γ}{Σ;(x)P,Δ ⟶ Γ} (−)L \frac{Σ ∪ \{y\};Δ ⟶ P[y/x],Γ}{Σ;Δ ⟶ (x)P,Γ} (−)R

Figure 2: Basic inference rules

Σ;Δ_{1} ⟶ P,Γ_{1} Σ;P,Δ_{2} ⟶ Γ_{2}
Σ;Δ_{1},Δ_{2} ⟶ Γ_{1},Γ_{2}

t a Σ-termΣ ∪ {x};Δ ⟶ Γ Σ;[t/x]Δ ⟶ [t/x]Γ

Figure 3: Two forms of the cut-rule

then we are forced to admit the reduction rule: if P reduces to Q_{1} and to Q_{2}, then P reduces to Q_{1} + Q_{2}: a dubious “reduction” rule. Fortunately, it is possible to axiomize the reduction nature of + and ! by using the clauses

∀_{o}P∀_{o}Q [P −∘P + Q] ∀_{o}P∀_{o}Q [Q −∘P + Q]
∀_{o}P [⊥ −∘!P] ∀_{o}P [!P ℘!P −∘!P] ∀_{o}P [P −∘!P]

These clauses recover the right introduction rules without forcing us to accept the corresponding left introduction rules.

Instead of translating π-calculus expressions into the syntax of linear logic, we shall simply use the syntax of the π-calculus. We shall not make any distinction now between agents and formulas over the logical constants | : o → o → o, (−) : (i → o) → o, nil : o and the non-logical constants ! : o → o, + : o → o → o, plus the constructors for prefixing and matching, written x(y).P, x̄y.P, and [x = y]P of types i → (i → o) → o, i → i → o → o, and i → i → o → o, respectively. We shall also assume that there is a denumerably infinite set of constants of type i.

Let Δ and Γ be finite, multisets of formulas. Let Σ be a signature, that is, a (possibly empty) set of typed constants. A term t is a Σ-term if t is closed and all constants in t are members of Σ. A sequent is a triple Σ;Δ ⟶ Γ where Δ∪Γ contains formulas all of whose non-logical constants are from the set Σ. The symbol Σ;Δ ⊢ Γ means that the sequent Σ;Δ −→ Γ has a proof in linear logic (inference rules for the fragment of linear logic needed here are in Figures 2 and 3). The standard proviso applies to (−)R, y ∉Σ; and to (−)L, t is a Σ-term. Notice that the only inference rule with more than one premise is the left introduction rules for multiplicative disjunction. The structural rules of contraction and weakening are not present. The symbol Σ;Δ ⊣⊢Γ means Σ;Δ ⊢ Γ and Σ;Γ ⊢ Δ.

The cut-elimination theorem for this logic shows that the inference rules in Figure 3 are admissible with respect to the basic set of rules.

Provability in this proof system is obviously decidable. We have not given any status to the non-logical constants and their axioms in this proof system as of yet. We do this in the next section.

3 Process clauses and process theories

A process clause is a closed formula of the form

∀x̄[P −∘Q_{1} | ···| Q_{m}]

where m ≥ 1, P is an agent expression, Q_{1},...,Q_{m} are atomic formulas with non-logical constants as their head symbols, and all free variables in P (called the body of the clause) are free in Q_{1}|···|Q_{m} (called the head of the clause). The quantified variables may be of type i, o, as well as higher-order types, for example, i → o. If m = 1, such a clauses is also called a single-conclusion clause; otherwise, it is called a multiple-conclusion clause. An instance of a process clause using Σ-terms (for a given Σ) is called a Σ-instance of that clause.

The propositional structure of process clauses is similar to the clauses studied by Andreoli and Pareschi [3] where & and ⊤ (erasure) are also permitted in the body of clauses: their formalism, however, does not permit universal quantification in the body of clauses nor quantification of higher-type variables.

A process theory is a set H = {H_{1},...,H_{n}} (n ≥ 0) of process clauses. An H-proof is a proof built using the rules in Figure 2 and one inference of the form

Σ;Δ ⟶ Γ,P

Σ;Δ ⟶ Γ,Q_{1},...,Q_{m}

for every clause ∀x̄[P −∘Q_{1}|···|Q_{m}] in H. When an H-clause is written as an inference rule in this way, that inference rule is called an H-inference rule. Let Σ be a signature that contains all the non-logical constants contained in clauses of H. We write Σ;Δ ⊢_{H} Γ to mean that the sequent Σ;Δ ⟶ Γ has an H-proof. The structure of H-proofs are particularly simple, as we shall now see.

The site of an instance of an inference rule is a multiset of occurrence of formulas in the concluding sequent defined using the following cases: if the inference rule is the initial rule proving the sequent Σ;P −→ P, then the multiset containing both occurrences of P is the site; the site for an introduction rule is the singleton multiset containing the formula occurrence containing the introduced logical constant; and the site for an H-inference rule based on the clause ∀x̄ [P −∘Q_{1} | ···| Q_{m}] is the multiset containing the occurrences of the instances of the formulas Q_{1},...,Q_{m}. Two inference rules permute if whenever instances of these two rules have a common sequent as a conclusion and the sites of these two inference rule instances are disjoint, then those inference rules can be composed in either order to yield identical premises to their composition. When doing a bottom-up search for proofs, the order in which permuting inference rules are applied is not important.

Proposition 1 The right rules, nil-R, |R, and (−)R and the H-inference rules all permute over each other.

Proof This proposition follows from simply checking all cases. The case where a (−)R inference rule is below an H-inference rule requires the assumption about process clauses that all free variables in the body of clauses are also free in their head.

Consider the process theory that contains the single process clause ∀P∀Q∀x[P | Q −∘x.P | x̄.Q]. The order of the two right introduction rules in

{Σ;P | Q | R ⟶ P,Q,R \atop Σ;P | Q | R ⟶ b.P,Q,b̄.R} ; Σ;P | Q | R ⟶ a.b.P,ā.Q,b̄.R

cannot be switched: the site of the lower rule contains a subformula that is in the site of the upper rule. Notice also that a sequent with right-hand side a.P,ā.Q,ā.R can be the result of an H-inference rule in two ways: the choice of one of these precludes the other choice.

Proposition 2 If Σ;Δ ⟶ Γ has an H-proof, it has an H-proof Ξ such that Ξ has an occurrence of a sequent Σ^{�};Δ −→ Γ^{�}where all inference rules above this sequent occurrence are left introduction rules and instances of the initial inference rule and all inference rules below this sequent occurrence are right introduction rules.

The sequent Σ^{�};Δ ⟶ Γ^{�}is called the crossover sequent for the proof Ξ. Proof Let Ψ be an H-proof of Σ;Δ ⟶ Γ. If there is no pair of inference rules such that the lower one is a left introduction rule and the upper one is a right introduction rule or an H-inference rule, then Ψ has the structure described for the Ξ in the proof. Otherwise, assume that such a pair of inference rules exists. It is then possible to permute the order of these two rules and still have a proof of the same endsequent. The fact that a |-L below a (−)-R rule can be permuted requires observing the general fact that if Σ;Δ ⟶ Γ has an H-proof then Σ^{�};Δ −→ Γ has an H-proof whenever Σ^{�}is a signature that contains Σ. A simple inductive argument then shows that by doing enough such permutations, all such pairs of inference rules can be removed.

Corollary 3 If Σ;Δ ⟶ Γ has an H-proof then Δ must be a singleton multiset.

Proof Assume not and let Σ;Δ ⟶ Γ be a sequent in which Δ contains more than one member and which has an H-proof Ξ of minimal height. Clearly, Σ;Δ ⟶ Γ is not an initial sequent. But it is simple to check that no matter what its last inference rule is, Ξ must contain a proper subproof of a sequent containing more than one formula in its antecedent. This contradicts the choice of Ξ.

Proposition 4 The two cut rules of Figure 3 are admissible in H-proofs.

Proof We outline this proof here since it is simplier than the usual cut-elimination theorem [5]. Let Ξ_{1} be an H-proof for Σ;Q ⟶ P,Γ_{1} and let Ξ_{2} be an H-proof for Σ;P −→ Γ_{2}. We must show that there is an H-proof for Σ;Q ⟶ Γ_{1},Γ_{2}. First, we can assume that the last inference rule in Ξ_{2} is a left introduction rule since cut permutes up through all the right introduction rules for proofs of this premise. Similarly, we can assume that the last inference rule in Ξ_{1} is either a right introduction rule or an H-inference rule in which the occurrence of P is in the site. Now, if P has a top-level logical constant, then Ξ_{1} does a right introduction of that constant and Ξ_{2} does a left introduction of that constant. The usual movement of cut upwards in the proof will work in this case. Finally, if P is atomic, then Γ_{2} contains only P, so we can simply use Ξ_{1} as the proof of Σ;Q ⟶ Γ_{1},Γ_{2}.

The proof that the other cut rule involving substitution is simplier and more direct.

Process calculi are generally described using a notion of reduction. Figures 4, 5, and 6 present a proof system for a formulation of reduction determined by a process theory H. The following proposition shows the close relation between ⊢_{H} and such reduction.

Proposition 5 Let H be a process theory and let reduction be defined with respect to it. Then Σ;Q ⟹ P has a proof if and only if Σ;P ⊢_{H} Q.

\overline{Σ;S ⟹ R} H

Figure 4: Theory reduction rules: provided that R −∘S is a Σ-instance of a clause in H.

\frac{Σ ∪ \{x\};P ⟹ P^{�}}{Σ;(x)P ⟹ P^{�}} INS t is a Σ-termΣ;Q ⟹ P[t/x]

Σ;Q ⟹ (x)P GEN

\frac{Σ;P ⟹ P^{�}}{Σ;P | Q ⟹ P^{�}| Q} PAR

Figure 5: Descent reduction rules: In INS, x is not free in P^{�}.

\frac{Σ;P ⊣⊢Q}{Σ;P ⟹ Q} REF \frac{Σ;P ⟹ Q Σ;Q ⟹ R}{Σ;P ⟹ R} TRANS

Figure 6: Structural reduction rules

Proof First, assume that Σ;Q ⟹ P has a reduction proof. Proceed by induction on the structure of that proof. If the proof is of height 1, then it is an instance of either a theory reduction rule or the REF rule. In each case, it follows immediately that Σ;P ⊢_{H} Q.

To handle the remaining structural rule, assume that the proof ends in an instance of the TRANS rule. By induction, Σ;R ⊢_{H} Q and Σ;Q ⊢ P, and thus Σ;R ⊢_{H} P by cut.

Assume that the last inference rule was a descent reduction rule. If that rule is INS, then induction guarantees that Σ ∪ {x};P^{�}⟶ P has a proof. Adding the (−)R rules yields a proof for Σ;P^{�}⟶ (x)P. Similarly, if that rule is GEN then induction provides a proof of Σ;P[t/x] −→ Q where t is a Σ-term. Adding the (−)L rule yields a proof of Σ;(x)P −→ Q. If that rule is PAR, then induction provides a proof of Σ;P^{�}⟶ P. Using the initial sequent Σ;Q ⟶ Q and the |L and |R rules yields a proof of Σ;P^{�}|Q ⟶ P |Q.

Now consider the converse of this proposition. That is, assume that Σ;P −→ Q_{1},...,Q_{n} has an H-proof. We prove by induction on the structure of a (cut-free) H-proof that Σ;Q_{1} | ···| Q_{n} ⟹ P has a reduction proof. (If n = 0 then Q_{1} | ···| Q_{n} is simply nil.)

Case initial: If the proof is an instance of the initial rule, then n = 1 and Q_{1} is P. The reduction proof is simply an instance of the REF rule.

Case nil-R: The final sequent is Σ;P −→ nil,Q_{1},...,Q_{n} and induction provides a proof of Σ;Q_{1} | ···| Q_{n} ⟹ P. Noticing that Σ;nil | R ⊣⊢R for any R, use the REF and TRANS rules to provide a reduction proof for Σ;nil | Q_{1} | ···| Q_{n} ⟹ P.

Case |R: The final sequent is Σ;P −→ P | Q,Q_{1},...,Q_{n} and induction provides a proof of Σ;(P | Q) | Q_{1} | ···| Q_{n} ⟹ P. If this is not the desired reduction sequent already, simply use REF and TRANS to associate the |’s differently.

Case (−)R: The final sequent is Σ;P ⟶ (x)Q,Q_{1},...,Q_{n} and induction provides a proof of Σ ∪ {y};Q[y/x]|Q_{1}|···|Q_{n} ⟹ P. Adding the INS proof rule yields a proof of Σ;(y)(Q[y/x]|Q_{1}|···|Q_{n}) ⟹ P. Since Σ;(y)(Q[y/x] | Q_{1} | ···| Q_{n}) ⊣⊢(x)Q | Q_{1} | ···| Q_{n}, a use of REF and TRANS yields a proof of Σ;(x)Q | Q_{1} | ···| Q_{n} ⟹ P.

Case H-inference rule: The final sequent is Σ;P −→ Q_{1},...,Q_{i},...,Q_{n} and R−∘Q_{1}|···|Q_{i} is a Σ-instance of a rule in H. Thus, induction provides a proof of Σ;R|Q_{i+1} |···|Q_{n} ⟹ P. But by the H-rule (Figure 4), we have Σ;Q_{1} | ···| Q_{i} ⟹ R. By n − i applications of PAR, we have Σ;Q_{1} | ···| Q_{n} ⟹ R | Q_{i+1} | ···| Q_{n}. A use of TRANS and we are finished.

Case nil-L: The final sequent is Σ;nil ⟶. But Σ;nil ⟹ nil follows from REF. Σ;Q_{1} | ···| Q_{n} ⟹ P. Case |L: The final sequent is Σ;P_{1}|P_{2} ⟶ Q_{1},...,Q_{n} and induction provides proofs of Σ;Q_{1}|···|Q_{i} ⟹

P_{1} and Σ;Q_{i+1}|···|Q_{n} ⟹ P_{2}, so i = 1,...,n. (Of course, it is permitted to permute the Q’s prior to splitting them.) Using n − i applications of PAR provides a reduction proof of Σ;Q_{1} | ···| Q_{n} ⟹ P_{1} | Q_{i+1} | ···| Q_{n}. One application of PAR yields Σ;P_{1}|Q_{i+1}|···|Q_{n} ⟹ P_{1}|P_{2}. Thus, one use of TRANS provides a reduction proof of Σ;Q_{1} | ···| Q_{n} ⟹ P_{1} | P_{2}.

Case (−)L: The final sequent is Σ;(x)P ⟶ Q_{1},...,Q_{n} and induction provides a proof of Σ;Q_{1} | ···| Q_{n} ⟹ P[t/x] for t a Σ-term. The GEN rule immediately yields Σ;Q_{1} | ···| Q_{n} ⟹ (x)P.

4 Reduction in the π-calculus

We should like to identify reduction in the π-calculus with the reduction relation defined in the previous section using the signature

Σ_{π} = {send: i → i → o → o, get: i → (i → o) → o, match: i → i → o → o, ! : o → o, + : o → o → o}

and the following theory, which we shall call the π-theory.

∀_{i}x∀_{i}y∀_{o}S∀_{i�o} R [Ry ℘ S −∘getx R ℘ sendx y S]
∀_{i}x∀_{i�o} P [P −∘matchx x P]
∀_{o}P∀_{o}Q [P −∘P + Q] ∀_{o}P∀_{o}Q [Q −∘P + Q]
∀_{o}P [⊥ −∘!P] ∀_{o}P [!P ℘!P −∘!P] ∀_{o}P [P −∘!P]

A π-proof is an H-proof, where H is the set of axioms displayed above. We write Σ;Δ ⊢_{π} Γ if the sequent Σ_{π} ∪ Σ;Δ ⟶ Γ has a π-proof. Notice that since Σ_{π} contains no constructors for type i, the signature Σ can be restricted to being composed only of tokens of type i. Thus, t is a Σ-term if and only if t ∈ Σ: the only values used during computations (search for proofs) are names and not general terms.

Since the notion of reduction is central to the definition of a process calculus, we must be very careful in making any claim to having captured the π-calculus as it is described in, say, [8, 9]. There seems to be at least the following significant differences with the description given in those reports.

1. Signatures are made explicit and reductions depend on them.

2. The + and ! combinators are treated only via computation rules: there are no rules for explicitly descending through them. Thus several reduction steps defined here are needed to account for a single reduction step of the π-calculus.

3. The GEN and INS rules do not correspond to any rules of [8, 9]. As a reduction rule, GEN does seem odd since it does not seem to be making anything simplier. Its main purpose seems to be that it allows the result of a reduction to discharge its dependence on any part of the surrounding signature. Notice that a version of the reduction rule for restriction in the π-calculus can be proved here: if Σ ∪ {x};P ⟹ Q can be proved then by one instance each of GEN and INS, we have a proof of Σ;(x)P ⟹ (x)Q.

Given our plan to use proof theory to organize the syntax of process calculi, these differences seem forced. Probably only additional results will tell us if what is defined here is significantly different from the π-calculus of [8]. Of course, the process calculi defined here may be of their own interest.

We shall think of the π-calculus as a first-order theory. In the next section we analysis the “propositional” fragment of the π-calculus. In particular, we shall only be interested in synchronization and not with value passing, binding, or restriction, or with match. Thus, agent expressions in the propositional calculus are defined via the grammar

P ::= nil | P_{1} | P_{2} | P_{1} + P_{2} | !P | a.P | ā.P,

where, a ranges over some fixed, finite set of names Σ_{0}. We refer to this propositional theory as the π_{0}- calculus. It is determined by the signature

Σ_{π_{0}} = {send: i → o → o, get: i → o → o, ! : o → o, + : o → o → o}

and the following set of process clauses.

∀_{i}x∀_{o}S∀_{o}R [R ℘ S −∘getx R ℘ sendx S]
∀_{o}P∀_{o}Q [P −∘P + Q] ∀_{o}P∀_{o}Q [Q −∘P + Q]
∀_{o}P [⊥ −∘!P] ∀_{o}P [!P ℘!P −∘!P] ∀_{o}P [P −∘!P]

We shall, of course, identify geta P and senda P with a.P and ā.P, respectively, and identify ¯ ā with a. A π_{0}-proof is an H-proof, where H is the set of axioms displayed above. We write Δ ⊢_{π_{0}} Γ if the sequent Σ_{π_{0}} ∪Σ_{0};Δ ⟶ Γ has a π_{0}-proof. Since agents of the π_{0}-calculus do not contain universal quantification, all occurrences of signatures in any π_{0}-proof are equal and, therefore, we shall choose not to display signatures. The π_{0}-calculus is essentially a subset of CCS, except for !, which can be defined approximately in CCS using the equation !C = C |!C.

5 An analysis of the propositional fragment

Given this proof-theoretic setting, a natural way to attribute meaning [[P]] to an agent P is via the definition

[[P]] = {W | ⊢_{π_{0}} P | W, where W is an agent }.

The goal would then be to say that two agents, P and Q, are equivalent, in some sense, if [[P]] = [[Q]]. Unfortunately, using this definition, all agents are equivalent since [[P]] is always empty: there is no notion of a “true” agent. The only notion we have so far is that of one agent reducing to (implied-by) another.

Since we are inside a logic containing many more logical constants than we are using so far, it is possible to introduce co-agents, one of which will be “truth.” Given some collection of co-agents, we shall define the meaning of agents using

[[P]] = {W | ⊢_{π_{0}} P | W, where W is a co-agent }.

Thus, co-agents will be used to probe the behavior of agents. It is important to make the following observation: no matter what we choose for co-agents, if [[P]] ⊆ [[Q]] then [[P + Q]] = [[Q]]. Thus, if [[P]] ⊆ [[Q]] is ever strictly true, we have not captured deadlock within our theory of equivalence.

In analyzing the π_{0}-calculus, we shall first introduce two co-agents, identified as the two (linear) logical connectives ⊤ (erasure) and & (additive conjunction) for which their right introduction rules are given in

\overline{Σ;Δ ⟶ ⊤,Γ}

⊤-R

Σ;Δ ⟶ Γ,W_{1} Σ;Δ ⟶ Γ,W_{2}

Σ;Δ ⟶ Γ,W_{1} & W_{2}

&-R

Figure 7: Proof rules for the two co-agent connectives ⊤ and &.

Figure 7. Assume for now that we define a co-agent to be any expression that contains at least one occurrence of either ⊤ or &. We can make the following observations regarding occurrences of ⊤ in [[P]].

• It is always the case that ⊤ ∈ [[P]].

• The agent P has an a-transition if and only if ā.⊤ ∈ [[P]].

• The agent P has an a-transition followed by a b-transition if and only if ā.b̄.⊤ ∈ [[P]].

Thus, P has a trace a_{1},...,a_{n} if and only if ā_{1}.···.ā_{n} .⊤ ∈ [[P]]. If ⊤ were the only co-agent, then the equivalence described by [[P]] = [[Q]] would be that of trace equivalence.

By allowing & as a co-agent expression, we can make more distinctions between the behaviors of agents. For example, let P be a.b.nil + a.(c.nil + d.nil) and let Q be a.(b.nil + c.nil) + a.d.nil. While these have the same traces, the co-agent ā.(c̄.⊤ & d̄.⊤) is a member of [[P]] but not of [[Q]]. Notice, however, that since [[a.b.nil]] ⊆ [[a.(b.nil + c.nil)]], it follows that [[a.(b.nil + c.nil)]] = [[a.b.nil + a.(b.nil + c.nil)]].

Clearly, co-agents are acting as testers. The logical constant ⊤ behaves very much as the w tester in [6]. The logical constant & specifies two tests that a process must satisfy simultaneous: in a sense, the process must be copied and the two copies must be able to satisfy two separate tests. Thus co-agents treat agents extensionally, that is, as black boxes whose internal structure is not examined directly. Consider what would happen if ◯ (the multiplicative conjunction) were permitted to also be a co-agent connective. The co-agent W_{1} ◯ W_{2} would require that the agent being tested be divided into two pieces, one of which must pass W_{1} and the other W_{2}. While this use of tensor may have its uses, we do not consider it any further here.

It will be important for a subsequent result (regarding bisimilarity) that we allow possibly infinite conjunctions. Let I be a denumerable set (possibly empty). The right introduction rule for &_{i�I} is given by the inference figure

\frac{⟶ Γ,W_{i_{1}} ···⟶ Γ,W_{i_{j}} ···}{⟶ Γ,&_{i�I}W_{i}} ,

where I = {i_{1},...,i_{j},...}. If the index set is empty, then &_{i�I} is the same as ⊤ and if the index set has two element, then &_{i�I} is the same as &. The term co-agents now refers to any agent expression containing at least one occurrence of &_{i�I}, where I is not a singleton.

The following proposition shows that if co-agents are only used to define testing equivalence, they only need to be built up out of prefixing and the co-agent combinator &_{i�I}.

Proposition 6 Define [[Γ]]_{1} to be the set of all multisets of agents and co-agents Δ such that ⊢_{π_{0}} Γ,Δ. Define [[Γ]]_{2} to be the set of co-agents W built exclusively from occurrences of the indexed & and prefixing so that ⊢_{π_{0}} Γ,W. For multisets of agents Γ and Ψ, [[Γ]]_{1} = [[Ψ]]_{1} if and only if [[Γ]]_{2} = [[Ψ]]_{2}.

Proof The proof that [[Γ]]_{1} = [[Ψ]]_{1} implies [[Γ]]_{2} = [[Ψ]]_{2} is immediate. Thus, assume that [[Γ]]_{2} = [[Ψ]]_{2} and that Δ is a multiset of agents and co-agents such that ⊢_{π_{0}} Γ,Δ. Consider the proof system given Figure 8. A π_{0}-proof of ⟶ Γ,Δ can then be extended to a proof in Figure 8 of ⟶ Γ R Δ, for some R built exclusively from occurrences of the indexed & and prefixing. Thus, R ∈ [[Γ]]_{2} and R ∈ [[Ψ]]_{2}. Now given a

\frac{⟶ Γ R Δ}{⟶ nil,Γ R Δ} \frac{⟶ P,Q,Γ R Δ}{⟶ P | Q,Γ R Δ} \frac{⟶ Γ,Q R Δ}{⟶ Γ,P R Δ}†

\frac{⟶ Γ R Δ}{⟶ Γ R nil,Δ} \frac{⟶ Γ R P,Q,Δ}{⟶ Γ R P | Q,Δ} \frac{⟶ Γ R Q,Δ}{⟶ Γ R P,Δ}†

\frac{⟶ P,Q,Γ R Δ}{⟶ a.P,ā.Q,Γ R Δ} \frac{⟶ P,Γ R Q,Δ}{⟶ a.P,Γ ā.R ā.Q,Δ} \frac{⟶ Γ R P,Q,Δ}{⟶ Γ R a.P,ā.Q,Δ}

for all i ∈ I ⟶ Γ R_{i} W_{i},Δ

⟶ Γ &_{i�I}R_{i} &_{i�I} W_{i},Δ

Figure 8: A proof system used for “interpolating” between agents and co-agents. The † proviso: Q −∘P is a instance of a single conclusion π_{0}-axiom.

π_{0}-proof of ⟶ Ψ,R and the proof of ⟶ Γ R Δ, it is an easy to construct a proof of ⟶ Ψ R Δ. Thus, ⊢_{π_{0}} Ψ,Δ and Δ ∈ [[Ψ]]_{1}. The converse inclusion is similar.

The following proposition describes the fact that in the bottom-up search for proofs involving co-agents, the top-level logical structure of co-agents can be addressed first. We shall strive to preserve this property when we add one more connective to the structure of co-agents.

Proposition 7 Assume that −→ Γ,W has a proof, where Γ is a multiset of agents and W is a co-agent built exclusively from occurrences of the indexed & and prefixing. Then this sequent has a proof Ξ such that for every occurrence of a sequent in Ξ, if the co-agent expression in that sequent is a top-level &_{i�I} then that sequent occurrence is the conclusion of a &_{i�I}-R introduction rule.

Proof This can be proved by a observing that if there is an inference rule in a proof of ⟶ Γ,W immediately below an instance of a &_{i�I}-R introduction rule, then the &_{i�I}-R introduction rule can be permuted lower.

So far co-agents are extracting only positive information. The equivalence of processes, [[P]] = [[Q]], does not come close to the notion of bisimulation since it is not possible to test for what a process cannot do. For this, it appears necessary to leave the usual logical connectives and their introduction rules and develop a notion of negation as “failing to pass a test” or of “negation-as-failure,” as it is often called in the logic programming literature.

A notion of negation-as-failure cannot be achieved by simply adding introduction rules. We shall use a hierarchy of proof systems {S_{n} | n = 0,1,2,...} such that S_{n} can handle a nesting of at most n occurrences of negation and where non-provable sequents in the S_{n} proof system yield initial sequents (axioms) for negation in the S_{n+1} proof system (S_{0} is identified with the π_{0} proof system). Even given this hierarchy of proof systems, negation can still cause us one serious problem. Notice that the sequent ⟶ a.nil,b̄.⊤ has no π_{0}-proof. Thus, in the S_{1} proof system, we shall accept the sequent ⟶ a.nil,¬b̄.⊤ as initial. If we do not add any further restrictions, there will also be an S_{1} proof of ⟶ a.nil + b.nil,¬b̄.⊤. This conclusion is not acceptable since there is a S_{0}-proof (and, hence, S_{1} proof) of ⟶ a.nil + b.nil,b̄.⊤. Thus, it would be possible for an agent (a.nil + b.nil) to pass a test (b̄.⊤) and its complement. A suitable solution to this problem is to insist that proofs in S_{n} introduce ¬ as early as possible; that is, require that any S_{n+1} proof of a sequent ⟶ Γ,¬W to be, in fact, an initial sequent of S_{n+1}. Notice that this condition is essentially equivalent to the one which can be verified for &_{i�I} in Proposition 7. With negation, however, this condition cannot be inferred so we must enforce it.

Given this motivation, we can now make the following definitions. Let C_{n} for n ≥ 0 be sets of expressions defined by the following recursion on the structure of formulas.

• If I is a denumerable (possibly empty) set and for all i ∈ I, W_{i} ∈ C_{n} then &_{i�I}W_{i} ∈ C_{n}.

• If P ∈ C_{n} then a.P ∈ C_{n} and ā.P ∈ C_{n}.

• If P ∈ C_{n} then ¬P ∈ C_{n+1}.

We now introduce, for each n ≥ 0, a proof system S_{n}. Sequents in S_{n}-proofs will be of the form ⟶ Γ,W where Γ is a multiset of agents and W ∈ C_{n}. For each n ≥ 0, S_{n} contains the right introduction rules for nil, |, and &_{i�I} as well as the inference rules for all the π_{0}-theory axioms. In particular, the only initial sequents in S_{0} are given by the &_{i�I}-R rule when I is empty. The systems S_{n+1} have as additional initial sequents ⟶ Γ,¬W, where the sequent ⟶ Γ,W does not have an S_{n}-proof. Such initial sequents are called negative initial sequents. An S_{n}-proof is a tree structure arrangement of such initial sequents and inferences with the following proviso: if the sequent ⟶ Γ,¬W has an occurrence in the tree, then that occurrence is an initial sequent. For n ≥ 0, we write ⊢^{n} Γ,W to mean that there is an S_{n}-proof of ⟶ Γ,W. Notice that ⊢_{π_{0}} Γ,W if and only if ⊢^{0} Γ,W. Let C_{ω} = ⋃_{n�0} C_{n}.

Notice that it is easy to extend Proposition 7 to S_{n} for n ≥ 0. That is, S_{n}-proofs can be assumed to be such that whenever a sequent occurrence has an occurrence of a &_{i�I} co-agent, that sequent occurrence is the conclusion of the &_{i�I} introduction rule.

Proposition 8 Let W ∈ C_{n}, let m ≥ n, and let Γ be a multiset of agent expressions. Then ⊢^{m} Γ,W if and only if ⊢^{m+1} Γ,W.

Proof By induction on m. If m = 0 then n = 0. Since W has no occurrences of negations, the result is immediate. Assume that m > 0. Let Ξ be an S_{m}-proof of ⟶ Γ,W. If Ξ has no negative initial sequents, then Ξ is both an S_{0} and S_{m+1}-proof. Thus, assume that Ξ contains the initial sequent ⟶ Δ,¬W^{�}. Since ¬W^{�}is a subformula of W, W^{�}∈ C_{n�1}. Also, there is no S_{m�1}-proof of −→ Δ,W^{�}. By the inductive hypothesis, there is no S_{m}-proof of ⟶ Δ,W^{�}so S_{m+1} contains the initial sequent ⟶ Δ,¬W^{�}. Since every initial sequent of Ξ is initial in S_{m+1}, Ξ is an S_{m+1} proof of ⟶ Γ,W. Conversely, let Ξ be an S_{m+1}-proof of ⟶ Γ,W. Again, let ⟶ Δ,¬W^{�}be a negative initial sequent in Ξ. Thus, W^{�}∈ C_{n�1} and there is no S_{m}-proof of ⟶ Δ,W^{�}. By the inductive hypothesis, there is no S_{m�1} proof of ⟶ Δ,W^{�}so ⟶ Δ,W^{�}is an initial sequent in S_{m}. Thus, Ξ is also an S_{m} proof.

Let Γ be a multiset of agent expressions and let W ∈ C_{ω}. We write ⊢^{ω} Γ,W if there is some n ≥ 0 such that ⊢^{n} Γ,R. Notice that if W ∈ C_{n} for some n ≥ 0, Proposition 8 implies that ⊢^{ω} Γ,W if and only if ⊢^{n} Γ,W.

Proposition 9 Let Γ be a multiset of agent expressions and let W ∈ C_{ω}.

(i)Either ⊢^{ω} Γ,W or ⊢^{ω} Γ,¬W.

(ii)It is not the case that ⊢^{ω} Γ,W and ⊢^{ω} Γ,¬W.

(iii)⊬^{ω} Γ,W if and only if ⊢^{ω} Γ,¬W.

(iv)⊢^{ω} Γ,W if and only if ⊢^{ω} Γ,¬¬W.

Proof To prove (i), let n be such that W ∈ C_{n}. Then ⟶ Γ,W is either provable or not provable in S_{n}. In the first case, ⊢^{ω} Γ,W. In the second case, ⊢^{n+1} Γ,¬W and therefore ⊢^{ω} Γ,¬W.

To prove (ii), let n be such that W ∈ C_{n} and assume that ⊢^{ω} Γ,W and ⊢^{ω} Γ,¬W. By Proposition 8, ⊢^{n} Γ,W and ⊢^{n+1} Γ,¬W. Given the restriction on proofs involving negations in proofs, −→ Γ,¬W is an initial sequent of S_{n+1} and thus there is no S_{n}-proof of ⟶ Γ,W, which is a contradiction.

To prove (iii), let n be such that W ∈ C_{n}. Thus by Proposition 8 ⊬^{ω} Γ,W if and only if ⊬^{n} Γ,W. But this is equivalent to ⊢^{n+1} Γ,¬W. By Proposition 8 again, this is equivalent to ⊢^{ω} Γ,¬W.

To prove (iv), notice that by (iii), ⊢^{ω} Γ,W is equivalent to ⊬^{ω} Γ,¬W, which (by (iii) again) is equivalent to ⊢^{ω} Γ,¬¬W.

For Γ a multiset of agent expressions, define [[Γ]] = {W ∈ C_{ω} | ⊢^{ω} Γ,W}.

Proposition 10 Let P and Q be two agent expressions. Then [[P]] ⊆ [[Q]] if and only if [[P]] = [[Q]].

Proof Assume that [[P]] ⊆ [[Q]] and that [[P]] ≠ [[Q]]. Thus, there is a W ∈ C_{ω} such that ⊢^{ω} Q,W but ⊬^{ω} P,W. By Proposition 9 (iii), ⊢^{ω} P,¬W. But this implies that ¬W ∈ [[P]] and ¬W ∈ [[Q]] which contradicts Proposition 9 (ii).

Before connecting the equivalence given by [[P]] = [[Q]] to known equivalences, we need to define the notion of labeled transition. Let a be an action (that is, a constant of type i). The three place relation P ⟹^{a}P^{�}is defined to hold if P^{�}|1 ⊢_{π_{0}} P |ā.1. Here, the constant 1 is some anonymous symbol for which no inference rules are provided. (It is possible to identify 1 with the constant of the same name used in linear logic [5] since the inference rules given for 1 there cannot be used in any cut-free π_{0}-proof of the sequent P^{�}| 1 −→ P | ā.1.) Given this definition, it follows that if P ⟹^{a}P^{�}and Q is an agent expression then P | a.Q ⟹ P^{�}| Q (simply replace 1 with Q).

If Γ is a multiset of formulas then |Γ denotes the parallel composition (using |) of all the formulas Γ in some fixed but arbitrary order.

Proposition 11 Let Γ be a multiset of agents, let a be an action, and let W ∈ C_{ω}. Then ⊢^{ω} Γ,ā.W if and only if there is a multiset of agents Ψ such that |Γ ⟹^{a}|Ψand ⊢^{ω} Ψ,W.

Proof First assume that ⊢^{ω} Γ,ā.W. A proof of −→ Γ,ā.W must contain a subproof where the last inference rule is

\frac{⟶ Γ^{�},R,W}{⟶ Γ^{�},a.R,ā.W} ,

for some multiset of agents Γ^{�}and some agent R. Set Ψ equal to the multiset Γ^{�}∪ {R}. Now the sequent (|Ψ) | 1 ⟶ Γ^{�},R,1 clearly has a π_{0}-proof (involving only |L rules and initial sequents). If we now add to this sequent all the right rules that were applied to build the proof of ⟶ Γ,a.W from ⟶ Γ^{�},R,W, we can construct a proof of (|Ψ) | 1 ⟶ Γ,ā.1 and of (|Ψ) | 1 ⟶ (|Γ) | ā.1. Thus, |Γ ⟹^{a}|Ψ.

For the converse, assume that Ψ is such that |Γ ⟹^{a}|Ψand ⊢^{ω} Ψ,W. The crossover sequent of the proof of (|Ψ) | 1 ⟶ Γ,ā.1 must be (|Ψ) | 1 ⟶ Γ^{�},1 for some multiset of agents Γ^{�}(see Proposition 2). Since (|Ψ) and (|Γ^{�}) are equal agent expressions up to associativity and commutativity of |, ⊢^{ω} Γ^{�},W. Now adding to the sequent ⟶ Γ^{�},W all those right rules that were used to prove (|Ψ)|1 ⟶ (|Γ)|ā.1 from (|Ψ)|1 ⟶ Γ^{�},1 yields a proof of ⟶ Γ,ā.W.

We can now show that co-agents act the same as formulas of the Hennessy-Milner modal logic. Assertion formulas are formulas containing the indexed conjunction ∧_{i�I} (for a denumerable index set I), the possibility modal ⟨a⟩ (for a an action), and the negation ¬. The logical constant true is equivalent to ∧_{i�I}A_{i} for the empty index set I. The satisfaction of an assertion A by a process expression P, written as P ⊧ A, is defined by the following induction on the structure of assertions.

• P ⊧ ∧_{i�I}A_{i} if P ⊧ A_{i} for every i ∈ I.

• P ⊧ ⟨a⟩A if there is an agent P^{�}such that P ⟹^{a}P^{�}and P^{�}⊧ A.

• P ⊧ ¬A if it is not the case that P ⊧ A.

Define the following bijection of C_{ω} into assertation formulas: (&_{i�I}W_{i})^{o} = ∧_{i�I}W_{i}^{o}, (a.W)^{o} = ⟨ā⟩W^{o}, and (¬W)^{o} = ¬W^{o}.

Proposition 12 Let W ∈ C_{ω} and let P be an agent expression. ⊢^{ω} P,W if and only if P ⊧ W^{o}.

Proof This proof is by induction on the structure of co-agents in C_{ω}. The cases for &_{i�I} and ¬ are immediate. Let W be a.W^{�}. If P ⊧ ⟨ā⟩(W^{�})^{o} then there is a P^{�}such that P ⟹^{ā}P^{�}and P^{�}⊧ (W^{�})^{o}. By the inductive hypothesis, ⊢^{ω} P^{�},W^{�}and by Proposition 11, ⊢^{ω} P,W. Conversely, if ⊢^{ω} P,a.W^{�}then, by Proposition 11, there is a P^{�}such that P ⟹^{ā}P^{�}and ⊢^{ω} P^{�},W. By the inductive hypothesis, P^{�}⊧ W^{o} and by the definition of ⊧, P ⊧ ⟨ā⟩(W^{�})^{o}.

The following proposition is now immediate.

Proposition 13 Let P and Q be agents. Then [[P]] = [[Q]] if and only if for every assertion A, P ⊧ A if and only if Q ⊧ A.

Since the Hennessy-Milner logic characterizes observational equivalence, P and Q are observational equivalence if and only if [[P]] = [[Q]]. It is possible to show this result directly without making use of the Hennessy-Milner logic but the proof would be essentially identical to the proof using this modal logic.

This derivation of the Hennessy-Milner logic via co-agents is rather satisfactory for at least two reasons. First, it is possible to understand agents and assertion formulas as part of the same logical system, here a theory in a fragment of linear logic. Second, the intensional prefixing operator gives rise to the intensional modal operator: the latter does not need to be added separately. Representing prefixing as two nonlogical constants of higher-order type might be considered one of the more controversial aspects of this representation. The fact that this choice also explains the modal operator provides us with more confidence in this choice.

In fact, the parsimony of our presentation of co-agents can be improved even further: negation ¬ is the only co-agent combinator that is necessary. For example, the expression ¬nil can be used for ⊤ (¬P for any agent P will also do) and the expression ¬(¬W_{1}+¬W_{2}) can be used for W_{1}&W_{2}. Thus, if we admit indexed sums ∑_{i�I} into π_{0}, the only co-agent combinator we need to introduce is the negation-as-failure-to-prove operator.

6 Conclusions

In this paper we have attempted to show one way that proof theory can be used to represent and organize the details of the π-calculus. This approach seems successful on more than one level: not only can the reflective and transitive closure of reduction be identified with entailed-by but also proof-theoretic notions of semantics provide a natural link to well studied semantics for concurrency. The derivation of the Hennessy-Milner modal logic via the notion of co-agents speaks strongly for the directness of this approach.

It should be commented on how this work relates to recent work by Abramsky. In [2], Abramsky approaches concurrency and proof theory using the eye of a functional programmer; that is, he asked the questions: “How does one realize multiple-conclusion proofs?” and “What does cut-elimination mean as a computation on such proofs?” His conclusions are that the realizers can be thought of as concurrent programs and that cut-elimination can be thought of as communication. Although his approach is very different than the approach given here, it helps to make clear that the connections between concurrency and proof theory are very deep and can be analyzed in fundamentally different ways.

Of course, there is a great deal of work left to be done in getting a full picture of the relationship between multiple-conclusion sequent calculus and process calculi. For example, Abramsky’s work on bisimulation as testing equivalence [1] should be related to the material in Section 5. A very good test of our approach would be to see if the modal logics recently described for the π-calculus in [10] can be motivated using the notion of co-agents.

References

[1] Samson Abramsky. Observation equivalence as a testing equivalence. Theoretical Computer Science, 53:225–241, 1987.

[2] Samson Abramsky. Proofs as processes. Copy of transparencies, 1991.

[3] J.M. Andreoli and R. Pareschi. Linear objects: Logical processes with built-in inheritance. New Generation Computing, 9:3-4, 1991. (Special issue of selected papers from ICLP’90).

[4] Gerhard Gentzen. Investigations into logical deductions, 1935. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68–131. North-Holland Publishing Co., Amsterdam, 1969.

[5] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[6] Matthew Hennessy. Algebraic Theory of Processes. MIT Press, 1988.

[7] Robin Milner. Functions as processes. Research Report 1154, INRIA, 1990.

[8] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, Part I. LFCS Report Series ECS-LFCS-89-85, University of Edinburgh, June 1989.

[9] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, Part II. LFCS Report Series ECS-LFCS-89-86, University of Edinburgh, June 1989.

[10]Robin Milner, Joachim Parrow, and David Walker. Modal logics for mobile processes. LFCS Report Series ECS-LFCS-91-136, University of Edinburgh, April 1991.