To appear in: Theoretical Computer Science (1994), Proceedings MFPS8.

On the π-Calculus and Linear Logic

G. Bellin ^{∗}  P. J. Scott ^{†}

July 20, 1994

Abstract

We detail Abramsky’s “proofs-as-processes” paradigm for interpreting classical linear logic (CLL) [13] into a “synchronous” version of the π-calculus recently proposed by Milner [27, 28]. The translation is given at the abstract level of proof structures. We give a detailed treatment of information flow in proof-nets and show how to mirror various evaluation strategies for proof normalization. We also give Soundness and Completeness results for the process-calculus translations of various fragments of CLL. The paper also gives a selfcontained introduction to some of the deeper proof-theory of CLL, and its process interpretation.

Contents

1 Introduction 2

2 The π-Calculus 5 2.1 Basic Synchronous π-calculus . . . . . . . . . . . . . . . . . . 5 2.2 Full Synchronous π-calculus . . . . . . . . . . . . . . . . . . . 7 3 Proofs-as-Processes 9

∗Research Supported by Esprit grant BRA Project 3245.

†Research supported by an operating grant from the Natural Sciences and Engineering Research Council of Canada, FCAR Team Grants from Québec, and a Bilateral Exchange Grant from NSERC and the Royal Society of Britain

3.1 The Abramsky Translation: the multiplicatives . . . . . . . . 10 3.2 The Abramsky Translation: the additives . . . . . . . . . . . . 12 3.3 The Abramsky Translation: the exponentials . . . . . . . . . . 15

4 Translating MLL Proof Structures 17 4.1 MLL Proof Structures . . . . . . . . . . . . . . . . . . . . . . 17 4.2 Translation of MLL proof structures . . . . . . . . . . . . . . 20

5 Information Flow 26 5.1 Pure structures . . . . . . . . . . . . . . . . . . . . . . . . . . 28 5.2 Translation of pure structures into the π-calculus . . . . . . . 30 5.3 Deadlock-free Structures . . . . . . . . . . . . . . . . . . . . . 32 5.4 Orienting Proof Nets and Linear λ-terms . . . . . . . . . . . . 35 5.5 Milner’s linear λ-terms . . . . . . . . . . . . . . . . . . . . . . 45

6 The Additives 49 6.1 Problems with the Additives . . . . . . . . . . . . . . . . . . . 49 6.2 Proof Structures with Boxes . . . . . . . . . . . . . . . . . . . 54 6.3 Slicings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 6.4 Translation of MALL proof structures . . . . . . . . . . . . . . 64

7 The Exponentials 68

8 Acknowledgements 71

1 Introduction

Milner’s π-calculus [25, 26] is a recent addition to a large and active literature on the foundations of concurrent computation. These theories attempt to analyze and clarify the world of concurrently communicating processes (and associated programming languages) in much the same way as lambda calculus and other models of computation have done for the sequential world [26].

In a different direction, Jean-Yves Girard [13, 16, 17, 18] has instituted the rapidly growing area of linear logic, a radical modification of traditional logic which appears to have strong connections with theoretical computer science. In several publications [16, 15] Girard has suggested that linear logic should have deeper connections with parallelism and concurrent computation. This suggestion was taken up more formally by Abramsky [1] in an influential series of lectures, and in some unpublished work of Robin Milner [24].

The Abramsky view is essentially a modification of the familiar formulaeas-types (Curry-Howard) isomorphism: instead of proofs being functions (qua lambda terms), Abramsky views proofs as processes (e.g. π-calculus or CCS terms). Processes are thought of as communicating through distinguished ports or channels, named by free variables. The key observation is that proof-theoretical communication (i.e. the Cut rule in the Gentzen formalism) is modelled by communication along a private internal channel (i.e. hiding) in the process-calculi world. It should follow that the dynamics of logical computation, namely the cut-elimination or normalization process for proofs, be reflected in the rewriting theory for process algebra terms.

Alas, this is precisely the point where the concurrency and logic worlds begin to diverge. For example, the fundamental case of cut-elimination requires modular or contextual rewriting (since we may need to eliminate a cut embedded high-up in a proof tree.) Most experts on concurrency theory are simply unwilling to allow rewriting within all contexts, particularly those involving nondeterministic choice +; typically an interaction with a process P + Q chooses one of the components, and the other component is immediately destroyed. The question is: to what extent can we represent logical computation within the accepted concurrency world?

Robin Milner [27] recently developed a version of the π-calculus (the synchronous π-calculus) purposely supporting some of the logical rewriting envisioned by Abramsky. In this paper, we analyze the Abramsky view in detail for the synchronous π-calculus. We shall translate proofs (and certain normalization strategies) for the three important levels of linear logic: the multiplicatives, the additives, and the exponentials. In the case of multiplicative linear logic, the π-calculus translation provides a lock-step simulation of proof net reduction. As soon as the additive and exponential connectives are included, again problems of rewriting in contexts begin to appear (even for the synchronous π-calculus). We show how we may soundly and completely reflect the proof theory (though not necessarily lock-step simulation) by different methods:

• Modify the π-calculus reduction strategies to more closely mimic those inherent in logic (e.g. (i) by introducing guarding of terms [25] or (ii)

by a version of Girard’s theory of slicing of proof nets [13, 6]).

• Modify linear logic evaluation strategies to take into account the extant theory of π-calculus (e.g. restriction to Geometry of Interaction-style evaluation strategies [17, 18])

One of the theses of this work is that the Abramsky-style translations (of linear logic) into the process world actually have less to do with logic than one might think: they are essentially only about the abstract pluggings in proof structures [13, 16, 12], and we formulate many of our results in this more general setting. This phenomenon may be already expected by experts in concurrency theory, who view process algebras as a theory of “hand-shaking” protocols (which have nothing to do with logic) but it came as a surprise to us. What seems particularly curious–given this “alogical” nature of π-calculus–is that much of the theory (as described below) is nonetheless coherent (and complete) for various logical proof reduction (normalization) strategies.

A second theme of this paper is that information flow in cut elimination is related to sending/receiving protocols in π-calculus. In Section 5, this intuition is made precise in a detailed analysis of information flow in pure nets [11, 22, 8] which is a theory of graphical networks for representing untyped lambda terms in the style of proof nets for linear logic. We shall show how to dynamically orient a proof-net (assigning the symbols I (for input) and O (for output)) in a manner coherent with respect to introduction and elimination rules for natural deduction, and cut-elimination (normalization). This permits a systematic analysis of orientation and information flow in the Abramsky π-translation, obviating (for example) the need for bidirectional buffers.

Finally, the paper contains a survey of more advanced proof-theory for linear logic, including additive boxes and Girard’s theory of slicing, and how to represent these notions in the π-calculus.

At this point, we should mention a few papers on related themes. The paper of Monteiro [29] gives a lock-step simulation of proof nets for multiplicative linear logic into a version of CSP, although the author does not handle the additives or exponentials. This paper is the first example of the kind of analysis considered here (apparently independent of Abramsky [2]) of a sound and faithful translation of logical deduction in a language of concurrency. The paper of Dale Miller [23] is based on a logic programming view of the π-calculus: Miller codes the π-calculus as a theory in linear logic, and discusses how techniques of logic programming (proof search, etc.) are useful in understanding some of the metatheory of the π-calculus. This paper has no direct connection with the Abramsky program of proofs-as-processes, although some of the syntactical considerations are mildly similar.

2 The π-Calculus

The following version of the π-calculus [24, 25] has recently been suggested by Milner [27] for its possible connections to linear logic, a connection we shall develop in more detail below.

2.1 Basic Synchronous π-calculus

There is an infinite family X of variables called names. We shall denote names by x, y, z, … ∈ X and vectors of names by x⃗ or x̃. The π-calculus describes certain basic entities known as processes, having the following syntactic forms:

• (νx)P P ∥ Q πP

where:

(i) The prefixes π are formal expressions of the form \overline{x}⟨y⃗⟩ or x(y⃗), where x is a name, and y⃗ is a vector of names, possibly of length zero. We say P is the scope of prefix π in the process πP.

(ii) νx and (y⃗) are name-binding operators with the obvious scopes. Thus in the expression (νx)P, the name x is bound and the scope of νx is P; the operation ν is known as hiding: the variable x in the process (νx)P is said to be a hidden name. Similarly, in the expression x(y⃗)P, the names y⃗ are bound (and x is free) and P is the scope.^{1} The intended interpretation is that π-calculus describes a theory of processes concurrently communicating through distinguished ports or channels (think of telephone systems or a computer network). The intended meaning of names [24] is that they represent communication channels, i.e. ports for the communicating behaviour of these interactive processes. A fundamental such operation is the “hand-shaking” protocol, in which one agent’s channel identifies itself to another agent’s channel, and the receiver signifies it is ready to receive the communication. This is encapsulated in the two syntactic operations \overline{x}⟨y⃗ ⟩P , which means “send the names y⃗ along the channel x and then do process P ”, and x(y⃗)P which means: “receive along x arbitrary names for the bound names y⃗ ”. Another fundamental operation is “hiding”, in which a channel is declared private and so is inaccessible to the outside world. Finally P ∥ Q denotes the process in which P and Q are acting concurrently (in parallel) while • denotes the nil process.

1More precisely, we may define the set of free and bound names in processes P (= fn(P) and bn(P), respectively ) as follows: (a) fn(•) = bn(•) = ∅. (b) fn(P ∥ Q) = fn(P)

∪ fn(Q) ; bn(P ∥ Q) = bn(P) ∪ bn(Q) . (c) fn(\overline{x}⟨y⃗⟩P) = \{\overline{x}, y⃗\}∪ fn(P) ; bn(\overline{x}⟨y⃗⟩P) = bn(P). (d) fn(x(y⃗)P) = fn(P) ∪ {x}; bn(x(y⃗)P) = bn(P) ∪ {y⃗}. (e) fn((νx)P) = fn(P)

\ {x}; bn((νx)P) = bn(P) ∪ {x}.

The following rules govern the behaviour of π-calculus terms. We assume there is a congruence relation ≡ on π-terms which satisfies the following additional properties:

1. ω_{1}ω_{2}P ≡ ω_{2}ω_{1}P provided no free variables become bound, nor any bound variables become free.

2. ω(P ∥ Q) ≡ ωP ∥ Q , provided bn(ω) ∩ fn(Q)= ∅.

3. ∥ –as a binary operation on processes– satisfies the axioms of a commutative monoid with unit •.

4. (νx)• ≡ •.

5. (νx)(νy)P ≡ (νy)(νx)P .

As usual, we identify processes which are identical except for change of bound variables (α-conversion). We often omit writing the process • (cf. [25] ), writing x̄⟨y⃗ ⟩ in place of x̄⟨y⃗ ⟩•.

We make the π-calculus into a rewriting system by assuming the following notion of basic 1-step reduction:

x̄⟨y⃗ ⟩P ∥ x(z⃗)Q ≻ P ∥ Q[y⃗/z⃗]

where Q[y⃗/z⃗] denotes the simultaneous substitution of the names y_{i} for the (possibly free) names z_{i} in Q. We consider the rewriting theory modulo ≡, so that for all contexts C we have: P ≻ Q ⟹ C[P] ≻ C[Q]

This version of the π-calculus allows some unexpected rewritings (modulo ≡); for example: x̄⟨y⃗ ⟩x(z⃗)P ≻ P [y⃗/z⃗]. Proof: x̄⟨y⃗ ⟩x(z⃗)P ≡ x̄⟨y⃗ ⟩(• ∥ x(z⃗)P) ≡ (x̄⟨y⃗ ⟩• ∥ x(z⃗)P) ≻ P [y⃗/z⃗].

2.2 Full Synchronous π-calculus

We add to the syntax of the basic theory above, an additional process formation rule : finite summation. That is, the processes now have the following form:

• (νx)P P ∥ Q πP P + Q

P + Q represents a process able to take part in one (but only one) of the alternatives P, Q ; however, the choice is not made by the process, but by the environment at the time of a particular interaction. We add to the previous congruence rules for ≡ the following rule

• The operation + –considered as an operation on processes– satisfies the axioms of a commutative monoid with identity •.

Moreover, we add to the reduction rules above the following additional basic rewrite rule:

(P + x̄⟨z⃗ ⟩Q) ∥ ((x(y⃗)R) + S) ≻ Q ∥ R[z⃗/y⃗]

We do not assume ≻ is a congruence with respect to + –i.e. we do not assume rewriting under a +. It is worth remarking that the choice operator + above has a powerful effect: it destroys all “side processes” P and S not actually involved in the interaction ^{2}. This is one of the main problematic operators in understanding π-calculus from the logical viewpoint.

2In particular, S is arbitrary, so may itself be of the form x(y⃗)S′. So, assuming commutativity of +, basic interactions of the above form could sometimes ( up to ≡) arbitrarily pick either component when rewriting a summand.

Two important notions from the ordinary π-calculus are guarding and distributivity. Guarding is a method of forcing certain communications to occur in a given order, thus imposing a restriction on the evaluation strategies available for π-calculus terms. Syntactically, a dot after a prefix, as in ω.P, denotes a process in which communication must occur with ω before any communication can occur within P ( so in a sense the prefix ω “guards” P against contact with ambient processes, as well as preventing internal communication within P until ω is discharged). Writing the dot “.” has no other formal status than to denote this ordering of evaluation. If we speak of synchronous π-calculus with guarding, we shall mean (unless otherwise stated) that all processes can have prefix sequences which may be mixtures of either guarded or unguarded ones.

Rewriting theory in the presence of guarding is a slight modification of that of the basic synchronous calculus above. We modify the rules mentioned in section 2.1, as follows:

• We can permute unguarded prefixes up to ≡ , with the usual provisos on free and bound variables, with the following restriction: properties (1) and (2) of the congruence ≡ do not apply if one of the prefixes ω_{i} or ω is a guarding prefix.

• A subterm ω.P can only be reduced via communication with ω, not through reduction within P.

In particular, under guarding rewriting is not contextual or compositional.

Example: The ordinary process term x̄⟨z⟩P ∥ x(y)Q rewrites as follows:

x̄⟨z⟩P ∥ x(y)Q ≻ P ∥ Q[z/y]

whereas the guarded term u(x).[x̄⟨z⟩P ∥ x(y)Q] is at the moment inert: it cannot have any internal action and can only communicate through the variable u.

Milner [25] uses guarding to constrain evaluation strategies (e.g. in simulating the lazy λ- calculus in the π-calculus). Similarly, in section 6.2 we shall use guarding to mirror certain restricted evaluation strategies in linear logic (needed for our completeness theorems for additive proof net reduction).

Distributivity (of ∥ and unguarded prefixes) with respect to + is discussed in [25] and other references referred to there. The main feature (from our viewpoint) is that distributive laws are needed to mirror the commutative reductions of linear logic (cf [13]).

3 Proofs-as-Processes

In this section we introduce a version of the Abramsky translation [2] mapping proofs in linear logic into process calculi, and discuss Soundness and Completeness Theorems for this translation. As mentioned in the Introduction, our treatment is an adaptation of the original Abramsky work to the synchronous π-calculus, a calculus better suited to this kind of analysis. The idea is to assign to a proof annotated with free variables, a process term whose free variables are exactly the variables in the conclusion of the proof:

⋮ . ; ⊢ x_{1} : A_{1}, …, x_{n} : A_{n}  ⇝  P x_{1}, …, x_{n}

One may think of the free variables x_{1}, …, x_{n} as “communication ports” in an interface connecting a process to its surroundings.

We assume the reader is familiar with the usual presentations of classical linear logic (CLL) by one-sided sequents [1, 13]. We consider, in separate sections below, an involutive negation ( )^{⊥} along with the three levels of CLL connectives emphasized by Girard [13], which are pairwise related by de Morgan duality: (i) multiplicatives: the connectives {⊗,^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} } , i.e. tensor and dual tensor (= par), (ii) additives : the connectives {&, ⊕}, i.e. product and coproduct , (iii) exponentials: the connectives {!,?} , which are storage operators. We write MLL for the multiplicative fragment, MALL for the multiplicative and additive fragment, and CLL for the full theory. Note that we ignore the role of the units in all that follows. For simplicity, we also consider only atomic axiom links.

Much of the proof theory used in this paper is standard; further details for the case of linear logic are contained in Girard’s original paper [13], Troelstra’s recent book [32], as well as in [6, 7], [12], etc.

3.1 The Abramsky Translation: the multiplicatives

Logical Rule  π-translation
⊢ x : A, y : A^{⊥}  Ixy = x(a)\overline{y}⟨a⟩
\begin{matrix}{⋮ . F \atop ⊢ w⃗ : Γ, x : A} & {⋮ . G \atop ⊢ v⃗ : Δ, y : B} \\ ⊢ w⃗ : Γ, v⃗ : Δ, z : A ⊗ B \end{matrix} ⊗  ⨂_{z}^{x,y}(F, G)w⃗v⃗z = νxy(\overline{z}⟨xy⟩(F w⃗x ∥ Gv⃗y))

{⋮ . F \atop ⊢ w⃗ : Γ, x : A, y : B} ; ⊢ w⃗ : Γ, z : A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}  (^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{z}^{x,y})(F)w⃗z = z(xy)F w⃗xy

\begin{matrix}{⋮ . F \atop ⊢ u⃗ : Γ, x : C} & {⋮ . G \atop ⊢ v⃗ : Δ, y : C^{⊥}} \\ ⊢ u⃗ : Γ, v⃗ : Δ \end{matrix} Cut Cut^{z}(F, G)u⃗v⃗ = νz(F u⃗[z/x] ∥ Gv⃗[z/y])

It is worth remarking that this translation makes two choices: we choose to interpret ⊗ uniformly as a sender and^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} uniformly as a receiver. Following the terminology of Abramsky and Milner, the operator I in the translation of the axiom is known as an axiom buffer. Note that axiom buffers also translate positive atoms as receivers and negative atoms as senders. A full discussion of information flow and these choices is in Section 5 below. Superscripts on the π-terms ⨂,^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , Cut denote bound variables.

The Cut Algebra for MLL

The following equations represent, in functional (combinator) form, the cut-elimination reductions in MLL.

Symmetric Reductions

(1)  Cut^{x}(F, G) = Cut^{x}(G, F)
(2)  Cut^{x}(F x, Ixy) ≻ F [y/x]
(3) Cut^{z}(⨂_{z}^{x,y}(F x, Gy),^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{z}^{x,y}(Hxy)) ≻ Cut^{y}(Gy, Cut^{x}(F x, Hxy))

(4)  ≡ Cut^{x}(F x, Cut^{y}(Hxy, Gy))

Commutative Reductions

(5)  Cut^{x}(^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{v}^{c,d}F xcd, Gx) = ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{v}^{c,d}Cut^{x}(F xcd, Gx)
(6)  Cut^{x}(⨂_{v}^{c,d}(F c, Gdx), Hx) = ⨂_{v}^{c,d}(F c, Cut^{x}(Gdx, Hx))

where in the first and second commutative reduction equations, ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} and ⨂ do not react with x.

Remark

Note that in the term ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} _{v}^{c,d} Cut^{x}(F xc, Gxd), Cut and Par obviously do not permute. In order to permute inferences, one needs the additional information that c, d occur in the same branch of the proof tree, as in (5) above.

Theorem 1 (Soundness) Let D be a proof in MLL and let π(D) be its π-calculus translation.

(i) If D ≻_{1} D′ by a 1-step symmetric reduction in the cut-elimination process, then π(D) ≻_{1} π(D′) in the synchronous π-calculus.

(ii) If D ≻_{1} D′ by a 1-step commutative reduction in the cut-elimination process, then π(D) ≡ π(D′) in the synchronous π-calculus.

Proof: By induction, following the steps in cut-elimination.

From part (ii) in the above theorem, we see that the π translation really acts on proofs modulo the order of the rules, thus on proof nets [13]. This theorem will be generalized in Sections 4, 5 below to the case of proof structures. We shall also discuss the completeness (or in categorical language, the local fullness) of the π-calculus translation.

It is important to observe that cut-elimination is a modular or compositional property: a reduction D ≻_{1} D′ may occur high up in the proof tree, not necessarily at the bottom node. This requires that reduction in the associated π-terms must be a congruence, i.e reduction must be contextual. This will be the case for the π-terms that arise in the MLL translation. But there will be problems with the Additives and Exponentials, as we shall see below.

3.2 The Abramsky Translation: the additives

Logical Rule  π-translation

{⋮ . P \atop ⊢ w⃗ : Γ, x : A} ; ⊢ w⃗ : Γ, z : A ⊕ B ⊕  L_{z}^{x}(P)w⃗z = (νx)(z(uv)ū⟨x⟩P_{w⃗x})

{⋮ . Q \atop ⊢ w⃗ : Γ, y : B} ; ⊢ w⃗ : Γ, z : A ⊕ B ⊕  R_{z}^{y}(Q)w⃗z = (νy)(z(uv)v̄⟨y⟩Q_{w⃗y})

\begin{matrix}{⋮ . P \atop ⊢ w⃗ : Γ, x : A} & {⋮ . Q \atop ⊢ w⃗ : Γ, y : B} \\ ⊢ w⃗ : Γ, z : A&B \end{matrix} &  &_{z}^{xy}(P, Q)w⃗z = ν(uv)z̄⟨uv⟩[u(x)P_{w⃗x}+v(y)Q_{w⃗y}]

The Cut Algebra: Additives

The following equations are true for proofs in MALL:

Symmetric Reductions

(7)  Cut^{z}(&_{z}^{x,y}(P_{x}, R_{y}), L_{z}^{u}(Q_{u})) ≻ Cut^{x}(P_{x}, Q[x/u])
(8)  Cut^{z}(&_{z}^{x,y}(P_{x}, R_{y}), R_{z}^{u}(Q_{u})) ≻ Cut^{x}(R_{x}, Q[x/u])

Commutative Reductions

(9) Cut^{d}(&_{z}^{x,y}(P_{xd}, Q_{yd}), R_{d}) = &_{z}^{x,y}(Cut^{d}(P_{xd}, R_{d}), Cut^{d}(Q_{yd}, R_{d}))

Theorem 2 (Weak Soundness) Let D be a proof in MALL and let π(D) be its π-calculus translation. Then we have:

1. Let C be any cut such that no &-rule occurs below C. If D ≻_{1} D′ by a symmetric reduction applied to the cut C then π(D) ≻ π(D′) .

2. If the π-calculus admits distributivity of ∥ and prefixes (including hiding) over + and if D ≻_{1} D′ by a commutative reduction then π(D) ≡ π(D′) .

Note that this theorem says the π-translation is sound only for eliminating certain specific cuts. This comes from the fact that ≻ is not a congruence with respect to + (see the Introduction and Section 2). For example, with respect to the restrictions in Theorem 2, eliminating a cut in a term of the form &_{z}^{xy}(P, Q)w⃗z would involve contextual rewriting under a +.

We include some examples of Theorem 2 (Weak Soundness for Additives).

Example 1: The proof below has a & below a cut.

\begin{matrix}{⊢ z : B, q′′ : B^{⊥} \atop ⊢ z : B, w′ : A^{⊥} ⊕ B^{⊥}} & \begin{matrix}\begin{matrix}\begin{matrix}⊢ x : A, p : A^{⊥} & ⊢ y : A, p : A^{⊥} \\ ⊢ w : A&A, p : A^{⊥} \end{matrix} &_{1} & {⊢ x′ : A, p′ : A^{⊥} \atop ⊢ x′ : A, w : A^{⊥} ⊕ A^{⊥}} ⊕L \\ ⊢ p : A^{⊥}, x′ : A \end{matrix} ; Cut_{1} ; ⊢ t : A^{⊥} ⊕ B^{⊥}, x′ : A & {⊢ y′ : B, q′ : B^{⊥} \atop ⊢ t : A^{⊥} ⊕ B^{⊥}, y′ : B} \\ ⊢ t : A^{⊥} ⊕ B^{⊥}, w′ : A&B \end{matrix} &_{2} \\ ⊢ z : B, t : A^{⊥} ⊕ B^{⊥} \end{matrix} ; Cut_{2}

This reduces to (by a symmetric reduction to Cut_{1}, and axiom reduction)

\begin{matrix}{⊢ z : B, q′′ : B^{⊥} \atop ⊢ z : B, w′ : A^{⊥} ⊕ B^{⊥}} & \begin{matrix}\overbrace{⊢ x′ : A, p : A^{⊥}}^{Ix′p} ; ⊢ t : A^{⊥} ⊕ B^{⊥}, x′ : A & {⊢ y′ : B, q′ : B^{⊥} \atop ⊢ t : A^{⊥} ⊕ B^{⊥}, y′ : B} \\ ⊢ t : A^{⊥} ⊕ B^{⊥}, w′ : A&B \end{matrix} \\ ⊢ z : B, t : A^{⊥} ⊕ B^{⊥} \end{matrix} ; Cut_{2}

To the first proof corresponds the π-term (with Cut_{1} and &_{1} in bold)

P tz = Cut_{2}^{w′}(R_{w′}^{q′′}(Izq′′),&_{w′}^{x′y′}(L_{t}^{p}(Cut_{1}^{w}(&_{w}^{xy}(Ixp, Iyp), L_{w}^{p′}(Ix′p′))), R_{t}^{q′}(Iy′q′)))

The process of cut-elimination illustrated above corresponds to rewriting a subterm of P tz as follows: the left hand branch before (and after) Cut_{1} is eliminated corresponds to the following subterm reductions:

(νwuvp′) ( w̄⟨uv⟩[u(x)(x(a)p̄⟨a⟩)+v(y)(y(b)p̄⟨b⟩)] ∥ w(uv)ū⟨p′⟩(x′(c)p̄′⟨c⟩) )

≻ (νuvp′) ( [u(x)(x(a)p̄⟨a⟩) + v(y)(y(b)p̄⟨b⟩)] ∥ ū⟨p′⟩(x′(c)p̄′⟨c⟩) )
≻ (νp′) ( (p′(a)p̄⟨a⟩) ∥ (x′(c)p̄′⟨c⟩) )
≻^{∗} x′(c)p̄⟨c⟩ , after extruding x′, interaction, and eliminating bound p′.
≡ Ix′p , which is the denoted proof of ⊢ x′ : A, p : A^{⊥}.

This illustrates Part 1 of Weak Soundness, except the condition “ no & - rule occurs below a cut”. To understand this restriction, suppose we attempt to continue reduction of the proof, by a symmetric reduction of Cut_{2}, noting that &_{2} is below a cut. We implement this by continuing to reduce the πterm P tz (having already reduced the inner subterm above.) The rightmost subterm of P tz is a sum; the summand containing R_{t}^{q′}(Iy′q′) has the form P_{0} ≡ v′(y′)(νq′)t(r′s′)s′⟨q′⟩(y′(d)q̄′⟨d⟩) for hidden v′. But in the π-calculus, we can rewrite a term occurring in the scope of a sum only after choosing the relevant summand; here, the term P_{0} is discarded by the previous steps. If we were to continue cut-elimination and apply a symmetric reduction to Cut_{2}, then in the associated reduction of the π-term P tz, we eventually obtain an irreducible π-term which does not correspond to a proof, because of the disappearance of P_{0}. We leave the calculation to the reader.

Example 2

We illustrate Part 2 of Weak Soundness. The proof

\begin{matrix}\begin{matrix}⊢ x : A, p : A^{⊥} & ⊢ y : A, p : A^{⊥} \\ ⊢ w : A & A, p : A^{⊥} \end{matrix} & & ⊢ p : A, q : A^{⊥} \\ ⊢ w : A & A, q : A^{⊥} \end{matrix} Cut

becomes, after a commutative reduction,

\begin{matrix}\begin{matrix}⊢ x : A, p : A^{⊥} & ⊢ p : A, q : A^{⊥} \\ ⊢ x : A, q : A^{⊥} \end{matrix} Cut & \begin{matrix}⊢ y : A, p : A^{⊥} & ⊢ p : A, q : A^{⊥} \\ ⊢ y : A, q : A^{⊥} \end{matrix} Cut \\ ⊢ w : A & A, q : A^{⊥} \end{matrix} ; &

and eventually becomes (after axiom reductions)

\begin{matrix}⊢ x : A, q : A^{⊥} & ⊢ y : A, q : A^{⊥} \\ ⊢ w : A & A, q : A^{⊥} \end{matrix} &

We can exactly represent these proof transformations by the following π-term rewritings, provided we allow distributivity of ∥ over +:

(νp) ( (νuv)w̄⟨uv⟩[u(x)x(a)p̄⟨a⟩ + v(y)y(b)p̄⟨b⟩] ∥ p(c)q̄⟨c⟩ )

≡ (νp) ( (νuv)w̄⟨uv⟩[u(x)x(a)p̄⟨a⟩ ∥ p(c)q̄⟨c⟩ + v(y)y(b)p̄⟨b⟩ ∥ p(c)q̄⟨c⟩] )
≻^{∗} (νuv)w̄⟨uv⟩[u(x)x(a)q̄⟨a⟩ + v(y)y(b)q̄⟨b⟩] (after axiom reductions).

3.3 The Abramsky Translation: the exponentials

Logical Rule  π-translation

{⋮ . Q \atop ⊢ u⃗ : Γ} ; ⊢ u⃗ : Γ, z :?A w  W_{z}(Q)u⃗ z = z(wdc)w̄Q

{⋮ . Q \atop ⊢ u⃗ : Γ, x : A} ; ⊢ u⃗ : Γ, z :?A d  D_{z}^{x}(Q)u⃗ z = (νx)z(wdc)d̄⟨x⟩Q

{⋮ . Q \atop ⊢ u⃗ : Γ, x :?A, y :?A} ; ⊢ u⃗ : Γ, z :?A c  C_{z}^{x,y}(Q)u⃗ z = (νxy)(z(wdc)c̄⟨xy⟩)Q

{⋮ . Q \atop ⊢ u⃗ :?Γ, x : B} ; ⊢ u⃗ :?Γ, z :!B !  \begin{matrix}!_{z}^{x}(Q)u⃗ z = !_{z}^{x}(Qu⃗ x) = \\ (νwdc)(z̄⟨wdc⟩ ∥ \\ w.(∥_{i=1,...,n} u_{i}(wdc)w̄) + d(x).Qu⃗x + \\ c(z′z′′).[(νu⃗′u⃗′′)(∥_{i=1,...,n} u_{i}(wdc)c̄⟨u′_{i}, u′′_{i}⟩ \\ ∥ !_{z′}^{x}(Qu⃗′ x) ∥ !_{z′′}^{x}(Qu⃗′′ x))]) \end{matrix}

For the rest of this paper, we assume the existence of the term !_{z}^{x}(Q)u⃗ z (as a solution to the appropriate recursion equation in the synchronous πcalculus). This deserves some discussion. One of our goals is to see how much of the structure of linear logic proofs is preserved in the translation to (synchronous) π-calculus terms. Milner’s congruence !Q ≡ Q ∥ !Q (or a variant such as !Q ≡ !Q ∥ !Q, etc. ) equates terms in a manner which does not directly correspond to proof reduction. In particular, in linear logic the cut algebra for the exponentials (see below) allows duplication of !Q only as a rewriting step, not as a congruence. Nonetheless, with such a rewriting interpretation of !Q, the soundness of the cut algebra for the exponentials (and, more generally, the proof net interpretation) follows, cf. Section 7 below.

Heuristically, in the above π-translation of the exponentials, the variables “w,d,c” represent the rules of weakening, dereliction, and contraction, resp. During communication (= cut-elimination), processes first identify themselves (“hand-shaking”) as coming from one of these rules. Once these identifications establish that the communication can indeed occur, then cutelimination is implemented through π-calculus rewriting (see the cut algebra below).

The Cut Algebra: Exponentials

The following equations are true for proofs in CLL:

Symmetric Reductions

Cut^{z}(W_{z}(P),!_{z}^{x}Q_{u⃗x}) ≻ Wu⃗(P) (10) Cut^{z}(D_{z}^{x}(P_{x}),!_{z}^{x}Q_{x}) ≻ Cut^{x}(P_{x}, Q_{x}) (11)

Cut^{z}(C_{z}^{xy}(P_{xy}),!_{z}^{x}(Q_{u⃗x})) ≻ (12)

Cu⃗′,u⃗′′ ; u⃗(Cut^{z′}(Cut^{z′′}(P [z′/x, z′′/y],!_{z′}^{x}Q′),!_{z′′}^{x}Q′′))

where Q′ = Q[u⃗′/u⃗] ( and similarly for Q′′) and Cu⃗′,u⃗′′ ; u⃗ denotes an iterated sequence of contraction combinators.

Commutative Reductions

(13)  Cut^{z}(!_{z}^{x}P_{x},!_{u}^{y}Q_{zy}) = !_{u}^{y}(Cut^{z}(!_{z}^{x}P x, Q_{zy}))

Theorem 3 (Weak Soundness) Let D be a proof in CLL and let π(D) be its π-calculus translation. Then we have: Let C be any cut such that no &- or !-rule occurs below C. If D ≻_{1} D′ by a symmetric reduction applied to the cut C, then π(D) ≻_{1} π(D′) .

There is no straightforward version of Soundness for the case of commutative reductions in CLL.

4 Translating MLL Proof Structures

We give a brief introduction to proof structures and nets, referring the reader to the literature [1, 13, 6, 12, 30, 16, 32] for more details.

The Gentzen rules for one-sided sequents for CLL are given in Section 3 above (in proof-term assignment form). In this section we consider multiplicative linear logic MLL [12, 14], whose formulas are built from {⊗,^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} } using linear negation ( )^{⊥} and de Morgan duality. In all that follows, we ignore the role of the units.

4.1 MLL Proof Structures

A link is an m+n-ary relation between formula occurrences, for some m, n ≥ 0, m + n ≠ 0. Suppose X_{1},…, X_{m+n} are in a link: if m > 0, then X_{1}, …, X_{m} are called the premises of the link; if n > 0, then X_{m+1}, …, X_{m+n} are called the conclusions of the link. If m = 0, the link is called an axiom link. Links are graphically represented as

\frac{X_{1}, …, X_{m}}{X_{m+1}, …, X_{m+n}}

We consider only logical axioms and multiplicative links of the forms

A A^{⊥}  {A A^{⊥} \atop cut} {A B \atop A ⊗ B}  {A B \atop A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B}

The first two links are known as axiom and cut links, respectively. We assume that the axiom and cut links are symmetric relations. Following common practice, we shall sometimes avoid writing the word “cut” in a cut link.

A proof structure S for propositional MLL consists of (i) a nonempty set of formula-occurrences (i.e., a multiset of formulas) together with (ii) a set of logical axioms and multiplicative links satisfying the properties:

1. Every formula-occurrence in S is the conclusion of one and only one link;

2. Every formula-occurrence in S is the premise of at most one link.

We shall draw proof structures in the familiar way as non- empty, not necessarily planar, graphs.

Proof structures for MLL can be defined inductively, i.e., S is a proof structure if it results from a finite number of applications of the following clauses:

(i) an axiom \overline{X X^{⊥}} is a proof structure;

(ii) if S′ and S′′ are proof structures, then so is S′ ∪ S′′;

(iii) if {S \atop X X^{⊥}} and \begin{matrix}S & ′ \\ X Y \end{matrix} are proof structures, then so are

S ; \underline{X X^{⊥}}  and  S′ ; \frac{X Y}{X ⊗ Y}  and  S′ ; \frac{X Y}{X^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} Y}

We define the following reductions on proof structures:

Axiom Reductions

⋮  ⋮
X  X^{⊥} X  reduces to X
⋮  ⋮

Symmetric Reductions

⋮_{1}  ⋮_{2}  ⋮_{3}  ⋮_{4}
X  Y  X^{⊥} Y^{⊥}
X ⊗ Y  X^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} Y^{⊥}

reduces to

\begin{matrix}⋮_{1} & ⋮_{3} & ⋮_{2} & ⋮_{4} \\ X & X^{⊥} & Y & Y^{⊥} \end{matrix}

Definition. A Danos-Regnier switching s in a proof structure consists in the choice, for each par link, of one of the premises of the link.

Definition. Given a proof structure S and a switching s, we define the undirected Danos-Regnier graph G_{s}(S) as follows:

- the vertices of G_{s}(S) are the formulas of S;

- there is an edge between vertices X and Y exactly when:

(i) X and Y are the conclusions of a logical axiom or the premises of a cut link;

(ii) X is a premise and Y the conclusion of a times link

(iii) Y is the conclusion of a par link and X is the occurrence selected by the switching s.

Definition. A proof structure R is a proof net for MLL if for every switching s of R, the graph G_{s}(R) is acyclic and connected (i.e., an undirected tree).

We shall denote the Danos-Regnier graph as G(R) (omitting the switching s) if there is no ambiguity, and refer to it as the D-R graph of R. For further information, cf. [12, 6].

Occasionally (e.g. in Section 5.3 below) we will consider the system of sequent calculus for multiplicative linear logic, with the additional structural rule of Mix, also called direct logic DL [7, 11, 31, 4, 10]:

mix : \frac{⊢ Γ ⊢ Δ}{⊢ Γ, Δ}

Definition. A proof structure R is a proof net for Direct Logic DL if for every switching s of R, the graph G_{s}(R) is acyclic (but not necessarily connected.)

The following fundamental result (Girard [13]) relates sequent calculus and proof nets for MLL.

Theorem 4 (Sequentialization Theorem) There exists a map ( . )^{−} from sequent derivations in MLL to proof nets for MLL with the following properties:

(a) Let D be a derivation of Γ in the sequent calculus for MLL; then (D)^{−} is a proof net with conclusions Γ.

(b) (Sequentialization) If R is a proof net with conclusions Γ for MLL, then there is a sequent calculus derivation D of Γ such that R = (D)^{−}.

(c) If D reduces to D′, then D^{−} reduces to (D′)^{−}.

(d) If D^{−} reduces to R′ then there is a D′ such that D reduces to D′ and R′ = (D′)^{−}.

A similar result can be stated for direct logic ([11, 7, 31]).

Given an MLL proof structure {S \atop A_{1},...,A_{n}} with distinguished conclusions A_{1}, …, A_{n} we want to associate to it a basic synchronous π-calculus term π({S \atop A_{1},...,A_{n}}) whose free names will be in bijective correspondence with the conclusions. The key point of this translation is that communication of π terms may only occur in correspondence with a cut link through a hidden channel. The hiding of this channel is explicitly given by a ν binding.This imposes a severe restriction on the behaviour of π-calculus terms in the image of our translation: free names will never communicate. This point will become clear in Proposition 4 below. As we show, the graphical properties of a proof structure will be faithfully reflected by the nesting of the bindings in the associated π-terms. Theorem 7 and its Corollaries below show this translation fully mirrors (in the π-calculus) the reduction process of proof structures (and thus proof nets). Throughout this section, we will only be using the basic synchronous π-calculus in Section 2.

4.2 Translation of MLL proof structures

The theorem below generalizes the entire discussion of Section 3.1 to the level of structures, emphasizing one of our main points: that the communication in the π-calculus, insofar as it relates to linear logic, is really only about the pluggings in proof structures, not the logic itself.

It is convenient to use the notation (νx = y) defined and implemented as follows:

(νx = y)P xy =_{def} (νzy)(\overline{z}⟨y⟩ ∥ z(x)P xy)

≻ (νy)P xy[y/x]
≡ (νu)P [u/x, u/y]

(14)

We now define a map π from proof structures to terms of the synchronous π-calculus. This mapping depends upon some fixed “typing assignment” of distinct names (= variables) to all formula occurrences, which we suppose fixed once and for all.

1. π(\overline{A A^{⊥}}) = x(u) ȳ⟨u⟩, represented as

x : A y : A^{⊥}

where x, y are in the (given) typing assignment.

2. Let π({R \atop A B Γ}) = P xyx̃ and let t be a name not occurring in P; then

π ( {R \atop \frac{A B}{A ⊗ B} Γ}) =_{def} (νxy) t̄⟨xy⟩ (P xyx̃)

represented as

\begin{matrix}x : A & P x̃ & y : B \\ t : A ⊗ B \end{matrix} ⊗

3. let π({R \atop A A^{⊥}}) = P xy . Then

π \binom{R}{\underline{A A^{⊥}}} =_{def} (νx = y)P xy

represented as

x : A P x̃ x : A^{⊥}

4. Let π({R \atop A B Γ}) =_{def} P xyx̃ and let p be a name not occurring in P; then

π ( {R \atop \frac{A B}{A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B} Γ}) =_{def} p(xy)(P xyx̃)

represented as

\begin{matrix}x : A & P x̃ & y : B \\ p : A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B \end{matrix} ^{.............................................................................................}

5. Let π({R \atop A B Γ}) and π({S \atop C D Δ}) be the translations of two proof structures. Then

π ({R \atop A B Γ} ∪ {S \atop C D Δ}) = π({R \atop A B Γ}) ∥ π({S \atop C D Δ})

To fix terminology, in a prefix a(x_{1}, …, x_{n}) or \overline{a}⟨x_{1}, …, x_{n}⟩ the occurrences of a or \overline{a} are called names in channel position (or simply channels) and the occurrences of x_{1}, …, x_{n} are called names in message position (or simply messages). Among names in channel position, \overline{a}⟨ ⟩ is a sender and a( ) is a receiver.

Remark The notation in the above translation is intended to signify the following: if we erase the variable names, we obtain the proof structure; if we erase the formulas, the notation indicates that the lowermost variables are the free names of the π term and the rest of the graph represents the binding structure of the variables in channel position.

Example The following is a proof structure R which is not a proof net:

a : A b : B

p : A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B p : A^{⊥} ⊗ B^{⊥} z : A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B d : B^{⊥} c : A^{⊥}
cut  r : (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) ⊗ B^{⊥}

It has the following translation into a π term:

(νzd)\overline{r}⟨zd⟩(νp)(p(ab)(I_{ac} ∥ I_{bd}) ∥ I_{pz})

where I denotes the translation of the appropriate axiom link, e.g. I_{ac} is the term a(u)\overline{c}⟨u⟩, corresponding to the axiom link \overline{a : A c : A^{⊥}}. (Recall we only consider atomic axiom links. ) We remark that, by Proposition 5 below, this translation will not depend on the order of the inductive construction of the proof structure.

Example (Deadlock) The deadlocked proof structure \overline{\underline{A A^{⊥}}} has the translation νx[x(a)x̄⟨a⟩] .

The next proposition gives some important syntactic properties of those π-terms which translate linear logic proofs:

Proposition 5 Let P = π(R), for some proof structure R. Then the following are true, modulo α-conversion:

(i) Every name occurs at most once or twice in channel position.

(ii) If x occurs twice in channel position in a process P, then both occurrences are bound by the same (νx), i.e. P can be written as (νx = y)P xy, where x is a sender and y a receiver. In particular, each free name x occurs at most once in a channel position. (“a communicating channel corresponds to a cut”);

(iii) If \overline{a}⟨x_{1}, …, x_{n}⟩ occurs in a process P , then x_{1}, …, x_{n} are bound, either by some c(x_{1}, …, x_{n}), (n = 1) or by (νx_{1}, …, x_{n}), (n = 2). (“senders send only private names”) Therefore, if ȳab and z̄cd occur in a process P,then a, b, c, d are all distinct. (“different channels send different messages”)

(iv) A message in a unary prefix is bound by (or binds) exactly one other unary prefix (“unary channels correspond to axiom links”);

(v) If x and y occur as messages in a binary prefix, then both x and y occur in P also in channel position. (“binary channels correspond to binary links”);

Since proof structures are inductively generated, it is possible to characterize exactly those π- terms which arise as the translation of proof structures, by adding some clauses to Proposition 4. We shall refrain from doing this here.

Proposition 6 If R is a proof structure, then π(R), modulo ≡, does not depend on the particular order of the inductive construction of R.

Proof. By induction on the number of links in R. E.g., let R be

\begin{aligned}& R′′ \\ \frac{B C}{B ⊗ C} & & \frac{B^{⊥} C^{⊥}}{B^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} C^{⊥}} \end{aligned}

and assume the lemma for π(R′′) = P′′xyuv. Then in the synchronous πcalculus we certainly have

p(uv) (νxy) t̄⟨xy⟩ P′′xyuv ≡ (νxy) t̄⟨xy⟩ p(uv) P′′xyuv

We now state two theorems which completely characterize the relationship between proof structure reducibility (and thus for proof nets) and the πcalculus translation considered here.

Theorem 7 (Weak Soundness) If R, S are proof structures for MLL, and if R ≻ S then π(R) ≻ π(S) .

Proof: This is a straightforward induction on the formation of proof structures.

The above result generalizes to proof structures Abramsky’s result for proofs stated earlier.

Theorem 8 (Local Fullness) For any proof structure R, if π(R) ≻ Q, then there is a proof structure S such that Q = π(S) and R ≻ S, as illustrated by the following diagram:

\begin{aligned}R & ≻ & S \\ π∨ & ∨ & π \\ π(R) & ≻ & Q \end{aligned}

Proof. Suppose π(R) ≻ Q. Since R is inductively generated, so is π(R) and we can argue by induction on the formation of π(R). Then by Proposition 5, part (i), (ii) and (iii), communication can occur only along a hidden channel

(∗)  \begin{matrix}π_{x_{1},...,x_{n}}(νa) (\overline{a}⟨x_{1}, …, x_{n}⟩P_{x_{1},...,x_{n}} ∥ a(y_{1}, …, y_{n})Q_{y_{1},...,y_{n}}) \\ ≻ π_{x_{1},...,x_{n}} (P_{x_{1},...,x_{n}} ∥ Q_{y_{1},...,y_{n}}[x_{1}/y_{1}, …, x_{n}/y_{n}]) \end{matrix}

Here Q_{y_{1},...,y_{n}} is the scope of the binder a(y_{1}, …, y_{n}) and π_{x_{1},...,x_{n}} is a prefix binding x_{1}, …, x_{n} whose scope in π(R) does not extend beyond the subterm indicated in (∗).

If n = 1, then by Proposition 5, part (iv), Q_{y_{1}} is a sender \overline{b}⟨y_{1}⟩ and communication (∗) corresponds to a reduction

⋮  ⋮
a : X^{⊥} a : X  b : X^{⊥} reduces to b : X^{⊥}
cut  ⋮  ⋮

i.e., the desired S is obtained from R by eliminating the cut and an axiom link as indicated.

If n = 2, then by Proposition 5, part (v), communication (∗) corresponds to a reduction from

⋮_{1}  ⋮_{2}  ⋮_{3}  ⋮_{4}
x_{1} : X  x_{2} : Y  y_{1} : X^{⊥} y_{2} : Y^{⊥}
a : X ⊗ Y  a : X^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} Y^{⊥}

cut

to

\begin{aligned}x_{1} : X^{⋮ .1} & x_{1} : X^{⊥}^{⋮ .3} \\ & cut \end{aligned}  \begin{aligned}x_{2} : Y^{⋮ .2} & x_{2} : Y^{⊥}^{⋮ .4} \\ & cut \end{aligned}

i.e., the desired S is obtained from R by replacing the times, par and cut links with two cuts as indicated.

Example (of Theorem 7): The proof structure R above Proposition 5 was translated by the term

π(R) = (νzd)\overline{r}⟨zd⟩(νp)(p(ab)(I_{ac} ∥ I_{bd}) ∥ I_{pz})

It is easy to verify that π(R) ≻ (νzd)\overline{r}⟨zd⟩z(ab)(I_{ac} ∥ I_{bd}) . Call this latter term Q. But then Q is the π-calculus translation Q ≡ π(S) of the following structure S (and moreover R ≻ S):

a : A b : B
p : A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B  d : B^{⊥} c : A^{⊥}
r : (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) ⊗ B^{⊥}

Corollary. If π(R) ≻ π(S) and R is a proof net, then S is a proof net too.

An alternate proof of local fullness for MLL proof structures will be considered in Section 5.3.

5 Information Flow

The reader may have observed that there are some arbitrary choices made in the above π-calculus translation: (i) we have chosen axiom buffers to be unidirectional– atoms become receivers, and negations of atoms senders, (ii) the times and par links become senders and receivers respectively. This has a very serious consequence: the translation is not preserved under substitution for propositional variables, since it depends on the identification of an atomic occurrence in an axiom. For this reason in the original Abramsky translation, axiom buffers were bidirectional, i.e. Abramsky translated the axiom ⊢ x : A, y : A^{⊥} as

π(\overline{x : A y : A^{⊥}}) = x(a)ȳ⟨a⟩ + y(a)x̄⟨a⟩

However, the use of + creates other problems, which will be discussed later in Section 6.1. Instead, we shall here develop an intrinsic notion of information flow for pure nets, thus obviating the need for bidirectional buffers ^{3}.

Terms of the λ-calculus have a natural direction, namely from the inputs to the output. This is obvious from the intended functional interpretation, as well as the dynamics of evaluation. V. Danos, L. Regnier [11, 30, 22], J. van de Wiele and others have studied pure nets, a formalism of ‘proof nets’ for untyped λ-calculus: pure nets are nets built from “formulas” I and O (representing input and output, resp.), using links of the forms

\overline{I O}  {O I \atop cut}  \begin{aligned}?I & & O \\ & O \end{aligned} ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}}  \begin{matrix}!O & I \\ I \end{matrix} ⊗ {O \atop !O} ! {?I …?I \atop ?I} contr

One motivation for this formalism is to think of the ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} -link as satisfying the domain “equation” D ≅ !D −∘ D (where we let D be O). This is just the familiar domain equation D ≅ D ⇒ D, under the Girard translation into linear logic [13]. Other notions of pure nets for untyped lambda calculus arise by imposing different domain equations [21].

One of the goals of the above work on pure nets is to understand information flow in the process of β-reduction. But the same questions arise in the typed setting. When we consider natural deduction derivations in intuitionistic logic under the Curry-Howard correspondence (i.e. qua simply typed lambda terms), we find the same flow of information in the process of normalization, and a direction in the derivations statically considered (the elimination part of the proof-tree becomes the input part and the introduction part of the proof-tree becomes the output part).

Proof nets could be designed as input-output graphs as well but, because of De Morgan dualities for classical (linear) connectives and contraposition laws, one expects that the roles of input and output should be fully interchangeable. In what follows we make this precise. Following Bellin and Van de Wiele [8], we show that (at least for MLL) we can always assign input-output directions to proof nets so that one arbitrarily chosen conclusion is the output and all the others the inputs; when this is done, we have an interpretation of the proof net as a natural deduction derivation. Conversely, all natural deduction derivations correspond to a proof net with an input-output orientation. Each translation of a classical net into intuitionistic natural deduction obviously yields a linear λ term, under the Curry Howard correspondence.

3The problem of substitution for propositional variables relates to whether the proofsas-processes view extends to second-order linear logic. We leave that issue open.

Communication between π-calculus processes also has a direction. Agents pass names, i.e., access to information; some agents are senders, others are receivers. A process of transfer of information, when regarded as a whole, has a certain direction. Its implementation in the π-calculus may involve a sequence of intermediate interactions – some of which may simply be identification protocols, where the information flows in both directions. These may have no direct logical meaning. Nevertheless, it makes sense to ask that an efficient π-calculus translation of some logical system should fundamentally reflect the flow of information in the ‘object calculus’. In section 5.5 below we examine in more detail Milner’s direct translation of linear λcalculus into the π-calculus, and briefly compare it to the one arising from the proofs-as-processes (and pure net) viewpoint.

5.1 Pure structures

It is convenient to prove Soundness and Local Fullness in a more abstract form, which does not depend on the particulars of the above translation. For this purpose, we introduce the notion of an untyped pure structure, in analogy to the notion of pure net used in the study of untyped lambda calculi [22, 11, 30]

Definition. A pure structure P is a proof structure built from occurrences of the symbols I, O, (for input and output) together with a set of links of the form

I O \begin{matrix}M & N \\ cut \end{matrix}  \begin{aligned}M_{1} & & M_{2} \\ & N \end{aligned}

where M, M_{i} and N are occurrences of the symbols I, O.

Remarks

(1) Notice that in pure structures we do not necessarily require premisses of cuts to be complementary: for example, \begin{matrix}I & I \\ cut \end{matrix} represents a deadlocked pure structure.

(2) Pure nets are a special class of pure structures in our sense (with additional links).

(3) For the purpose of studying the translation of multiplicative proof structures, the above links suffice. A more general setting (possibly useful for studying larger classes of π-calculus terms) might allow axiom links of the forms \overline{O O_{1} … O_{p}} \overline{I O_{1} … O_{p}}, with p ≥ 0.

Pure structures, just like ordinary proof structures, can also be defined inductively: cf. section 4 above. Also in analogy with ordinary proof structures, we define the following reductions on pure structures:

1. Axiom reductions.

⋮  ⋮
O I  O reduces to O
⋮  ⋮

2. Symmetric reduction:

⋮_{1}  ⋮_{2}  ⋮_{3}  ⋮_{4}
M  N  M′ N′
I  O

reduces to

\begin{matrix}⋮_{1} & ⋮_{3} & ⋮_{2} & ⋮_{4} \\ M & M′ & N & N′ \end{matrix}

Definitions. Let P be a pure structure and S be an ordinary proof structure. An injective map τ : P → S is said to preserve a link L of P if

L \frac{X_{1}, …, X_{m}}{Y_{1}, …, Y n} ↦ \frac{τ(X_{1}), …, τ(X_{m})}{τ(Y_{1}), …, τ(Y_{n})}.

Similarly, an injective δ : S → P preserves L in S if

L \frac{X_{1}, …, X_{m}}{Y_{1}, …, Y n} ↦ \frac{δ(X_{1}), …, δ(X_{m})}{δ(Y_{1}), …, δ(Y_{n})}.

An injective link-preserving map τ : P → S is called a typing of P; an injective link-preserving δ : S → P is called an orientation of S.

5.2 Translation of pure structures into the π-calculus

Let P be the set of pure structures and let Π_{0} be a set of π-calculus terms satisfying conditions (i) − (v) of Proposition 4.

We define a representation π_{pure} of pure structures into π-calculus terms as follows. For each P ∈ P we define a π-calculus term π_{pure}(P) by induction on the definition of P. We will let π_{pure}(I) be a receiver x( ), and π_{pure}(O) a sender \overline{x}⟨ ⟩. To verify that π_{pure}(P) ∈ Π_{0}, in particular, that all free names in π_{pure}(P) are pairwise distinct, we make sure that at each step of the construction “fresh” free names are used. This can be implemented as follows. We have two lists ℓ_{f} and ℓ_{b} of names; at the beginning of the process of translation we have an infinite ℓ_{f} and empty ℓ_{b}. Let concatenation be denoted by “.”

(i) π_{pure}(\overline{I O}) = a(x)\overline{b}⟨x⟩, where ℓ_{f} = a.b.restℓ_{f}; now set ℓ_{f} := restℓ_{f}, and ℓ_{b} := x.ℓ_{b} respectively;

(ii) if P = P′ ∪ P′′, then π_{pure}(P) = π_{pure}(P′) ∥ π_{pure}(P′′), where π_{pure}(P′) and π_{pure}(P′′) are previously given.

(iii) if π_{pure}({P \atop M N}) = P_{x,y}, then

π_{pure} \binom{P}{\underline{M N}} = (νx = y)P_{x,y} = (νz)P_{x,y}[z/x, z/y]

where z = first(ℓ_{f}). Now set ℓ_{f} := restℓ_{f} and ℓ_{b} := z.x.y.ℓ_{b}.

(iv) if π_{pure}({P \atop M N}) = P_{x,y}, then

π_{pure} ( P ; \frac{M N}{I} ) = a(x, y)P_{x,y}

and

π_{pure} ( P ; \frac{M N}{O} ) = (νx, y)\overline{a}⟨x, y⟩P_{x,y}

where a = first(ℓ_{f}). Now set ℓ_{f} := rest(ℓ_{f}) and ℓ_{b} := x.y.ℓ_{b}.

Remark: There is also a dual translation π_{pure}^{⊥} which interchanges the rôles of sender and receiver, i.e. the interpretation of I and O.

Analogously to the previous Theorem 6 (Soundness), one obtains for pure structures:

Theorem 9 (Soundness) If P, P′ are pure structures for MLL such that P ≻ P′, then π_{pure}(P) ≻ π_{pure}(P′) and also π_{pure}^{⊥}(P) ≻ π_{pure}^{⊥}(P′).

We now prove local fullness for pure structures:

Theorem 10 (Local Fullness) For any pure structure P, if π_{pure}(P) ≻ Q, then there is a pure structure P′ such that Q = π_{pure}(P′) and P ≻ P′, as illustrated by the following diagram:

\begin{aligned}P & ≻ & P′ \\ π_{pure}∨ & ∨ & π_{pure} \\ π_{pure}(P) & ≻ & Q \end{aligned}

and similarly for π_{pure}^{⊥}

Proof The proof is the same as that given in section 4.2., with ‘pure structure’ in place of ‘proof structures’.

5.3 Deadlock-free Structures

The next useful result shows that the two π-calculus translations of pure structures and ordinary proof structures (respectively) are the same, modulo an orientation:

Proposition Let S be a proof structure for MLL with atomic axioms only. Let P be the pure structure with the same form as S but with all formula occurrences replaced by I’s and O’s as follows: atoms map to I, negations of atoms map to O . Then there is a unique orientation δ : S → P which maps atoms to I, negations of atoms to O, satisfying

(§§) \overline{δ(X) δ(X^{⊥})} = \overline{I O},  δ(X ⊗ Y) = O,  δ(X^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} Y) = I.

and which makes the following diagram commute:

S ·····\begin{matrix}δ \\ · \end{matrix}····· > P
[figure: π] ∨π_{pure}
π(S)

The proof is immediate.

Proposition. Let S be a proof structure for MLL with atomic axioms only and let δ be an orientation satisfying (§§).

(i) If S ≻ S′, then δ(S) ≻ δ(S′).

(ii) If δ(S) ≻ P′, then we can find a S′ such that S ≻ S′ and P′ = δ(S′).

Proof. A reducible cut link \underline{P P^{⊥}} or \underline{A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B A^{⊥} ⊗ B^{⊥}} in S is mapped to a cut link of the form \underline{I O}, which is reducible. Conversely, a reducible cut link \underline{I O} in δ(S) can only be the image of a reducible cut \underline{P P^{⊥}} or \underline{A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B A^{⊥} ⊗ B^{⊥}} in S.

We now give an alternate proof of Local Fullness:

Theorem 11 (Local Fullness) For any MLL proof structure S, if π(S) ≻ Q as π-calculus terms, then there is a proof structure S′ such that Q = π(S′) and S ≻ S′, as illustrated by the following diagram:

\begin{aligned}S & ≻ & S′ \\ π∨ & ∨ & π \\ π(S) & ≻ & Q \end{aligned}

Proof: Consider the following diagram:

S  \overline{≻} \overline{>} S′ \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}
[figure: δ]  \begin{matrix}· \\ · \\ · \\ · \\ · \\ · \\ ∨ \end{matrix}δ
π∨  P  \overline{≻} \overline{>} P′
[figure: π_{pure}]  ∨π_{pure}
π(S)  \overline{≻} \overline{>} π(P′)

By the local fullness of pure structures, there is a pure structure P′ filling-in the bottom cell of the diagram. We thus must find a proof structure S′ and an orientation δ with the above properties. The previous two Propositions complete the proof.

Definitions.

(i) A pure structure P is called deadlock-free if no links of the form \underline{I I}, \underline{O O} or \underline{\overline{I O}} occur in P.

(ii) A reduction sequence P_{0} ≻ P_{1} ≻ … ≻ P_{n} is deadlock-free if every P_{i} is deadlock free.

(iii) An orientation δ : S → P is computationally consistent if every reduction sequence starting from S is mapped by δ to a deadlock-free reduction sequence.

What are the general structures that are guaranteed to be deadlock- free? We recall (see Section 4.1) that a proof structure satisfying the acyclicity

condition (but not necessarily connectedness) is a proof net for Direct Logic DL namely, multiplicative linear logic MLL with the structural rule of Mix [6, 4, 16, 10].

Theorem 12 (Deadlock-free nets) Let S be a proof net for MLL or direct logic and let δ be an orientation of S satisfying (§§). Then δ is computationally consistent.

Proof. The reader should check that under the assignment (§§) to an axiom reduction of proof nets (Section 4.1) there corresponds an axiom reduction of pure structures (Section 5.1) and to a symmetric reduction of proof nets there corresponds a symmetric reduction of pure structures where M is the dual of M’ and N is the dual of N’. It remains to show that the orientation \overline{\underline{IO}} cannot be obtained as a result of the cut-elimination process, i.e., that the configuration \overline{\underline{XX^{⊥}}} cannot be obtained as a result of the cutelimination process for proof-nets. This follows from the well-known fact that cut-elimination preserves acyclicity of the D-R graphs. To check it, suppose that a proof-structure R′ comes from R by a symmetric reduction and that for some switching s, s(R′) contains a cycle. Various cases occur depending on whether or not the cycle passes through one or more of the ‘new’ cut links in R; in each case one may choose a switching for the indicated par links which yields a cycle in R, contrary to the hypothesis. For instance, if the cycle passes through both the ‘new’ cut links then either it has the form (a) … \underline{X X^{⊥}} … \underline{Y Y^{⊥}} … or the form (b) … \underline{X^{⊥} X} … \underline{Y Y^{⊥}} . . .. In case (a) in R take a Left switch for the new par link; in (b), … X … Y, X⊗Y, X … is a cycle in s(R) for any choice of the switch for the new par link, etc.

Corollary. Let S_{1}, S_{2} be proof nets for direct logic, let S result from S_{1} and S_{2} by adding a cut link between them. If δ_{1}, δ_{2} are orientations on S_{1}, S_{2}, respectively, satisfying (§§), then the induced orientation δ = δ_{1} ∪ δ_{2} on S is computationally consistent.

Remark. The converse statement, that every computationally consistent pure structure is typable in direct or linear logic, is false. Indeed there are incorrect proof-structures that reduce to a proof-net; for instance

\overline{A^{⊥} A} \overline{A A^{⊥}} \overline{A^{⊥} A}  \overline{A^{⊥} A} \overline{A^{⊥} A} \overline{A^{⊥} A}
A ⊗ A A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥} reduces to cut cut

cut

Therefore the following pure structure is computationally consistent

\overline{I  O} \overline{O I}  \overline{I  O}  \overline{I  O} \overline{I  O} \overline{I  O}
O  I  reduces to  cut  cut

cut

So this pure structure, when typed, does not become a proof-net for either linear or direct logic. Therefore our notion of computational consistency, which arises naturally from the consideration of cut-elimination as logical computation and from the notion of deadlock for a π-calculus term, is not sufficient to characterize proof-nets for direct logic.

Intuitively, the acyclicity condition for D-R-graphs (which characterizes proof-nets in direct logic) seems to express absence of deadlock in a logical computation; clearly, a stronger notion of deadlock than ours is needed to characterize correctness for such nets. We shall not pursue the matter further here (cf. recent work of A. Asperti [5]).

Another example of computationally consistent orientation will be considered in Section 5.4 below.

5.4 Orienting Proof Nets and Linear λ-terms

The present section is based on joint work by G.Bellin and J. van de Wiele ([8]).

The system IMLL of intuitionistic multiplicative linear logic is based on a language with the connectives −∘ and ⊗; there is a symbol for falsity (we use ⊥ as in classical linear logic) but no property of falsity is assumed for here. Linear negation is defined as A^{⊥} =_{df} A −∘ ⊥. The sequent calculus rules and the associated term assignment (of “linear” lambda terms) are familiar [20, 1]. For example, in addition to λ-abstraction and substitution, the following rules for ⊗ are assumed:

⊗R : \frac{y⃗ : Γ ⊢ t : A z⃗ : Δ ⊢ u : B}{y⃗ : Γ, z⃗ : Δ ⊢ t ⊗ u : A ⊗ B}

⊗L : \frac{y⃗ : Γ, x : A, y : B ⊢ t : C}{y⃗ : Γ, z : A ⊗ B ⊢ let z be x ⊗ y in t : C}

For simplicity, we consider only proof nets S for MLL with the property that every axiom link contains an atomic formula and its linear negation. Given such a proof net S, consider orientations δ : S → {O, I} (which can also be written as δ : S → P) satisfying the following restrictions:

axiom: \overline{O I}  cut:  \underline{I O}

tensor: (1)\frac{O I}{I}  (2)\frac{I O}{I}  (3)\frac{O O}{O}

par: (4)\frac{I O}{O}  (5)\frac{O I}{O}  (6) \frac{I I}{I}

As usual[13], axiom and cut links are assumed symmetric in I and O.

Theorem 13 (Bellin, van de Wiele) The following hold:

(a) If S is a proof net with a chosen conclusion A, and s is a D-R switching for S, then s and A determine an orientation δ_{s,A} : S → {I, O} satisfying (1)−(6). Moreover, the chosen conclusion is assigned O and all the other conclusions are assigned I.

(b) There exists a map ( . )^{i} from IMLL sequent derivations to MLL proof nets with orientations, satisfying:

(b_{1}) Let D be a derivation of Γ ⊢ A in the sequent calculus for IMLL; then (D)^{i} is a proof net S with an orientation δ : S → {I, O}; the conclusion ⊗Γ^{δ} −∘ A^{δ} of S is equivalent to ⊗Γ −∘ A in classical MLL.

(b_{2}) Let S be a proof net with conclusions Γ, A. If an orientation δ for S is computationally consistent, then there exists a sequent Γ^{δ} ⊢ A^{δ} and a derivation D of it in the sequent calculus IMLL such that (D)^{i} = S.

(b_{3}) If S is a proof-net with cut and s′ is a partial switching undefined above all cut-links, then there exists a total switching s such that the orientation δ determined by s is computationally consistent.

(b_{4}) If D reduces to D′, then D^{i} reduces to (D′)^{i}.

(b_{5}) If (S, δ) = D^{i} and S reduces to S′ then there is a D′ such that D reduces to D′ and S′ = (D′)^{i}.

Using the linear λ-term assignment to IMLL sequents, one obtains from (b):

Corollary 14 Let M be a linear λ-term as above. Then M corresponds to a proof net with orientation δ : S → {I, O}. Conversely, if S is a proof net with conclusion C, then every computationally consistent orientation δ : S → {I, O} determines a linear λ-term of type C^{δ} .

Thus, an oriented proof net for classical MLL yields a linear λ-term, whose output type is assigned O and whose arguments are assigned I.

Proof of Theorem. (a): Let S be a proof net with conclusions C_{1}, …, C_{n}, and let s be a D-R switching for S together with a choice of a conclusion C_{i}. We define an orientation δ : S → {I, O} as follows.

• Let C_{i} ↦ O. Starting from C_{i}, we follow the D-R graph s(S).

• Proceeding upwards – from the conclusion to both premises of a times link and from the conclusion of a par link to the premise which is chosen by the switch – we always assign O to formulae encountered (O-paths); • When, proceeding upwards, we reach an axiom \overline{P Q} and assign O,

say, to P, then we continue by letting Q ↦ I and proceed downwards from Q;

• proceeding downwards – from a premise to the conclusion of a times link and from the selected premise to the conclusion of a par link – we always assign I for formulas encountered (I-paths); however

• In the case of a times link \frac{A_{0} A_{1}}{A_{0} ⊗ A_{1}} if A_{i} ↦ I (and hence A_{0} ⊗ A_{1} ↦

I), then we let A_{1−i} ↦ O and also start another process proceeding upwards from A_{1−i}; the case of a cut link is similar; and so on.

Each subroutine of the procedure ends either with a premise of a par link which is not selected by the switch for that link or at a conclusion, in both cases after having assigned I to the formula-occurrence in question. Since the D-R graph is acyclic, the I − O assignment is unique and the procedure terminates; since the D-R graph is connected, the assignment is total. Thus we have an orientation δ : S → {I, O} such that if δ(C_{i}) = O, then δ(C_{j}) = I, for all j ≠ i.

Remark. It can also be proved that any I − O assignment satisfying conditions (1)-(6) above, when applied to any proof net yields C_{i} ↦ O for some conclusion of the proof-net in question. (In particular, this holds when applied to a subnet of an oriented proof net.) Indeed, given δ : S → {I, O} and a conclusion C_{j} with δ(C_{j}) = I, we proceed as follows:

• proceeding upwards, follow the unique I-path up to an axiom;

• proceeding downwards from an axiom, follow the unique O-path until either (i) a conclusion C_{i} is reached with δ(C_{i}) = O, or (ii) a premise A_{i} of a times link such that δ(A_{i}) = O but for the conclusion we have δ(A_{0} ⊗ A_{1}) = I;

• since in case (ii) above we must have δ(A_{1−i}) = I, we continue upwards from A_{1−i}, and so on.

Since the D-R graph is acyclic, case (b) can occur only a finite number of times; thus eventually we reach a conclusion C_{i} of S such that δ(C_{i}) = O, as claimed (end of remark).

Proofs of (b), (b_{1})-(b_{3}) (the rest is straightforward): Girard’s Sequentialization Theorem (see section 4.1) provides a map ( . )^{−} from classical MLL sequent proofs (thus from IMLL proofs) to proof nets (cf. also [20]) which determines a bijection between the inferences of a derivation D and the links of S = (D)^{−}. The active formulas and the principal formula of an inference in D correspond to the premises and the conclusion, respectively, of a link in S. Orientations exist, by (a). This provides the map ( . )^{i} in (b).

Case I: Cut free proof nets. We consider first the translation of cut-free proof nets (which are trivially computationally consistent). Given an orientation δ : S → {I, O}, by Girard’s theorem let D be a classical sequent derivation such that S = (D)^{−}. We simultaneously define the intuitionistic derivation D^{δ} and for each formula A in D^{δ}, the translation A^{δ}. We write A_{O} if δ(A) = O and A_{I} if δ(A) = I; we write A_{O}^{δ} for the translation of A when δ(A) = O, etc.

• For P atomic, we let P_{O}^{δ} = P = (P_{I}^{⊥})^{δ} and P_{I}^{δ} = P^{⊥} = (P_{O}^{⊥})^{δ}. Thus

⊢ P_{I}^{⊥}, P_{O} ↦ P ⊢ P ⊢ P_{O}^{⊥}, P_{I} ↦ P^{⊥} ⊢ P^{⊥}

• Given A_{O}^{δ}, B_{O}^{δ}, let (A ⊗ B)_{O}^{δ} = A_{O}^{δ} ⊗ B_{O}^{δ}; thus

\frac{⊢ Γ_{I}, A_{O}  ⊢ Δ_{I}, B_{O}}{Γ_{I}, Δ_{I} ⊢ (A ⊗ B)_{O}}  ↦  \frac{Γ_{I}^{δ} ⊢ A_{O}^{δ}  Δ_{I}^{δ} ⊢ B_{O}^{δ}}{Γ_{I}^{δ}, Δ_{I}^{δ} ⊢ A_{O}^{δ} ⊗ B_{O}^{δ}}

• Given A_{O}^{δ}, B_{I}^{δ}, let (A ⊗ B)_{I}^{δ} = A_{O}^{δ} −∘ B_{I}^{δ}; thus

\frac{⊢ Γ_{I}, A_{O}  ⊢ B_{I}, Δ_{I}, C_{O}}{⊢ Γ_{I}, (A ⊗ B)_{I}, Δ_{I}, C_{O}}  ↦  \frac{Γ_{I}^{δ} ⊢ A_{O}^{δ}  B_{I}^{δ}, Δ_{I}^{δ} ⊢ C_{O}^{δ}}{Γ_{I}^{δ}, A_{O}^{δ} −∘ B_{I}^{δ}, Δ_{I}^{δ} ⊢ C_{O}^{δ}}

• Conversely, given A_{I}^{δ} and B_{O}^{δ}, let (A ⊗ B)_{I}^{δ} = B_{O}^{δ} −∘ A_{I}^{δ} and proceed symmetrically to the previous case.

• Given A_{I}^{δ}, B_{O}^{δ}, let (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)_{O}^{δ} = A_{I}^{δ} −∘ B_{O}^{δ}; thus

\frac{⊢ Γ_{I}, A_{I}, B_{O}}{⊢ Γ_{I}, (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)_{O}}  ↦  \frac{Γ_{I}^{δ}, A_{I}^{δ} ⊢ B_{O}^{δ}}{Γ_{I}^{δ} ⊢ A_{I}^{δ} −∘ B_{O}^{δ}}

• Conversely, given A_{O}^{δ} and B_{I}^{δ}, let (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)_{O}^{δ} = B_{I}^{δ} −∘ A_{O}^{δ} and proceed symmetrically to the previous case.

• Finally, given A_{I}^{δ}, B_{I}^{δ}, let (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)_{I}^{δ} = A_{I}^{δ} ⊗ B_{O}^{δ}; thus

\frac{⊢ Γ_{I}, A_{I}, B_{I}, C_{O}}{⊢ Γ_{I}, (A^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B)_{I}, C_{O}}  ↦  \frac{Γ_{I}^{δ}, A_{I}^{δ}, B_{I}^{δ} ⊢ C_{O}^{δ}}{Γ_{I}^{δ}, A_{I}^{δ} ⊗ B_{I}^{δ} ⊢ C_{O}^{δ}}

Case II: proof nets with Cut. In the case of a proof-net S with Cut links, by the sequentialization theorem we obtain a sequent derivation D containing subderivations

\begin{matrix}D′ ; ⋮ . ; ⊢ Γ, A & D′′ ; ⋮ . ; ⊢ Δ, A^{⊥} \\ ⊢ Γ, Δ \end{matrix}

and we need to show that A_{I}^{δ} = (A^{⊥})_{O}^{δ} or A_{O}^{δ} = (A^{⊥})_{I}^{δ}. This is not true in general, if we take arbitrary switchings on the par links occurring above A and A^{⊥} in S. Let R′ be the subnet of S given by (D′)^{−} and similarly, let R′′ = (D′′)^{−}. Consider the pure structures δ(R′) = P′ and δ(R′′) = P′′; in P′ and P′′ consider the subtrees corresponding to the hereditary subformulas of A and A^{⊥}: what we need is that such subtrees be dual, e.g.,

\begin{matrix}\begin{aligned}\begin{aligned}I & & O \\ & I \end{aligned} & & \begin{aligned}I & O \\ & O \end{aligned} \\ & O \end{aligned} & \begin{aligned}\begin{matrix}O & I \\ O \end{matrix} & & \begin{aligned}O & & I \\ & I \end{aligned} \\ & I \end{aligned} \\ cut \end{matrix}

Using the cut-elimination theorem we show that this requirement can be met, by induction on the length of the cut-elimination procedure.

• If the proof net R_{1} reduces to R_{2} by an axiom reduction

⋮  ⋮
P  P^{⊥} P  reduces to P
⋮  ⋮

and δ_{2} : R_{2} → {I, O} is computationally consistent, then it is immediate to define a computationally consistent δ_{1} : R_{1} → {I, O}, as no new par links are to be considered.

• Suppose R_{1} reduces to R_{2} by a symmetric reduction

⋮_{1}  ⋮_{2}  ⋮_{3}  ⋮_{4}
A B  A^{⊥} B^{⊥} L A ⊗ B  A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B^{⊥}

reduces to

\begin{matrix}⋮_{1} & ⋮_{3} & ⋮_{2} & ⋮_{4} \\ A & A^{⊥} & B & B^{⊥} \end{matrix}

and suppose we have a computationally consistent orientation δ_{2} : R_{2} → {I, O} so that A^{δ} = (A^{⊥})^{δ} and B^{δ} = (B^{⊥})^{δ}: we need to choose a switching for the new par link L so as to extend δ_{2} to a computationally consistent δ_{1} : R_{1} → {I, O}. By Girard’s sequentialization theorem the above reduction step corresponds to the reduction from D_{1} to D_{2}, say, by the steps

from

\begin{matrix}D′ ; ⋮ . ; ⊢ Γ, A & D′′ ; ⋮ . ; ⊢ Δ, B \\ ⊢ Γ, Δ, A ⊗ B \end{matrix} D′′′ ; ⋮ . ; ⊢ Λ, A^{⊥}, B^{⊥} ; ⊢ Λ, A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B^{⊥}
⊢ Γ, Δ, Λ to

D′ ; ⋮ . ; ⊢ Γ, A \begin{matrix}D′′ ; ⋮ . ; ⊢ Δ, B & D′′′ ; ⋮ . ; ⊢ Λ, A^{⊥}, B^{⊥} \\ ⊢ Δ, Λ, A^{⊥} \end{matrix}
⊢ Γ, Δ, Λ

Notice that R′′′ = (D′′′)^{−} is a subnet of R_{2} = (D_{2})^{−}, and that by part (a) at most one of A^{⊥}, B^{⊥} can be assigned value O by δ_{2}.

• case (i) δ_{2}(A^{⊥}) = O: let the switch for the link L be Left;

• case (ii) δ_{2}(B^{⊥}) = O: let the switch for the link L be Right;

• case (iii) δ_{2}(A^{⊥}) = I = δ_{2}(B^{⊥}): choose the switch for L arbitrarily.

In case (ii) we obtain δ_{1} extending δ_{2} with

⋮_{1}  ⋮_{2}  ⋮_{3}  ⋮_{4}
O I  I  O
I  O

which reduces to

\begin{matrix}⋮_{1} & ⋮_{3} & ⋮_{2} & ⋮_{4} \\ O & I & I & O \end{matrix}

Letting Δ = Θ, C, we obtain a translation thus:

\begin{matrix}⋮ . ; Γ_{I}^{δ_{1}} ⊢ A_{O}^{δ_{1}} & ⋮ . ; B_{I}^{δ_{1}}, Θ_{I}^{δ_{1}} ⊢ C_{O}^{δ_{1}} \\ Γ_{I}^{δ_{1}}, A_{O}^{δ_{1}} −∘ B_{I}^{δ_{1}}, Θ_{I}^{δ_{1}} ⊢ C_{O}^{δ_{1}} \end{matrix}  ⋮ . ; Λ_{I}^{δ_{1}}, (A^{⊥})_{I}^{δ_{1}} ⊢ (B^{⊥})_{O}^{δ_{1}} ; Λ_{I}^{δ_{1}} ⊢ (A^{⊥})_{I}^{δ_{1}} −∘ (B^{⊥})_{O}^{δ_{1}}
Γ_{I}^{δ_{1}}, Θ_{I}^{δ_{1}}, Λ_{I}^{δ_{1}} ⊢ C_{O}^{δ_{1}}

Indeed using the induction hypothesis we obtain

B_{I}^{δ_{1}} = B_{I}^{δ_{2}} = (B^{⊥})_{O}^{δ_{2}} = (B^{⊥})_{O}^{δ_{1}} and (A^{⊥})_{I}^{δ_{1}} = (A^{⊥})_{I}^{δ_{2}} = A_{O}^{δ_{2}} = A_{O}^{δ_{1}} hence A_{O}^{δ_{1}} −∘ B_{I}^{δ_{1}} = (A^{⊥})_{I}^{δ_{1}} −∘ (B^{⊥})_{I}^{δ_{1}} and the indicated Cut is correct. Case (i) is symmetric. In case (iii) we obtain δ_{1} extending δ_{2} with

⋮_{1}  ⋮_{2}  ⋮_{3}  ⋮_{4}
O O  I  I
I  O

which reduces to

\begin{matrix}⋮_{1} & ⋮_{3} & ⋮_{2} & ⋮_{4} \\ O & I & O & I \end{matrix}

Letting Λ = Ξ, D, we obtain a translation thus:

\begin{matrix}⋮ . ; Γ_{I}^{δ_{1}} ⊢ A_{O}^{δ_{1}} & ⋮ . ; Δ_{I}^{δ_{1}} ⊢ B_{O}^{δ_{1}} \\ Γ_{I}^{δ_{1}}, Δ_{I}^{δ_{1}} ⊢ A_{O}^{δ_{1}} ⊗ B_{O}^{δ_{1}} \end{matrix}  ⋮ . ; (A^{⊥})_{I}^{δ_{1}}, (B^{⊥})_{I}^{δ_{1}}, Ξ_{I}^{δ_{1}} ⊢ D_{O}^{δ_{1}} ; (A^{⊥})_{I}^{δ_{1}} ⊗ (B^{⊥})_{I}^{δ_{1}}, Ξ_{I}^{δ_{1}} ⊢ D_{I}^{δ_{1}}
Γ_{I}^{δ_{1}}, Δ_{I}^{δ_{1}}, Ξ_{I}^{δ_{1}} ⊢ D_{O}^{δ_{1}}

indeed, using the induction hypothesis we obtain A_{O}^{δ_{1}} = A_{O}^{δ_{2}} = (A^{⊥})_{I}^{δ_{2}} = (A^{⊥})_{I}^{δ_{1}} and B_{O}^{δ_{1}} = B_{O}^{δ_{2}} = (B^{⊥})_{I}^{δ_{2}} = (B^{⊥})_{I}^{δ_{1}} hence A_{O}^{δ_{1}} ⊗ B_{O}^{δ_{1}} = (A^{⊥})_{I}^{δ_{1}} ⊗ (B^{⊥})_{I}^{δ_{1}}.

Finally it is not difficult to show that all translations are classically equivalent: we argue by induction on the length of the sequent calculus derivation and use the provable classical equivalence of A ⊗ B with (A −∘ B^{⊥})^{⊥} and (B −∘ A^{⊥})^{⊥}, etc.

Remarks

1. For the purposes of the Corollary, we could argue directly and translate each proof net for MLL with a computationally consistent orientation δ : S → {I, O} into a natural deduction derivation in IMLL. This requires developing properties of the subnets of a proof net. Instead we prefer to use Girard’s sequentialization theorem.

2. As pointed out to us by M. Hyland, the procedure for constructing orientations in (a) can be formulated as a finite game, where the opponent begins and chooses D-R switches and O-paths, while the player replies by choosing I-paths. This appears related to recent work of Hyland and Ong on game-theoretic semantics for linear logic.

3. The procedure to construct orientations in (a) can be extended to the whole system of Linear Logic, but the translation ( . )^{δ} in (b_{1})-(b_{3}) cannot be extended in general. We omit the counterexamples; however the problem is Contraction (either explicitly in the exponentials or implicitly in the side doors of additive boxes.) A reasonable theory of computationally consistent orientations for the additives has been developed, but we omit it here for reasons of space.

Example:

The proof net

|  |
A B  B^{⊥} C  C^{⊥}  D D^{⊥} A^{⊥}
A ⊗ B  B^{⊥} ⊗ C  C^{⊥} ⊗ D  D^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥}

with the choice of A ⊗ B as output receives the orientation

|  |
O O I  O I  O I  I
O  I  I  I

These data represent the natural deduction derivation

\begin{matrix}D ⊗ A & \begin{aligned}[A] & \begin{aligned}C −∘ B & & \begin{matrix}D −∘ C & [D] \\ C \end{matrix} −∘ E \\ & B \end{aligned} ; −∘ E \\ & A ⊗ B \end{aligned} ; ⊗I \\ A ⊗ B \end{matrix} ; ⊗E

The following gives another orientation of the same net, with the choice of D^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A^{⊥} as output:

|  |
I  O I  O I  O I  O
I  I  I  O

These data represent the derivation

\begin{matrix}B −∘ ¬A & \begin{aligned}C −∘ B & & \begin{matrix}D −∘ C & [D] \\ C \end{matrix} −∘ E \\ & B \end{aligned} ; −∘ E \\ ¬A \end{matrix} ; −∘ E ; D −∘ ¬A ; −∘ I

and so on.

Define a map γ on the hereditary premises of the cut formulas of S as follows. For every cut link L : \underline{X X^{⊥}}, let

• X ↦ X^{⊥}

• if \frac{Y_{1} Y_{2}}{Y} and \frac{Y_{1}^{⊥} Y_{2}^{⊥}}{Y^{⊥}} are hereditary premises of X, X^{⊥}, respectively, and Y ↦ Y^{⊥}, then Y_{1} ↦ Y_{1}^{⊥} and Y_{2} ↦ Y_{2}^{⊥}.

Lemma. If S is a proof net for direct logic or multiplicative linear logic such that only atomic formulas occur in axiom links, any orientation δ : S → P is computationally consistent if and only if for every hereditary premise of a cut link in P, the map φ = δ ∘ γ ∘ δ^{−1} dualizes the orientation (i.e., φ(I) = O and φ(O) = I).

Sketch of proof. Because of the assumption that only atomic formulas occur in axiom links, the above definition is total on the set of the hereditary premises of all cut links. Since S is a proof net, a configuration \underline{\overline{X X^{⊥}}} will never occur as a result of cut-elimination from S. Given any orientation δ : P → S, together with its inverse τ : S → P, we prove by induction on the length of a reduction sequence that δ ∘ φ ∘ τ inverts I and O if and only if no pure structure in the reduction sequence contains an irreducible cut.

Any Danos-Regnier switching, for example, induces such an orientation, by the work in Section 5.4. We obtain a translation of proof nets into synchronous π-calculus by considering the composite R ⟶^{δ} P ⟶^{π_{pure}} π_{pure}(P). We could also use the π_{pure}^{⊥} translation. In all cases, soundness and local fullness hold, according to section 5.2.

5.5 Milner’s linear λ-terms

The following is R. Milner’s direct translation [27] of the linear λ-calculus into the π-calculus :

[[λxM]]u =_{def} u(xv) [[M]]v

[[MN]]u =_{def} (νv) ([[M]]v ∥ (νx)\overline{v}⟨xu⟩x(w)[[N]]w)

(where x is not free in N).

[[x]]u =_{def} \overline{x}⟨u⟩

It is interesting to compare Milner’s translation of the linear λ-calculus with our “logical” translations into oriented proof nets: (i) the Abramsky translation π and (ii) the translation π^{o}δ obtained from Bellin and de Wiele’s result.

Lambda abstraction

The following (intuitionist) proof represents lambda abstraction:

⋮ . ; x : A ⊢ M : B ; ⊢ λx.M : A −∘ B ^{−∘ R} .

Using one-sided sequents (in classical linear logic) this becomes:

{⋮ . M \atop ⊢ x : A^{⊥}, v : B} ; ⊢ ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (M) : A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ^{^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}} ,

which corresponds to the proof net

{⋮ . S \atop A^{⊥} B} ; A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B ,

with orientation

{⋮ . δ(S) \atop I O} ; O

Let ≪M ≫xv be the Abramsky translation π(R). From the translation for ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} , we obtain:

≪λx.M ≫ u = u(xv)≪M ≫xv

Note that this is precisely the same translation as Milner obtains. But δ(A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) = O, hence the translation π ∘ δ(R) has the dual form of a sender.

Application

The following (intuitionist) proof represents application MN in natural deduction

\begin{matrix}⋮ . ; M : A −∘ B & ⋮ . ; N : A \\ MN : B \end{matrix}

which in the sequent calculus ILL becomes

\begin{matrix}\begin{aligned}{⋮ . M \atop ⊢ A −∘ B} & \begin{matrix}A ⊢ A & B ⊢ B \\ A, A −∘ B ⊢ B \end{matrix} ^{−∘ L} \\ & A ⊢ B \end{aligned} ; cut & {⋮ . N \atop ⊢ A} \\ ⊢ B \end{matrix} ; cut

Translating into classical LL one-sided sequents (letting A −∘ B be A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B) and reducing the lower-most cut yields the following representation of application

\begin{aligned}{⋮ . M \atop ⊢ A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B} & \begin{matrix}{⋮ . N \atop ⊢ A} & ⊢ B^{⊥}, B \\ ⊢ A ⊗ B^{⊥}, B \end{matrix} ⊗ \\ & ⊢ B \end{aligned} ; cut

The last proof translates into the following proof net:

\begin{aligned}{⋮ . M \atop v : A^{⊥}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} B} & \begin{matrix}{⋮ . N \atop w : A} & z : B^{⊥} \\ A ⊗ B^{⊥} \end{matrix} \\ & cut \end{aligned}  u:B I_{uz}

with orientation

{⋮ . δ(M) \atop O} \begin{matrix}{⋮ . δ(N) \atop O} & I \\ I \end{matrix}  O

Let ≪ M ≫ v and ≪ N ≫ w be π-terms, with free names v (resp. w), translating the above proofs by the Abramsky translation. We have:

≪ MN ≫u = νvwz(≪ M ≫ v ∥ v̄⟨wz⟩(≪ N ≫ w ∥ I_{uz}))
= νvwz(≪ M ≫ v ∥ v̄⟨wz⟩(≪ N ≫ w ∥ u(b)z̄⟨b⟩))

We note that Milner’s term for MN is essentially an “optimized” version of our term: the logic gives an additional axiom buffer I_{uz} whereas Milner’s translation gives a direct implementation. We may think of this axiom buffer as a “dangling wire”, which a more efficient, direct implementation would avoid.

On the other hand, in the translation π^{o}δ(R), since we have δ(A ⊗ B^{⊥}) = I, the agent corresponding to A ⊗ B^{⊥} becomes a receiver, rather than a sender.

Variables

The variable x is interpreted as an axiom buffer, viz. \overline{u : A x : A^{⊥}}. So we have:

≪x≫u = u(a)\overline{x}⟨a⟩

We see that the Milner translation is more direct: instead of sending information from x to the port u via channel a, Milner directly sends u !

So how do we explain that both Milner and Abramsky translate linear λ terms using the dual of the π^{o}δ translation and turn an O-formula into a receiver and an I-formula into a sender?

According to the basic philosophy of the π-calculus, π-terms consist of agents in an interacting environment; thus λ-calculus computations are interpreted into the π-calculus as interactions between certain agents and their environment. An environment in which a term λx.M can interact is one where an input can be received for x and a new environment is created for M with such an input. An environment v making the application MN possible can be thought as an agent sending information to M; in particular, such information includes the name x by which the main input channel of M is identified henceforth, if such an input exists. The name x is also given to an input channel which controls the new environment of the term N; since the names v and x are made private (i.e. are bound variables), the information flow is tightly controlled in the new process.

6 The Additives

6.1 Problems with the Additives

To handle the additive connectives of linear logic, we consider the full synchronous π- calculus. Unfortunately, the additives illustrate the divergence of pure logic from the concurrency world. We shall begin by illustrating the problems.

Problems with the Axioms

Recall, in the last section, we mentioned that the original Abramsky translation [2, 3] considers the axioms as bidirectional buffers. That is, one translates^{4}

π(\overline{A A^{⊥}}) = x(u) ȳ⟨u⟩ + y(u) x̄⟨u⟩

Consider the proof net

x : A  \begin{matrix}y : A^{⊥} & y : A \\ cut \end{matrix}  z : A^{⊥}

Assuming axioms are bidirectional buffers, we obtain the following π-term:

νy[x(u)\overline{y}u + y(u)\overline{x}u ∥ y(u)\overline{z}u + z(u)\overline{y}u]

Allowing distributivity (of ∥ with respect to +) in the full synchronous π-calculus causes troubles: using distributivity, we may multiply out the expressions (like polynomials). The two cross-terms x(u)\overline{y}u ∥ z(u)\overline{y}u and y(u)\overline{x}u ∥ y(u)\overline{z}u will be deadlocked.

There are at least three obvious choices of what to do:

1. Use unidirectional buffers, as in the last section, which must then be shown to be coherent with respect to the rest of the translation of the additives.

4As will become clear below, + is related to the translation of boxes. This seems to fit with the remark of Girard [13], 2.4, p.45, “Technically speaking … axioms are boxes”.

2. Ban distributivity at the level of translation of axioms.

3. Garbage collect deadlocked terms.

Although it seems fairly common in the concurrency world to consider garbage collection as a reasonable solution in such problems [25], the logical status of having deadlocked terms with garbage collection is somewhat unclear. It is certainly contrary to the spirit of translating logical deduction in a sound and faithful way.

Problems with Additive Reduction

We shall now discuss some of the thorny problems with additive reductions. The reader unfamiliar with proof boxes might find it helpful to first read Section 6.2 (Proof Structures with Boxes) below, or to use it as a reference for what follows.

To analyze the representation of the additive connectives [13] in the synchronous π-calculus, consider the sequent calculus introduction rule for &

\frac{⊢ Γ, A ⊢ Γ, B}{⊢ Γ, A&B}

where Γ is a multiset of formula occurrences (often called a context) . Recall the behaviour of the cut-elimination process:

Symmetric reduction

\begin{matrix}\begin{matrix}D_{0} ; ⋮ . ; ⊢ Γ, A_{0} & D_{1} ; ⋮ . ; ⊢ Γ, A_{1} \\ ⊢ Γ, A_{0}&A_{1} \end{matrix} & & D_{2} ; ⋮ . ; ⊢ A_{i}^{⊥}, Δ ; ⊢ A_{0}^{⊥} ⊕ A_{1}^{⊥}, Δ ⊕ \\ ⊢ Γ, Δ \end{matrix} ; cut

reduces to

\begin{matrix}D_{i} ; ⋮ . ; ⊢ Γ, A_{i} & D_{2} ; ⋮ . ; ⊢ A_{i}^{⊥}, Δ \\ ⊢ Γ, Δ \end{matrix} cut

Commutative reduction

\begin{matrix}\begin{matrix}D_{0} ; ⋮ . ; ⊢ C, Γ, A & D_{1} ; ⋮ . ; ⊢ C, Γ, B \\ ⊢ C, Γ, A&B \end{matrix} & & … \\ ⊢ D, Δ, A&B \end{matrix} R

reduces to

\begin{matrix}\begin{matrix}D_{0} ; ⋮ . ; ⊢ C, Γ, A & … \\ ⊢ D, Δ, A \end{matrix} R & \begin{matrix}D_{1} ; ⋮ . ; ⊢ C, Γ, B & … \\ ⊢ D, Δ, B \end{matrix} R \\ ⊢ D, Δ, A&B \end{matrix} ; &

where R is a cut rule (cf. the Cut algebra in section 3.2).

In sequent calculus the introduction rule for & is contextual in the sense that the contexts in the premises and conclusion must be the same multiset Γ; for the inference to be correct, a test for the identity of the contexts is required.

However, proof-theory does not specify when such a test must be performed: by permuting the & rule with the rules below it (as in commutative reductions) the test could be delayed and performed on a larger context.

As pointed out by Girard [16] and Abramsky [1], the meaning of the connective & (with) seems to involve notions of choice: A&B asserts the availability of two courses of action, the choice being an “external” one, i.e. not determined by the subject who makes the assertion, hence cannot be inferred from the given deductive context. On the other hand, the dual connective ⊕ (plus) asserts an alternative “internal” choice, which is determined by the speaker.

The key dynamical point is that, with respect to symmetric reductions, the choice between the two subderivations D_{0} and D_{1} leading to ⊢ Γ, A&B is determined during the process of cut-elimination by the information contained in the derivation D_{2} of ⊢ A^{⊥}⊕B^{⊥}, Δ. If a formula C_{i} in ⊢ C_{1}, …, C_{n}, A&B becomes itself a cut formula, then the interaction expressed by the elimination of such a cut is frozen unless and until interaction through A&B has happened. Additive Commutative Reductions are therefore necessary if we want to either (i)change the order of communication, or (ii) to make interaction through C_{i} possible, if interaction through A&B never happens.

In the theory of proof-nets, the issue of finding an optimal representation for additives is still under active research. There are at least three candidates:

(i) additive boxes, (ii) additive contraction links, and (iii) slices, of which (i) and (iii) find analogues in the π-calculus translations considered below.

Additive proof boxes (see Section 6.2 below) were introduced by Girard [13] to correspond to the contextually-dependent rules of sequent calculus. In particular, the requirement “testing the identity of contexts” of the &- introduction rule is expressed by “putting in a box” the proof-nets corresponding to the derivations of the premises. As in sequent calculus, the choice of the context is not unique: additive boxes can be expanded (cf. the Additive Commutative Reductions in section 6.1 below). This representation suggests the idea of breaking the &-rule into three processes: two yielding the premises of the inference and a third one starting with the “non-logical axiom” ⊢ Γ, A&B. This seems inappropriate: we may insist that a unique flow of information runs through the three processes and therefore search for a representation of proofs without the additive box.

Additive contraction links together with a binary &-link

\frac{A B}{A&B}  \frac{C_{1} C_{1}}{C_{1}}  …  \frac{C_{n} C_{n}}{C_{n}}

implement the idea of a unique flow of information. These links seem implicit in the &-rule of sequent calculus; but to obtain an adequate representation we must also include information corresponding to testing for the identity of contexts, i.e., that there are subnets S_{1} with conclusions A, Γ and S_{2} with conclusions B, Γ.

Slices were introduced in the Appendix of Girard’s original paper [13]; the intuition seems to be that at each &-rule we really have two independent subarguments, one including a step \frac{A}{A&B}, the other a step \frac{B}{A&B}; Here additive contractions disappear, but an external test then verifies that the subarguments coincide from certain points of the context; i.e., from those points different slices must be identified and only the set of all slices with all these identifications has a correct logical meaning.

The different representations have different dynamical behaviours. The first two representations, in presence of the Additive Commutative Reductions, do not enjoy the the Church-Rosser property; for a simple example, consider the possible ways of eliminating the cut in the proof nets corresponding to

\begin{matrix}\begin{matrix}⊢ A, A^{⊥} & ⊢ A, A^{⊥} \\ ⊢ A&A, A^{⊥} \end{matrix} & & \begin{matrix}⋮ . ; ⊢ A, A^{⊥} ⊗ (B^{⊥} ⊕ C^{⊥}), B & ⋮ . ; ⊢ A, A^{⊥} ⊗ (B^{⊥} ⊕ C^{⊥}), C \\ ⊢ A, A^{⊥} ⊗ (B^{⊥} ⊕ C^{⊥}), B&C \end{matrix} & \\ ⊢ A&A, A^{⊥} ⊗ (B^{⊥} ⊕ C^{⊥}), B&C \end{matrix} ; cut

In the representation through slices, Additive Commutative Reductions modify only the places where the external test is performed, not the slices themselves. In fact, slices were introduced by Girard [13] as an invariant in the cut-elimination process. However, if the test of correctness has to be performed during cut-elimination, the reduction steps in different slices must be correlated. Attempts to consider a mathematical theory of slices independently of the boxes of which they are slices have so far produced a rather complicated syntax.

How does our π-calculus translation relate to the additives ? The translation of the & rule given in section 3.2 corresponds closely to the translation of the corresponding proof net with additive box: indeed communication through the channel \overline{z} (corresponding to the principal door of the box) yields a communication through one of the channels u or v, i.e., a choice of one of the summands P_{w⃗ x} or Q_{w⃗ y}. The problem is that in the synchronous π-calculus it may also be possible to commute some of the prefixes and to obtain a communication through some channel in w⃗, which yields a completely arbitrary choice of one of the summands (cf. section 2.2). Essentially for this reason, local fullness fails for the translation of section 3.2 ^{5}.

To recover local fullness, we reintroduce some restrictions from the asynchronous π calculus [25], namely the use of guarding prefixes, as in section 2.2. Since guarding prefixes prohibit rewriting in the guarded context, only certain logical reduction strategies can be represented, see theorem 14 below.

From the logical viewpoint, if would be desirable if the π-calculus could faithfully represent the categorical notion of weak product (i.e. the additive connective &, with its symmetric reductions). This would require a notion of congruence which permits rewriting under the + as well as in a guarded context, but the theory of synchronous π-calculus has not yet decided this issue.

5Categorically speaking, the Cut Algebra for the additives (symmetric reductions) expresses the fact that & must be a weak product; in most models & is actually a product.

This is completely at odds with the behaviour of +

Additive Commutative Reductions can be naturally represented in the translation of section 2.2, if distributivity of ∥ with respect to + is permitted. This is clearly incompatible with guarding. Therefore no evaluation strategy involving additive commutative reduction can be fully represented.

To fully represent every reduction strategy we are led to avoid the use of + in Abramsky’s translation, replacing it with ∥, as first suggested in [24]. Once this idea is fully developed, it turns out to provide a translation of Girard’s theory of slices, as shown in theorem 18 below.

6.2 Proof Structures with Boxes

We consider proof structures for MLL extended with

• Nonlogical Axioms i.e., links \overline{X, X_{1}, …, X_{n}}

For Multiplicative and Additive Linear Logic MALL (without constants) we use the additive links

• Plus Links {A_{0} \atop A_{0} ⊕ A_{1}} {A_{1} \atop A_{0} ⊕ A_{1}}

and the additive boxes

• & Boxes

A&B  C_{1}  … C_{n}

For the full propositional system (without constants) we also add links for the exponential operator ? and the !-boxes as follows:

• Weakening Axiom ?A In order to verify the correctness of proof nets Weakening axioms are given with an attachment to some other formula occurrence (we represent it by \overline{?A} ⇁ C).

• Dereliction Link {A \atop ?A}

• Contraction Link {?A ?A \atop ?A}

• ! Boxes

!A ?C_{1}  … ?C_{n}

We give a precise definition of proof boxes.

Definition. A proof box B(R_{1}, …, R_{n}, A) is a relation where R_{1}, …, R_{n} are pairwise disjoint proof structures and A is a non-logical axiom.

Any conclusion of a proof structure R_{i} is called a premise of the box; occurrences in the non-logical axiom A are called the conclusions of the box B. The premises and the conclusions of each box will be in some correspondence with each other (to be specified case by case); in all cases, a box B(R_{1}, …, R_{k}, \overline{X, X_{1}, …, X_{n}}) has the property that for each i ≤ k the conclusions of R_{i} are exactly Y, X′_{1}, …, X′_{n}, where Y is an immediate (proper) subformula of X and where X′_{j} and X_{j}, j ≤ n, are occurrences of the same formula. The occurrence X is then called the principal door and X_{1}, …, X_{n} the auxiliary doors of the box.

• In a !-box B(R_{1}, A), the axiom A must have the form \overline{!A,?Γ}; the principal door is the indicated occurrence of !A; the conclusions of R_{1} must be exactly A,?Γ. (Here if Γ = C_{1}, …, C_{n}, then ?Γ = ?C_{1}, …, ?C_{n}.)

• In a &-box B(R_{1}, R_{2}, A), the axiom A must have the form \overline{A&B, Γ}; the principal door is the indicated occurrence of A&B, the conclusions of R_{1} are exactly A, Γ and the conclusions of R_{2} are exactly B, Γ.

Graphically:

R_{1}  R_{1} R_{2}
!:  ?Γ, A  &:  Γ, A Γ, B
?Γ,!A  Γ, A&B

In this graphical representation it is intuitively clear what it means for a formula, a substructure or a box to be inside or outside a given box.

We can define proof structures with boxes for full propositional Linear Logic inductively as follows. Let lnk be a set of correct propositional links (logical axioms, weakening axioms with attachments, times, par, plus, dereliction, contraction links). Then

1. a logical axiom is a proof structure with boxes;

2. if R′ and R′′ are proof structure with boxes, the so is R′ ∪ R′′

3. if

{R \atop A A^{⊥}}  and  {R′ \atop A B}  and  {R′′ \atop A}

are proof structures with boxes and \frac{A B}{C} or \frac{A}{C} are links in lnk then

R ; \underline{A A^{⊥}} and {R′′ \atop A ↽ ?B} and \frac{{R′ \atop A B}}{C} and \frac{{R′′ \atop A}}{C}

are proof structures with boxes; 4. if S_{1} is a proof structure with boxes, whose conclusions are exactly

A,?B_{1}, …,?B_{n} and A = \overline{!A,?B_{1}, …,?B_{n}} is a nonlogical axiom, then S_{1} ∪ A with the box B(S_{1}, A) is a proof structure with boxes;

5. if S_{1} and S_{2} are proof structures with boxes, whose conclusions are exactly A, Γ and B, Γ, respectively, and if A = \overline{A&B, Γ} is a nonlogical axiom, then S_{1} ∪ S_{2} ∪ A together with the box B(S_{1}, S_{2}, A) is a proof structure with boxes.

We may also give a direct definition of proof structures S with boxes analogous to that in Section 4.1. It is clear that if we remove the set of boxes box from the definition of S = (fml, lnk, box), then we obtain a collection (fml, lnk) = (S_{1}, …, S_{k}) of proof structures with nonlogical axioms.

Definition. A switch for a contraction link a choice of one of the premises (cf. the par link). Let S be a proof structure with multiplicative links, and, in addition, nonlogical axioms \overline{X, X_{1}, …, X_{n}} and plus, weakening, dereliction, contraction links. If s is a switching for S, then define the D-R graph as before, with the following additions:

• for each nonlogical axioms \overline{X, X_{1}, …, X_{n}}, introduce edges (X, X_{1}), (X_{1}, X_{2}), …, (X_{n−1}, X_{n});

• for each plus link \frac{A_{i}}{A_{0} ⊕ A_{1}} introduce an edge (A_{0} ⊕ A_{1}, A_{i}); similarly

for dereliction links;

• for each weakening axiom with attachment, introduce an edge corresponding to the attachment;

• for each contraction link, introduce an edge between the conclusion and the premise chosen by the switching (as in a par link).

We say that S is a proof net with nonlogical axioms if for each switching s, the graph s(S) is acyclic and connected. Finally, we say that a proof structure with boxes S = (fml, lnk, box) is a proof net with boxes if each S_{i} in (fml, lnk) = (S_{1}, …, S_{k}) is a proof net with nonlogical axioms.

Reductions for proof structures with additive boxes are (in addition to the previously defined MLL reductions):

Additive Symmetric Reductions:

⋮ R_{1} R_{2}

A_{i}^{⊥}  A_{1} Γ A_{2} Γ
A_{1}^{⊥} ⊕ A_{2}^{⊥}  A_{1}&A_{2} Γ
⋮

reduces to

\begin{matrix}⋮ & R_{i} \\ A_{i}^{⊥} & A_{i} Γ \end{matrix}

Additive Commutative Reduction:

R_{1} R_{2}
R_{0}  D Γ A_{1} D Γ A_{2}
Δ D^{⊥}  D Γ A_{1}&A_{2}
⋮

reduces to

R_{0}  R_{1}  R_{0}  R_{2}

Δ \underline{D^{⊥} D} Γ A_{1} Δ \underline{D^{⊥} D} Γ A_{2}

Δ Γ A_{1}&A_{2}

⋮ Exponential Symmetric Reductions:

Weakening /!:

R_{1}
A ?C_{1}, …,?C_{n}
\overline{?A^{⊥}}  !A ?C_{1}, …,?C_{n}
⋮

reduces to

\overline{?C_{1}} … \overline{?C_{n}} ; ⋮

Dereliction /!:

⋮ R_{1}

A^{⊥}  A ?Γ
?A^{⊥}  !A ?Γ
⋮

reduces to

⋮  R_{1}
A^{⊥}  A ?Γ
⋮

contraction /!:

⋮ R_{1}

?A^{⊥} ?A^{⊥}  A ?Γ
?A^{⊥}  !A ?Γ
⋮

reduces to

R_{1}  R_{1}
⋮  A ?Γ  ?Γ A  ⋮
?A^{⊥}  !A ?Γ  ?Γ !A  ?A^{⊥}
⋮  ⋮

contractions ?Γ

Exponential Commutative Reductions:

\begin{matrix}R_{1} & R_{2} \\ A ?Γ ?(D^{⊥}) & D ?Δ \\ !A ?Γ ?(D^{⊥}) & !D ?Δ \\ ⋮ & ⋮ \end{matrix}

reduces to

R_{2}
R_{1}  D ?Δ
A ?Γ ?(D^{⊥}) !D ?Δ

!A ?Γ ?Δ
⋮  ⋮

6.3 Slicings

An additive slice is a proof structure whose formulas are in the language of MALL and whose links are logical axioms, cut, times and par links, and in addition

{A_{i} \atop A_{0} ⊕ A_{1}} ⊕  and  {A_{i} \atop A_{0}&A_{1}} & for i = 0, 1

A slicing Sℓ(R) of a proof structure with boxes is a family ⟨Q_{i}, ι_{i}⟩_{i∈I} where Q_{i} is a slice and ι_{i} : Q_{i} → R is an embedding such that X and ι(X) are occurrences of the same formula, defined by induction on the definition of R as follows:

1. if R is a logical axiom A = \overline{X, X^{⊥}}, then Sℓ(R) = ⟨A, id⟩;

2. if R is R_{1} ∪ R_{2} and Sℓ(R_{1}) = ⟨Q_{i}, ι_{i}⟩_{i∈I} Sℓ(R_{2}) = ⟨Q′_{j}, ι′_{j}⟩_{j∈J} then we set Sℓ(R) = ⟨Q_{i} ∪ Q′_{j}, ι_{i} ∪ ι′_{j}⟩_{i∈I,j∈J};

3. let ∘ be either ⊗ or ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ; if

R = \frac{{R′ \atop A B}}{A ∘ B} ,  and  Sℓ({R′ \atop A B}) = ⟨Q′_{i}, ι′_{i}⟩_{i∈I},

then Sℓ(R) = ⟨Q_{i}, ι_{i}⟩_{i∈I} where

Q_{i} = Q′ ; \frac{A B}{A ∘ B}

and ι_{i} is ι′_{i} extended with the assignement A ∘ B ↦ A ∘ B; similarly, if R results from R′ by introducing a cut link, or a plus link;

4. let A = \overline{A_{1}&A_{2}, Γ}; suppose R is B(R_{1}, R_{2}, A) and Sℓ(R_{1}) = ⟨Q′_{i}, ι′_{i}⟩_{i∈I}, Sℓ(R_{2}) = ⟨Q′′_{j}, ι′′_{j}⟩_{j∈J}, where I and J are disjoint; then let

Sℓ(R) = ⟨Q_{k}, ι_{k}⟩_{k∈I∪J}, where

Q_{k} = Q′_{k} ; \frac{A_{1}}{A_{1}&A_{2}}  if k ∈ I, Q_{k} = Q′′_{k} ; \frac{A_{2}}{A_{1}&A_{2}}  if k ∈ J

and where ι_{k} is ι′_{k} (resp ι′′_{k}), extended with the assignment A&B ↦ A&B.

It is possible to consider slicings independently of any inductive definition, but we will not do this here (cf [6]).

Within each slice we define symmetric reductions as for multiplicative structures and, in addition,

\begin{matrix}⋮ & ⋮ \\ A_{i}^{⊥} & A_{i} \\ A_{0}^{⊥} ⊕ A_{1}^{⊥} & A_{0}&A_{1} \end{matrix}

reduces to

\begin{matrix}⋮ & ⋮ \\ A_{i}^{⊥} & A_{i} \end{matrix}

On the other hand, a slice with a link of the form

\begin{matrix}⋮ & ⋮ \\ A_{i}^{⊥} & A_{1−i} \\ A_{0}^{⊥} ⊕ A_{1}^{⊥} & A_{0}&A_{1} \end{matrix}

represents a logical inconsistency and a computational deadlock (we shall call it an additive deadlock) and must be deleted in the process of normalization (garbage collection!).

The set of slices occurring in Sℓ(R) is invariant under commutative reductions (although the associated embeddings change):

Lemma. If R ≻ R′ by a commutative reduction, then

Sℓ(R) = ⟨Q_{i}, ι_{i}⟩_{i∈I} and Sℓ(R′) = ⟨Q_{i}, ι′_{i}⟩_{i∈I}

Let S be a proof structure with boxes. If we remove all boxes, we obtain a set {R_{1}, …, R_{n}} of pairwise disjoint proof structures possibly with nonlogical axioms. We say that S is a proof net with boxes if each R_{i} is a proof net with nonlogical axioms.

We now give a version of soundness and local fullness for the representation of additive proof nets (with boxes) via slicing. This is an extension of the discussion in Girard [13]; for more details see Bellin [6].

Let R be a proof net with boxes and consider its set of slices ⟨Q_{i}, ι_{i}⟩_{i∈I}. Each cut C in R corresponds to a set of cuts C_{i} in the set of slices (by taking the inverse images of the ι’s). Reducing C in one step will correspond to simultaneously reducing all the C_{i}. However, in the case of additive reductions, some of the Q_{i} will be in an additive deadlock. So when we do the cut-reduction, we put each deadlocked slice into a garbage collector G (this will be regarded as a reduction step for that slice). Thus the Soundness theorem takes the following form:

Theorem 15 (Soundness for Slicing) Let R be a proof net with boxes. Let R ≻ S. Then Sℓ(R) ≻ Sℓ(S) ∪ G, where G is the set of slices in an additive deadlock.

Local fullness takes the following form:

Theorem 16 (Local fullness for Slicing) Let R be a proof net with boxes and let C be a cut therein. If Sℓ(R) ≻ F by a simultaneous reduction of all the cuts C_{i} in the inverse image of C under the ι’s, then there exists a proof net S such that R ≻ S by reduction of the cut C and F = Sℓ(S) ∪ G, where G is a set of slices in additive deadlock.

6.4 Translation of MALL proof structures

The π-translations given in section 3 and 4 can be extended to MALL as follows:

π ( {R \atop \frac{A}{A ⊕ B} Γ}) = (νx) z(u v) \overline{u}x (P_{xx̃})

π ( {R \atop \frac{B}{A ⊕ B} Γ}) = (νx) z(u v) \overline{v}x (P_{xx̃})

and

π (  \begin{matrix}R_{1} R_{2} \\ Γ, A Γ, B \\ Γ, A&B \end{matrix}  ) = ν(uv) \overline{z}⟨uv⟩. [u(x).Q′_{xw̃} + v(y).Q′′_{yw̃}]

where P = π(R), Q′ = π(R_{1}), and Q′′ = π(R_{2}).

This can be represented as:

\frac{{Px̃ \atop x : A}}{z : A ⊕ B}  and  \frac{{Px̃ \atop x : A}}{z : A ⊕ B}

and

Q′ Q′′
x : A w̃ : Γ y : B w̃ : Γ
u  v
z : A&B w̃ : Γ,

Corresponding to the additive symmetric reductions we have

P_{0} ≡ (νz)[(νx) z(u v) \overline{u}x P_{xx̃} ∥ ν(u v) \overline{z}⟨u v⟩. [u(x).Q′_{xw̃} + v(y).Q′′_{yw̃}]]
≻
(νu v) [(νx) \overline{u}x P_{xx̃} ∥ [u(x).Q′_{xw̃} + v(y).Q′′_{yw̃}]]
≻
(νx) [P_{x,x̃} ∥ Q′_{xw̃}]
(∗∗)  and
P_{0} ≡ (νz)[(νy) z(u v) \overline{v}y P_{yỹ} ∥ ν(u v) \overline{z}⟨u v⟩. [u(x).Q′_{xw̃} + v(y).Q′′_{yw̃}]]
≻
(νu v) [(νy) \overline{v}y P_{yỹ} ∥ [u(x).Q′_{xw̃} + v(y).Q′′_{yw̃}]]
≻
(νy) [P_{y,ỹ} ∥ Q′′_{yw̃}]

The names u and v in (νx) z(u v) \overline{u}x (P_{xx̃}) or (νx) z(u v) \overline{v}x (P_{xx̃}) or ν(uv) \overline{z}⟨uv⟩. [u(x).Q′_{xw̃} + v(y).Q′′_{yw̃}] will be called choice names; these names determine which subprocess will be retained or discharded in the above reduction. To emphasize their rôle, we shall denote choice names by boldface letters in what follows, and similarly for the exponentials in the next section.

Now we prove a restricted form of soundness and local fullness of the π-translation of proof structures for MALL.

Theorem 17 The π-translation of proof structures in MALL is sound and locally full with respect to the normalization strategy reducing the cuts which lie outside all additive boxes.

Proof: Soundness is easy. For the local fullness, we argue by induction on the formation of π(S). The only successful communications will have the forms (*) (see Theorem 7) and (**) above. The case of reduction (*) is as before, for the multiplicatives. For the sake of simplicity, we regard the two steps in (**) as a single rewriting step. Suppose that the P_{0} in (**) is a subterm of P^{∗}. By the properties of the asynchronous prefixes no interaction involving a channel in Q′_{xw̃} or Q′′_{yw̃} may occur in P^{∗}. Hence only interaction with the choice terms u or v can determine the choice of summand in P_{0}. Therefore terms of the form

(νu v) [(νy) \overline{v}y P_{yỹ} ∥ [u(x).Q′_{xw̃}]

(additive deadlock) will never result in the reduction process.

Thus we see that the “communication protocols” of the choice names determine the behaviour of the relevant processes and guarantee that deadlocked slices are deleted.

We also consider a π-translation of slicings of a proof structure for MALL; to this end, we extend the translation in section 4.2. Let R be a proof structure with additive boxes and let P = π(R). Moreover, let σ be a function defined on the set all the subterms of the form Q_{1} + Q_{2} in P which chooses either Q_{1} or Q_{2}; let P_{σ} be the result of the following operations: (i) erase all guardings (i.e. dots), (ii) replace each subterm of the form Q_{1} +Q_{2} in P with σ(Q_{1} + Q_{2}), Call such a P_{σ} a slice of the term P. Finally, if Σ = {σ_{1}, …, σ_{n}} is the set of all distinct slices of P, then we define the slicing of P to be

∥_{σ∈Σ} P_{σ}

where we assume all the P_{σ} have disjoint free variables (if necessary, by renaming).

Alternatively, we can define the π-translation of the slices of a proof structure directly. We proceed as in the case of additive proof structures, except that for the &-links we omit guarding and take:

π ( {R \atop \frac{A}{A&B} Γ}) = (νxu v) \overline{z}⟨u v⟩ u(x) (P_{xx̃})

π ( {R \atop \frac{B}{A&B} Γ}) = (νxu v) \overline{z}⟨u v⟩ v(x) (P_{xx̃})

The two definitions coincide:

Proposition. Let F = {Q_{i}}_{i∈I} be the set of slices in Sℓ(R), and let Π = ∥_{σ∈Σ} P_{σ} be the slicing of the term π(R); then π(F) = Π.

In other words, there is a natural bijection between the different notions of slices, whether at the level of proof structures or represented as π-terms.

The following proposition is also clear:

Proposition Let R be a proof structure with additive boxes and let P = π(R); Proposition 5 holds for each slice of P, with the exception of (iv), (v), which fail for choice names only.

The bijection between slices of nets vs slices of π-terms extends to the operational (normalization) behaviour:

Theorem 18 The π-translation of slicings in MALL is sound and locally full with respect to every normalization strategy.

Proof: Since π(Sℓ(R)) contains no +, it behaves as a term satisfying Proposition 5, except perhaps for choice names. These choice names can only interact in reductions of the form

P_{0} ≡ (νz)[(νx) z(u v) \overline{u}x P_{xx̃} ∥ ν(u v) \overline{z}⟨u v⟩. [u(x).Q′_{xw̃}]]
≻
(νu v) [(νx) \overline{u}x P_{xx̃} ∥ [u(x).Q′_{xw̃}]]
≻
(νx) [P_{x,x̃} ∥ Q′_{xw̃}]

(∗ ∗ ∗)  and
P_{0} ≡ (νz)[(νy) z(u v) \overline{v}y P_{yỹ} ∥ ν(u v) \overline{z}⟨u v⟩. [u(x).Q′_{xw̃}]]

≻

(νu v) [(νy) \overline{v}y P_{yỹ} ∥ [u(x).Q′_{xw̃}]]

additive deadlock

Dually, for the slicing which deletes the left summand. Thus we see that a reduction in π(Sℓ(R)) yields an additive deadlock if and only if so does a reduction in Sℓ(R).

Finally, we can extend the Bellin-van de Wiele orientations to the case of proof nets for MALL, as well as for the exponentials, as mentioned in the remarks after Theorem 13. Alas, not all such orientations are computationally consistent. The π-translations resulting from such orientations are obtained as in the multiplicative case, but with the additive part as defined at the beginning of this section. Unfortunately, as mentioned in that remark (loc. cit.), the translation ( )^{δ} which yields linear lambda terms (cf. Corollary 14) does not directly extend beyond the multiplicatives.

7 The Exponentials

What has been done for the additives can be extended to the exponentials: namely, we may extend the translations π defined for MALL with the following. (The reader is referred to the comments in Section 3.3.)

π (\overline{?A}) = z(wdc)\overline{w}

π ( {R \atop \frac{A}{?A} Γ}) = (νx)z(wdc)d̄⟨x⟩ P_{x}

π ( {R \atop \frac{?A ?A}{?A} Γ}) = (νxy)(z(wdc)c̄⟨xy⟩) P_{xy}

and

π ( \begin{matrix}R_{1} \\ ?Γ, A \\ ?Γ !A \end{matrix} ) = !_{z}^{x} Q_{x ũ} =

= (νwdc)\overline{z}⟨wdc⟩ \{ \begin{matrix}w().(∥_{i≤|ũ|} u_{i}(wdc)w̄) \\ + \\ d(x).Q_{x ũ} \\ + \\ c(z′z′′).(νũ′ũ′′)(∥_{i≤|ũ|} u_{i}(wdc)\overline{c}⟨u′_{i}, u′′_{i}⟩ ∥ !_{z′}^{x} Q_{x ũ′} ∥ !_{z′′}^{x} Q_{x ũ′′}) \end{matrix}

Exponential Symmetric Reductions:

The reduction from

R_{1}
A ?Γ
\overline{?A^{⊥}}  !A ?Γ
⋮

where ?Γ = ?C_{1}, …,?C_{n} to

\overline{?C_{1}} … \overline{?C_{n}} ; ⋮

corresponds to

(νz) (z(wdc)\overline{w} ∥ !_{z}^{x}Q_{x ũ}) ≻_{∗}(∥_{i≤|ũ|} u_{i}(wdc)w̄)

using the recursive definition of !_{z}^{x}Q_{x ũ} and two ordinary reduction steps. The reduction from

⋮ R_{1}

A^{⊥}  A ?Γ
?A^{⊥}  !A ?Γ
⋮

to

⋮  R_{i}
A^{⊥}  A ?Γ
⋮

corresponds to

(νz) ((νxy)(z(wdc)d̄⟨x⟩) P_{x} ∥ !_{z}^{x}Q_{x ũ}) ≻_{∗}(νx) (P_{x} ∥ Q′_{x ũ}) using the recursive definition of !_{z}^{x}Q_{xũ} and two ordinary reduction steps.

The reduction from

⋮ R_{1}

?A^{⊥} ?A^{⊥}  A ?Γ
?A^{⊥}  !A ?Γ
⋮

to

R_{1}  R_{1}
⋮  A ?Γ  ?Γ A  ⋮
?A^{⊥}  !A ?Γ  ?Γ !A  ?A^{⊥}
⋮  ⋮

contractions

?Γ

corresponds to

(νz) ((νxy)(z(wdc)c̄⟨xy⟩) P_{xy} ∥ !_{z}^{x}Q_{x ũ})≻_{∗}
(νũ′ũ′′)(∥_{i≤|ũ|} u_{i}(wdc)\overline{c}⟨u′_{i}, u′′_{i}⟩(νxy)(P_{xy} ∥ !_{x}^{x′} Q_{x′ ũ′} ∥ !_{y}^{x′′} Q_{x′′ ũ′′}))

using the recursive definition of !_{z}^{x}Q_{x ũ} and two ordinary reduction steps.

Thus the above reductions are sound with respect to the reduction strategy that applies symmetric reductions outside all boxes. Moreover, if rewriting using the recursive definition of !_{z}^{x}Q_{x ũ} can be done without producing deadlocked terms–hence, without garbage collection, then we can obtain local fullness as before, since the summands in the right-hand side of that definition are guarded by their prefixes, as in the additive case. As mentioned earlier, this would seem to depend on how the rewriting theory of the recursive definition of π-terms such as !_{z}^{x}Q_{x ũ} is implemented. The latter awaits further development of the synchronous π-calculus. Moreover, for now, nothing can be said about local fullness of the above translation until details of such an implementation are given.

8 Acknowledgements

We have benefitted from numerous discussions with colleagues during the preparation of this paper. We would particularly like to thank Samson Abramsky and Robin Milner for their continuing support and interest, as well as many thoughtful comments. Also special thanks to Mads Dam, Davide Sangiorgi, and David Turner for helpful discussions on many aspects of concurrency theory, and to an anonymous referee for his insightful comments.

G. Bellin wants to thank Gordon Plotkin and Robin Milner for their kind invitation and support at the Laboratory for Computer Science, Edinburgh during 1990-92 . P. J. Scott would also like to thank LFCS, its director G. Plotkin, and the Department of Computer Science, University of Edinburgh, for their kind hospitality during his Sabbatical (1991-92), when this work was carried out.

References

[1] S. Abramsky. Computational Interpretations of Linear Logic, Theoretical Computer Science , 111, 1993, pp. 3-57.

[2] S. Abramsky. Proofs-as-processes. Seminar talk, Dept. of Computer Science, University of Edinburgh, 1992.

[3] S. Abramsky and R. Jagadeesan. New Foundations for the Geometry of Interaction, Information and Computation Vol. 111, Number 1, 1994, pp. 53-119. Preliminary version, in: IEEE Symposium on Logic in Computer Science (LICS), 1992, pp. 211-222.

[4] S. Abramsky and R. Jagadeesan. Games and Full Completeness Theorem for Multiplicative Linear Logic, J. Symbolic Logic, Vol.59, No.2, pp. 543-574.

[5] A. Asperti. Causal Dependencies in Multiplicative Linear Logic with MIX, manuscript. To appear in: Mathematical Structures in Computer Science.

[6] G. Bellin. Proof Nets for Multiplicative and Additive Linear Logic, Report LFCS-91-161, May 1991, Dept. of Computer Science, Univ. of Edinburgh.

[7] G. Bellin. Mechanizing Proof Theory: Resource-Aware Logics and Proof-Transformations to Extract Implicit Information, Phd Thesis, Stanford University. Available as: Report CST-80-91, June 1990, Dept. of Computer Science, Univ. of Edinburgh.

[8] G. Bellin and J. van de Wiele. Proof Nets and Typed Lambda Calculus, manuscript.

[9] A. Blass. A game semantics for linear logic. Annals of Pure and Applied Logic, 56, 1992, pp. 183-220.

[10] R. Blute. Linear logic, coherence and dinaturality, Theoretical Computer Science 115, 1993 , pp. 3-41.

[11] V. Danos. La logique linéaire appliquée à l’étude de divers processus de normalisation et principalement du λ-calcul, Thèse de doctorat, U. Paris VII, April 1990.

[12] V. Danos and L. Regnier. The Structure of Multiplicatives, Arch. Math. Logic , 1989, 28, pp. 181-203.

[13] J-Y. Girard. Linear Logic, Theoretical Computer Science 50, 1987, pp. 1-102.

[14] J-Y. Girard. Multiplicatives, Rend. Sem. Matem. (Torino) , 1987 (Special Issue: Logic and Computer Science, New Trends and Applications, Oct. 1986), pp. 11-33.

[15] J-Y. Girard. Linear Logic and Parallelism, manuscript, 1987.

[16] J-Y. Girard. Towards a Geometry of Interaction, in: Categories in Computer Science and Logic, ed. by J.W. Gray and A. Scedrov, Contemp. Math, 92, AMS, 1989, pp. 69-108.

[17] J-Y.Girard. Geometry of Interaction I: Interpretation of system F, in: Logic Colloquium ’88 , ed. R. Ferro, et al. North-Holland, 1989, pp. 221-260.

[18] J-Y.Girard. Geometry of Interaction 2: Deadlock-free Algorithms. COLOG-88 (P. Martin-Löf, G. Mints, eds.) Springer LNCS, 417, 1990, pp. 76-93.

[19] J-Y. Girard, Y.Lafont, and P. Taylor. Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7 , Cambridge University Press, 1989.

[20] J-Y. Girard, A. Scedrov, and P.J. Scott, Bounded Linear Logic, Theoretical Computer Science,97, No. 1, pp.1-66.

[21] G. Gonthier, M. Abadi, and J.J.Levy. Linear logic without boxes. In: Proc. of the Seventh Symposium on Logic in Computer Science (LICS), Comp Soc. Press, IEEE, 1992.

[22] P. Malacaria and L. Regnier. Some Results on the Interpretation of λ-calculus in Operator Algebras, Logics in Computer Science (LICS), 1991, Amsterdam, IEEE Computer Press, pp. 63-72.

[23] D. Miller. The π-calculus as a theory in linear logic: Preliminary results, Proc. 1992 Workshop on Extensions to Logic Programming, Springer LNCS 660, eds. E. Lamma and P. Mello, 1993, pp. 242-265.

[24] R. Milner. Personal notes.

[25] R. Milner. The polyadic π-Calculus: a tutorial, in: Logic and Algebra of Specification, eds. F.L Bauer, W. Brauer, and H. Schwichtenberg , Springer-Verlag, 1993.

[26] R. Milner. Turing Award Lecture, 1992.

[27] R. Milner. The Synchronous π-Calculus. Unpublished lectures, Dept. of Computer Science, University of Edinburgh, 1992.

[28] R. Milner. Action Structures and the π-calculus, to appear in: Proceedings of NATO Advanced Study Institute, Proof and Computation (held at Marktoberdorf), 1993. (Also available as an LFCS report, Dept. of Computer Science, University of Edinburgh.)

[29] E. Monteiro. Linear Logic as CSP, to appear in: J. Logic and Computation.

[30] L. Regnier. Lambda-calcul et réseaux. Thèse de doctorat, U. Paris VII, Mathématiques, 1992.

[31] C. Retoré. Réseaux et Séquents Ordonnés Thèse de doctorat, U. Paris VII, Mathématiques, 1993.

[32] A. S. Troelstra. Lectures on Linear Logic, CSLI Lecture Notes (V. 29), Center for the Study of Language and Information, Stanford University, 1992.

Gianluigi Bellin Equipe de Logique mathématique Université Paris VII 2 Place Jussieu 75251 Paris cedex 05 France

bellin@logique.jussieu.fr Philip J. Scott Dept. of Mathematics Univ. of Ottawa 585 King Edward Ottawa, Ont. Canada K1N 6N5

scpsg@acadvm1.uottawa.ca