Planar and Braided Proof-Nets for Multiplicative Linear Logic with Mix

G. Bellin ^{∗} A.Fleury

July 16, 1997

Abstract

We consider a class of graphs embedded in R^{2} as noncommutative proof-nets with an explicit exchange rule. We give two characterization of such proof-nets, one representing proof-nets as CW-complexes in a two-dimensional disc, the other extending a characterization by Asperti. As a corollary, we obtain that the test of correctness in the case of planar graphs is linear in the size of the data. Braided proofnets are proof-nets for multiplicative linear logic with Mix embedded in R^{3}. In order to prove the cut-elimination theorem, we consider proof-nets in R^{2} as projections of braided proof-nets under regular isotopy.

Contents

1 Introduction 2

2 Language 4 2.1 Links and Proof-Structures . . . . . . . . . . . . . . . . . . . . 5

3 A combinatorial characterization. 8 3.1 Subnets of Proof-Nets . . . . . . . . . . . . . . . . . . . . . . 11 4 A characterization in terms of concurrent processes 13

∗Research supported by EC Individual Fellowship Human Capital and Mobility, contract n. 930142. Both authors thank Jacques van de Wiele, for having contributed to the development of the ideas in this paper.

5 Weak Cut Elimination 19

6 Open problems 22

1 Introduction

Usual representations of proofs as graphs consider only abstract graphs. But graphs may also be studied as embedded in a space: in proof-theory this means giving explicit consideration to the rule of Exchange, as found in Gentzen’s calculus of sequents; in the theory of monoidal categories, one weakens the property of symmetry. Notice that the rule of Exchange is the only structural rule of Linear Logic which is not disciplined: it is either regarded as implicit or forbidden (or strictly restricted as in the case of cyclic linear logic [11]).

In the literature three cases arise: abstract graphs are used to study commutative logic and symmetric monoidal categories; planar diagrams occur in non-commutative linear logic and in non-symmetric monoidal categories; diagrams embedded in the three dimensional space give raise to braided monoidal categories. By analogy, we speak of braided linear logic or braided proof-nets [6].

In this paper we consider multiplicative linear logic with Mix in the planar and braided cases. The case of multiplicative logic without Mix was studied by the second author in his thesis [8]. There are both logical and geometrical reasons to consider the rule of Mix

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

for instance in the study of classical systems and in the theory of concurrency [2]. Notice also that the usual geometric interpretation of the tensor product of morphisms in monoidal categories is the juxtaposition of morphisms. To recover such a construction in the context of Linear Logic we must add the rule of Mix.

We are concerned with the issues of correctness, sequentialization, identity of proofs and cut elimination for geometric representations. A correctness criterion is an algorithm to verify whether a graph corresponds to a proof; a sequentialization algorithm gives a proof-graph the tree-like ordering of a sequent calculus derivation precisely when the graph is correct. Conceptually, proof-graphs should be identified when they correspond to the same intuitive argument; technically, an identity criterion should allow us to define cutelimination as a confluent and, if possible, local process.

We find that the two-dimensional representations of proofs have very interesting algorithmic properties. The restriction to non-commutative logic is not essential as we can easily recover the commutativity of the connectives by introducing an explicit Exchange rule (the cyclic rule of Exchange will be implicit in the syntax). One of the main results of this paper is to provide two simple correctness criteria for such planar graphs, that terminate in time linear in the size of the data. On the contrary, no linear criterion is known for abstract graphs.

The first criterion is a combinatorial condition on two-cells, which also allows a simple characterization of the subnets of a proof-net. In the case of abstract graphs, these computations involve a rather complex inductive construction [4].

The second criterion is inspired by Asperti’s characterization of proofs as concurrent processes, in the spirit of Petri Nets: it involves concurrent agents, which must synchronize at axioms and par links – in our generalization, also at Exchange links. Asperti’s criterion may be regarded as the appropriate generalization to the case of MLL^{−} with Mix of Girard’s no short trip condition.

The application of Asperti’s criterion in our noncommutative context (section 4) allows us to dispose of Asperti’s switches: here the process interpretation of A⊗B always requires performing B before A. As a consequence, only one test of Asperti’s condition is needed to verify correctness and therefore the test terminates in linear time. Moreover, a proof directly corresponds to precisely one distributed process; this fact displays a connection between classical logical systems and the theory of concurrency in a vivid way.

In the planar representation of proofs questions arise concerning the cutelimination process and the identity of proofs; in our context those questions can be answered by considering planar proofs as projections of threedimensional objects. Here proofs are regular isotopy classes of graphs embedded in R^{3} and the process of cut-elimination is defined in a natural way. Notice also that in monoidal categories (as the ∗-autonomous ones) it is an important issue whether to define symmetry as an equality between monoidal functors or as a natural equivalence. This leads to the consideration of braided monoidal categories ([10]). This fact too suggests a connection between Linear Logic and the topology of R^{3}.

2 Language

We use the familiar language of multiplicative linear logic, with propositional atoms P_{0}, P_{1}, …, an involution ( . )^{⊥} without fixed points (linear negation) on the atoms, formulas built up from atoms and their linear negation using the connectives ⊗ (times), ℘ (par); negation for compound formulas is defined as usual by noncommutative de Morgan laws:

(A ⊗ B)^{⊥} =_{d} B^{⊥}℘A^{⊥} (A℘B)^{⊥} =_{d} B^{⊥} ⊗ A^{⊥}

We also use a label cut, which is not a formula, as in [9].

We formalize MLL^{−} in a sequent calculus, where sequents are sets of formula-occurrences with a cyclic ordering; the rules are familiar:

IDENTITY \ NEGATION

identity  cut
\overline{⊢ P^{⊥}, P}  \frac{⊢ Γ, A  ⊢ A^{⊥}, Δ}{⊢ Γ, cut, Δ}

STRUCTURE

mix  exchange
\frac{⊢ Γ  ⊢ Δ}{⊢ Γ, Δ}  \frac{⊢ Γ, A, B, Δ}{⊢ Γ, B, A, Δ}

LOGIC

times  par
\frac{⊢ Γ, A  ⊢ B, Δ}{⊢ Γ, A ⊗ B, Δ}  \frac{⊢ Γ, A, B, Δ}{⊢ Γ, A℘B, Δ}

Remark. In the case of the Mix rule, the cyclic order of the conclusion is intuitively obtained as follows: open the cycles arbitrarily and then glue them together. We leave it to the reader to provide a precise definition. The symbol cut is explicitly indicated, because it may become active later in an exchange rule.

The formulas A and B in the premise of an Exchange are called the active formulas and the formulas B, A in the conclusion the principal formulas of the inference.

2.1 Links and Proof-Structures

For the standard definitions of links and proof-structures for commutative MLL^{−}, we refer to the definitions in the papers [3, 9]. The following variant definition is simpler, and evidently equivalent to the standard one. Proofstructures can be regarded as abstract oriented graphs, where formulas are associated with oriented edges and links with vertices. In a non-commutative context, the crossing of two edges is regarded as a link, the exchange link.

Given a graph, we give each vertex the counterclockwise orientation on the incident edges; then there is a ‘canonical’ embedding of the graph into a surface, which can be roughly described as follows: paste a disk on the edges following the counterclockwise orientation of the vertices, but leaving vertices with only one incident edge (e.g., the conclusions of a proof-structure) on the boundary of the surface. For instance, the following two proof-structures have a canonical embedding into a cylinder and a torus, respectively, as in fig. 1,

(a) and (b).

A B  A^{⊥} B^{⊥}  A B  A^{⊥} B^{⊥}
A ⊗ B  A^{⊥} ⊗ B^{⊥}  A ⊗ B  A^{⊥} ⊗ B^{⊥}
(A ⊗ B)℘(A^{⊥} ⊗ B^{⊥})

On the other hand, using the explicit exchange, we produce a graph whose associated canonical surface is a 2-dimensional disk, as in fig. 1, (c).

⊗  ⊗ (b) canonical embedding in a torus ⊗ ⊗  ℘ ⊗ ⊗ (a) canonical embedding in a cilinder (c) embedding in a disc

Fig. 1

The main idea of this paper, further developed in the thesis of the second author [8], is to consider embeddings in a two-dimensional disk and to define a correctness condition for proof-nets in terms of the resulting the 2-cells.

Definition. (i) A proof-structure is a finite 2-dimensional CW-complex, which is isomorphic to a closed disk D_{2}. The 0-cells (i.e., vertices) are of three kinds:

1. axioms, of incidence 2 (binary links);

2. Cut, times and par links (ternary links) and conclusions on the bound-

ary, of incidence 3;

3. exchange links, of incidence 4 (quaternary links)

as represented in figure 2. As usual, if D is a CW-complex, then ∂D denotes the boundary of D. The 1-cells lying on the boundary are oriented counterclockwise; the other 1-cells have the orientation indicated in figure 2 and are typed, i.e., a unique formula is assigned to the arrow. Namely, an edge incident to the boundary which does not lie on it must be oriented towards it; such an edge is called a conclusion of the proof-structure. For vertices not on the boundary and among the edges incident to a link, those oriented towards it are the premises, the other are the conclusions of the link; binary and quaternary links have two conclusions, ternary links one. The ordering of 0-cells and 1-cells induced by the arrows will be called the structural orientation. We say that a vertex v′ is above a vertex v if there is a directed path from v′ to v.

AXIOM A  A^{⊥}  CUT A^{⊥}  A cut CONCLUSION C EXCHANGE TIMES  PAR ℘ ⊗ A  B A ⊗ B  A  B A℘B A  A B  B

Fig.2

Proposition. In every proof-structure from every 0-cell there is a directed path to a conclusion of the proof-structure.

Proof. Suppose there is a vertex v_{0} from which we can reach neither the boundary nor a logical link by a directed path. Consider the set V of all vertices that are reachable by a directed path from v_{0}. It follows that every v ∈ V belongs to a cyclic directed path p_{v}. Consider the 2-cell outside the union of all the p_{v}, for v ∈ V: this cell is not a disk, contrary to the definition of a CW-complex.

Suppose from v_{0} we reach a logical link v_{1}, but not the boundary. Follow the arrow from v_{1} across exchange links to the next logical link v_{2}, go to the conclusion and follow the arrow, and so on. Since the proof-structure is finite, a non-terminating path must be cyclic and reach again a vertex v_{i}, necessarily from a premise. But this is impossible, since the arrows are typed by propositional formulas, which cannot be proper subformulas of themselves, or by the label cut, which cannot occur inside a formula.

The argument in the second paragraph of the proof applies in general to abstract graphs. The argument of the first paragraph does not exclude the presence of cyclic directed path, but it will be shown that in the case of proof-nets the structural orientation is a partial ordering.

3 A combinatorial characterization.

Definition. (Correctness criterion) We define a subset C of the 2-cells set inductively thus:

1. the 2-cells on the boundary are in C;

2. if the 2-cells c_{1} and c_{2} are adjacent to the conclusion of a par link and belong to C, then the third 2-cell c adjacent to the premises of the par link is in C;

3. if the 2-cells c_{1}, c_{2} and c_{3} are adjacent to the conclusions of an Exchange and belong to C, then the fourth 2-cell c adjacent to the premises of the Exchange is in C.

A proof-structure is a proof-net if all 2-cells are in C.

Theorem 1. Let R be a proof-structure embedded in a 2-dimensional disk. Then R is a proof-net if and only if there exists a sequent derivation D such that R = (D)^{−}.

The if part is left to the reader as an easy exercise. The only if part is the Sequentialization Theorem below.

Example. Corresponding to the derivation

\begin{matrix}⊢ A^{⊥}, A & ⊢ B, B^{⊥} \\ ⊢ A^{⊥}, A ⊗ B, B^{⊥} \end{matrix} ⊗ ⊢ A^{⊥}, B^{⊥}, A ⊗ B exchange

⊢ A^{⊥}℘B^{⊥}, A ⊗ B ℘

\begin{matrix}\begin{matrix}⊢ A^{⊥}, A & ⊢ B, B^{⊥} \\ ⊢ A^{⊥}, A ⊗ B, B^{⊥} \end{matrix} & ⊗ \\ ⊢ B^{⊥}℘A^{⊥}, A ⊗ B \end{matrix} ; ℘

⊢ A^{⊥}℘B^{⊥}, cut, A ⊗ B cut

we construct the proof-structure embedded in a disk as follows.

cut ℘  ⊗ ℘ ×_{0} ×_{0}  ×_{0} ⊗  ×_{1} ×_{2} ×_{1}

Fig.3

Here a cell which has been put in the set C at the i-th stage of the procedure is marked with a cross ×_{i}. Notice that planarity is essential to our combinatorial characterization: the first two examples in fig.1 show that our procedure fails to detect incorrect proof-structures on a cylinder or a torus.

Sequentialization Theorem. There is an effective procedure which given a proof-net R yields a sequent derivation D such that R = (D)^{−}.

Proof. By induction on the number of 2-cells in the proof-structure d.

Case 0. If the graph can be partitioned in two disconnected graph, then we can apply the induction hypothesis and the rule of Mix.

Case 1. There is no par link nor any Exchange, hence all cells are on the boundary. Then we can certainly find a times link which is splitting, i.e., such that its removal yields two disconnected proof-structures. Then the induction hypothesis followed by a times rule concludes the case.

⊗

Suppose now that cases 0 and 1 do not apply; then by the inductive definition of C there are 2-cells that have been reached from two or three cells on the boundary. Let c be one such cell and let L be the par or Exchange link whose premises are adjacent to c.

Case 2. If all the conclusions of L are on the boundary, then we can remove L, apply the induction hypothesis and the rule L.

Case 3. Otherwise, let L be the par or Exchange link indicated in figure 4.

d′  ℘  d′

Fig. 4

Notice that we can cut the disk across one of the conclusion of L; of the two resulting disks let d′ be the one which does not contain L. We can transform d′ into a correct proof-structure by introducing an axiom link; such a proof-structure d′ is clearly a proof-net and has certainly one 2-cell less than d and at least one link different from the new axiom. Therefore we can apply the induction hypothesis and obtain a sequent derivation D′. The last inference of D′ cannot be an axiom; therefore we find a link L′ in d′ to which either case 1 or case 2 can be applied. But then we can apply the induction hypothesis to L′ already in d and conclude the proof as above.

3.1 Subnets of Proof-Nets

Definitions. (i) A substructure S of a proof-structure R is constructed in the following manner. First embed a disk D_{2} in R so that (1) the image of the boundary of D_{2} does not contain any link (i.e., a 0-cell which is not on the boundary) and (2) if a 1-cell intersects the boundary of D_{2}, then it does so trasversally and exiting the disk. Such an embedding determines a CW-complex (obviously, the one inside the disk), and the latter is itself a proof-structure. A subnet is a substructure which is also a proof-net.

(ii) In our context, a nonlogical axiom link \overline{A_{1}, …, A_{m}}, with m > 0, is a vertex with m exiting arrows. If S is a substructure of R, then (R \ S) ∪ ∂S is called the complementary context; it may be regarded as a proof-structure with a non-logical axiom link \overline{A_{1}, …, A_{m}}, where A_{1}, …, A_{m} are all the 1-cells of R which are cut by the boundary of S: simply contract S to a point. A context for which the combinatorial condition is satisfied may be called a proof-net with nonlogical axioms.

(iii) A subnet S of R is normal if both S and its complementary context \overline{S} are proof-nets. The kingdom (the empire) of A in R is the smallest (the largest) normal subnet with A as a conclusion.

Thus a classification of the normal subnets amounts to the characterization of all possible sequentializations of a proof-net. For this purpose we may consider the following variant of our combinatorial condition. The set C contains now 0-cells and 2-cells. We proceed inductively, according to fig. 5: we may put in C the cells marked by a square, only if the crossed cells are already in C.

CUT CONCLUSION AXIOM  EXCHANGE TIMES  PAR ⊗  ℘cut

Fig.5

An easy induction shows that this version of combinatorial correctness criterion is not more restrictive than the original one. It can be shown that, given a proof net R and any sequentialization D of R, the order of inferences of D is preserved by the order in which the 0-cells are put in C in some execution of the procedure.

As an application, let A be an arrow exiting from a vertex v. First, perform all the steps of the procedure that are possible without putting v in C, then stop. Let K(A) be the set of all 0-cells that are not in C at this point, together with all the 1-cells adjacent to them. Next, execute all the steps of the procedure that must be performed before we may be able to put v in C, and only those, then stop. Let E(A) be the set of all 0-cells that are not in C at this point, together with all the 1-cells adjacent to them. (We write also K(v) and E(v)).

Proposition. The kingdom (the empire) of A in R is the substructure generated by K(A) (by E(A)).

How is the above proposition related to the characterization of kingdoms and empires in the case of abstract graphs (see [4])?

Definition. A chain ⌈v, v′⌉ in a proof-structure is a path across 2n+1 links, with the following properties:

(1) v = v_{0}, v_{2n} = v′ and for 0 < i < n, v_{2i} is a times or cut link;

(2) for 0 ≤ j < n, v_{2j+1} is an axiom or exchange link;

(3) for 0 ≤ j < n, v_{2j+1} is above v_{2j} and v_{2j+2}.

In a similar way we define a chain ⌈v, v′⌋ across 2n links where v′ = v_{2n−1} is above v_{2n−2}. Write v′ ≺ v if v′ is above v.

Proposition. (i) A subnet S of a proof-net R is normal if and only if for every v and v′ in S every chain between v and v′ in R occurs entirely within S.

(ii) Let v be a vertex in R.Then the kingdom of v is the subnet generated by

⋃_{γ} ⋃_{w∈γ} K(w) ∪ {w : w ≺ v}

where γ ranges over chains ⌈v′, v′′⌉, for vertices v′, v′′ ≺ v.

Proof. See [4].

The condition there is no cyclic chain would also give an inefficient correctness criterion, analogue to the standard correctness condition for abstract graphs [4, 7]. But we can do better than searching all possible chains: only some chains have to be tested, and this can be done in linear time, as we show in the next section.

4 A characterization in terms of concurrent processes

We consider a variant of Asperti’s token game [2]; the original formulation by Asperti is in terms of Petri Nets; we speak informally of trips of tokens in a proof-structure and regard this condition as the right generalization of Girard’s no-short-trip condition to the case of MLL^{−} + Mix.

There are tokens of type ↑ and ↓. Given a multiplicative proof-structure R, in the initial position we have a token of type ↑ on each conclusion of R; the game succeeds if it reaches the terminal position where there is a token of type ↓ on each conclusion of R; the permissible movements of the tokens are those in accordance with the following instructions:

• case of an axiom link \overline{A A^{⊥}}:

from a pair ↑A, ↑A^{⊥} go to the pair ↓A, ↓A^{⊥};

• case of a par link \frac{A B}{A℘B}:

from ↑A℘B go to the pair ↑A, ↑B;
from the pair ↓A, ↓B, go to ↓A℘B;

• case of an exchange link \frac{A B}{B′ A′}:

from ↑B′ ↑A′ go to the pair ↑A, ↑B;
from the pair ↓A, ↓B, go to ↓B′, ↓A′;

• case of a times link \frac{A B}{A ⊗ B}:

from ↑A ⊗ B go to ↑B;

from ↓B go to ↑A;

from ↓A go to ↓A ⊗ B.

The case of cut is identical to that of a times link, and will no longer be mentioned.

Remark. In the original correctness condition by Asperti, where proofstructures for MLL^{−} are abstract graphs, for each proof-structure there are several games determined by times switches. Here in a non-commutative context, we verify correctness with only one Asperti game, thus in linear time! The positions of the game for times corresponds to the Right switching on all times links; we could have taken uniformly the Left switching without loss of generality; but not every switching would work. The first two cases of fig. 1 shows that the uniform Right switching fails to detect incorrect proof-structures in the case of abstract graphs.

Definitions. (i) A deadlock is a position of the tokens which is reachable from the initial position from which the game cannot successfully terminate.

(ii) Given a proof-structure, a causal path for the Asperti game is a path of n + 1 edges together with n transitions such that one of the following cases occurs:

1. either the transition t_{i} takes a token from the edge e_{i−1} and puts a token in the edge e_{i};

2. or the edge e_{i−1} is the right premise of a times link, the edge e_{i} is the conclusion of the same link and the transition t_{i} puts a token of type ↓ in e_{i} (so that the transition t_{i} was preceded by a transition t′ from e_{i−1} putting a token of type ↑ on the other premise of the times link);

3. or the edge e_{i−1} is the conclusion of a times link, e_{i} is the left premise of the same link by the switch and the transition t_{i} puts a token of type ↑ in e_{i} (so that the transition t_{i} must be preceded by a transition t′ from e_{i−1} putting a token of type ↑ on the other premise of the times link);

4. or the edge e_{i−1} is a conclusion of an Exchange, the edge e_{i} is the other conclusion of the exchange and the transition t_{i} puts a token of type ↓ in e_{i}. Notice that in this case in the Asperti game the transition t_{i} must be preceded by a transition t′ putting tokens of type ↑ on both premises of the Exchange link.

Given a proof-structure, let M_{0} and M_{T} denote the initial and terminal position of the Asperti game, respectively.

Proposition 1. (i) In any computation M_{0} ⇒ M′ every transition can be fired at most once.

(ii) We cannot have infinite computations starting from M_{0}.

(iii) In any computation M_{0} ⇒ M_{T} every transition is fired exactly once.

Proof. (cf. [2], 3.13, 3.15, 3.16) (i) Show by induction on the length of the computation M_{0} ⇒ M′ and by inspection of cases that for every edge e there are at most two transition t and t′ putting a token on e, where t puts a token of type ↑, t′ one of type ↓ and t must precede t′. (ii) follows from (i) and the finiteness of proof-structures. (iii) If a transition t is not fired on some edge e, then the terminal position M_{T} cannot be reached, by the proposition in section 2.1.

Proposition 2. In some computation M_{0} ⇒ M′ there is a deadlock if and only if a cyclic chain is a causal path.

Sketch of proof. (see [2], Theorem 3.24.) (if) It is easy to see that the transitions in a cyclic causal path can never be performed. (only if) There is a conclusion C and a transition t putting a token ↓ on C, such that t cannot be fired. Following the hereditary preconditions of t, i.e., the transitions that would make t possible, we construct an infinite causal path ending with C, and this path is a chain. Since the proof-structure is finite, the chain must be cyclic.

Proposition 3. Let R = (D)^{−} for some sequent derivation D. Then the Asperti game does not end in a deadlock.

Proof. By induction on the length of the derivation (cf. [2], 4.1).

Theorem 2. Let R be a proof-structure embedded in a 2-dimensional disk. Then R satisfies the combinatorial criterion if and only if the Asperti game terminates without deadlock.

Proof. (only if) If R satisfies the combinatorial criterion then it is sequentializable (Theorem 1), hence every Asperti game is deadlock-free by Proposition 3. (if) Suppose the combinatorial condition fails, i.e., R \ C ≠ ∅. Let γ = ∂C \ ∂R.

The exchange rule may determine singular points in γ_{0} of the form

×  × (a)  (b) × ×

which we remove. It can be easily checked that these are the only singular points of γ_{0}.

Let γ_{0} be a connected component of γ. Starting from γ_{0} we need to construct a cyclic chain which is a causal path. To this end we give γ_{0} the clockwise orientation (denoted by a solid arrow in the figures below), which makes γ_{0} a directed path, though not necessarily a causal path. In the case of singularities (a) and (b) we proceed as follows:

×  ×  × ×

obtaining a nonempty disjoint union of cyclic directed paths. Notice that γ cannot cross a link in the following positions, since in this case all the cells adjacent to the link would belong to C.

×  ℘  ×  ×  ×  ×

Suppose such a path γ_{1} does not contain one of the following critical configurations:

℘  ⊗ ×  ×  × (c)  (d)  (e)

then we claim that γ_{1} can be regarded as a causal path. The reader should check that a transition of the Asperti game can be assigned for each passage of γ_{1} through a link. There remain the case of an axiom link, 5 cases of a times links, 4 cases of a par link and 11 cases of an exchange link. Some typical cases are given in the picture below.

AXIOM  × ×  × × ×  × ×  ×  × × × × PAR TIMES  EXCHANGE ×  × ×  ℘ ℘ ⊗ ⊗

If a cyclic directed path γ_{1} contains some critical configuration (c), (d) and (e), then we produce a cyclic directed path γ_{2} containing a lower number of critical cases; this concludes the proof, by induction on the number of critical cases.

Let d_{1} be the disk with boundary γ_{1}. Starting from the link L of a critical case, we construct a new directed path π by descending along the structural orientation of the edges. If a subpath π_{1} of π is cyclic, then it is a causal path. Otherwise, we eventually reach γ_{1}, necessarily from the premise of a link L′ different from L. In this way we have split d_{1} in two disks d′ and d′′; let γ′ = ∂d′ and γ′′ = ∂d′′. If π reaches L_{1} from the right premise then we let γ_{2} = γ′′, otherwise we let γ_{2} = γ′. We define a directed cyclic path by giving the clockwise orientation to γ_{2}.

d’  d” d π

Suppose γ_{2} = γ′; let e_{1} and e_{2} be the edges in γ_{2} immediately preceeding and following π, respectively; let π_{2} be the concatenation e_{1} ∗ π ∗ e_{2}. Since π crosses all links from a premise to a conclusion, e_{1} is a premise of L, and e_{2} is a conclusion of L′, the path π_{2} is a causal path. On the other hand, if γ_{2} = γ′′, then for similar reasons the reverse of the path π_{2} is a causal path. This shows that γ_{2} contains a lower number of critical cases than γ_{1}.

5 Weak Cut Elimination

It is not immediately obvious how to define Cut reductions in our noncommutative environment. For instance, we cannot define the multiplicative cut-reduction as the transformation

reduces to cut ℘  cut cut d ⊗ a  b  c  a  b  c × ×  ×

since the resulting proof-structure may no longer be correct, even if the original one was a proof-net – in our example, the 2-cell d is never reached, as we cannot propagate across the indicated exchange because of its orientation.

On the contrary, there is a natural and indeed compelling topological intuition of proof-nets as braided objects in a 3-dimensional space, where cut-elimination is performed as efficiently as in the familiar case of abstract graphs. Here a very strong notion of isotopy is available, due to Reidemeister, and we will regard our planar representition as a projection of braided proofnets. Nevertheless, it seems plausible that the algorithmic content of a planar representation should depend on the particular notion of isotopy; for this reason, we will work with the regular isotopy , i.e., the isotopy corresponding to Reidemeister’s equivalences II and III, without assuming equivalence I:

∼ ∼∼ R III: R II: R IV:  and ∼

but not

R I:  ∼

It is not difficult to see that by using the equivalences (II), (III) and (IV) we can obtain the following reduction:

reduces to  cut cut  CUT - EXCHANGE

and similarly if the premise of the cut passes above the other edge. In this paper the notion of a braided proof-net is only needed for this use of the regular isotopy in Cut-Exchange reduction: otherwise, we work with their planar projections. The logical cut-reduction is the following:

reduces to cut ℘  CUT - REDUCTION  cutcut ⊗ a  b  c  a  b  c

Weak Cut-Elimination Theorem. Given a proof-net R with conclusions Γ, there is a sequence of reductions yielding a cut-free proof-net S with conclusion Γ.

Proof. By induction on the number n of logical links, i.e., links different from an Exchange. Given a proof-net R and a cut e, write S for k(e): we modify S and transform R into a proof-net R′ with less logical links. If one premise of e is a conclusion of an axiom v, then we eliminate both links e and v and the result is immediate.

Case 1. Suppose the no premise of e is the conclusion of an Exchange, then we can apply a logical reduction to S, yielding S′. Let e′ and e′′ be the new cuts, where e′ ∈ k(e′′). We claim that S′ is still a proof-net: indeed, in S we can “cross” the indicated times link only at a stage when the 2-cell adjacent to its premises has already been crossed; the corresponding stage of the verification of correctness in S′ is one where we have “crossed” all 2-cells adjacent to the conclusions of the new exchange, and we are ready to “cross” this new exchange and the 2-cell adjacent to its premises. The claim follows.

Let R_{0} = R\S. In R let p be the path from e to the boundary, consisting of conclusions e_{i} of exchanges such that e is above e_{i}. In R_{0} draw a copy p′ of p parallel to p, so that the resulting strip contains no link and is adjacent only to premises of exchanges; let R′_{0} be resulting configuration.

R_{0}  R′_{0}

Let R′ be the result of replacing R′_{0} for R_{0} and S′ for S so that in R′ the new cuts e′ and e′′ are connected to the boundary by the paths p and p′, respectively. By induction on the number of 2-cells in the new strip, starting from the boundary, we can see that the correctness condition terminates in R′ if and only if it terminates in R; thus R′ is a proof-net containing only n − 1 logical links, as required.

Case 2. If one of the premises of the cut is conclusion of an exchange, let r be the number of links (including Exchange) in k(e): apply a Cut-Exchange reduction to S yielding a substructure S′; it is easy to see that S′ is indeed a proof-net. Let R′ be the result of replacing S′ for S in R: then R′ is also a proof-net. The kingdom of e in S′ has r − 1 links, since one exchange link has been “pushed below” the link e. We repeat this step until no premise of e is conclusion of an exchange and then we apply the reduction of Case 1. This concludes the proof of the Weak Cut-elimination theorem.

6 Open problems

Many directions of research are open, not necessarily in convergent directions. On one hand, it would be important to give an isotopy invariant characterization of proofs in R^{3}. On the other hand, we interpret Exchange in R^{2} as synchronization of processes. What dynamical and computational interpretation is to be given of Exchange in R^{3}, where one edge passes above the other? This open question is relevant to the work on strict noncommutative proof-nets by Abrusci [1].

Another, more puzzling example can be seen in our logical reduction step for cut: when we replace a cut with two cuts of lower logical complexity, the new cuts must be written in a certain order if the resulting proof-structure is to remain correct (section 5). This rather misterious order of cuts in a noncommutative environment is certainly worthy of further investigations.

References

[1] V. Abrusci. Noncommutative Proof Nets, in Advances in Linear Logic, J-Y. Girard, Y Lafont and L. Regnier editors, London Mathematical Society Lecture Note Series 222, Cambridge University Press, 1995, pp. 271-296.

[2] A. Asperti. Causal Dependencies in Multiplicative Linear Logic with MIX. Mathematical Structures in Computer Science, 5, 1995, pp. 351-380.

[3] G. Bellin and J. van de Wiele. Subnets of Proof-nets in MLL^{−}, in Advances in Linear Logic, J-Y. Girard, Y Lafont and L. Regnier editors, London Mathematical Society Lecture Note Series 222, Cambridge University Press, 1995, pp. 249-270.

[4] G. Bellin. Subnets of Proof-nets in MLL + MIX, Accepted by Mathematical Structures in Computer Science, 1994.

[5] G.Bellin and P. Scott. On the π-calculus and linear logic, with an introduction by S.Abramsky, Theoretical Computer Science 135 (1994), pp. 11-65.

[6] R. Blute. Hopf Algebra and Linear Logic, in Mathematical Structures in Computer Science, 6, 1996, pp. 189-217.

[7] A. Fleury and C. Retoré. The Mix Rule, Mathematical Structures in Computer Science 4, 1994, pp. 273-85.

[8] A. Fleury. La règle d’ échange, Thèse de doctorat, 1996, U. Paris VII.

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

[10] A. Joyal and R. Street. Geometry of the Tensor Calculus I, Advances in Mathematics 88, 1991.

[11] D. N. Yetter. Quantales and (noncommutative) linear logic, Journal of Symbolic Logic 55, 1990, pp. 41-64.

Gianluigi Bellin Arnaud Fleury bellin@logique.jussieu.fr fleury@logique.jussieu.fr Equipe de Logique mathématique Université Paris VII 2 Place Jussieu 75251 Paris cedex 05 France