The π-calculus as a theory in linear logic:

Preliminary results ^{∗}

Dale Miller

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

                      dale@cis.upenn.edu

October 29, 1992

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 “entailed-by”. 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 axiomatize 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-agents 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 directly represent formulas in the Hennessy-Milner modal logic.

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 be to use logic more immediately by trying to match combinators of the given process calculus directly to logical connectives and, if a combinator fails to match, trying to axiomatized it directly and uniformly in logic.

For our purposes here, we shall consider a formal system to be a logic if it has a sequent calculus presentation that admits a cut-elimination theorem. Of course, this definition of logic is not formal unless formal definitions of sequent calculi and cut-elimination are provided. We shall not attempt formal definitions of these two terms here: we simply make use of a couple examples of sequent calculus systems. A constant of the formal system will be considered logical if it has left and right introduction rules. A non-logical constant is any other constant whose meaning is specified by axioms or theories: such constants do not, in general, participate in a cut-elimination theorem.

∗This paper appears in the Proceedings of the 1992 Workshop on Extensions to Logic Programming, edited by E.

Lamma and P. Mello, Lecture Notes in Computer Science, Springer-Verlag.

There seems to be two broad ways in which connections between concurrency and proof theory can be and are being developed: one uses proof reduction and the other proof search.

The functional programming approach. Functional programs can be viewed as natural deduction proofs and computation on them as the process of proof normalization. Using familiar correspondences between natural deduction proofs and normalization with sequent calculus and cutelimination in intuitionistic logic [Pot77, Fel91], functional programs can be seen as sequent proofs and computation as cut-elimination. Traditionally, the sequents used are of the form Δ ⟶ G, where Δ is a set of propositions (generally typing judgments) and G is a single proposition. Such sequents are called single-conclusion sequents.

Following ideas of Girard presented in [Gir87], Abramsky [Abr90, Abr91] has extended this interpretation of computation to multiple-conclusion sequents, that is, sequents of the form Δ ⟶ Γ, where Δ and Γ are both sets (actually, multisets) of propositions. In this setting, cut-elimination specifies concurrent programming. In particular, Abramsky presents a method for “realizing” the computational content of multiple-conclusion proofs in linear logic that yields concurrent programs in CCS, CSP, and the π-calculus. In these realized programs, cut-elimination in proofs is modeled by communication.

The logic programming approach. In the logic programming setting, programs are theories (collections of formulas) describing the meaning of non-logical constants and computation is identified with the search for cut-free sequent proofs. Here, the sequent Σ; Δ ⟶ G is used to represent the state of an idealized logic programming interpreter in which the current set of non-logical constants is Σ, the current logic program (theory) about those constants is the set of formulas Δ and the formula to be established, called the query or goal, is G.

A logic and proof system will be consider a logic programming language if a simple kind of goal-directed search is complete. This kind of definition of logic programming was first given in [MNPS91] for single-conclusion sequents, where the technical notion of uniform proof provides an analysis of goal-directed search. A uniform proof is a cut-free, single-conclusion sequent proof where every sequent whose right-hand side is non-atomic is the conclusion of a right-introduction rule. In an interpreter attempting to find a uniform proof, the structure of the right-hand side (the goal) can be reflected directly into the proof being constructed. The given logic and proof system is called an abstract logic programming language if a sequent has a proof if and only if it has a uniform proof. First-order and higher-order variants of Horn clauses and the more expressive hereditary Harrop formulas can be used as the basis of abstract logic programming languages [MNPS91].

In abstract logic programming languages, the search semantics of a logical connective in the goal is independent from its context (the program): contexts are only considered to help in proving atomic formulas. For example, if our logical system is intuitionistic logic, an attempt to prove the sequent Σ; Δ ⟶ G_{1} ∨ G_{2} could be replaced by a proof of either Σ; Δ ⟶ G_{1} or Σ; Δ ⟶ G_{2}, no matter what formulas are contained in Δ. This is not a complete strategy for full intuitionistic logic: while there is a proof of the sequent Σ; p∨q ⟶ q ∨p, its last inference rule is not ∨-R, that is, there are no proofs of Σ; p ∨ q ⟶ q or of Σ; p ∨ q ⟶ p. When the syntax of programs are restricted adequately, completeness of uniform proofs can be established. The resulting restriction then determines a logic programming language. Within this setting, cut-elimination plays the meta-theoretic role of guarantor of canonical models for logic programs (see, for example, [Mil92, HM92]).

Unfortunately, the definition of uniform proofs given here is restricted to only single-conclusion sequent proofs systems. Extending this notion of goal-directed search to multiple conclusion sequents runs into the following simple problem: if the right-hand side of a sequent contains two or more non-atomic formulas, how should the logical connectives at the head of those formulas be introduced? There seems to be two choices. One approach simply requires that one of the possible introductions be done. This has the disadvantage that there might be an interdependency between right-introduction rules in that one may need to appear lower is a proof than another. In this case, logical connectives in the goal would not reflect directly and simply into the structure of the proof. A second approach requires that all right-hand rules should be done simultaneously. Although it is difficult to deal with simultaneous rule application in the sequent calculus, we can employ permutations of inference rules within the sequent calculus [Kle52]. That is, we can require that if two or more right-introduction rules can be use to derive a given sequent, then all possible orders of applying those right-introduction rules can be obtained from any other order simply by permuting right-introduction inferences. Using this second approach, we shall say that a cut-free sequent proof Ξ is uniform if for every subproof Ψ of Ξ and for every non-atomic formula occurrence B in the right-hand side of the endsequent of Ψ, there is a proof Ψ′ that is equal to Ψ up to permutation of inference rules and is such that the last inference rule in Ψ′ introduces the top-level logical connective occurring in B. It is easy to see that this definition of uniform proof generalizes the one given above for single-conclusion sequents.

As we shall see , the π-calculus can be viewed as a multiple-conclusion logic programming language in the sense that certain sequents are provable if and only if they have multiple-conclusion uniform proofs.

Our analytic tools are taken from the sequent calculus, especially the refinement of that subject found in linear logic [Gir87], and from logic programming, particularly the topics of goal-directed provability and 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 [MPW89a, MPW89b, Mil91, MPW91] as a particular example of a process calculus. This calculus is, of course, rich and presents several interesting challenges.

2 Translating π-calculus expressions into logic

Besides assuming some familiarity with sequent calculus, we shall also assume that the reader is familiar with the π-calculus as given in either [Mil90] or [MPW89a]. The principle mechanism of the π-calculus is the synchronization of two agents and the sending of a name from one agent to another. Synchronization is familiar from CCS; value passing is new to the π-calculus. The expression x̄z.P describes an agent that is willing to transmit the value z on the wire x (x and z are names). The expression x(y).Q denotes an agent that 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. The central computational step of the π-calculus is the 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), provided that z is not free in x(y).R. This scope restriction is always easy to accommodate since we shall assume that αconversion is available for changing the name of bound variables. This expression can now be reduced to (z)(P |Q|R[z/y]), where 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 (using α-conversion) and sending them outside their scope is an important part of the computational power of the π-calculus.

The silent transition τ is not discussed at all in this paper: although the techniques described below should be able to address τ, the appropriate methods for this have not yet been investigated.

Below we describe three translations of π-calculus agent expressions into logical expressions. The first two are simple duals of each other; the third is a simplification of the first.

The disjunctive translation. The first translation requires the logical constants ⊕ (additive disjunction), &(par, multiplicative disjunction), ? (the exponential “why not”), ∀, and ⊥ (the identity for & ). Given its dependence on the additive and multiplicative disjunctions of linear logic, this translation is called the disjunctive translation. The following three simply typed, nonlogical constants are also required (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 meta-level that contains the simply typed λ-calculus and quantification at higher-order types.

The disjunctive 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 ⟩⟩ = send x y ⟨⟨P ⟩⟩ ⟨⟨x(y).P ⟩⟩ = get x λy⟨⟨P ⟩⟩
⟨⟨[x = y]P ⟩⟩ = match x 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 −∘ get x R & send x y S]
∀_{i}x∀_{i→o}P [P −∘ match x 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. A similar treatment of higher-order type quantification for Horn clauses can be found in [NM90].

The conjunctive translation. It is trivial to dualize the disjunctive translation 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 axiomatized with the formulas

∀_{i}x∀_{i}y∀_{o}S∀_{i→o}R [get x R ⊗ send x y S −∘ Ry ⊗ S]
∀_{i}x∀_{o}P [match x x P −∘ P]

This translation is called conjunctive because it uses the multiplicative and additive conjunctions.

The formal analysis below is completely dualizable, so there appears to be no formal reason to pick one translation over the other. 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.

The following two extra-logical motivations can be offered for choosing the disjunctive translation over the conjunctive translation.

Goal reduction in logic programming and agent reduction in the π-calculus. In logic programming based on single-conclusion sequents, a uniform proof that results from the successful search for a proof of a sequent Σ; Δ ⟶ G records the goal reductions applied to G in the right-hand side of the proof’s sequent when read from the bottom of the proof. If the disjunctive translation is used, a similar observation can be applied to the π-calculus: agent reduction is recorded in the right-hand sides of the sequents when read from the bottom. Andreoli and Pareschi [AP91] have made a similar choice in the representation of agent reduction using a kind of multiple-conclusion Horn clause. The conjunctive translation estranges this parallel since reductions would take place on the left-hand side.

Scope extrusion as a multiple-conclusion phenomenon. A natural notion of scoping occurs in logic programming based on single-conclusion sequents. For example, the search for a uniform proof of the sequent Σ; Δ ⟶ D ⊃ G reduces to the search for a uniform proof of the sequent Σ; Δ, D ⟶ G. If Δ is considered to be the current program held by a logic programming interpreter, then D can be seen as a program unit that is added to the current program during a computation. A notion of modular programming for logic programming was developed in [Mil89] based on this simple observation. To enforce that this notion of modular programming obeys the correct notion of scoping, single conclusion sequent calculus is required. Consider, for example, searching for a uniform proof of the sequent Σ; Δ ⟶ G_{1} ∨ (D ⊃ G_{2}) using the usual intuitionistic introduction rules for ∨-R and ⊃-R [Gen69]. This search would lead to the search for proofs of either the sequent Σ; Δ ⟶ G_{1} or Σ; Δ, D ⟶ G_{2}. In particular, the formula D is only available to help prove the formula G_{2}: its scope does not include G_{1}. This formula is, however, classically 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. Gentzen’s characterization of the differences between intuitionistic and classical logics as arising from differences in using single and multiple conclusion sequents provides an elegant analysis of scope extrusion. Consider the following sequent proof.

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

The occurrence of p in the left of the initial sequent has as its scope all the formulas on the right: in the intuitionistic case, there can only be one such formula on the right and, hence, scope cannot be liberalized in this way.

If the disjunctive translation is used, scope extrusion in the π-calculus can be accounted for in an analogous fashion. In this case, however, scope extrusion arises between the interaction of the ∀-R rule and multiple conclusions. For a simple example, consider the sequent Σ; p ⟶ (∀x_{i}.q) ∨ (∃y_{i}.p), where we assume that Σ has no constant whose type contains i. This sequent is provable only if we admit multiple conclusion sequents in its proof. Below is a proof of this sequent.

{Σ, x : i; p ⟶ q, p \atop Σ, x : i; p ⟶ q, ∃y_{i}.p} ; Σ; p ⟶ ∀x_{i}.q, ∃y_{i}.p ; Σ; p ⟶ (∀x_{i}.q) ∨ (∃y_{i}.p)

Here, it is an eigen-variable that has its scope liberated. As we shall see, scope extrusion in the π-calculus will be explained by this use of eigen-variables. In the conjunctive translation, similar proofs are possible but the correspondence to scope extrusion in logic programming would disappear and the distinctions between single-conclusion and multiple-conclusion sequents would not then be relevant.

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 the disjunctive translation and assuming that + and ! are mapped to logical constants.

Structural equivalence. Before describing our final translation (a variant of the disjunctive translation), we present a simple method for determining structural equivalence between two agents. By Σ; P ⊢ Q we mean that the formula Q is provable from the formula P given the signature of constants Σ: a formal definition for this three-place predicate is given shortly. The notation Σ; P ⊣⊢ Q simply means that Σ; P ⊢ Q and Σ; Q ⊢ P. We shall extend the domain of ⊢ and ⊣⊢ by allowing P and Q to be agent expressions: in this case, one of the above two translations is used to coerce an agent into a formula. Notice that the extension of Σ; P ⊣⊢ Q is independent of which translation is used and if Σ is held fixed, the resulting binary relation is an equivalence. Also, since no axioms about communication or matching are used, only the logical identities are used to determine this equivalence. As a result, this equivalence to a good candidate for structural equivalence. Figure 1 provides some examples of Σ; P ⊣⊢ Q and Σ; P ⊢ Q (for which we assume the use of the disjunctive translation described above).

A final translation. 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 6), 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, 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 axiomatize the reduction nature of + and ! by using the clauses

\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

\frac{Σ; Δ_{1} ⟶ P, Γ_{1} Σ; P, Δ_{2} ⟶ Γ_{2}}{Σ; Δ_{1}, Δ_{2} ⟶ Γ_{1}, Γ_{2}}  \frac{t a Σ-term Σ ∪ \{x\}; Δ ⟶ Γ}{Σ; [t/x]Δ ⟶ [t/x]Γ}

Figure 3: Two forms of the cut-rule

∀_{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 encode 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 notation Σ; Δ ⊢ Γ 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 rule (−)R has the proviso that y ∉ Σ, and the rule (−)L has the proviso that 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 notation Σ; Δ ⊣⊢ Γ means Σ; Δ ⊢ Γ and Σ; Γ ⊢ Δ. Again, the relation ⊣⊢ will be used as structural equivalence. Since we have reduced the number of logical connectives, this equivalence is now weaker than is described in Figure 1. For example, P + Q is no longer ⊣⊢ related to Q + P.

The cut-elimination theorem for linear logic [Gir87] shows that the inference rules in Figure 3 are admissible with respect to the basic set of rules. Given the cut-elimination theorem, provability in this proof system is obviously decidable. Note that we have not given any status to the non-logical constants and their axioms in this proof system. We do this in the next section.

3 Process clauses and process theories

We now step back from the particular example of the π-calculus to consider some general considerations of the logical framework we have picked.

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 x̄ may be of type i and o, as well as higherorder 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 [AP91] where & and ⊤ (erasure) are also permitted in the body of clauses: their formalism, however, permits neither universal quantification in the body of clauses nor quantification of highertype variables.

A process theory is a finite, possibly empty, set H of process clauses. An H-proof is a proof built using the rules in Figure 2 and one inference of the form

\frac{Σ; Δ ⟶ Γ, 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 site is the multiset containing both occurrences of P; 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. For example, the following two proof fragments demonstrate that (−)R and |R permute over each other.

{Σ, y : i; Δ ⟶ P, Q, [y/x]R, Γ \atop Σ; Δ ⟶ P, Q, (x)R, Γ}

Σ; Δ ⟶ P | Q, (x)R, Γ

{Σ, y : i; Δ ⟶ P, Q, [y/x]R, Γ \atop Σ, y : i; Δ ⟶ P | Q, [y/x]R, Γ}

Σ; Δ ⟶ P | Q, (x)R, Γ

We assume here that y ∉ Σ.

Proposition 1 All pairs of right rules (nil-R, |R, and (−)R) and H-inference rules 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].

Here, prefixing is represented by two non-logical constants, both of type i → o → o. The order of the two H-rules in the proof fragment

{Σ; 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 or H-inference 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 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 on its left. This contradicts the choice of Ξ. □

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

Proof.

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 or the initial sequent rule since cut permutes up through all the right introduction rules and H-inference 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} ends in a right introduction of that constant and Ξ_{2} ends in a left introduction of that constant. The usual movement of cut upwards in a proof will work in this case. Finally, if P is atomic, then Γ_{2} is the multiset that consists of just P, so we can simply use Ξ_{1} as the proof of Σ; Q ⟶ Γ_{1}, Γ_{2}.

The proof that the other cut rule involving substitution is admissible is simpler and more direct. □ The following proposition demonstrates that process theories can be viewed as multiple conclusion

logic programming languages.

Proposition 5 The sequent has an H-proof if and only if it has a uniform H-proof.

Proof. Assume that Ξ is a cut-free, atomically closed sequent proof. An atomically closed proof is a proof in which all initial sequents contain only atomic formulas: it is easy to show that a sequent has a proof if and only if it has an atomically closed proof. Using the definition of uniform proofs for multiple conclusion sequents given in the introduction, we now show that Ξ is, in fact, a uniform proof. Let Ψ be a subproof of Ξ that proves the sequent Σ; Δ ⟶ Γ and let B be a non-atomic formula occurrence in Γ. Since the sites of H-rules contain only atoms and since initial sequent rules involve only atoms, the top-level logical connective of B must be introduced somewhere is Ψ. Given that all left rules can be permuted upward through a proof and that all right-rules and H-inference rules also permute over each other, a series of permutations can carry the proof Ψ into a proof Ψ′ in

\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  \frac{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.

which the last inference rule introduces the top-level logical connective of B. Thus, Ξ is a uniform proof. □

Process calculi are generally described using a notion of reduction. We will focus on unlabeled reduction, such as is found in [Mil90]; an example of labeled reductions is used in Section 5. 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 6 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.

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.

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 −∘ get x R & send x y S]
∀_{i}x∀_{i→o}P [P −∘ match x 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.

Notice that it is very easy to accommodate definition of agents using process clauses: the definition C(x̄) = P, where the free variables of P are contained in the list x̄, can be translated to the process clauses ∀x̄[P −∘ C(x̄)]. Such clauses can be added to the base π-theory.

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, [MPW89a, MPW89b]. 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 may be needed to account for a single reduction step of the π-calculus.

3. The GEN and INS rules do not correspond to any rules of [MPW89a, MPW89b]. As a reduction rule, GEN does seem odd since it does not seem to be making anything simpler. 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 [MPW89a]. Of course, the process calculi defined here may be of their own interest.

5 An analysis of the propositional fragment

Because the π-calculus communicates values of type i only, we shall think of the π-calculus as a first-order theory. In this 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 −∘ get x R & send x 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 get a P and send a 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.

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 extend the notion of agents to co-agents, one of which will be “truth.” Given some notion 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 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]].

\overline{Σ; Δ ⟶ ⊤, Γ} ⊤-R  \frac{Σ; Δ ⟶ Γ, W_{1}  Σ; Δ ⟶ Γ, W_{2}}{Σ; Δ ⟶ Γ, W_{1} & W_{2}} &-R

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

• 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 [Hen88]. 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 such a tensor tester 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-agent 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 7 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 π_{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 coagents, 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.

\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, Δ}

\frac{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.

Proposition 8 If ⟶ Γ, 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. Instead 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 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} (Proposition 8). 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 8 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 9 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 9 implies that ⊢^{ω} Γ, W if and only if ⊢^{n} Γ, W.

Proposition 10 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 9, ⊢^{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 9 ⊬^{ω} Γ, W if and only if ⊬^{n} Γ, W. But this is equivalent to ⊢^{n+1} Γ, ¬W. By Proposition 9 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 11 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 10 (iii), ⊢^{ω} P, ¬W. But this implies that ¬W ∈ [[P]] and ¬W ∈ [[Q]] which contradicts Proposition 10 (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 rule or axiom is provided. (It is possible to identify 1 with the constant of the same name used in linear logic [Gir87] 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 | ā.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 12 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 applying 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 defined to be ∧_{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 assertion formulas: (&_{i∈I}W_{i})^{o} = ∧_{i∈I}W_{i}^{o}, (a.W)^{o} = ⟨ā⟩W^{o}, and (¬W)^{o} = ¬W^{o}.

Proposition 13 Let W ∈ C_{ω} and let P be an agent expression. Then ⊢^{ω} 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 12, ⊢^{ω} P, W. Conversely, if ⊢^{ω} P, a.W′ then, by Proposition 12, 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 14 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 non-logical 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.

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 [Abr87] should be related to the material just presented. A very good test of our approach would be to see if the modal logics recently described for the π-calculus in [MPW91] can be motivated using the notion of co-agents.

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. Acknowledgements. The anonymous reviewers of an earlier draft of this paper have suggested several improvements to presentation of this paper. The author has been funded in part by ONR N00014-88-K-0633, NSF CCR-91-02753, and DARPA N00014-85-K-0018.

References

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

[Abr90] Samson Abramsky. Computational interpretations of linear logic. Technical Report Research Report DOC 90/20, Imperial College, October 1990.

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

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

[Fel91] Amy Felty. A logic program for transforming sequent proofs to natural deduction proofs. In Peter Schroeder-Heister, editor, Extensions of Logic Programming: International Workshop, Tübingen FRG, December 1989, volume 475 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1991.

[Gen69] 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.

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

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

[HM92] Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Journal of Information and Computation, 1992. Invited to a special issue of papers from the 1991 LICS conference.

[Kle52] Stephen Cole Kleene. Permutabilities of inferences in gentzen’s calculi LK and LJ. Memoirs of the American Mathematical Society, 10, 1952.

[Mil89] Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, 6:79 – 108, 1989.

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

[Mil91] Robin Milner. The polyadic π-calculus: A tutorial. LFCS Report Series ECS-LFCS-91-180, University of Edinburgh, October 1991.

[Mil92] Dale Miller. Abstract syntax and logic programming. In Logic Programming: Proceedings of the First and Second Russian Conferences on Logic Programming, number 592 in Lecture Notes in Artificial Intelligence, pages 322–337. Springer-Verlag, 1992. Also available as technical report MS-CIS-91-72, UPenn.

[MNPS91] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

[MPW89a] 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.

[MPW89b] 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.

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

[NM90] Gopalan Nadathur and Dale Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777 – 814, October 1990.

[Pot77] Garrel Pottinger. Normalization as a homomorphic image of cut-elimination. Annals of Mathematical Logic, 12(3):223–357, 1977.