Two paradigms of logical computation in Affine Logic?

G. Bellin ^{∗}

June 29, 2001

Abstract

We propose a notion of symmetric reduction for a system of proofnets for Multiplicative Affine Logic with Mix (MAL + Mix) (namely, multiplicative linear logic with the mix-rule the unrestricted weakeningrule). We prove that such a reduction has the strong normalization and Church-Rosser properties. A notion of irrelevance in a proof-net is defined and the possibility of cancelling the irrelevant parts of a proof-net without erasing the entire net is taken as one of the correctness conditions; therefore purely local cut-reductions are given, minimizing cancellation and suggesting a paradigm of “computation without garbage collection”. Reconsidering Ketonen and Weyhrauch’s decision procedure for affine logic [14, 3], the use of the mix-rule is related to the non-determinism of classical proof-theory. The question arises, whether these features of classical cut-elimination are really irreducible to the familiar paradigm of cut-elimination for intuitionistic and linear logic.

Contents

1 Introduction 2 2 Sequent Calculus of MAL + Mix 10

∗Paper submitted in 1999, revised in 2001. Research supported by EPSRC senior research fellowship on grant GL/L 33382. This research started during a visit to the University of Leeds in 1997: thanks to Stan Wainer, John Derrick and Michael Rathjen and Diane McMagnus for their hospitality. Thanks to Martin Hyland, Edmund Robinson and especially Arnaud Fleury for extremely useful discussions during the final revision.

2.1 Mix and Weakening permutations . . . . . . . . . . . . . . . . 11 2.2 Weakening reductions and expansions . . . . . . . . . . . . . . 12

3 Additive Mix 15 3.1 Properties of Additive Mix . . . . . . . . . . . . . . . . . . . . 15 3.2 Additive Mix: reductions and permutations . . . . . . . . . . 16

4 Proof-nets for MAL + Mix 18 4.1 Proof-structures and proof-nets . . . . . . . . . . . . . . . . . 18 4.2 Computation and Elimination of irrelevance . . . . . . . . . . 19 4.3 Examples and properties of irrelevance elimination . . . . . . . 22 4.4 Mix-elimination . . . . . . . . . . . . . . . . . . . . . . . . . . 25

5 Cut-elimination modulo irrelevance 30

6 Symmetric reductions require Mix 33

1 Introduction

1. Classical Multiplicative Affine Logic is classical multiplicative linear logic with the unrestricted rule of weakening, but without the rule of contraction. Classical affine logic is a much simpler system than classical logic, but it provides similar challenges for logical computation, both in the sense of proof-search and of proof normalization (or cut-elimination). For instance, the problem of confluence of cut-elimination (the Church-Rosser property) is already present in affine logic, but here we do not have the problem of non-termination. Affine logic is also simpler than linear logic from the point of view of proof-search: e.g., propositional linear logic is undecidable, yet becomes decidable when the unrestricted rule of weakening is added. Provability in constant-only multiplicative linear logic is NP-complete, yet it is decidable in linear time for constant-only multiplicative affine logic, as it is shown below.

The tool we will use here, proof-nets for affine logic, is older than the notion of a proof-net for linear logic. In a 1984 paper [14], J. Ketonen and R. Weyhrauch presented a decision procedure for first-order affine logic (called then direct logic) which essentially consists in building cut-free proofnets, using the unification algorithm to determine the axioms. The 1984 paper is sketchy and it has been corrected (see [2, 3], where the relation between the decision procedure and proof-nets for MLL^{−} are discussed), but it contains the main ideas exploited in the present paper, namely, the construction of proof-nets free from irrelevance through basic chains. Yet neither the 1984 paper nor its 1992 revisitation contained a treatment of cut-elimination.

2. The problem of non-confluence for classical affine logic is non-trivial: the following well-known example (given in Lafont’s Appendix to [13]) reminds us that the Church-Rosser property is non-deterministic under the familiar asymmetric cut-reductions.

Example 1.

d_{1} ; ⋮ . ; ⊢ Γ ; ⊢ Γ, A ^{w^{1}} d_{2} ; ⋮ . ; ⊢ Δ ; ⊢ Δ, ¬A w_{2}

⊢ Γ, Δ reduces to

d_{1} ; ⋮ . ; ⊢ Γ ; weakenings
⊢ Γ, Δ or to

d_{2} ; ⋮ . ; ⊢ Δ ; weakenings
⊢ Γ, Δ

Asymmetric reductions.

Indeed classical logic gives no justification for choosing between the two indicated reductions, the first commuting the cut-rule with the left application of the weakening-rule (“pushing d_{2} up into d_{1}”, thus erasing d_{2}), the second commuting the cut-rule with the right application of the weakeningrule (“pushing d_{1} up into d_{2}”, thus erasing d_{1}). Therefore the cut-elimination process in MAL, a fortiori in LK, is non-deterministic and non-confluent.

Compare this with normalization in intuitionistic logic. In the typed λ calculus a cut / left weakening pair corresponds to substitution of t : A for a variable x : A which does not occur in u : B; such a substitution is unambiguously defined as u[t/x] = u. Moreover in Prawitz’s natural deduction NJ [18] the rule corresponding to weakening-right is the rule “ex falso quodlibet” and the normalization step for such a rule involves a form of η-expansion:

d ; ⋮ . ; ⊥ ; A ∧ B  reduces to \begin{matrix}d ; ⋮ . ; ⊥ ; A & d ; ⋮ . ; ⊥ ; B \\ A ∧ B \end{matrix}

Such a reduction does not yield cancellation. Thus the cut-elimination procedure for the intuitionistic sequent calculus LJ inherits one sensible reduction strategy from natural deduction: “push the left derivation up into the right one”. In the case of a weakening / cut pair it is always the left dedution to be erased.

3. Here we are interested in exploring an obvious remark: for classical logic in addition to the asymmetric reductions of Example 1, there is a symmetric possibility, the “Mix” of d_{1} and d_{2}.

Example 1, continued

d_{1} ; ⋮ . ; ⊢ Γ ; ⊢ Γ, A w_{1} d_{2} ; ⋮ . ; ⊢ Δ ; ⊢ Δ, ¬A w_{2}

⊢ Γ, Δ reduces to \begin{matrix}d_{1} ; ⋮ . ; ⊢ Γ & d_{2} ; ⋮ . ; ⊢ Δ \\ ⊢ Γ, Δ \end{matrix} Mix

Symmetric reduction.

Instead of choosing a direction where to “push up” the cut-rule, we do both asymmetric reductions, using the mix-rule.

The idea is loosely related to a procedure well-known in the literature for the case when both cut-formulas result from a contraction-rule, with the name cross-cut reduction. Let d_{1} and d_{2} be derivations of the left and right premises of the cut-rule:

Example 2.

d_{1} =  \begin{matrix}d′_{1} ; ⋮ . ; ⊢ Γ, A, A ; ⊢ Γ, A & d′_{2} ; ⋮ . ; ⊢ ¬A, ¬A, Δ ; ⊢ ¬A, Δ \\ ⊢ Γ, Δ \end{matrix}  = d_{2}

Let d_{ℓ} be obtained by commuting the cut-rule with the left application of the contraction-rule and symmetrically, let d_{r} be obtained by commuting the cut-rule with the right application of the contraction-rule. The cross-cut reduction is defined as follows:

d_{ℓ} = \begin{matrix}d′_{1} ; ⋮ . ; ⊢ Γ, A, A & d′_{2} ; ⋮ . ; ⊢ ¬A, ¬A, Δ ; ⊢ ¬A, Δ \\ ⊢ Γ, Δ, A \end{matrix} ; cut_{1} \begin{matrix}d′_{1} ; ⋮ . ; ⊢ Γ, A, A ; ⊢ Γ, A & d′_{2} ; ⋮ . ; ⊢ ¬A, ¬A, Δ \\ ⊢ ¬A, Γ, Δ \end{matrix} cut_{2}

⊢ Γ, Γ, Δ, Δ cut

contractions ⊢ Γ, Δ

= d_{r}

Cross-cut reduction.

4. As it stands the symmetric reduction of Example 1 could not be taken very seriously as a confluent notion of cut-reduction. One issue is the fact that a weakening inference may be permuted with many other inferences in a sequent derivation, and such permutations may considerably modify the structure of the proof; it would therefore be useful to have some notion of a normal form for weakening. Two standard notions can be found in the literature: these amount to applying the weakening-rule either (i) as high as possible, i.e., at the level of axioms, or (ii) as low as possible. The first solution is not available for multiplicative connectives without the contraction-rule; the second solution still leaves room for many ambiguities.

But there is one case where no ambiguity is possible, that of a weakening / multiplicative disjunction pair, where the weakening-rule introduces a formula which is active in the disjunction-rule and the other active formula has ancestors in axioms (or, similarly, the case of a weakening-rule introducing a conclusion of the derivation). It turns out that every derivation can be transformed into one where all applications of the weakening-rule are of this form, through weakening-reductions. This property may adopted as a notion of weakening normal form, but there are two problems: first, if we apply the cut-rule to two derivations in weakening normal form, the resulting derivation may not be in weakening normal form and, second, if we define weakening-reductions like permutations of inferences in the sequent calculus, then they do not yield a unique normal form (Section 2). A second issue is the nature of the mix-rule: this rule does not simply represent distinct possibilities of proof-transformation. On the contrary, it contributes to create proofs with very rich and complicated structure. However using the unrestricted weakening-rule if a sequent is derivable with Mix then it is derivable without Mix, i.e., the structural rule Mix is eliminable:

\begin{matrix}d_{1} ; ⋮ . ; ⊢ Γ & d_{2} ; ⋮ . ; Δ \\ ⊢ Γ, Δ \end{matrix} Mix

may be transformed into d_{1} ; ⋮ . ; ⊢ Γ ; weakenings

⊢ Γ, Δ but also into d_{2} ; ⋮ . ; ⊢ Δ ; weakenings

⊢ Γ, Δ

The ambiguity may be resolved by taking both reducts. More generally, for all n we may introduce an n-ary rule Additive Mix building a derivation d of ⊢ Γ out of n derivations d_{1}, …, d_{n} of ⊢ Γ:

\frac{d_{1}, …, d_{n}}{⊢ Γ} AM(n).

Then every application of Additive Mix may be permuted below other inferences. Thus the replacement of the multiplicative mix-rule with the additive mix-rule seems to capture the practice of disentangling simpler and more basic arguments from a more complicated one; conversely, the use of the multiplicative mix-rule may be explained as a compact notation unifying different ways of proving the same conclusions (Section 3). But the procedure Sep which eliminates the multiplicative mix-rule and permutes occurrences of Additive Mix below other inferences is computationally very expensive: therefore it would be desirable to find a more effective procedure to eliminate the multiplicative mix-rule.

5. If we look again at the direct logic decision procedure [14, 3], we see that two of our problems had already been solved there by the notion of a chain. Given a sequent Γ and a formula C in Γ, the procedure selects one (positive or negative) atomic subformula P in C and tries to find another subformula P of opposite polarity in some D ∈ Γ; in the terminology of proof-nets, it builds an axiom \overline{P, P^{⊥}}. Then the paths of subformulas from C to P and from P^{⊥} to D are included in the chain; moreover, if a conjunct is in the chain, say A in A ⊗ B, but the other conjunct B is not, then the procedure selects an atomic subformula Q of B and tries to find another axiom \overline{Q, Q^{⊥}}, and so on. The procedure will stop if all conjuncts have been matched by exactly one axiom. Now we apply this procedure within a proof-net R for multiplicative affine logic with Mix (MAL + Mix): it yields a path through the proof-net; if only one premise of a par link in in the path, then we introduce the other premise by a weakening-link; similarly for conclusions which are not reached by the path. The substructure S obtained in this way is a proof-net for MAL, multiplicative affine logic without Mix. If we repeat this procedure for all possible choices of axioms, we have a more efficient proof-net counterpart of the Sep procedure above. Moreover, the proof-net S corresponds to a sequent derivation in weakening normal form: we call it a proof-net free from irrelevance.

6. Given a proof-net for multiplicative affine logic with Mix, we may define a linear-time pruning algorithm, which yields a proof-net free from irrelevance, as follows ([3], section 7.5):

(0) a weakening-formula is irrelevant;

(1) if the conclusion of a link is irrelevant, all its premises are irrelevant;

(2) if a formula in a logical axiom is irrelevant, so is the other;

(3) if one premise of a times-link or of a cut-link is irrelevant, so is the conclusion and the other premise;

(4) if both premises of a par-link are irrelevant, then the conclusion is irrelevant.

Clearly this resembles Girard’s definition of the empire of a formula in MLL^{−} without Mix (cfr. [10], Facts 2.9.4). What is important for us is that from the linear-time pruning algorithm we can draw two consequences, one relevant to problems of computational complexity, the other to the definition of confluent normalization procedures.

Given a proof-structure S without attachments for the weakening-links and satisfying the acyclicity property (of every Danos-Regnier graph), consider the problem of deciding whether attachments may be added to the weakeninglinks of S so that the resulting proof-structure S′ is a proof-net. By a result of P. Lincoln and T. Winkler [15] this problem is NP-complete in the strong sense, thus it is as hard as the problem of finding a proof of Γ, given any MLL^{−} sequent Γ. But if we consider only proof-net without irrelevance the problem of attaching the weakening-links is trivial, as they can be attached to a premise of a par-link or to a conclusion: the elimination of irrelevance algorithm yields a proof-structure free from irrelevance in linear time. It follows that provability in constant-only affine logic is decided in linear time by the pruning algorithm: since axioms are precisely the subformulas 1, a sequent is provable if and only if the result of pruning the subtree of its formuals is non-empty.

Another remarkable feature of the pruning algorithm is that, regarded as a notion of reduction of proof-nets for MAL + Mix, it is confluent. It should be noticed that this algorithm cannot be defined by permutations of inferences in the sequent calculus: this follows from the study of the subnets of proof-nets [2], see examples in Section 4.3. It is this remark that allowed the research to take off, as it showed that proof-nets could be used to identify some invariants of proofs with respect to the behaviour of the weakening-rule.

7. The use of the proof-net representation of proofs and the notion of the irrelevant part I(R) in a proof-net R are essential also to define a confluent notion of cut-reduction. Irrelevance is not stable under cut-elimination: if R_{1} reduces to R_{2} and R_{2} reduces to R_{3} then we may have I(R_{1}) ⊂ I(R_{2}) but also I(R_{3}) ⊂ I(R_{2}). Therefore we cannot actually eliminate irrelevance during cut-elimination: we may metaphorically say that we need cut-elimination without garbage collection. The goal is to eliminate cut through stricly local operations, e.g., by reducing the logical complexity of the cut-formula in a weakening / cut pair. This could be achieved if we could expand weakeninglinks following the model of natural deduction. Unfortunately such an expansion is incorrect in the sequent calculus: let P be atomic, then ⊢ 1, P ⊗ P is derivable in MAL using one weakening-rule, but there is no way to expand the application of the weakening-rule into two weakening-rules with atomic conclusion P.

The solution proposed here is to define proof-nets modulo irrelevance. Given a proof-structure S without attachments for the weakening-links and satisfying the acyclicity property of every Danos-Regnier graph, we require R \ IR ≠ ∅ as an additional correctness condition; namely, we require that it should be possible to eliminate irrelevance without annihilating the proof-structure, but we do not actually eliminate irrelevance as in [14, 3]. Then the “incorrect” expansions can be introduced, since they belong to the irrelevant part; the additional weakening-links introduced in this way will eventually be annihilated by the cut-elimination procedure. As a consequence, in the intermediate steps of the cut-elimination procedure only the pruning of R_{i}, i.e., R_{i} \ IR_{i} will be sequentializable. Moreover, during the cut-elimination procedure some weakening-links may be annihilated whose attachments guaranteed the connectedness condition for the original proof-net; therefore we may start with a proof-net with cut links in multiplicative affine logic without Mix and obtain a cut-free one in multiplicative affine logic with Mix.

8. Many researchers have studied the cut-elimination process for classical logic and defined well-behaved notions of reduction and reduction strategies, enjoying the confluence and strong normalization properties. A common feature of many works is that they recognize the non-determinism of classical cut-elimination as the root of both non-confluence and non-termination and then try to to eliminate non-determinism by disambiguating classical logic. A way to do so is through translations into intuitionistic and linear logic. Such a use of linear logic is exemplified in Girard [11] and it has been developed extensively by V. Danos, J-B. Joinet and H. Schellinx, see, e.g., [7, 8]. Through the modalities of linear logic the area of a proof-net which may be erased in a weakening / cut reduction is always determined modulo permutation of !- boxes. Interesting properties of classical cut-elimination are identified in this way, which can be related to known reduction strategies for the λ-calculus. However, it should be clear that the translations of classical logic into linear logic have the same function as the translations into intuitionistic logic, namely to extend the computational paradigm of intuitionistic logic to classical logic. In the case of affine logic, such translations yield “computations with garbage collection”.

Another approach is to look for dynamical properties of classical logic that are alternative and irreducible to those of intuitionistic and linear logic. It would be natural to expect that the classical cut-elimination should reflect the symmetries that arise from the fact that classical negation is an involution. In Girard [11] a mathematically precise notion of symmetry is given for the notion of cut-reduction in the proof-net representation. The set of substitutions [p_{i}/p_{i}^{⊥}] where p_{i} is an atom in a proof-net may be regarded as the set of generators of a group acting on the graph. A notion of cut-reduction is symmetric if every proof-net which is invariant under the action of the group of substitutions is transformed by such a reduction into a proof-net which is also invariant. An example in [11] shows that a symmetric cut-reduction for classical logic cannot be defined without the use of the mix-rule. Our definition of cut-reduction for MAL with Mix would appear to be symmetric this technical sense. The cross-cut reduction of Example 2 is not symmetric, but a symmetric variant of it may perhaps be defined using the mix-rule (see section 6 below).

Most recently, Bierman and Urban [6] have developed a term calculus for classical logic which represents a very large variety of strongly normalizing, but non-confluent reduction strategies for classical sequent calculus. Bierman and Urban also regard non-determinism as the distinguishing feature of classical dynamics. The treatment of Mix in the present paper, in particular the elimination of the multiplicative mix-rule through Additive Mix, suggests that our proof-net representation may provide a concise notation for classical non-determinism. Indeed the notion of cut-elimination without garbage collegion may also have a common-sense explanation in terms of nondeterminism: if we cannot predict the future development of a process, we should be very conservative about what may be discarded or not.

Can we conclude with a positive answer to the question in the title? Do we really have a notion of cut-elimination for classical affine logic whose properties are alternative and irreducible to the familiar reduction strategies for intuitionistic and linear logic? It may be premature to give an answer. But the time may be ripe for a reconsideration of proof-nets for affine logic. Indeed an increasing number of researchers (e.g., [20]) seem to agree today that although the dynamics of classical logic may not be as elegant and pleasing as that of intuitionistic logic, a task of research is to develop tools to study it as it is, allowing the possibility that it may be very different from what we already know.

2 Sequent Calculus of MAL + Mix

Definition 1. (i) The propositional language of Multiplicative Affine Logic MAL is built from the propositional constants 1 and ⊥ and propositional variables, using the connectives ⊗ (times) and ℘ (par) of Multiplicative Linear Logic.

(ii) The language of Constant-only MAL is the fragment of MAL consisting of the formulas which do not contain propositional variables.

(iii) The sequent calculus for propositional MAL + Mix is given by the following axioms and rules:

identity rules

logical axiom: ⊢ A^{⊥}, A

{1 axiom: \atop ⊢ 1} cut: ; \frac{⊢ Γ, A^{⊥} ⊢ Δ, A}{⊢ Γ, Δ}

structural rules

exchange:

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

weakening: ; \frac{⊢ Γ}{⊢ Γ, A}

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

logical rules times:

\frac{⊢ Γ, A ⊢ Δ, B}{⊢ Γ, Δ, A ⊗ B,}

par: ; \frac{⊢ Γ, A, B}{⊢ Γ, A℘B}

The sequent calculus for classical MAL + Mix.

Given a derivation d in MAL + Mix, let us write #ax, #1 for the number of occurrences of logical axioms and of 1 axioms, and #⊗, #cut, #mix, #w and #℘ for the number of applications of the times-, cut-, mix-, weakeningand par-rules and finally #conc for the number of conclusions in d.

Lemma 1. Every sequent derivation in MAL + Mix satisfies the following equations:

#ax = # ⊗ + #cut + #mix + 1

#℘ + #conc + #1 = # ⊗ + #w + #2mix + 2

Proof. By induction on the length of the derivation. For instance, let the last inference of d be a times-rule with immediate subderivations d_{1} and d_{2}; let #ax_{1}, #ax_{2} and #ax be the number of logical axioms in d_{1}, d_{2} and in d, respectively and similarly for the other axioms and rules. Then we have

#ax = #ax_{1} + #ax_{2}

= (# ⊗_{1} +#⊗_{2}) + (#cut_{1} + #cut_{2}) + (#mix_{1} + #mix_{2}) + 2

= (# ⊗_{1} +# ⊗_{2} +1) + #cut + #mix + 1
= # ⊗ +#cut + #mix + 1
℘ + #conc + #1 = (#℘_{1} + #℘_{2}) + (#conc_{1} + #conc_{2} − 1) + (#1_{1} + #1_{2})

= (#℘_{1} + #℘_{2}) + (#conc_{1} + #conc_{2}) + (#1_{1} + #1_{2}) − 1 = (# ⊗_{1} +#⊗_{2}) + (#w_{1} + #w_{2}) + 2(#mix_{1} + #mix_{2}) + 4 − 1

= (# ⊗_{1} +# ⊗_{2} +1) + #w + 2#mix + 2
= # ⊗ +#w + 2#mix + 2

2.1 Mix and Weakening permutations

Definition 2. (i) Let m/r be a pair of consecutive inferences in a derivation d, where m is an instance of Mix and either r is not a par-rule or r is a par-rule but all the ancestors of its active formulas occur in the same branch above the mix-rule. Then the inferences m/r are permutable, i.e., we may obtain a derivation d′ which is like d, except for having a consecutive pair of inferences r/w in place of w/r. Thus the only exceptions to the permutability of the mix-rule below other inferences are of the following form:

\begin{matrix}d_{1} ; ⋮ . ; ⊢ Γ, A & d_{2} ; ⋮ . ; ⊢ B, Δ \\ ⊢ Γ, A, B, Δ \end{matrix} Mix ⊢ Γ, A℘B, Δ par

For every occurrence m of the mix-rule in d there is a set of applications of the par-rule p_{1}, …, p_{n} such that m cannot be permuted below p_{1}, …, p_{n}.

(ii) Similarly, if r/m is a consecutive pair of inferences, where m is an instance of the mix-rule, then the inferences are permutable, but if r is a times-rule, cut-rule or mix-rule rule, then there are two ways of permuting, i.e., pushing the mix-rule up to the left premise of r or to the right one.

(iii) Let w/r be a pair of consecutive inferences in a derivation d, where w is an instance of the weakening-rule introducing a formula X and X is not active in r; then the inferences w/r are permutable, i.e., we may obtain a derivation d′ which is like d, except for having a consecutive pair of inferences r/w in place of w/r.

(iv) Similarly, if r/w is a consecutive pair of inferences, where w is an instance of the weakening-rule, then the inferences are permutable, but if r is a timesrule, cut-rule or mix-rule, then there are two ways of permuting, i.e., pushing the weakening-rule up to the left premise of r or to the right one.

Remark. Weakening and Mix permutations are reversible.

2.2 Weakening reductions and expansions

Definition 3. (i) In the sequent calculus for MAL we have the following weakening-reductions:

weakening / par reduction:

{⊢ Γ \atop ⊢ Γ, A} weak ⊢ Γ, A, B

weak

⊢ Γ, A℘B par reduces to

{⊢ Γ \atop ⊢ Γ, A℘B} weak

weakening / times reduction to the right:

⊢ Γ, A {⊢ Δ \atop ⊢ Δ, B} weak

⊢ Γ, Δ, A ⊗ B times reduces to ⊢ Δ ; weakenings ⊢ Γ, Δ, A ⊗ B

weakening / times reduction to the left:

{⊢ Γ \atop ⊢ Γ, A} weak ⊢ Δ, B ⊢ Γ, Δ, A ⊗ B times

reduces to ⊢ Γ ; weakenings ⊢ Γ, Δ, A ⊗ B

weakening / cut reduction to the right:

⊢ Γ, A {⊢ Δ \atop ⊢ Δ, A^{⊥}} weak

⊢ Γ, Δ cut reduces to ⊢ Δ ; weakenings ⊢ Γ, Δ

weakening / cut reduction to the left:

{⊢ Γ \atop ⊢ Γ, A} weak ⊢ Δ, A^{⊥} ⊢ Γ, Δ cut

reduces to ⊢ Γ ; weakenings ⊢ Γ, Δ

Definition 3. (cont.) (ii) The inference eliminated by any one of the above reduction will be called irrelevant. A sequent derivation which contains no irrelevant inference is said to be in weakening normal form.

Lemma 2. In the sequent calculus for MAL every sequent derivation d can be transformed into a derivation d’ in weakening normal form. The derivation d′ is not unique.

(ii) A derivation in weakening normal form has the following properties:

1. every formula introduced by an application of the weakening-rule becomes active only in the premise of an application of the par-rule where the other active formula has an ancestor in an axiom;

2. both premises of an application of the times-rule have ancestors in (different) axioms.

Proof. (i) For every instance w of the weakening-rule, permute w below all inferences until either (a) the formula X introduced by w is active in the inference r immediately below, or (b) there is no logical inference below w. In the first case a weakening-reduction applies, unless r is a par-rule and the other active formula has not been introduced by a weakening-rule. The process is non-deterministic: in cases when weakening / times reductions to the right and to the left are both applicable, a random choice is required. (ii) By induction on the length of a derivation in weakening normal form.

Remarks. (i) Weakening / par reductions are always reversible, i.e., we have the following expansion rule:

weakening / par expansion:

{⊢ Γ \atop ⊢ Γ, A℘B} weak

expands to

{⊢ Γ \atop ⊢ Γ, A} weak ⊢ Γ, A, B

weak

⊢ Γ, A℘B

par

(ii) All other reductions are irreversible and produce a genuine loss of information.

(iii) In the sequent calculi for classical or intuitionistic logic the use of the weakening-rule can be standardized in two ways, by prescribing that all applications of the weakening-rule must occur either as low as possible or as high as possible (i.e., at the level of the axioms) in a derivation. In MAL, in absence of the contraction-rule only the first option is available for multiplicative connectives. In particular, in MAL + Mix we cannot assume that every formula introduced by Weakening is atomic: consider a cut-free derivation of ⊢ 1, P ⊗ P, where P is an atom different from 1.

(iv) On the other hand, for additive connectives in absence of the contractionrule only the second option is available, i.e., applying the weakening-rule as high as possible.

More precisely, we could define the propositional language of Additive Affine Logic AAL using the additive connectives & (with) and ⊕ (plus):

with: ; \frac{⊢ Γ, A ⊢ Γ, B}{⊢ Γ, A&B,}  plus_{i} : ; \frac{⊢ Γ, A_{i}}{⊢ Γ, A_{0} ⊕ A_{1}} i = 0, 1.

Proposition 1. In the sequent calculus for AAL every sequent derivation d can be transformed into a unique derivation d’ with the property that every formula introduced by the weakening-rule is atomic.

Proof. Repeatedly apply permissible permutations of inferences and the following expansions:

weakening / with expansion:

d ; ⋮ . ; ⊢ Γ ; ⊢ Γ, A&B weak

expands to

d ; ⋮ . ; ⊢ Γ ; ⊢ Γ, A weak d ; ⋮ . ; ⊢ Γ ; ⊢ Γ, B weak

⊢ Γ, A&B times

weakening / plus expansion:

{⊢ Γ \atop ⊢ Γ, A_{0} ⊕ A_{1}} weak

expands to

{⊢ Γ \atop ⊢ Γ, A_{i}} weak ⊢ Γ, A_{0} ⊕ A_{1}

plus

3 Additive Mix

For all n we have an n-ary rule Additive Mix which builds a derivation d of ⊢ Γ out of n derivations d_{1}, …, d_{n} of ⊢ Γ. We use the following notation:

\frac{d_{1}, …, d_{n}}{⊢ Γ} AM(n).

We have the following reduction:

Mix-elimination

\begin{matrix}d_{1} ; ⋮ . ; ⊢ Γ & d_{2} ; ⋮ . ; Δ \\ ⊢ Γ, Δ \end{matrix} Mix reduces to

d_{1} ; ⋮ . ; ⊢ Γ ; weakenings
⊢ Γ, Δ

d_{2} ; ⋮ . ; ⊢ Δ ; weakenings

⊢ Γ, Δ

⊢ Γ, Δ AM(2)

3.1 Properties of Additive Mix

The rule Additive Mix has the following properties:

1 The order of the premises is immaterial, i.e., we assume an AM-exchange rule of the form

\frac{d_{1}, …, d_{i}, d_{i+1}, … d_{n}}{⊢ Γ} ∼ \frac{d_{1}, …, d_{i+1}, d_{i}, … d_{n}}{⊢ Γ}

2. The derivations of the premises are paiwise distinct, i.e., we assume an AM-contraction rule of the form

\frac{d_{1}, …, d_{i−1}, d_{i}, d_{i}, d_{i+1}, … d_{n}}{⊢ Γ} reduces to \frac{d_{1}, …, d_{i−1}, d_{i}, d_{i+1}, … d_{n}}{⊢ Γ}

3. Consecutive applications of AM can be unified, i.e., we assume an AMmerging rule of the form

\begin{matrix}{d_{1}, …, d_{m} \atop ⊢ Γ} AM(m) & {d_{n+1}, …, d_{n+m} \atop ⊢ Γ} AM(n) \\ ⊢ Γ \end{matrix} ; AM(2)reduces to {d_{1}, …, d_{n+m} \atop ⊢ Γ} AM(n + m)

4. The rule AM-contraction can be strengthened according to different notions of identity of proofs. For instance, let us put d ∼ d′ if and only if (d)^{−} and (d′)^{−} are the same proof-net with attachments. Then the AM-contraction rule becomes:

\frac{d_{1}, …, d_{i}, d′_{i}, … d_{n}}{⊢ Γ} where d_{i} ∼ d′_{i} reduces to \frac{d_{1}, …, d_{i}, … d_{n}}{⊢ Γ}

5. A sequent derivation in MAL + AM is in AM normal form if it has at most one application of Additive Mix as the last inference.

Convention. We assume that the AM-contraction in the strong form (4) is always applied without mention, and similarly for the AM-merging rules. We work with derivations modulo the AM-exchange rule.

3.2 Additive Mix: reductions and permutations

AM / exchange permutation:

\begin{matrix}{d_{1}, …, d_{n} \atop ⊢ Γ, A, B} & AM(n) \\ ⊢ Γ, B, A \end{matrix} exch

reduces to

d_{1} ; ⋮ . ; ⊢ Γ, A, B ; ⊢ Γ, B, A exch … d_{n} ; ⋮ . ; ⊢ Γ, A, B ; ⊢ Γ, B, A exch

⊢ Γ, B, A AM(n)

AM / weakening permutation:

\begin{matrix}{d_{1}, …, d_{n} \atop ⊢ Γ} & AM(n) \\ ⊢ Γ, A \end{matrix} weak

reduces to

d_{1} ; ⋮ . ; ⊢ Γ ; ⊢ Γ, A weak … d_{n} ; ⋮ . ; ⊢ Γ ; ⊢ Γ, A weak

⊢ Γ, A AM(n)

AM / par permutation:

\begin{matrix}{d_{1}, …, d_{n} \atop ⊢ Γ, A, B} & AM(n) \\ ⊢ Γ, A℘B \end{matrix} par

reduces to

d_{1} ; ⋮ . ; ⊢ Γ, A, B ; ⊢ Γ, A℘B par … d_{n} ; ⋮ . ; ⊢ Γ, A, B ; ⊢ Γ, A℘B par

⊢ Γ, A℘B AM(n)

AM / times permutation:

{d_{1}, …, d_{m} \atop ⊢ Γ, A} AM(m) {d′_{1}, …, d′_{n} \atop ⊢ B, Δ} AM(n) ⊢ Γ, A ⊗ B, Δ times reduces to

\begin{matrix}d_{i} ; ⋮ . ; ⊢ Γ, A & d_{j} ; ⋮ . ; ⊢ B, Δ \\ … ⊢ Γ, A ⊗ B, Δ … \end{matrix} cut

⊢ Γ, A ⊗ B, Δ AM(m · n)

for i ≤ m, j ≤ n.

AM / cut permutation:

\begin{matrix}{d_{1}, …, d_{m} \atop ⊢ Γ, A} AM(m) & {d′_{1}, …, d′_{n} \atop ⊢ A^{⊥}, Δ} AM(n) \\ ⊢ Γ, Δ \end{matrix} cut

reduces to

\begin{matrix}d_{i} ; ⋮ . ; ⊢ Γ, A & d_{j} ; ⋮ . ; ⊢ A^{⊥}, Δ \\ … ⊢ Γ, Δ … \end{matrix} cut

⊢ Γ, Δ AM(m · n)

for i ≤ m, j ≤ n.

We define a procedure Sep of elimination of Mix, which takes a derivation d in MAL + Mix and returns a derivation Sep(d) in MAL + AM without Mix, in AM normal form:

1. Given a derivation d and a mix-rule m in d, permute m as low as possible, obtaining a derivation d_{m} where either m is the last inference or m is immediately followed by a par-rule p such that m cannot be permuted below p.

2. Apply the mix-elimination rule to the mix-rule m in d_{m}, yielding a derivation d′_{m}, which contains an application AM(2) of Additive Mix.

3. Permute the inference AM(2) below all inferences of d′_{m}, thus obtaining a derivation d_{m}^{∗} ending with an application of Additive Mix.

4. Let Sep(d) = d_{m}^{∗} if d_{m}^{∗} contains no mix-rule; otherwise, select a new application of the mix-rule in d_{m}^{∗} and start again with (1).

The procedure Sep has the desirable property that it does not create irrelevant inferences.

Theorem 1. (i) Let d be a derivation of Γ in MAL + Mix. The result of applying the procedure Sep to d

Sep(d) = {d_{1}, …, d_{n} \atop Γ}

is a derivation in MAL + AM without Mix in AM normal form.

(ii) If d is in weakening normal form, then so is Sep(d).

Proof. (ii) If at the end of step 1 the mix-rule m is the last inference, then no irrelevant inference is created at steps (2) or (3), so d_{m}^{∗} is still in weakening normal form. Otherwise at the end of step (1) the Mix m is followed by some par-rule p_{1}, …, p_{k} which are not permutable above m, therefore none of their active formulas is introduced by a weakening-rule; since d is in weakening normal form, it follows from Lemma 2.(ii) that all the formulas active in all p_{i} have ancestors in axioms. Therefore at the end of step (2) the Additive Mix AM(2) is immediately followed by an application of the par-rule which is not irrelevant and, moreover, after one application of the AM / par permutation both conclusions of the new par-rules have ancestors in some axiom. Finally, if a times-rule t occurs below m in d_{m} at the end of step (1), then a formula active in t is descendant of the conclusion of one of the p_{i}: otherwise, in step 1 t would be permutable above m. The same holds for cut-rules occurring in d_{m} below m. It follows that the Additive Mix permutations at step (3) do not introduce irrelevant inferences, i.e., d_{m}^{∗} is still in weakening normal form.

4 Proof-nets for MAL + Mix

4.1 Proof-structures and proof-nets

Definition 4. (i) A proof-structure for MAL + Mix is a directed graph whose edges are labelled with formulas and whose vertices (links) are of one of the following forms:

In link the incoming edges are called the premises and the outgoing edges are the conclusions of the link. The transitive closure ≺ of the relation between links (equivalently, between edges) determined by the direction of the edges is a partial ordering (since the edges are typed with propositional formulas) and it is called the structural orientation. A ≺ B reads “A is a hereditary premise of B” or simply “A is above B”. A bottom link is just a special case of a weakening-link.

(ii) Given a proof-structure S for MAL + Mix an attachment of a weakeninglink w is an edge from the weakening-link to a new vertex which lies in another edge ℓ of S. We write S^{a} for S toghether with a set of attachments for all the weakening-links of S. The geometric properties of attachments are fully determined as follows:

• a weakening-link w with its attachment a(w) has the same properties as a logical axiom;

• the new vertex where the attachment a(w) and the edge ℓ meet has the

same properties as a times-link.

(iii) A switching for a proof-structure S is a choice for every par-link in S of one of its premises.

(iv) Let S^{a} be a proof-structure with attachments for the weakening-links. Given a switching s for S^{a}, the Danos-Regnier graph sS^{a} is the graph resulting from S^{a} by deleting from each par-link the edge which is not the premise chosen by s.

(v) A proof-structure S^{a} with attachments for the weakening-links is a proofnet if for every switching s the Danos-Regnier graph sR^{a} is acyclic (correctness criterion for MAL + Mix).

Theorem 2. (i) There exists a map ( )^{−} from sequent derivations to proofstructures together with choices a_{1}, …, a_{r} of attachments for the weakeninglinks such that (d)^{−} = R^{a_{i}} is a proof-net, the attachments being given by any a_{i}, for i ≤ r.

(ii) (Sequentialization Theorem) Conversely, if R^{a} is a proof-net, then there exists a sequent derivation d and a choice a_{1}, …, a_{n} of attachments for the weakening-links such that (d)^{−} = R^{a}, and a = a_{i} for some i ≤ n.

Proof. (ii) For every weakening-link w in R^{a}, let A be its conclusion and let ℓ be the edge, labelled with B, which a(w) is attached to: replace w, a(w) and ℓ with a logical axiom ax followed by a times-link t. The proofstructure R′ thus obtained is labelled with different formulas than R^{a}, but it has exactly the same geometric properties, so it is a proof-net in MLL^{−} + Mix and can be sequentialized as usual. In a sequent derivation d′ such that (d′)^{−} = R′, let t′ be the times-rule whose principal formula A^{⊥} ⊗ B corresponds to the new times-link t. Since the only active ancestor of A^{⊥} is in the axiom ax, we may permute t′ upwards to the left so that ax and t′ are consecutive inferences and then replace them both with a weakening-rule:

\begin{matrix}⊢ A, A^{⊥} & ⋮ . ; ⊢ B, Γ \\ ⊢ A, A^{⊥} ⊗ B, Γ \end{matrix} is replaced by ⋮ . ; ⊢ B, Γ ; ⊢ A, B, Γ

By repeating this procedure for all weakening-links of R^{a} we clearly obtain a derivation d such that (d)^{−} = R^{a}.

4.2 Computation and Elimination of irrelevance

One of the uses of proof-nets for multiplicative logic without Weakening MLL^{−}, is to classify sequent derivations: we prove that given sequent derivations d and d′ in MLL^{−} we have (d)^{−} = (d′)^{−} if and only if there exists a sequence of derivations d = d_{1}, d_{2}, …, d_{n} = d′ such that for all i < n, d_{i} and d_{i+1} differ only for a permutation of two consecutive inferences (cfr. [5]). A similar result holds for MLL^{−} + Mix (cfr. [2]).

In presence of the weakening-rule, thus already in MLL with Weakening restricted to a ⊥-rule, we do not know how to obtain such a theorem. In [10] proof-nets are defined using weakening-boxes, thus the position of each weakening-rule in a given sequential proof d is fixed in the proof-net (d)^{−}.

The standard solution, which we have followed above, is the use of attachments for the weakening-links. But from the point of view of the classification of sequent derivations the notion of proof-nets with attachments is perhaps worse that that of proof-nets with weakening-boxes: given a box, there are several ways of making the attachment. In any event, this notion fails to identify sequential proofs modulo permutations of weakening-rule.

We turn now to the notion of a proof-net modulo irrelevance, which at least succeeds in minimizing the disturbances caused by weakening-links. As recalled in the Introduction, given a proof-structure S without attachments for the weakening-links and satisfying the acyclicity property (of every Danos-Regnier graph), the problem of deciding whether attachments may be added to the weakening-links of S so that the resulting proof-structure S′ is a proofnet is NP-complete in the strong sense [15]. On the other hand in a proof-net free from irrelevance the weakening-links can only be attached to a premise of a par-link or to a conclusion. Moreover, the following algorithm identifies and possibly eliminates irrelevance in linear time.

Definition 5. (computation of irrelevance algorithm, cfr. [10, 3]) Let S be a proof-structure without attachments.

(i) The irrelevant part i(w) of S determined by a weakening-link w is the smallest subgraph closed under the following rules:

• the weakening-link w and its conclusion are in i(w);

• if the premises A and B of a par-link v are in i(w), then v and its conclusion A℘B are in i(w);

• if either premise A or B of a times-link v is in i(w), then v and its conclusion A ⊗ B are in i(w); similarly, if A and B are premises of a cut-link;

• if u ≺ v and v is in i(w), then u and its conclusions are in i(w); in particular, if u is a logical axiom in i(w), then both its conclusions are in i(w).

(ii) The doors of i(w) in S are the edges which are in i(w) and are premises of links whose conclusions are not in i(w). Clearly all the doors of i(w) are either conclusions of S or premises of par-links.

(iii) Let w be a weakening-link in S. Write S^{w} for S \i(w), with the addition of a weakening-link w_{D} with conclusion D for every door D of i(w). If S has attachments and w is attached to an edge ℓ through a(w), then we may assume that ℓ ∉ i(w), otherwise such an attachment would generate a cyclic D-R-graph and S could not be a proof-net. Therefore we may define a set of attachments a′ for S^{w} as follows:

• a′(w′) = a(w′), if w′ occurs both in S and in S^{w};

• a′(w_{D}) is attached to ℓ, for all doors D of i(w), otherwise.

(iv) The pruning map given by S ↦ S^{w} for w ∈ S may be regarded as a notion of reduction, which has the Church-Rosser property.

Lemma 3. Let w_{1} and w_{2} be weakening-links in S. Then S^{w_{1}w_{2}} = S^{w_{2}w_{1}}.

Proof. Let D_{1} be a door of i(w_{1}), thus a premise of a par-link p. Suppose that the other premise D_{2} of the same par-link is in i(w_{2}) and apply the irrelevance computation algorithm and eliminate i(w_{2}) in S^{w_{1}} and i(w_{1}) in S^{w_{2}}. In both cases the conclusion D of p is included in the irrelevant part i(w_{2}) or i(w_{1}) and the par-link p is removed both in S^{w_{1}w_{2}} and in S^{w_{2}w_{1}}.

Definition 5. (cont.) (v) Let w_{1}, …, w_{n} be all the weakening-links in S. By Lemma 3 S^{w_{1},...,w_{n}} = S^{w_{σ(1)},...,w_{σ(n)}} for any permutation σ of 1, …, n. The irrelevant part I(S) of the proof-structure S is defined as S \ S^{w_{1},...,w_{n}}, where w_{1}, …, w_{n} are all the weakening-links of S. A proof-structure R is irrelevance free if R = R \ I(R). We write P(R) = R \ I(R) for the pruning operation given by the computation of irrelevance algorithm.

(vi) A proof-structure R for MAL + Mix is a proof-net modulo irrelevance if R \ I(R) is non-empty and R (without attachments) satisfies the acyclicity condition for all D-R graphs.

Remark. Notice that if S = P(R), then a canonical attachment a for S is given simply by a choice of a conclusion C to which we may attach all conclusions of S which are introduced by a weakening-link. Indeed all conclusions of a weakening-link which are premises of a par-link may be canonically attached to the other premise ℓ (which is not introduced by a weakening-link). Therefore if S has just one conclusion, there is only one canonical attachment a and we may omit mentioning it.

Theorem 3. There exists a ‘context-forgetting’ map ( )^{−} from sequent derivations in MAL + Mix to proof-nets with the following properties:

(i) Let d be a sequent derivation, and let R^{a} be the proof-net such that (d)^{−} = R^{a}. Then P(R^{a}) is non-empty (in fact, it contains at least one axiom and at least one conclusion); if d is in weakening normal form, then P(R) = R

(ii) (Sequentialization) If R is a proof-net modulo irrelevance, then there is a sequent calculus derivation d in weakening normal form such that P(R) = (d)^{−}.

Proof. (see [3] for the special case MAL without Mix.) (i) By induction on the length of d. (ii) In P(R) weakening-links can be given canonical attachments: as a consequence, the usual proof of sequentialization for MLL^{−} + Mix goes through without the detour used in the proof of Theorem 2 (ii).

Corollary. Provability in Constant-only MAL + Mix is in P.

Proof. In Constant-only MAL we may consider only proofs whose axioms are 1-axioms (a logical axiom can be replaced by a 1 axiom together with a ⊥-weakening). Thus to test whether ⊢ Γ is provable, we need only to check whether the proof-structure R which consists of the tree of subformulas of Γ is a proof-net modulo irrelevance. To decide this in linear time, apply the computation of irrelevance algorithm to R and check whether R ≠ I(R).

4.3 Examples and properties of irrelevance elimination

We need to justify our algorithm for the computation of irrelevance. For this purpose we recall some facts about the structure of subnets of proof-nets in MLL^{−} with Mix (cfr. [2]).

Definition 6. (i) A non-logical axiom in a proof-structure is a link with no premise and n conclusions, for some n. Danos-Regnier graphs for proofnets with non-logical axioms are defined as before and so is the notion of a proof-net with non-logical axioms for MAL + Mix (with attachment of weakening-link).

(ii) Let R^{a} be a proof-structure for MAL + Mix and let S be a substructure of R^{a} with conclusions C_{1}, …, C_{n}. The complementary substructure \overline{S} of S in R^{a} consists of all edges and links in R^{a} \ S with the addition of a non-logical axiom with conclusions C_{1}, … C_{n}.

(iii) Let R^{a} be a proof-net for MAL + Mix. A subnet S of R^{a} is a normal subnet if the complementary substructure \overline{S} of S in R^{a} is a proof-net with a non-logical axiom. A normal subnet S of R^{a} has the property that there exists a sequent calculus derivation d and a subderivation d_{0} of d such that (d)^{−} = R^{a} and (d_{o})^{−} = S.

(iv) Let R^{a} be a proof-net for MAL + Mix; let A be an edge and let v_{0} be a link in R^{a}. The kingdom kA [or the empire eA] of A in R^{a} is the smallest [the largest] normal subnet of R^{a} which has A as a conclusion. The kingdom kv_{0} [or the empire ev_{0}] of v_{0} in R^{a} is the smallest [the largest] normal subnet of R^{a} which has v_{0} as a lowermost link (so that the conclusions of v_{0} are all conclusions of R^{a}).

(v) The kingdom of A in R^{a} is the smallest set closed under the inductive conditions:

1. A ∈ kA;

2. If v is an axiom with conclusions X_{1}, …, X_{n}, then

kv = kX_{1} = … = kX_{n};

3. If v is a times-link with premises X, Y, then

kv = k(X ⊗ Y) = kX ∪ kY ∪ {X ⊗ Y };

4. If v is a par-link with premises X, Y, then

kv = k(X℘Y) = ⋃_{s} ⋃_{Z∈path_{s}(X,Y)} kZ ∪ {X℘Y },

where s ranges over all switchings of R.

(v) The empire of a link v in R^{a} is the smallest subnet of R^{a} containing the set of all links v′ such that for no switching s there is a path path_{s}(v, v′) reaching v “from below” (in the structural orientation).

Remarks. (i) The computation of irrelevance algorithm was presented first in section 7.5 of [3]. It is similar to Girard’s characterization of the empire of a formula in a proof-net for MLL^{−}, cfr. Facts 2.9.4 in [10]. More precisely, for any edge A in a proof-structure R write e^{−}A for the part of R satisfying Girard’s characterization. Now let w be any weakening-link in in a proof-structure R for MAL without attachments and let us introduce an attachment a(w) connecting w to some other edge. Then i(w) = e^{−}(a(w)), i.e., i(w) may be regarded as the result of applying Girard’s algorithm for the empire of the edge a(w). Notice that e^{−}(A) has different properties in MLL^{−} and in MLL^{−} + Mix. In MLL^{−} + Mix e^{−}A is a subnet, but not necessarily a normal subnet (cfr. [2] section 2.3), i.e., it may not be possible to find a sequentialization d of R such that e^{−}A corresponds to a subderivation of d; this remains true in the case of MAL + Mix as it is shown by the following examples.

(ii) Consider the following proof-net with conclusions (1℘B) ⊗ (1℘C), (C^{⊥}℘B^{⊥}) ⊗ A, 1, where the irrelevant part (marked with a solid broken line) is a subnet which is not normal:

Example 3.

A sequentialization of such a proof-net is the following derivation d:

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}⊢ 1 & ⊢ B, B^{⊥} \\ ⊢ 1, B, B^{⊥} \end{matrix} & Mix \\ ⊢ 1℘B, B^{⊥} \end{matrix} & \begin{matrix}\begin{matrix}⊢ 1 & ⊢ C, C^{⊥} \\ ⊢ 1, C, C^{⊥} \end{matrix} & Mix \\ ⊢ 1℘C, C^{⊥} \end{matrix} \\ ⊢ (1℘B) ⊗ (1℘C), C^{⊥}, B^{⊥} \end{matrix} ; ⊢ (1℘B) ⊗ (1℘C), C^{⊥}℘B^{⊥} & {⊢ 1 \atop ⊢ 1, A} \\ ⊢ (1℘B) ⊗ (1℘C), (C^{⊥}℘B^{⊥}) ⊗ A, 1 \end{matrix}

The proof-net obtained by pruning the irrelevant part is sequentialized in the following derivation, which is not obtainable from d by permutation of inferences:

\begin{matrix}\begin{matrix}{⊢ 1 \atop ⊢ 1, B} ; ⊢ 1℘B & {⊢ 1 \atop ⊢ 1, C} ; ⊢ 1℘C \\ ⊢ (1℘B) ⊗ (1℘C) \end{matrix} & {⊢ 1 \atop ⊢ (C^{⊥}℘B^{⊥}) ⊗ A, 1} \\ ⊢ (1℘B) ⊗ (1℘C), (C^{⊥}℘B^{⊥}) ⊗ A, 1 \end{matrix} Mix

(iii) Suppose irrelevance computation algorithm had been defined using the notion of kingdom: if the conclusion A℘B of a par-link is in i(w), then we should let k(A℘B) ⊂ i(w). We show that this procedure, regarded as a notion of reduction, does not have the Church-Rosser property. Consider the following proof-net with conclusions 1, X ⊗ (A^{⊥}℘B^{⊥}), (B℘C) ⊗ (A℘D^{⊥}), (D℘(G^{⊥}℘G)) ⊗ ((H℘H^{⊥})℘E), E^{⊥} ⊗ F, (F ℘C^{⊥}) ⊗ Y, 1.

Example 4.

(a) If we eliminate irrelevance starting from the weakening-link with conclusion X, then k(A^{⊥}℘B^{⊥}) is included in i(X) and pruned first, so the link (B℘C) ⊗ (A℘D^{⊥}) is removed. Next we proceed to the weakeninglink with conclusion Y, so k(F^{⊥}℘C^{⊥}) is pruned: but now the only links in it are the par-link itself, a weakening-link with conclusion C^{⊥} and an axiom \overline{F, F^{⊥}}. Finally we prune i(F) and we are left with a non-empty subnet with conclusions (D℘(G^{⊥}℘G)) ⊗ ((H℘H^{⊥})℘E), in addition to two 1 links (and weakening-links).

(b) If we eliminate irrelevance starting with i(Y) then k(F^{⊥}℘C^{⊥}) is pruned, and the times-links (B℘C) ⊗ (A℘D^{⊥}), (D℘(G^{⊥}℘G)) ⊗ ((H℘H^{⊥})℘E) and E^{⊥} ⊗ F are removed as they belong to k(F^{⊥}℘C^{⊥}). Therefore after pruning i(X) we are left with nothing else than two 1-links (and weakening-links).

Notice that our official computation of irrelevance algorithm yields in the more conservative pruning which is also given by (a).

4.4 Mix-elimination

Definition 7. Let R^{a_{0}}, S^{a_{1}} be proof-nets with attachments for weakeninglinks.

(i) A map φ : R → S preserves links (different from weakening-links) if it is a morphism of labelled directed graphs with respect to the links other than weakening-links. In other words, for every vertex v other than a weakeninglink in R, if v has incoming arrows labelled A_{1}, …, A_{m} and outgoing arrows labelled B_{1}, …, B_{n}, then φ(v) is a vertex of R′ with incoming arrows also labelled A_{1}, …, A_{m} and outgoing arrows also labelled B_{1}, …, B_{n}. However, φ may map a weakening-link to a link of another kind.

(ii) A one-to-one map of labelled graphs φ : R^{a} → S^{b} is an embedding if it preserves links and whenever a weakening link w of R^{a} has a non-canonical attachment a(w) = ℓ, then b(φ(w)) = φ(ℓ).

(iii) A covering of R^{a} is a set of embeddings φ_{i} : S_{i}^{a_{i}} → R^{a}, for i ≤ n, such that every edge in R is in the image of some φ_{i}.

(iv) The same definitions obviously apply to proof-nets without attachments.

We are going to define a procedure S that given a proof-net R^{a} for MAL + Mix generates a covering {φ_{i} : S_{i}^{a_{i}} → R^{a}}_{i≤n} (cfr. [14, 3]).

(I) Let C be a conclusion of R^{a}. We generate a data structure chain(C) as follows:

1. Select a link v with no premises such that v ≺ C and let path_{C,v} ⊂ chain(C);

i. if v is a logical axiom or a 1 axiom, then go to step (2);

ii. if v is a weakening-link w, then consider the edge ℓ which a(w) is attached to: if ℓ′ is the lowermost edge such that ℓ ⪯ ℓ′ and ℓ′ ∉ chain(C) then let path_{ℓ′,ℓ} ⊂ chain(C); finally, repeat step (1), choosing a link v′ with no premises such that v′ ≺ ℓ.

2. For every times-link or cut-link t in chain(C), select a link v with no premises such that v ≺ t and let path_{t,v} ⊂ chain(C); if v is a weakeninglink, then go to step (1.ii.);

3. For every logical axiom ax in chain(C), if B is a conclusion of ax which is not in chain(C), then let ℓ be the lowermost edge such that B ⪯ ℓ and ℓ ∉ chain(C) and let path_{ℓ,ax} ⊂ chain(C). Then return to step (2).

(II) We repeat this procedure making different choices at steps 1, 2, 3 and with different conclusions C′, until no new chain is generated. Let {chain_{1}^{a_{1}}, …, chain_{n}^{a_{n}}} be the chains eventually obtained, where a_{i} is the restriction of a to chain_{i}.

(III) For i ≤ n, we transform chain_{i} into a proof-structure S_{i}^{a_{i}} by adding weakening-links with canonical attachments:

• let p be a vertex in chain_{i} corresponding to a par-link of R such that one premise ℓ is in chain_{i}, but the other premises C is not: introduce a weakening-link w labelled C in chain_{i}, together with an attachment a_{i}(w) to the premise ℓ:

• let C′ be a conclusion of R which does not belong to chain_{i}: introduce a weakening-link w labelled C′ in chain_{i}, with an attachment a_{i}(w) to a selected conclusion C.

(IV) Let {S_{1}^{a_{1}}, …, S_{n}^{a_{n}}} be the data thus obtained. We denote by S the operation such that S(R) = {S_{1}^{a_{1}}, …, S_{n}^{a_{n}}}. Let F = {S_{1}^{a_{1}}, …, S_{n}^{a_{n}}}: we write P(F) = {P(S_{1}^{a_{1}}), …, P(S_{n}^{a_{n}})}.

Theorem 4. (i) Let R^{a} be a proof-net with conclusions Γ in MAL + Mix. The operation S(R) = {S_{1}^{a_{1}}, …, S_{n}^{a_{n}}} yields a covering {φ_{i} : S_{i}^{a_{i}} → R^{a}}_{i≤n}, where the S_{i}^{a_{i}} are proof-nets in MAL without Mix.

(ii) PS(R^{a}) = SP(R^{a}).

Proof. (i) Let R^{a} be a proof-net with conclusions Γ. Each S_{i} is a proofstructure: the inclusion map ι : S_{i} → R preserves times-links and cut-links by step (I.2.), axiom links by step (I.3.) and each S_{i}^{a_{i}} has conclusions Γ by step (III). Moreover ι : S_{i}^{a_{i}} → R^{a} is an embedding because the attachments a_{i} contain the restriction of a to chain_{i} and all other weakening-links have canonical attachments. Also by construction it is clear that every edge v in R^{a} is in the image of some φ_{i}. Therefore S(R) yields a covering.

Each S_{i}^{a_{i}} is a proof-net: a cyclic Danos-Regnier graph in S_{i}^{a_{i}} would be one in R. We need to show that S_{i}^{a_{i}} is a proof-net in MAL without Mix. The number of axioms, times-links and cut-links in S_{i}^{a_{i}} is determined by the procedure S, which after the first axiom selects an axiom for each times-link or cut-link encountered. Therefore by Lemma 1 any sequentialization of S_{i}^{a_{i}} is a derivation with no mix-rule.

(ii) Notice that SP(R^{a}) ⊂ S(R^{a}). Indeed the chains obtained by the procedure S applied to P(R^{a}) are also obtained by the procedure S applied to R^{a} starting with a conclusion C in P(R^{a}) and remaining in P(R^{a}) by selecting a logical axiom or a 1 axiom at steps (1) and (2) of the procedure; this is always possible since C ∈ P(R^{a}). The chains chain_{1}, …, chain_{k} obtained in this way will be called basic chains. Let SP(R) = {S_{1}^{a_{1}}, …, S_{k}^{a_{k}}}.

Furthermore notice that the procedure P applied to S(R^{a}) transforms chains into basic chains. Indeed computing and eliminating irrelevance from a link w considered at a step (I.ii.) has the effect of removing the part of the chain visited up to that step: but this would also have been achieved by starting with the conclusion C′ below ℓ′ and by selecting path_{C′,ℓ′} and so on. We conclude that P transforms S(R^{a}) into SP(R^{a}), and therefore PS(R^{a}) = SP(R^{a}).

Definition 8. Let R^{a} be a proof-structure for MAL + Mix such that R ≠ I(R). Let ax be an axiom of R^{a} and let R_{ax}^{a} be the result of replacing ax in R^{a} with two weakening-links if ax is a logical axiom or with one weakeninglink if ax is a 1 axiom. The set of axioms in R^{a} is minimal if for every ax in R^{a}, R_{ax} =I(R_{ax}).

We give a direct proof that the connectedness condition of all D-R graph is equivalent to the minimality condition on axioms. We need the following fact:

Fact: Given a proof-net with attachments R^{a} for MAL + Mix and any D-R switching s, any connected component of sR^{a} containing a weakeninglink w contains also an axiom of R^{a}, which is reached from w by crossing attachments and then always proceeding upwards in the structural orientation.

Proof. Let the attachment a(w) be connected to an edge ℓ_{1}; let S_{ℓ_{1}} be the smallest substructure ending with ℓ_{1} and consider the uppermost links in S_{ℓ_{1}} which are connected to ℓ_{1} in sR^{a}. If any such vertex is an axiom link, then we are done. Otherwise given a weakening-link w_{1}, let ℓ_{2} be the edge which a(w_{1}) is connected to, and consider the substructure ending with ℓ_{2}, and so on. In every case we proceed upwards in the structural orientation. Eventually we must reach an axiom.

Proposition 2. ([3], section 6). Let R^{a} be a proof-net for MAL + Mix. R^{a} be a proof-net for MAL without Mix if and only if its set of axioms is minimal. Thus the minimality condition on axioms is equivalent to the condition of connectedness of all D-R graphs.

Proof. Since R^{a} is a proof-net, by Theorem 3 I(R) ≠ R. Suppose sR^{a} is disconnected, for some switching s. If R^{a} consists of disconnected proofstructures, then the removal of an axiom in one substructure does not affect the computation of irrelevance in another disconnected substructure so R^{a} does not satisfy the minimality condition on axioms. If R^{a} as a proof-structure is connected, then we may assume that there are par-links p_{1}, … p_{k} such that their premises belong to different connected components of sR^{a}. Select a switching s_{1} so that if the D-R graph determined by s_{1} reaches a premise ℓ_{1} of p_{i} then s_{1} choses the other premise ℓ_{2} and a switching s_{2} which makes the opposite choices. Therefore the switchings s_{1} and s_{2} determine two connected components α and β of s_{1}S_{i}^{a_{i}} and s_{2}S_{i}^{a_{i}} respectively, where α and β contain different premises of the links p_{i}. It is easy to see that the removal of one axiom in α may at most make α irrelevant, but not β.

Conversely, if every D-R graph sR^{a} is connected, then R^{a}, as a proof-net with attachments, has properties similar to those of proof-nets for MLL^{−}, and it is easy to show by induction on the ordering of the kingdoms (cfr. Lemma 3 in [5]) that the removal of one axiom in R^{a} induces R^{a} = I(R^{a}).

Example 5.

Example 5 shows a proof-net R in MLL^{−} + Mix (top figure), representing a proof of

⊢ D℘C^{⊥}, C ⊗ (B^{⊥}℘(B℘A)), (A^{⊥}℘D^{⊥}) ⊗ E, E^{⊥},

together with S(R), namely, {S_{1}, S_{2}, S_{3}} (below, from left to right). Here:

• S_{1} is determined by the chain which starts either with D℘C^{⊥} or with (A^{⊥}℘D^{⊥}) ⊗ E and reaches the axioms \overline{D, D^{⊥}}, and \overline{E, E^{⊥}};

• S_{2} is determined by the chain which starts either with D℘C^{⊥} or with C ⊗ (B^{⊥}℘(B℘A)), reaches the axioms \overline{C^{⊥}, C} and chooses \overline{B^{⊥}, B};

• S_{2} is determined either (i) by the chain which starts with C⊗(B^{⊥}℘(B℘A)), reaches the axioms \overline{C^{⊥}, C} and \overline{E, E^{⊥}} after choosing \overline{A, A^{⊥}} or (ii) by the chain which starts with (A^{⊥}℘D^{⊥}) ⊗ E and reaches the axioms \overline{E, E^{⊥}},

\overline{A, A^{⊥}} and \overline{C^{⊥}, C}.

5 Cut-elimination modulo irrelevance

In this section we define a procedure of cut-elimination for proof-nets modulo irrelevance: this notion of reduction is based on a notion of weakeningexpansion which applies to the irrelevant part of a proof-net, but is not admissible in general. Therefore this notion of reduction does not extend to proof-nets with attachments of the weakening-links.

It is essential to notice that the notion of the irrelevant part of a proof-net is highly unstable under our notion of reduction: if R_{1} reduces to R_{2} and R_{2} reduces to R_{3}, it may very well be the case that I(R_{1}) ⊂ I(R_{2}) but also I(R_{2}) ⊃ I(R_{3}). Therefore in the cut-elimination process we will mark the irrelevant part of a proof-net, not remove it.

The cut-reduction for proof-nets modulo irrelevance for MAL + Mix are the same as those of MLL without units. In addition, there is the two weakenings / cut reduction which annihilates a cut-link whose premises are bot conclusions of weakening-links. Moreover there are the weakening-expansions:

• if a premise A ⊗ B [A^{⊥}℘B^{⊥}] of a cut-link is conclusion of a timeslink [par-link] and the other premise of the cut-link is conclusion of a weakening-link w, then w is replaced by a par-link [times-link] whose premises are conclusions of weakening-links w_{1} and w_{2}.

Theorem 5. (i) If R is a proof-net modulo irrelevance and R reduces to R′, then R′ is a proof-net modulo irrelevance.

(ii) The cut-elimination process for proof-nets modulo irrelevance for MAL + Mix has the strong normalization and Church-Rosser property.

Proof. (i) If sR is acyclic for every switching s, where there is no attachment for weakening links in R, then the usual argument for MLL^{−} + Mix shows that sR′ is acyclic for every switching s. If P(R) is non-empty, then P(R′) is non-empty by Lemma 4. (ii) Notice that if a cut-link occurs in R, then exactly one among the five reduction or expansions applies to it. Moreover, such operations are strictly local.

Lemma 4. Let R be a proof-net modulo irrelevance for MAL + Mix. If R reduces to R′, then P(R′) = R′ \ I(R′) is non-empty.

Proof of lemma 4. First notice that weakening-expansions cannot make any relevant part of the proof-net irrelevant. Also in a times /par reduction if one premise of the times-link is in the irrelevant part, then the cut-link itself is irrelevant, and similarly if both premises of the par-link are irrelevant. Consider a times /par reduction where the par-link with conclusion A^{⊥}℘B^{⊥} has one and only one irrelevant premise, e.g., B^{⊥} is conclusion of a weakening link w. Suppose both cut-links resulting from the reduction were irrelevant in R′. Since {A, A^{⊥}} ⊂ I(R′) but A, A^{⊥} ∉ I(R) it must be the case that by computing I(w) in R′ we reach either A or A^{⊥}. Now the algorithm for the computation of I(w) starts with B^{⊥}, the conclusion of w, and continues as in the computation of e^{−}(B): but since R′ is like R except for the local rewriting of the cut-link in question, it follows that not only in R′ but already in R we must have A ∈ e^{−}B or A^{⊥} ∈ e^{−}B. It is easy to show that for some switching s there exists a path path_{s}(A, B) or path_{s}(A^{⊥}, B) in sR. But this contradicts the acyclicity condition of the Danos-Regnier graphs for R.

Remark. Let R^{a} be a proof-net with attachments and suppose a weakeningexpansion is applied to R, yielding S with a new times-link: then there may be no system of attachments b such that S^{b} is a proof-net. This can be seen by Lemma 1: if R satisfies #ax = #⊗ + #cut +1 then in S the number of times-links is increased by one coeteris paribus. A stronger result would be to show that if S is the cut-free proof-structure resulting from cut-elimination, then there exists a system of attachments b such that S^{b} is a proof-net. We will not pursue the matter here.

Example 6.

Remark. Example 6 shows that the Church-Rosser property is lost if we erase the irrelevant part, instead of just marking it, during the cut-elimination process: e.g., after one reduction step, we would erase either e^{P} or e^{−}p^{⊥}. Notice that after two more steps, (an axiom reduction and a two weakenings / cut reduction) we obtain two disconnected proof-nets: therefore our cutelimination process essentially requires the use of the mix-rule.

6 Symmetric reductions require Mix

Can we define a symmetric reduction for proof-nets with contraction-links? An example in the Appendix B2 of Girard [11] shows that in order to do so we need the rule Mix. Let a and b atomic formulas and consider the proof-net π associated with a proof of ⊢ a∧b, a∧¬b, ¬b∧a, ¬a∧¬b, and the proof-net π′ to which π reduces as indicated in figure below.

Example 7.

The reduction above is the only one which has the following property of symmetry. Let a\¬a the substitution operation which replaces every edge a with an edge ¬a throughout the proof-net. Consider the group of substitutions S consisting of

{identity, a\¬a, b\¬b, a\¬a and b\¬b}

on the graphs π and π′. This group acts transitively on both π and π′; both π and π′ are invariant under the substitutions of S – under the assumption that axioms, cut-links and contraction-links are symmetric, i.e., not ordered.

It is easy to see that every asymmetric reduction, sending π to one of the connected components of π′, does not preserve the property of invariance under substitution. Therefore Girard’s example shows that there cannot be any symmetric cut-elimination for classical logic which does not use the rule Mix. It is also an easy exercise to see that (the proof-net translation of) the cross-cut reduction (as described in the intoduction) applied to the proof-net π yields a proof-net π′′ which is not invariant under some substitution. The problem of finding a proof-net representation for classical logic is therefore entirely open.

References

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

[2] G. Bellin. Subnets of proof-nets in multiplicative linear logic with Mix, Mathematical Structures in Computer Science, 1997, vol.7, pp.663-699.

[3] G. Bellin and J. Ketonen. A Decision Procedure Revisited: Notes on Direct Logic, Linear Logic and its Implementation, Theoretical Computer Science 95, 1992 n. 1, pp. 115-142.

[4] G. Bellin and P. J. Scott. Selected papers of the meeting on Mathematical Foundations of Programming Semantics (MFPS 92), Part 1 (Oxford 1992), Theoretical Computer Science 135, 1994 n. 1, pp. 11-65.

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

[6] C. Urban and G. M. Bierman. Strong Normalization of Cut-Elimination in Classical Logic, Fundamenta Informaticae XX, 2000, pp. 1-32.

[7] V. Danos, J-B. Joinet and H. Schellinx. LKQ and LKT: Sequent calculi for second order logic based upon linear decomposition of classical implication, 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. 211-224.

[8] V. Danos, J-B. Joinet and H. Schellinx. A new deconstructive logic: linear logic. Preprint n.52, Équipe de Logique Mathématique, Université Paris VII, Octobre 1994.

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

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

[11] J-Y. Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science (1991), vol. 1, pp. 255-296.

[12] J-Y. Girard. On the unity of logic. Annals of Pure and Applied Logic 59, 1993, pp.201-217.

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

[14] J.Ketonen and R.Weyhrauch. A Decidable Fragment of Predicate Calculus, Theoretical Computer Science 32, 1984 pp. 297-307.

[15] P. Lincoln and T. Winkler. Constant-only multiplicative linear logic is NPcomplete. Selected papers of the meeting on Mathematical Foundations of Programming Semantics (MFPS 92), Part 1 (Oxford 1992), Theoretical Computer Science 135, 1994 n. 1, pp. 155-169.

[16] M. Parigot. Free Deduction: an analysis of computation in classical logic. In Voronkov, A., editor, Russian Conference on Logic Programming, pp. 361-380. Sprinver Verlag. LNAI 592, 1991.

[17] M. Parigot. Strong normalization for second order classical natural deduction. in Logic in Computer Science, pp. 39-46. IEEE Computer Society Press. Proceedings of the Eight Annual Symposium LICS, Montréal, June 19-23, 1992.

[18] D. Prawitz. Natural deduction. A proof-theoretic study. Almquist and Wiksell, Stockholm, 1965.

[19] D. Prawitz. Ideas and Results in Proof Theory, in Proceedings of the Second Scandinavian Logic Symposium, ed. Fenstad, North-Holland, 1971.

[20] Edmund Robinson. Proof Nets for Classical Logic, preprint, Dagstuhl workshop 1141/1 on Semantic Foundations of Proof-search, April 2001.

http://www.dcs.qmw.ac.uk/ edmundr.

Gianluigi Bellin

Facoltà di Scienze  Department of Computer Science
Università di Verona  Queen Mary and Westfield College
Strada le Grazie  University of London
Ca’ Vignal 2  Mile End Road
37134 Verona - ITALY  London E1 4NS - UK

Email: bellin@sci.univr.it.  Email: bellin@dcs.qmw.ac.uk.