On Proof Normalization in Linear Logic^{∗}

Didier Galmiche and Guy Perrier

CRIN - CNRS & INRIA Lorraine Campus Scientifique - B.P. 239 54506 Vandœuvre-les-Nancy Cedex France e-mail: galmiche{perrier}@loria.fr

Abstract We present a proof-theoretic foundation for automated deduction in linear logic. At first, we systematically study the permutability properties of the inference rules in this logical framework and exploit these to introduce an appropriate notion of forward and backward movement of an inference in a proof. Then we discuss the naturally-arising question of the redundancy reduction and investigate the possibilities of proof normalization which depend on the proof search strategy and the fragment we consider. Thus, we can define the concept of normal proof that might be the basis of works about automatic proof construction and design of logic programming languages based on linear logic.

1 Introduction

Linear logic is a powerful and expressive logic with connections to a variety of topics in computer science. We are mainly interested by the significance it may have in different domains as logic programming or program synthesis through theorem proving. As a matter of fact, classical linear logic (denoted CLL) is a logic of actions introducing notions like controlled and strict resource management [12, 13]. It disallows both weakening and contraction in general although they are introduced for local use through modalities and it conserves a constructive character with a deep symmetry. Linear logic can be an appropriate framework to study logic programming (better than intuitionistic or classical logic) [3, 6, 16], concurrent aspects in logic programming [4, 18], Petri nets reachability [24]. The main point is the resource-sensitive aspect of this logic used, for example, for functional programming [19]. In previous works, we considered the synthesis of correct programs using a theorem proving approach in constructive logics with extraction of programs from proofs [8, 9]. Based on intuitionistic logics , they can present some limits due to the non-symmetrical character of such logics. But we could try to consider this approach in linear logic through an appropriate λ-calculus as logical language [1, 20]. In fact, the first point is to understand what a proof or a proof net is, in some fragments of linear logic, and also to be able to construct proofs of linear logic formulas. Hence, a theorem prover in linear logic can be a first step towards some effective applications of CLL based on the development of proofs like logic programming. For efficiency reasons, the construction of a linear logic prover imposes of course restrictions to an adequate fragment of CLL. Some recent works have been devoted to this important topic [14, 16]. Starting from the fragment of linear Horn clauses, they try to extend it in various following ways. The difficulty is then to extend the expressiveness of the language and to keep, at the same time, the efficiency of the initial kernel. Concerning efficiency criteria, we noticed that these works had a common point: the necessity to normalize, as much as possible, the proofs in these fragments, using some properties about inference permutability. Aiming also to extend logic programming, [2] has chosen another approach that consists in, starting from full linear logic, searching for equivalence between proofs in order to normalize them with the central notions of invertibility and focusing. In [27], we have a study about proof search strategies in CLL for a bottom-up direction with the same notions and also for a top-down direction based on specific resolution method. Even if, it is not the central point, permutability properties appears in these approaches. It is a classical concept in works on the conception of efficient proof search methods in non-classical logics [26, 29]. Thus, our approach begins with a systematical study of the inference permutability possibilities in full linear logic aiming to efficient proof construction mechanization. A first attempt in this direction has been developed in [10] where we have focused on the additive and multiplicative fragment of CLL and proposed an algorithm for automated deduction in this fragment. In this paper we completely refine the permutability notion and we extend the approach to full linear logic. Thus, after having systematically studied, the inference permutability properties, we define specific movements of inference in a proof and we analyze the redundancy reduction in a proof. Then, we are able to propose new proof forms (called normal proofs) that define complete and tractable proof subclasses and we discuss its interest for proof construction. Compared to other approaches on bottom-up and top-down theorem proving, we mainly focus on logical bases through a complete study of the inference permutabilities that could justify further choices of some fragments of CLL adequate for applications as logic programming. From this point, we should be in a position to study more seriously, in further work, the linear logic as a good framework for automated deduction, logic programming and also for the programming with proofs approach. We present in section 2 the linear logic framework (language and inference system) and recall some basic definitions. Section 3 shows a complete study of the permutability properties of inferences and, in section 4, we deal with the notion of movement of an inference in a proof. Section 5 presents how to reduce some redundancies in a proof by appropriate reduction and by cut elimination. Section 6 defines the notion of normal proof and to use it for the mechanization of proof construction in CLL in an adapted interpretor. In section 7, we emphasize the importance of this approach for designing logic programming languages in adequate fragments of linear logic. Finally, in section 8, we discuss the connections with related works in different fragments of CLL and then we conclude on the usefulness of these results for application embedding linear logic proofs development.

∗Theoretical Computer Science, vol. 135, n^{o} 1, pp 67-110, december 1994

2 Linear logic

Classical linear logic (CLL) has been introduced by Girard [12] as a logic of actions. Born from the semantics of second order lambda-calculus, linear logic is more expressive than traditional logics (classical or intuitionistic ones). Compared to classical logic, two structural rules weakening and contraction are dropped from the Gentzen-type rules and thus we obtain a system where each resource (hypothesis) must be used exactly once. Thus, conjunction and disjunction, that allow resource sharing, are split into a multiplicative version (⊗, ℘) disallowing resource sharing and an additive version (&, ⊕) requiring resource sharing. To restore power of classical logic two modal operators ! and ? are introduced knowing that !F allows unlimited consumption of F and ?F allows unlimited use of F. Moreover, the logical constants true, false are split into four constants 1, ⊥, 0 and ⊤ and an involutive negation (denoted (.)^{⊥}) is introduced. Characterized by the absence of structural rules and by a specific treatment of the negation, CLL has proofs that can be considered as actions and introduces a dynamical resource management in these proofs without directional character (no distinction between input and output). We refer the reader to [12, 13, 25, 28] for a broad explanation of the purpose and the meaning of linear logic.

2.1 The language

The language consists of

a) a set of finite terms T erm[V] on a countable set of variables V,

b) a countable set of atoms At each having an arity. It allows to construct a set Atom of atomic formulas: if n is the arity of the atom a and t_{1}, t_{2}, ..., t_{n} ∈ T erm[V] then a(t_{1}, t_{2}, ..., t_{n}) is an atomic formula,

c) a set of logical operators Op = {0, 1, ⊥, ⊤, ()^{⊥},!,?, ⊗, ℘, &, ⊕, ∀, ∃}. It allows to construct a set F orm of formulas that are the formulas of CLL, following the grammar

F ::= 0|1| ⊥ |⊤|A|F^{⊥}|?F |!F |F ⊗ F |F ℘F |F &F |F ⊕ F |∀xF |∃xF.

with A ∈ Atom and x ∈ V.

Here we manipulate sequents without left-hand sides, using the following notation conventions: variables ∈ V will be referred by the letters u, x, y, z, terms ∈ T erm[V] by the letters r, s, t, atoms ∈ At by the letters a, b, c, atomic formulas ∈ Atom by the letters A, B, C, formulas ∈ F orm by the letters F, G, H, multisets of formulas ∈ F orm by the letters Γ, Δ. Moreover, the letters can possibly be indexed by integers.

2.2 The linear sequent calculus

The inference system we use is the classical linear sequent calculus [12]. Let us recall that a sequent ⊢ F_{1}, ..., F_{n} is a finite multiset of formulas of F orm. Thus, we implicitly take into account the exchange rule and consider the commutative linear logic. We present now the inference rules of the linear sequent calculus.

1) \underline{Identity Group}

\overline{⊢ A, A^{⊥}} ax  \frac{⊢ F, Γ ⊢ F^{⊥}, Δ}{⊢ Γ, Δ} Cut

\frac{⊢ Δ}{⊢?F, Δ} w?  \frac{⊢?F,?F, Δ}{⊢?F, Δ} c?

\frac{⊢ F_{1}, Γ_{1} ⊢ F_{2}, Γ_{2}}{⊢ F_{1} ⊗ F_{2}, Γ_{1}, Γ_{2}} ⊗  \frac{⊢ F_{1}, F_{2}, Γ}{⊢ F_{1}℘ F_{2}, Γ} ℘

2) \underline{Structural Group} 3) \underline{Logical Group} ∘ Multiplicative rules

\overline{⊢ 1} 1  \frac{⊢ Γ}{⊢ ⊥, Γ} ⊥

∘ Additive rules

\frac{⊢ F_{1}, Γ ⊢ F_{2}, Γ}{⊢ F_{1}&F_{2}, Γ} &  \frac{⊢ F_{1}, Γ}{⊢ F_{1} ⊕ F_{2}, Γ} ⊕_{1}  \frac{⊢ F_{2}, Γ}{⊢ F_{1} ⊕ F_{2}, Γ} ⊕_{2}  \overline{⊢ ⊤, Δ} ⊤

∘ Exponential rules

\frac{⊢ F,?Γ}{⊢!F,?Γ} !  \frac{⊢ F, Γ}{⊢?F, Γ} ?

∘ Quantifiers rules

\frac{⊢ F [y/x], Γ}{⊢ ∀xF, Γ} ∀ \frac{⊢ F [t/x], Γ}{⊢ ∃xF, Γ} ∃

In the ∀ rule, y is not free in Γ and in F if y is different of x.

Let us remark that there is no rule for the constant 0 and that the linear negation, that is essential for the symmetrical character of CLL, is defined by the following equalities:

F^{⊥⊥} = F, 1^{⊥} =⊥, ⊥^{⊥} = 1, ⊤^{⊥} = 0, 0^{⊥} = ⊤,
(F ⊗ G)^{⊥} = F^{⊥}℘ G^{⊥} and (F ℘ G)^{⊥} = F^{⊥} ⊗ G^{⊥}.
(F &G)^{⊥} = F^{⊥} ⊕ G^{⊥} and (F ⊕ G)^{⊥} = F^{⊥}&G^{⊥}.
(∀xF)^{⊥} = ∃xF^{⊥} and (∃xF)^{⊥} = ∀xF^{⊥}.
(!F)^{⊥} =?F^{⊥} and (?F)^{⊥} =!F^{⊥}.

Remark 2.1 If we consider full linear logic, it is equivalent to work with sequents without lefthand side part (system called CLL) or with left-hand side part (system called CLL’). It is due to the property of the linear negation that allows to move a formula from one side to the other in a sequent, by changing it into its negation. We have chosen to work in CLL for simplification purposes but, for applications as logic programming, CLL’ presents some advantages: for example, it can be restricted without difficulty to a fragment of linear logic without negation. As a matter of fact, the translation of the results for CLL in CLL’ can be easily performed.

2.3 Derivations in CLL

Before proceeding further in our study, it is necessary to fix some vocabulary relatively to the notion of derivation and proof in CLL. Let us recall that an inference is an instance of a rule of the system defined above and the type of an inference I is the name of the corresponding rule, that is denoted by type(I) In a derivation, it will be necessary to follow the evolution of the formulas from the time when they are introduced (called principal) to the time when they are used, disappearing or becoming subformulas (called active). To take into account this evolution, it will be necessary to mark them in the derivations. We thus give the following definitions.

2.3.1 Principal and active formulas, contexts

Definition 2.1 A principal formula of an inference I, such that type(I) ≠ c?, is a formula of the conclusion that did not exist in the premises.

If type(I) = c? the principal formula is the result of the contraction of the two formulas in the premise.

Definition 2.2 The principal part of an inference I (denoted by Δ_{p}(I), Δ′_{p}(I), ...) is the multiset of its principal formulas.

Example 2.1 For the inference I_{1} ≡ \overline{⊢ A, A^{⊥}} we have Δ_{p}(I_{1}) = \{A, A^{⊥}\}.

For the inference I_{2} ≡ \frac{⊢ F, Δ ⊢ F^{⊥}, Δ′}{⊢ Δ, Δ′} we have Δ_{p}(I_{2}) = ∅.

Definition 2.3 An active formula of an inference I, such that type(I) ≠ c?, is a formula in a premise that does not exist in the conclusion. If type(I) = c?, I has two active formulas (?F,?F) that are the ones contracted in one formula (?F).

Definition 2.4 The active part of the i-th premise of an inference I (denoted by Δ_{a}^{i}(I)) is the multiset of its active formulas.

Example 2.2 Considering I ≡ \frac{⊢ F, G, Γ}{⊢ F ℘G, Γ} we have Δ_{a}^{1}(I) = \{F, G\}.

For I ≡ \frac{⊢ Γ}{⊢?F, Γ} we have Δ_{a}^{1}(I) = ∅.

Considering the inference I ≡ \frac{⊢ Γ_{1}, F ⊢ Γ_{2}, G}{⊢ Γ_{1}, Γ_{2}, F ⊗ G} we have Δ_{a}^{1}(I) = \{F \} and Δ_{a}^{2}(I) = \{G\}.

Definition 2.5 The context of an inference premise is the complement of its active part.

We can classify the inference rules in two categories: the ones depending on the context of the premises (those of the &, ! or ∀ type) and the others. It is due to the fact that the application of the rules &, ! or ∀ is possible under some conditions on the premise contexts. For &, the contexts of the two premises have to be identical, for ! the context of the premise has to be of the form ?Δ and for ∀ the variable y associated to the inference cannot be free in the premise context.

2.3.2 Marked derivations and proofs

We use the classical representation with binary trees labelled with sequents for defining the notions of derivation (or deduction) and proof [7]. Let us recall some definitions.

Definition 2.6 (i) An hypothesis of a derivation is a sequent labelling one of its leaves. (ii) An intermediate conclusion is a sequent that is not an hypothesis (i.e, not labelling a leave). (iii) The conclusion of a derivation is the sequent labelling the root of this tree. (iv) A proof in CLL is a derivation without hypotheses.

(v) A sequent ⊢ Δ is provable if there exists a proof with ⊢ Δ as conclusion.

It appears important to be able to follow the evolution of a formula in a proof and to do that we consider the marking of each of its inferences.

Definition 2.7 A marked inference is an inference with a function from the premises to the conclusion, that allows to identify formulas in the premises with formulas or sub-formulas in the conclusion. A marked proof is a proof where each inference is marked.

We can illustrate this notion with the following example

Example 2.3 In the case of ⊢ A,?A ⊕ F,?A, we can obtain two different marked proofs

\frac{\frac{\frac{\overline{⊢ A, A_{1}^{⊥}}}{⊢ A,?A_{1}^{⊥}}}{⊢ A,?A_{1}^{⊥},?A_{2}^{⊥}}}{⊢ A,?A_{1}^{⊥} ⊕ F,?A_{2}^{⊥}}  \frac{\frac{\frac{\overline{⊢ A, A_{1}^{⊥}}}{⊢ A,?A_{1}^{⊥}}}{⊢ A,?A_{1}^{⊥},?A_{2}^{⊥}}}{⊢ A,?A_{1}^{⊥},?A_{2}^{⊥} ⊕ F}

In general, the choice is neutral w.r.t. inference properties that we want to study. In the rest of the paper, even it is not explicit, we only consider marked proofs.

Definition 2.8 Let A be a formula of an intermediate conclusion of a proof Π of CLL, I an inference of Π, we say that A is introduced by I if A is a principal formula of I.

Definition 2.9 Let A be a formula of an intermediate conclusion of a proof Π of CLL, I an inference of Π, we say that A is actived in I if A is an active formula of I.

Remark 2.2 A formula can be introduced by several inferences. For example, let us consider the following CLL-proof

\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A ⊕ B, A^{⊥}} ⊕_{1}  \frac{\overline{⊢ B, B^{⊥}}}{⊢ A ⊕ B, B^{⊥}} ⊕_{2}}{⊢ A ⊕ B, A^{⊥}&B^{⊥}} &

The formula A ⊕ B of the conclusion is introduced by two inferences: one of type ⊕_{1} and one of type ⊕_{2}.

Hence, after this presentation of the logical framework we consider, we can now focus on the first important notion that is the permutability of inferences in a proof.

3 Inference permutability

We take as our point of conceptual departure the notion of inference permutability in full linear logic. It is a basic notion that appears to be very important for an efficient proof search (and theorem proving) in non-classical logics [26, 29]. We want to systematically study the possibilities we can obtain, from a given proof in CLL, other proofs by a simple permutation of two inferences that are consecutive in the proof tree. As an example, we take a proof where an inference of type & immediately precedes an inference of type ⊕_{1}. Let us consider the proof Π:

\frac{\frac{Π_{1} \{ \begin{matrix}: \\ ⊢ F, G, Δ \end{matrix}  Π_{2} \{ \begin{matrix}: \\ ⊢ F, H_{1}, Δ \end{matrix}}{⊢ F, G&H_{1}, Δ} &}{⊢ F ⊕ H_{2}, G&H_{1}, Δ} ⊕_{1}

From this form, we can easily deduce the following proof Π′

\frac{\frac{Π_{1} \{ \begin{matrix}: \\ ⊢ F, G, Δ \end{matrix}}{⊢ F ⊕ H_{2}, G, Δ} ⊕_{1}  \frac{Π_{2} \{ \begin{matrix}: \\ ⊢ F, H_{1}, Δ \end{matrix}}{⊢ F ⊕ H_{2}, H_{1}, Δ} ⊕_{1}}{⊢ F ⊕ H_{2}, G&H_{1}, Δ} &

This illustrates that the permutation between an inference of type & and an inference of type ⊕_{1} is always possible in one direction. The following counter-example shows that it is not possible in the other direction. Let us consider the proof

\frac{\frac{\frac{\overline{⊢ A, A^{⊥}} id \overline{⊢ B, B^{⊥}} id}{⊢ A ⊗ B, A^{⊥}, B^{⊥}} ⊗}{⊢ (A ⊗ B) ⊕ (C ⊗ B), A^{⊥}, B^{⊥}} ⊕_{1}  \frac{\frac{\overline{⊢ C, C^{⊥}} id \overline{⊢ B, B^{⊥}} id}{⊢ C ⊗ B, C^{⊥}, B^{⊥}} ⊗}{⊢ (A ⊗ B) ⊕ (C ⊗ B), C^{⊥}, B^{⊥}} ⊕_{2}}{⊢ (A ⊗ B) ⊕ (C ⊗ B), A^{⊥}&C^{⊥}, B^{⊥}} &

It is clear here that we cannot permutate the inferences of type ⊕_{1} and &. Thus, it seems interesting to see what happens for each pair of inference types and then to analyze the consequences of the permutability opportunities. Let us remark that, when two inferences are consecutive in a proof, it is not always relevant to consider their permutations. For example, if a principal formula of the first inference is active in the second inference then the order cannot be changed. Hence, the following appropriate definition

Definition 3.1 Let us consider a proof Π in CLL, we say that I_{1} and I_{2} two inferences of Π are in permutation position if they verify the conditions: (α) I_{2} follows directly I_{1} in Π (denoted by I_{1}\_{Π}I_{2}) , (β) the principal part in I_{1} is disjoint of the active part of j-th premise of I_{2} where it appears, i.e., Δ_{p}(I_{1}) ≠ Δ_{a}^{j}(I_{2}).

Intuitively, the notion of permutability is easy to understand. It means the possibility to invert two inferences in a proof without disturbing the rest of the proof (the parts below and above the inferences). In a previous work on deduction in the additive and multiplicative fragment of CLL [10], we have called it perfect-permutability (pp). Should one inference be of type &, there is some difficulty because of the duplication of the other inference (due to the duplication in the context). In [10] we have translated this variant by the notion of quasi-permutability (qp). But such definitions were rough and here we have refined them and embedded it in the following general definition.

Definition 3.2 Let us consider a proof Π in CLL, I_{1} and I_{2} inferences of Π being in permutation position, I_{1} is permutable with I_{2} in Π if there exists inferences I′_{1} and I′_{2} such that

(i) type(I′_{1}) = type(I_{1}) and type(I′_{2}) = type(I_{2}), (ii) the conclusion of I′_{2} coincides with a premise of I′_{1}, (iii) if type(I_{2}) = & and J_{1} is the other inference immediately preceding I_{2} in Π then type(J_{1}) = type(I_{1}). (iv) if type(I_{1})= & there exists an other inference J′_{2}, such that type(J′_{2}) = type(I_{2}) and the conclusion of which coincides with the second premise of I′_{1}.

(v) Let us consider the derivation (called permutation object) composed by I_{1} (and J_{1} if type(I_{2}) = &) followed by I_{2} and the derivation (called permutation result) composed by I′_{2} (and J′_{2} if type(I_{1})= &) followed by I′_{1}, both have the same conclusion and the same hypotheses modulo a duplication of some of them and a renaming of certain free variables. In the other cases, we say that I_{1} is not permutable with I_{2}.

Let us illustrate the definition with the example and the counter-example presented in the beginning of this section.

Example 3.1 Let us consider the previous proof, named Π, with

I_{1} = \frac{⊢ F, G, Δ ⊢ F, H_{1}, Δ}{⊢ F, G&H_{1}, Δ} & and I_{2} = \frac{⊢ F, G&H_{1}, Δ}{⊢ F ⊕ H_{2}, G&H_{1}, Δ} ⊕_{1}

I_{1} and I_{2} are in permutation position because conditions α and β (Definition 3.1) are satisfied, i.e., Δ_{p}(I_{1}) = {G&H_{1}} and Δ_{a}(I_{2}) = {F } are disjoint.

Let us consider I′_{1} = \frac{⊢ F ⊕ H_{2}, G, Δ ⊢ F ⊕ H_{2}, H_{1}, Δ}{⊢ F ⊕ H_{2}, G&H_{1}, Δ} & and I′_{2} = \frac{⊢ F, G, Δ}{⊢ F ⊕ H_{2}, G, Δ} ⊕_{1},

the conditions (i), (ii), (iii) (Definition 3.2) are satisfied.

Moreover, I_{1} being of type &, there exists J′_{2} = \frac{⊢ F, H, Δ}{⊢ F ⊕ H_{2}, H, Δ} ⊕_{1} that verifies the condition

(iv). The condition (v) is also easily satisfied and then I_{1} is permutable with I_{2}.

Example 3.2 Let us consider the previous proof denoted Π′ with

I_{1} = \frac{⊢ A ⊗ B, A^{⊥}, B^{⊥}}{⊢ (A ⊗ B) ⊕ (C ⊗ B), A^{⊥}, B^{⊥}} ⊕_{1}

I_{2} = \frac{⊢ (A ⊗ B) ⊕ (C ⊗ B), A^{⊥}, B^{⊥} ⊢ (A ⊗ B) ⊕ (C ⊗ B), C^{⊥}, B^{⊥}}{⊢ (A ⊗ B) ⊕ (C ⊗ B), A^{⊥}&C^{⊥}, B^{⊥}} &

I_{1} and I_{2} are in permutation position because conditions α and β (Definition 3.1) are verified, i.e., Δ_{p}(I_{1}) = {(A ⊗ B) ⊕ (C ⊗ D)} and Δ_{a}(I_{2}) = {A^{⊥}} are disjoint. But the condition (iii) is not verified and thus I_{1} is not permutable with I_{2}.

Definition 3.3 A proof Π′ is obtained by permutation of I_{1} with I_{2} in Π if it is obtained by replacing the permutation object relatively to I_{1} and I_{2} by the permutation result (modulo a renaming of free variables and duplication of tree branchs above the permutation object)

The operation of permutation of two inferences in a proof implies (because of its involutive character) an equivalence relation between proofs.

Definition 3.4 Let Π and Π′ be two proofs of CLL, Π′ is equivalent to Π modulo an inference permutation (denoted by Π′ ∼ Π) if there exists two inferences I_{1} and I_{2} in Π such that Π′ is obtained by permutation of I_{1} with I_{2} in Π.

Definition 3.5 Let Π and Π′ two proofs of CLL, Π′ is equivalent to Π modulo the inference order (denoted Π′ ∼^{∗} Π) if there exists a finite sequence Π_{1}, ..., Π_{n} of n proofs in CLL (n ≥ 1) such that (i) Π_{1} ≡ Π and Π_{n} ≡ Π′, (ii) for i ∈ [1, n − 1], Π_{i} ∼ Π_{i+1}.

Theorem 3.1 The relation ∼^{∗} is an equivalence relation

We will now systematically study the permutability properties of two inferences in a proof according to their types. Let us remark that the types ⊕_{1} and ⊕_{2} have the same properties and then we gather them into one denoted ⊕.

Theorem 3.2 (permutability theorem) Let t_{1} and t_{2} be two types of inference, in the following array,

(i) the case(t_{1}, t_{2}) in the following array contains p if and only if for any inferences I_{1} and I_{2} of type t_{1} and t_{2} being in permutation position in a proof Π, I_{1} is permutable with I_{2}. (ii) the case(t_{1}, t_{2}) contains np if and only if there exists two inferences I_{1} and I_{2} of type t_{1} and t_{2} being in permutation position in a proof Π, which are not permutable. (iii) the case(t_{1}, t_{2}) contains a cross × if and only if for any inferences I_{1} and I_{2} of type t_{1} and t_{2} in a proof Π, I_{1} is never in permutation position with I_{2}.

\begin{matrix}t_{2}\t_{1} & cut & ⊗ & ℘ & & & ⊕ & ? & w? & c? & ! & ∀ & ∃ & ⊥ \\ cut & p & p & p & p & p & p & p & p & np & p & p & p \\ ⊗ & p & p & p & p & p & p & p & p & np & p & p & p \\ ℘ & np & np & p & p & p & p & p & p & np & p & p & p \\ & & np & np & np^{∗} & np^{∗} & np & np & np & np^{∗} & np & np^{∗} & np & np^{∗} \\ ⊕ & p & p & p & p & p & p & p & p & np & p & p & p \\ ? & p & p & p & p & p & p & p & p & p & p & p & p \\ w? & p & p & p & p & p & p & p & p & p & p & p & p \\ c? & np & np & p & p & p & p & p & p & p & p & p & p \\ ! & np & × & × & × & × & np & p & p & × & × & × & × \\ ∀ & np & p & p & p & p & p & p & p & np & p & np & p \\ ∃ & p & p & p & p & p & p & p & p & np & p & p & p \\ ⊥ & p & p & p & p & p & p & p & p & np & p & p & p \end{matrix}

Proof 3.1 By case analysis according to the partition of the inference rules into two groups: the ones that depend on the context, i.e, of type &,!, ∀ and the other ones. The complete proof is given in the appendix A.

Let us remark that the np^{∗} in the line of & indicate that this non-permutability is relative to our definition but it can be overcome by a special treatment (see subsection 4.2). We can analyze the array presented in theorem 3.2, column by column. When a column, like the one of ℘, contains only one np, it means that we will be able to move forward (or down) an inference of type ℘ in a proof. By repetition of this elementary operation, we will move forward, as far as possible, such an inference. But two problems can stop such a movement: an inference of type & or an inference where the principal formula of the other one becomes active (the inferences are no more in permutation position). We can also analyze the array line by line. When a line, like the one of ? contains only p, it means that we will be able to move backward (or up) an inference of type ? in a proof. By repetition of this elementary operation, we will move backward, as far as possible, such an inference. The only problem that can stop such a movement is an inference introducing the active formula of the other (the inferences are no more in permutation position). This double analysis leads us to classify the inference types into two groups: the ones we can move backward and the others we can move forward as far as possible, in a proof. Now, we will study now in details these possible contradictory movements in a proof in full linear logic.

4 Inference movement in a LL proof

In this section, we define the notion of movement of an inference in a proof. We are mainly interested by movements on an inference towards the top of the proof (called backward or up movement) and towards the bottom of the proof (called forward or down movement).

4.1 Backward movement

Intuitively, it is an iteration of the movement of backward permutation of an inference in a proof. This movement can be complicated by the presence of an inference of type & that duplicates the inference in backward movement. Then, by such a movement, an inference can be duplicated the number of times it goes across inferences of type &. Taking this problem into account leads us to the following definition

Definition 4.1 Let Π be a proof of LL and I an inference of Π, a proof Π′ of LL is obtained by backward movement of I in Π if there exists a sequence Π_{0}, .., Π_{n} of proofs in LL and a sequence Inf_{0}, ..., Inf_{n} of inference sets such that

(i) for any i ∈ [0, n], Inf_{i} is an inference set of Π_{i} (inferences open to permutability), (ii) Π_{0} ≡ Π, Π_{n} ≡ Π′, Inf_{0} ≡ {I}, (iii) for any i ∈ [0, n − 1], Π_{i+1} is obtained from Π_{i} by permutation of an inference I_{i}^{1} with an inference I_{i}^{2} of Inf_{i}. I_{i}^{′1} and I_{i}^{′2} (and possibly J_{i}^{′2}) being the corresponding inferences of Π_{i+1} then Inf_{i+1} is the union of the inferences of Π_{i+1} in Inf_{i} and of I_{i}^{′2} (and possibly J_{i}^{′2}). Inf_{n} is called the inference set of Π′ resulting of the backward movement of I in Π.

Let us illustrate this definition by an example.

Example 4.1 Let us consider the proof Π_{0} of LL

\frac{\frac{\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A ⊕ B, A^{⊥}} ⊕_{1} \frac{\overline{⊢ B, B^{⊥}}}{⊢ A ⊕ B, B^{⊥}} ⊕_{2}}{⊢ A ⊕ B, A^{⊥}&B^{⊥}} & \overline{⊢ C, C^{⊥}}}{⊢ (A ⊕ B) ⊗ C, A^{⊥}&B^{⊥}, C^{⊥}}  ⊗}{⊢ (A ⊕ B) ⊗ C, A^{⊥}&B^{⊥}, C^{⊥},?C} w?

we can obtained by backward movement of w? in Π_{0} the following proof Π_{3}

\frac{\frac{\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A, A^{⊥},?C} w?}{⊢ A ⊕ B, A^{⊥},?C} ⊕_{1} \frac{\frac{\overline{⊢ B, B^{⊥}}}{⊢ B, B^{⊥},?C} w?}{⊢ A ⊕ B, B^{⊥},?C} ⊕_{2}}{⊢ A ⊕ B, A^{⊥}&B^{⊥},?C} & \overline{⊢ C, C^{⊥}}}{⊢ (A ⊕ B) ⊗ C, A^{⊥}&B^{⊥}, C^{⊥},?C}  ⊗

We observe that the inference w? get over an inference of type & by backward movement in Π_{0}, with its duplication as main effect and then the inference set of Π_{3} resulting of the movement of w? consists of two inferences w?.

Let us consider again the array of theorem 3.2, line by line, to see which inference types are well adapted to the backward movement. After a first analysis, it seems to be cut, ⊗, ⊕,?, w?, ∃, ⊥, but the last one can also be adequate for forward movement, as we will notice it after. Concerning the inference of type w?, by the theorem 3.2, there is no problem for backward movement of such inference. Moreover, it does not need an active formula and it is always in permutation position with the inferences that precede it immediately. So we can move it backward up to the axioms. This is illustrated by the above example and expressed by the following theorem

Theorem 4.1 (backward movement of w?) Let Π be a proof in LL and I an inference of Π of the w? type, there exists a proof Π′ obtained by backward movement of I in Π such that any inference I’ of Π′ resulting of this movement is immediately preceded by an axiom.

Proof 4.1 By induction on h (h ≥ 1), height of Π_{1}, subtree of Π with I’s premise as root.

• h = 1. I is immediately preceded by an axiom in Π and then we can consider Π′ ≡ Π.

• Let us assume the property true for a height h (≥ 1) and prove it for h + 1. Let us consider a proof Π and an inference I of Π of w? type such that the subproof tree Π_{1}, having the premise of I as root, is of height h+1, the inference I_{1} that immediately precedes I in Π, is not an axiom because h + 1 ≥ 2. Moreover, I has no active formula and then I_{1} is in permutation position with I and is permutable with it by theorem 3.2.

1) \underline{type(I_{1}) ≠ &} Let Π′′ be the proof obtained by permutation of I_{1} with I in Π and I′′ the inference of Π′′ corresponding to I, the subproof tree Π′′_{1} of Π′′, having I′′ as root, has the height h and thus we can apply the induction hypothesis to it. Then, there exists a proof Π′ obtained by backward movement of I′′ in Π′′ such that any inference I′ of Π′, resulting from this movement, is immediately preceded by an axiom. By the composition of this backward movement with the permutation that transforms Π into Π′, we obtain a backward movement that leads from Π to Π′. Thus, the property is true for h+1.

2) \underline{type(I_{1}) = &} This case is similar to the previous one except that I is split by the permutation into two inferences I′′ and J′′ and thus we have to apply the induction hypothesis twice.

Concerning the type ?, the only difference with the previous one is that each inference of the ? type contains an active formula and its backward movement is stopped by the inferences introducing this active formula. We have the following result

Theorem 4.2 (backward movement of ?) Let Π be a proof in LL and I an inference of Π of the ? type, there exists a proof Π′ obtained by backward movement of I in Π such that any inference I’ of Π′ resulting of this movement is immediately preceded by an inference introducing the active formula of I’.

Proof 4.2 The proof is similar to the Theorem 4.1 proof.

Apparently, by theorem 3.2, the backward movement of a cut inference can be hold up by an inference of type !. But, as shown by the example below, this problem can be solved and the cut inference has the same behavior than the ? inference and consequently it leads to an analogous result.

Example 4.2 Let us consider an example of backward movement of a cut inference in the following proof Π_{0}

\frac{\frac{\frac{\frac{\overline{⊢ B, B^{⊥}}}{⊢ B,?B^{⊥}} ?}{⊢ B,?B^{⊥},?A^{⊥}} w?}{⊢!B,?B^{⊥},?A^{⊥}} ! \frac{\frac{\frac{\overline{A, A^{⊥}}}{⊢ A,?A^{⊥}} ?}{⊢!A,?A^{⊥}} ! \overline{⊢ B, B^{⊥}}}{⊢!A, (?A^{⊥}) ⊗ B, B^{⊥}}  ⊗}{⊢!B,?B^{⊥}, (?A^{⊥}) ⊗ B, B^{⊥}} cut

We cannot permute the cut inference with the ! inference on the left-hand side, whereas the permutation is possible with the inference of type ⊗. By such a movement we obtain the proof Π_{1}

\frac{\frac{\frac{\frac{\frac{\overline{⊢ B, B^{⊥}}}{⊢ B,?B^{⊥}} ?}{⊢ B,?B^{⊥},?A^{⊥}} w?}{⊢!B,?B^{⊥},?A^{⊥}} !  \frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A,?A^{⊥}} ?}{⊢!A,?A^{⊥}} !}{⊢!B,?B^{⊥},?A^{⊥}} cut  \overline{⊢ B, B^{⊥}}}{⊢!B,?B^{⊥}, (?A^{⊥}) ⊗ B, B^{⊥}}  ⊗

The permutation of the cut inference with the ! inference in left-hand side is now possible and we obtain the proof Π_{2}

\frac{\frac{\frac{\frac{\frac{\overline{⊢ B, B^{⊥}}}{⊢ B,?B^{⊥}} ?}{⊢ B,?B^{⊥},?A} w?  \frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A,?A^{⊥}} ?}{⊢!A,?A^{⊥}} !}{⊢ B,?B^{⊥},?A^{⊥}} cut}{⊢!B,?B^{⊥},?A^{⊥}} !  \overline{⊢ B, B^{⊥}}}{⊢!B,?B^{⊥}, (?A^{⊥}) ⊗ B, B^{⊥}}  ⊗

At this time, the movement stops because the cut inference is no longer in permutation position with its immediate predecessors.

Theorem 4.3 (backward movement of cut) Let Π be a proof in LL and I an inference of Π of the cut type, there exists a proof Π′ obtained by backward movement of I in Π such that for any inference I’ of Π′ resulting of this movement, the inferences preceding immediately I’ introduce its active formulas.

Proof 4.3 By induction on the number n of inferences preceding I in Π.

• n = 0. There is no proof Π where I is not preceded by an inference and thus the property is true.

• Let us assume the property true until any order n and prove that it is true for n+1. Let us consider a proof Π and I an inference of type cut preceded by n+1 inferences in Π,

1) \underline{One inference immediately preceding I is not of the ! type and does not introduce an active} \underline{formula of I}. Let I_{1} such an inference, by theorem 3.2, we can permute I_{1} with I to obtain a proof Π′′ where the inferences corresponding to I are preceded by n inferences. Thus, we can apply the induction hypothesis and we obtain by backward movement of these inferences in Π′′ a proof Π′ verifying the given criteria. By composition of these movements with the permutation leading from Π to Π′′ we obtain a backward movement from Π to Π′.

2) \underline{The inferences immediately preceding I are of type ! or introduce an active formula of I}. 2.1) The inferences immediately preceding I introduce the active formulas of I. In this case the proof Π′ we search is Π. 2.2) One inference immediately preceding I is of type ! and does not introduce an active formula of I.

Let I_{1} be such an inference being of the form \frac{⊢?F, G,?Δ_{n}}{⊢?F,!G,?Δ_{n}} where ?F is active in I, the other

inference preceding immediately I contains !F^{⊥} in this conclusion and necessarily introduces !F^{⊥}. Then Π has the following form

\frac{\frac{⊢?F, G,?Δ_{n}}{⊢?F,!G,?Δ_{n}} ! \frac{⊢ F^{⊥},?Δ′_{n}}{⊢!F^{⊥},?Δ′_{n}} !}{⊢!G,?Δ_{n},?Δ′_{n}} cut

We can then permute I_{1} with I to obtain the proof

\frac{\frac{⊢?F, G,?Δ_{n} \frac{⊢ F^{⊥},?Δ′_{n}}{⊢!F^{⊥},?Δ′_{n}} !}{⊢ G,?Δ_{n},?Δ′_{n}} cut}{⊢!G,?Δ_{n},?Δ′_{n}} !

There are n inferences preceding the new cut and then we can apply the induction hypothesis to them and go on as in the case 1).

Concerning the types ⊗, ⊕ and ∃, the potential obstacle of the inferences of type ! cannot be bypassed as for the cuts. This point is illustrated in the following example.

Example 4.3 Let us consider a backward movement of ⊗ in the following proof Π_{0}

\frac{\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A℘A^{⊥}} ℘}{⊢ A℘A^{⊥},?B} w? \frac{\frac{\overline{⊢ C, C^{⊥}}}{⊢ C,?C^{⊥}} ?}{⊢!C,?C^{⊥}} !}{⊢ (A℘A^{⊥})⊗?C^{⊥},!C,?B} ⊗

we obtain by permutation of w? with ⊗ the proof Π_{1}

\frac{\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A℘A^{⊥}} ℘ \frac{\frac{\overline{⊢ C, C^{⊥}}}{⊢ C,?C^{⊥}} ?}{⊢!C,?C^{⊥}} !}{⊢ (A℘A^{⊥})⊗?C^{⊥},!C} ⊗}{⊢ (A℘A^{⊥})⊗?C^{⊥},!C,?B} w?

The permutation of ⊗ with ! is not possible and the backward movement stops at this step.

Theorem 4.4 (backward movement of ⊗, ⊕, ∃) Let Π be a proof in LL and I an inference of Π of type ⊗, ⊕ or ∃, there exists a proof Π′ obtained by backward movement of I in Π, such that any inference I’ of Π′ resulting of this movement is immediately preceded by an inference that introduces an active formula of I′ or by an inference of ! type.

Proof 4.4 The proof has the same scheme as in the case of weakening.

It is also possible to move backward (or up) the inferences of ! type in a proof. But, taking into account the particular behaviour of the ! rule, this movement is not possible by successive permutations but only possibly by jumps from an intermediate conclusion of the form ⊢ F,?Δ to another one of the form ⊢ F,?Δ′, if we do not have & in the fragment we consider.

4.2 Forward movement

Intuitively, it is an iteration of the forward movement of an inference that permutes with another in a proof. This movement can be complicated by the meeting, during this process, of an inference of type & with a contrary effect as for backward movement. Then, by such a movement, the inference is not duplicated but merged with another one that provides from the other branch of the proof tree. Thus, starting from a set of inferences, we terminate the movement with only one inference. That is the reason why the forward movement notion is defined by duality from the backward movement.

Definition 4.2 Let Π be a proof of LL and I an inference of Π, a proof Π′ of LL is obtained by forward movement of I in Π if there exists an inference I′ of Π′ such that Π is obtained by backward movement of I′ in Π′ and I is one of the resulting inferences. I′, that is unique, is called the inference resulting of the forward movement of I in Π.

Let us illustrate this definition by an example

Example 4.4 Let us consider a forward movement of ∀ in a proof. Let Π_{0} be the proof

\frac{\frac{\frac{\frac{\frac{\overline{⊢ a(x), a(x)^{⊥}}}{∃ya(y), a(x)^{⊥}} ∃}{⊢ ∃ya(y), ∀za(z)^{⊥}} ∀ \overline{⊢ B, B^{⊥}}}{⊢ (∃ya(y)) ⊗ B, ∀za(z)^{⊥}, B^{⊥}}  ⊗}{⊢ (∃ya(y)) ⊗ B, ∀za(z)^{⊥}, (B^{⊥} ⊕ c(x))} ⊕_{1}}{⊢ (∃ya(y)) ⊗ B, (∀za(z)^{⊥})℘(B^{⊥} ⊕ c(x))} ℘

By permutation of ⊗ and ∀ we obtain the proof Π_{1}

\frac{\frac{\frac{\frac{\frac{\overline{⊢ a(x), a(x)^{⊥}}}{⊢ ∃ya(y), a(x)^{⊥}} ∃ \overline{⊢ B, B^{⊥}}}{⊢ (∃ya(y)) ⊗ B, a(x)^{⊥}, B^{⊥}}  ⊗}{⊢ (∃ya(y)) ⊗ B, ∀za(z)^{⊥}, B^{⊥}} ∀}{⊢ (∃ya(y)) ⊗ B, ∀za(z)^{⊥}, (B^{⊥} ⊕ c(x))} ⊕_{1}}{⊢ (∃ya(y)) ⊗ B, (∀za(z)^{⊥})℘(B^{⊥} ⊕ c(x))} ℘

By permutation of ⊕_{1} and ∀ we obtain the proof Π_{2}. The permutation implies the renaming of the variable x in the subtree having the conclusion of ⊗ as root.

\frac{\frac{\frac{\frac{\frac{\overline{⊢ a(u), a(u)^{⊥}}}{⊢ ∃ya(y), a(u)^{⊥}} ∃ \overline{⊢ B, B^{⊥}}}{⊢ (∃ya(y)) ⊗ B, a(u)^{⊥}, B^{⊥}}  ⊗}{⊢ (∃ya(y)) ⊗ B, a(u)^{⊥}, B^{⊥} ⊕ c(x)} ⊕_{1}}{⊢ (∃ya(y)) ⊗ B, ∀za(z)^{⊥}, (B^{⊥} ⊕ c(x))} ∀}{⊢ (∃ya(y)) ⊗ B, (∀za(z)^{⊥})℘(B^{⊥} ⊕ c(x))} ℘

Let us consider again the array of theorem 3.2, column by column, to see which inference types are well adapted to the forward movement. The result is that ,after analysis, the adequate inferences are ℘, &, c?, ∀, ⊥. On the contrary of what happens for the case of backward movement, they all have the same behavior (or almost, because of c? we are obliged to extend the notion of permutability of two inferences). Then we have only one theorem, illustrated by the above example. Apparently, the inferences of type w? and ⊕ could rank also among this category but we shall see at the end of the proof 4.5. why it is false.

Theorem 4.5 (forward movement of ℘, &, c?, ∀, ⊥) Let Π be a proof in LL and I an inference of Π of type ℘, &, c?, ∀, ⊥, there exists a proof Π′ obtained by forward movement of I in Π such that the inference I’ of Π′ resulting of this movement is either the last inference of Π′ or is followed by an inference with the principal formula of I as the active formula.

Proof 4.5 By structural induction on Π. We can restrict this proof to a proof Π where the principal formula of I is not active afterwards (it is then in the conclusion of Π) without loosing generality. Let us denote I_{l} the last inference of Π.

1) \underline{I ≡ I_{l}} The proof Π′ is equal to Π.

2) \underline{I ≢ I_{l}} 2.1) \underline{type(I_{l}) ≠ &}. We apply the induction hypothesis to the subproof Π_{1} of the premise of I_{l} that contains the principal formula of I. By forward movement of I in Π_{1} we obtain a proof Π′_{1} ending with an inference I′_{1} resulting of this movement. Let us replace Π_{1} by Π′_{1} in Π, by theorem 3.2, I′_{1} is permutable with I_{l} and we obtain the proof Π′ through this permutation.

2.2) \underline{type(I_{l}) = &}. Let F be the principal formula of I, Π has the following form:

\frac{Π_{1} \{ \begin{matrix}: \\ ⊢ F, G, Δ \end{matrix} Π_{2} \{ \begin{matrix}: \\ ⊢ F, H, Δ \end{matrix}}{⊢ F, G&H, Δ}

Let us assume, for example, that I is an inference of Π_{1} and let J be the inference of Π_{2} introducing F, we distinguish two cases, according to the relationship between the type of J and the type of I. α) \underline{F ≢?F′}. In this case, I and J have the same type and we apply the induction hypothesis to Π_{1} with I and to Π_{2} with J. By forward movement of I in Π_{1} we obtain a proof Π′_{1} ending with an inference I_{1} resulting from this movement. In the same way, by forward movement of J in Π_{2} we obtain a proof Π′_{2} ending with an inference J_{1} resulting from this movement. By replacing Π_{1} and Π_{2} by Π′_{1} and Π′_{2} respectively in Π and then by permutation of I_{1} with I_{l} we obtain the proof Π′. β) \underline{F ≡?F′}. In this case, we apply the induction hypothesis on Π_{1}. By forward movement of I in Π_{1}, we obtain a proof Π′_{1} ending with an inference I_{1}, resulting from this movement, that is necessarily of c? type. Let us replace Π_{1} by Π′_{1} in Π to obtain the following proof

\frac{Π′_{1} \{ \frac{\begin{matrix}: \\ ⊢?F′,?F′, G, Δ \end{matrix} \} Π′′_{1}}{⊢?F′, G, Δ} c?  \begin{matrix}: \\ ⊢?F′, H, Δ \end{matrix} \} Π_{2}}{⊢?F′, G&H, Δ} &

By introducing an inference of type w? at the end of Π_{2}, we can then permute I_{1} with I_{l} to obtain the proof Π′ (it implies an extension of the permutability notion but it is not a problem).

\frac{\frac{Π′′_{1} \{ \begin{matrix}: \\ ⊢?F′,?F′, G, Δ \end{matrix}  \frac{\begin{matrix}: \\ ⊢?F′, H, Δ \end{matrix} \} Π_{2}}{⊢?F′,?F′, H, Δ} w?}{⊢?F′,?F′, G&H, Δ} &}{⊢?F′, G&H, Δ} c?

Remark 4.1 The following counter-examples illustrate well why the previous theorem can not be applied to the inferences of type ⊕ or w?.

\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A, A^{⊥} ⊕ B^{⊥}} ⊕_{1} \frac{\overline{⊢ B, B^{⊥}}}{⊢ B, A^{⊥} ⊕ B^{⊥}} ⊕_{2}}{⊢ A&B, A^{⊥} ⊕ B^{⊥}} &  \frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢?A, A^{⊥}} ? \frac{\overline{⊢ 1}}{⊢?A, 1} w?}{⊢?A, A^{⊥}&1} &

Concerning the inferences of type !, it seems difficult to move forward such inferences in a proof. It is true when we try to move it by successive permutations. But the ! inferences have the specific property, under some conditions, to be able to disappear in some points of a proof to appear again much further forward. It is pointed out in the following theorem Theorem 4.6 (forward jump of !) If a sequent of the form ⊢!F,?Δ is provable then there exists a proof of this sequent which ends with the inference introducing !F.

Proof 4.6 If a sequent of the form ⊢!F,?Δ is provable and Π is a proof of it, we can modify it in the following way. At first, we replace, by starting from the final conclusion in all intermediate conclusions, the formula !F by F to the inferences which introduce it and we delete these

inferences. Next, we add the following inference \frac{⊢ F,?Δ}{⊢!F,?Δ} at the end of the proof.

It is clear that the resulting tree is definitely the proof we search.

A consequence of this theorem is a possibility of forward jump of ! in a proof.

Remark 4.2 If we consider the inference types, we observe that we have different groups of inferences with respect to the permutability properties and the movement of an inference in a proof. We have two principal groups of inference types that are the ones to move down and the ones to move up. Let us remark that the partition between the both groups depends on the proof search direction (bottom-up or top-down) we choose, as we will see in section 6. Moreover, they correspond to the groups of connectives obtained by partition in [2] with respect to a notion of synchronization and determinism. But there are differences concerning the treatment of ? and !. The connective ?, considered as asynchronous by Andreoli [2], corresponds in our work to the three rules c?, w? and ? that behave differently. ! that is member of the group of synchronous connectives is moved forward in our work. Our own classification is based only on permutability properties in the framework and on their logical consequences. That is the reason why we do not tell about the constants 0, 1 and ⊤ that are produced by axioms.

5 Redundancy reduction

The study of the forward and backward movement in the CLL proofs provides through the previous results and theorems tools to order the inferences inside a proof with a view to giving what can be called a normal form. Before defining this notion, let us treat a question that is strongly connected to this objective: how can we eliminate some reasons of redundancy in a proof ?

Definition 5.1 A proof of CLL is redundant if two of its consecutive intermediate conclusions are identical.

If, from a given proof, it is easy to construct an equivalent one which is not redundant, it is more difficult to construct directly, from a given sequent, a non-redundant proof (without needing to check it a posteriori).

5.1 Cut elimination

The cut rule is one of the reasons for redundancy. If the theorem 4.3. motivates the backward movement of cut inferences in a proof then it does not eliminate them. Let us consider this result on cut elimination as an extension of this theorem. Considering a proof of CLL, a cut can be moved backward up to the inferences introducing its active formulae. These ones have dual types and then we can move it again of one step. After this, we can apply again the theorem and so on... But how can we be sure that this process terminates ? Neither the height of the successive proofs nor the inference number decreases systematically during this process. Thus it is necessary to define an appropriate new decreasing function presented below, which is possible with the notion of complexity of cuts in a proof.

5.1.1 Complexity of cuts in a proof

Definition 5.2 (formula complexity) Let Π be a proof of CLL and F a formula occurrence in the conclusion of an inference I of Π, the complexity of the formula F the integer c(F) is defined inductively by:

- if F ∈ Δ_{p}(I) and if type(I) ∈ {ax, w?, ⊥} then c(F) = 1.

- if F ∈ Δ_{p}(I) and if Δ_{a}(I) ≠ ∅ then c(F) = 1 + max{c(G), G ∈ Δ_{a}(I)}.

- if F ∉ Δ_{p}(I) then c(F) = max{c(F′), F′ premise of I and F ≡ F′}.

Definition 5.3 (cut complexity) Let Π a proof of CLL and I a cut inference in Π the active formulae of which being F and F^{⊥}, the complexity of the cut I is the integer defined by c(I) = c(F) + c(F^{⊥}).

Until now, these definitions do not present difficulties, but the next one is more subtle. If we define the complexity of the cuts in a proof as the maximum of the complexity of its different cuts, it can be very difficult to prove that we can decrease this complexity. The reduction of the complexity of a particular cut could imply the increasing of another cut, being above. That motivates the following definition

Definition 5.4 (cuts complexity in a proof) Let Π be a CLL proof, the complexity of the cuts of Π is the integer c(Π) that is equal to zero if Π has no cuts and to the maximum of the complexities of cuts \underline{that are not preceded by another one}.

5.1.2 Cut elimination

Theorem 5.1 (complexity reduction) Let Π be a proof in CLL of a sequent ⊢ Δ with only one cut, there exists a proof Π′ of ⊢ Δ such that c(Π′) < c(Π).

Proof 5.1 The complete proof is given in appendix B.

The cut elimination theorem is a direct consequence of the theorem 5.1, but its proof uses a particular strategy of cut reduction and thus our theorem is a theorem of weak normalization knowing that strong normalization is verified for linear logic [12].

Theorem 5.2 (cut elimination) If ⊢ Δ is a provable sequent of CLL then there exists a proof of ⊢ Δ without cuts.

Proof 5.2 Let Π be a proof of CLL, for n ∈ [0, c(Π)] we have the property P(n): there exists a proof Π_{n} with the same conclusion as Π such that c(Π_{n}) = c(Π) − n. This property is an immediate consequence of the theorem 5.2. It is sufficient then to apply P (c(Π)).

Theorem 5.3 (of subformula) Let Π be a CLL proof without cuts and ⊢ Δ its conclusion, for any intermediate conclusion ⊢ Δ′ of Π, a formula of ⊢ Δ′ is a subformula of ⊢ Δ.

Proof 5.3 By induction on h, height of ⊢ Δ′ in Π.

• h = 0. In this case ⊢ Δ′ is ⊢ Δ and the property is true.

• Let us assume the property true for any order h and show that it is true for h+1. Let ⊢ Δ′ be an intermediate conclusion of Π being at the height h+1, it is a premise of an inference I the conclusion of which is at height h. Let F be a formula of ⊢ Δ′, I is not a cut and then there exists a formula F′ of a sequent ⊢ Δ′′ such that F is a subformula of F′ (extending the subformula notion for ∃ and ∀). ⊢ Δ′′ being at height h in Π , the induction hypothesis is applied to it and F′ is a subformula of a formula F′′ of ⊢ Δ. Then, by transitivity, we deduce that F is a subformula of F′′.

Let us recall that this theorem of sub-formula is naturally the basis of proof search methods in bottom-up approaches but also in top-down approaches.

5.2 Weakening and contraction reduction

The cuts often generate redundancy in a proof but it is not the only reason. For example, the following proof

\frac{\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢?A, A^{⊥}}}{⊢?A,?A, A^{⊥}}}{⊢?A, A^{⊥}}

is redundant but does not contain cuts. It seems that it is connected to weakening and contraction rules that interact.

Definition 5.5 A proof Π of CLL is under weakening and contraction reduction if for any intermediate conclusion under the form ⊢?F,?F, Δ,

(i) if it is the conclusion of a w? rule introducing a formula ?F then there exists an inference J (≠ c?) introducing the other formula ?F. (ii) if it is the premise of a c? rule with ?F being one of its active formulae then, for each formula ?F, there exists an inference J (≠ w?) that introduces it.

Remark 5.1 In the case where the weakening is done immediately after the axioms the condition (i) is always true and then (ii) is the only condition to satisfy.

Theorem 5.4 For any CLL proof Π with ⊢ Δ as conclusion there exists a proof Π′ of ⊢ Δ under weakening and contraction reduction that is obtained by elimination of some weakening or contraction inferences and also addition of some intermediate conclusions.

Proof 5.4 By induction on h, height of the proof Π.

• h = 0. There is no proof Π with h = 0 and thus the property is true.

• Let us assume that we have the result for any proof tree with height h et prove it for h+1. Let Π be such a proof tree, if it is under weakening and contraction reduction we have the expected result, if not it contains an intermediate conclusion ⊢ Δ_{1} of the form ⊢?F,?F, Δ that does not verify the condition (i) and (ii) of definition 5.5. α) \underline{Δ does not verify the condition (i)}. We suppress in Π the weakening the conclusion of which is ⊢ Δ_{1} and all contractions introducing one of the formulae ?F and we add ?F to intermediate conclusions situated between them. Thus, we obtain a proof Π′′ of height h-1 with the same conclusion as Π and we can apply the induction hypothesis to it. β) \underline{Δ does not verify the condition (ii)}. We use the same proof schema as in α.

Theorem 5.5 A proof of CLL without cuts and contractions is not redundant.

Proof 5.5 This proof is based on the fact that for each inference the conclusion contains a number of logical connectives greater than the one of each premise.

Unfortunately, the theorem is false if we allow the contractions. Here we give an example illustrating this point.

\frac{\frac{\frac{\frac{\frac{_{\overline{⊢ A, A^{⊥}}  \overline{⊢ A, A^{⊥}}}}{⊢ A ⊗ A^{⊥}, A, A^{⊥}} ⊗}{⊢?(A ⊗ A^{⊥}), A, A^{⊥}} ? \overline{⊢ A, A^{⊥}}}{⊢?(A ⊗ A^{⊥}), A ⊗ A^{⊥}, A, A^{⊥}}  ⊗}{⊢?(A ⊗ A^{⊥}),?(A ⊗ A^{⊥}), A, A^{⊥}} ?}{⊢?(A ⊗ A^{⊥}), A, A^{⊥}} c?

This proof is redundant and without cuts. It is even under weakening and contraction reduction. That shows that we have not exhausted the subject of redundancies elimination in the proofs.

6 Proof normalization

From the previous results about the permutability of inferences, the movements of an inference in a proof and the treatment to reduce some redundancies, we aim to analyze the possibilities of reducing the non-determinism of the proof search process. In this section, we study the proof normalization depending on the strategy we use for proof construction. We will see in a next section that it might depend also from the fragment of CLL we consider. Thus, we are able to define the notion of normal proof that is a special form of proof with certain constraints on the order in which the inference rules must be applied. It is a way to consider the mechanization of proof construction in full linear logic, these normal proofs constituting a complete subset of proofs in CLL. But it would be necessary, in further work, to consider in addition semantical properties to improve new strategies for theorem proving in CLL.

6.1 Normalization and construction strategy

Undependently of the construction strategy, the possibility to construct proofs without cuts is essential. For a top-down proof search, it allows an goal-oriented procedure because of the sub-formula property and for a bottom-up proof search we have a decomposition process of the formulas of the sequent to prove. The theorems about the inference movements lead to a relative ordering of the inferences in a proof. Considering a proof as an object, the normalization corresponds to a double movement: maximum up or down movements of certain inferences in a proof. Considering a proof more as a process (being interested by the construction), the normalization corresponds to the application as soon as possible of certain inferences and as late as possible of other inferences. The theorems of section 4 help us to determinate a first criterion to choose the inferences to move backward (up) or forward (down): the facility to do it. For example, theorem 4.5. allows to immediately decompose a formula having & is principal connector when it appears in a goal during a bottom-up proof search. In the contrary, for a top down search, the application of the & rule is done as late as possible. But this criterion about facility is the not the only one. Another one consists of the proof strategy we have chosen (bottom-up or top-down). Thus, for top-down search, we have to move up the inferences that are easy to control from the premises and to move down at maximum the others. For a bottom-up, we have to move down the inferences that are easy to control from the conclusion and to move up at maximum the others. For instance, if we consider the weakening rule w?, we observe that it is not controllable from the premise and from the conclusion. Thus, we have to apply this rule as late as possible for top-down and bottom-up proof directions. The analysis for the contraction rule c? is different because it is not controllable from the conclusion but more easier from the premise. Thus, we have to apply the rule as soon as possible for a top-down strategy and as late as possible for a bottom-up strategy. Let us consider the following example

\frac{\frac{\frac{:}{⊢ F,?G, Δ_{1}}  \frac{:}{⊢ H,?G, Δ_{2}}}{⊢ F ⊗ H,?G,?G, Δ_{1}, Δ_{2}}  ⊗}{⊢ F ⊗ H,?G, Δ_{1}, Δ_{2}} c?

⊢ (F ⊗ H) ⊕ K,?G, Δ_{1}, Δ_{2} ⊕

We have, for a bottom-up approach, moved up c? as far as possible but in this case, we do not apply the focusing principle [2, 10] that means here that if we decompose the formula (F ⊗H)⊕K we have to go on with it until ⊗ or ⊕ is not the principal connective (it is not the case in this example). Thus, if we want to keep the movement of c? compatible with thus principle, we can modify the ⊗-rule to the following

\frac{⊢ F, Γ_{1},?Δ ⊢ G, Γ_{2},?Δ}{⊢ F ⊗ G, Γ_{1}, Γ_{2},?Δ} ⊗′

This rule is easily derivable from the initial ⊗ rule and is also complete and it is easy to prove that the sequent modified calculus with ⊗′ preserves completeness [27]. Thus, from now, we consider this new version of the sequent calculus. When we have fixed the direction of an inference movement in a proof, we have to known until where this movement is possible. The general answer is simple: in the proof (as object) the inferences will be moved up until the inferences where the active formulas are introduced and moved down until the inferences where their principal formulas become active. That are consequences of the results in section 4. Moreover, we have to consider the coherence of these movements. To be more concrete, we want now consider the bottom-up construction of proof in CLL, aiming the analysis the non-determinism forms and their reasons and the reduction possibilities due to the normalization. A similar and dual study might be done for CLL and the top-down proof strategy.

6.2 Normalization and non-determinism reduction

Let us consider a sequent ⊢ Δ to prove in CLL, a bottom-up proof search consists in building the proof tree from the conclusion to the axioms. The process is a construction of a sequence of goal expansions, an expansion of a goal ⊢ Δ′ consisting in replacing it by the premises of an inference that has ⊢ Δ′ as conclusion. During each step, there are three fundamental selection choice points where we have non determinism: the choice of a goal (to satisfy), the choice of a principal formula in a goal and finally, from a given goal and a principal formula, the choice of an inference with this goal as conclusion and this formula as the principal one.

a) \underline{The choice of a goal}. The non-determinism concerning this choice is a ”don’t care” non-determinism in the sense that whatever the goal we choose, the result does not change as its form. It is true for normal proofs or not. But the choice has consequences on time and space resources used to determine the goal. The study about permutability of inferences in a proof and the resulting theorem 3.2 can help us to elaborate some strategies. A sequent is often an element of a particular fragment of CLL and the permutation of inferences (and then the normalization) can be done more efficiently depending on the sort of fragments. Then it is pertinent to consider the goals being in fragments where we expect good normalization properties. Other considerations, from a semantical point of view, can help to refine the goal choice. For example, a goal being in the multiplicative fragment of CLL is interesting because we can apply the duality property [11] to it.

b) \underline{The choice of a principal formula}. This choice concerns partially a ”don’t know” non-determinism and a ”don’t care” non-determinism. The proof normalization will allow to reduce it directly.

• if the goal has the form ⊢!F,?Δ′ then theorem 4.6 allows us to surely choose !F as principal formula of an inference of ! type and to replace the current goal by ⊢ F,?Δ′.

• if the goal includes a formula having ℘, &, ∀, ⊥ as principal connective then we can surely choose it as principal formula of the next inference that will reduce the goal (theorem 4.5).

• if the goal does not have the previous forms and if it contains formulas that are not literals, the choice of the principal formula corresponds to a ”don’t know” non-determinism. But when we fix the principal formula F, we determinate the principal formula of the inferences that immediately follow. If F has ⊕, ⊗, ∃ as principal operator, we can surely choose its components, when they are not positive literals or not of the form ?G, as principal formulas of the inferences that immediately follow (theorem 4.4). If F has the form ?G, it can be produced by three different rules c?, w?, and ?. We surely choose an inference of w? type if the goal can be proved by an axiom followed by a sequence of weakenings (theorem 4.1). Else, if F is produced by the ? rule, by theorem 4.2. we can choose the active formula as principal formula of the next inference and if F is produced by the c? rule, one of the two active formulas is the principal formula of the inference that immediately follows.

• if the goal has only literals, it is either not provable or it is the conclusion of an axiom. c) \underline{The choice of an inference} Having a principal formula, its external connective determines the inference rule to realize the expansion of the proof tree, except in the case of ? and also ⊕ for which we have two possibilities. The choice between ⊕_{1} and ⊕_{2} corresponds to a ”don’t know” non-determinism that is difficult to reduce. The rule being fixed, it does not mean that the corresponding inference is completely fixed. It is true in general, except for ∃ and ⊗. For ∃, we have to choose the term associated to the inference. For ⊗, we have to split the context into two parts that is an important source of ”don’t know” non-determinism difficult to reduce. In the both cases we can postpone the choice at the level of axioms by using lazy methods. To summarize, the search of a normal proof imposes constraints to the general algorithm for the choice of the principal formula, that reduce significantly the ”don’t know” non-determinism of it. Moreover, it could help us to elaborate specific tactics and strategies for the choice of the goal to prove. But it does provide mechanisms for calculating expansions when they are not determined by the principal formula. Thus, normal proofs provide logical foundations for the proof search for a given sequent.

6.3 Normal proofs

To the normalization of proofs considered as processes, corresponds a normalization of the proofs considered as objects. For the full linear logic and for the bottom-up proof search direction, we can now define the notion of normal proof. Let us begin to introduce this definition, by considering T_{↓} and T_{↑} the sets of inference types defined by T_{↓} = {℘, &, ∀, ⊥} and T_{↑} = {⊗, ⊕_{1}, ⊕_{2}, c?, w?,?, ∃}.

Definition 6.1 A proof Π of CLL is said normal if

(i) Π is without cuts, (ii) Π is under weakening and contraction reduction, (iii) any intermediate conclusion ⊢ Δ verifies: if ⊢ Δ has the form ⊢!F,?Δ′ then it is the immediate conclusion of an inference of ! type else if ⊢ Δ contains a formula introduced by an inference of type ∈ T_{↓}

then it is the immediate conclusion of an inference of type ∈ T_{↓}

else if ⊢ Δ contains a formula introduced by an inference of type ∈ T_{↑} \ {?, c?, w?} then for each premise which is not ⊢!F,?Δ′, the active formula , if it is not a positive literal, is the principal formula of the preceding inference. else if ⊢ Δ has a formule ?F as principal formula then we have three possible cases

(1) ⊢ Δ is the conclusion of a w? rule and the preceding inferences are weakenings or axioms.

(2) ⊢ Δ is the conclusion of a c? rule and the preceding inference is an inference of type ? introducing one of the active formulas of the inference ending with ⊢ Δ

(3) ⊢ Δ is the conclusion of an inference of ? type and the

active formula, if it is not a positive literal, is the principal formula of the preceding conclusion.

An intermediate conclusion which verifies this criterion is said normal.

Example 6.1 The following proof

\frac{\frac{\frac{\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A ⊕ B, A^{⊥}} ⊕_{1}  \frac{\overline{⊢ B, B^{⊥}}}{⊢ A ⊕ B, B^{⊥}} ⊕_{2}}{⊢ A ⊕ B, A^{⊥}&B^{⊥}} & \overline{⊢ C, C^{⊥}}}{⊢ (A ⊕ B) ⊗ C, A^{⊥}&B^{⊥}, C^{⊥}}  ⊗}{⊢ (A ⊕ B) ⊗ C, (A^{⊥}&B^{⊥})℘C^{⊥}} ℘ \overline{⊢ D, D^{⊥}}}{⊢ ((A ⊕ B) ⊗ C) ⊗ D, (A^{⊥}&B^{⊥})℘C^{⊥}, D^{⊥}}  ⊗

is not in normal form because it contains intermediate conclusions which are not normal, for example ⊢ (A ⊕ B) ⊗ C, A^{⊥}&B^{⊥}, C^{⊥}. It contains a formula introduced by an inference of type ∈ T_{↓} (i.e., A^{⊥}&B^{⊥}) and it is the immediate conclusion of an inference of type ∈ T_{↑} (i.e., ⊗). For the same sequent to prove, the following proof is in normal form

\frac{\frac{\frac{\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A ⊕ B, A^{⊥}} ⊕_{1} \overline{⊢ C, C^{⊥}}}{⊢ (A ⊕ B) ⊗ C, A^{⊥}, C^{⊥}}  ⊗ \overline{⊢ D, D^{⊥}}}{⊢ ((A ⊕ B) ⊗ C) ⊗ D, A^{⊥}, C^{⊥}, D^{⊥}}  ⊗  \frac{\frac{\frac{\overline{⊢ B, B^{⊥}}}{⊢ A ⊕ B, B^{⊥}} ⊕_{2} \overline{⊢ C, C^{⊥}}}{⊢ (A ⊕ B) ⊗ C, B^{⊥}, C^{⊥}}  ⊗ \overline{⊢ D, D^{⊥}}}{⊢ ((A ⊕ B) ⊗ C) ⊗ D, B^{⊥}, C^{⊥}, D^{⊥}}  ⊗}{⊢ ((A ⊕ B) ⊗ C) ⊗ D, A^{⊥}&B^{⊥}, C^{⊥}, D^{⊥}} &}{⊢ ((A ⊕ B) ⊗ C) ⊗ D, (A^{⊥}&B^{⊥}) ℘ C^{⊥}, D^{⊥}} ℘

We present now the proof normalization theorem, the proof of which gives us a procedure for the transformation and normalization of given proofs.

Theorem 6.1 (normalization theorem) For any proof Π of CLL there exists a normal proof Π_{n} of LL with the same conclusion

Proof 6.1 Let us call a quasi-normal proof a proof that verifies all normality criteria of the definition 6.1 except possibly (ii). According to theorem 5.4, it is sufficient to prove that, for any CLL proof there exists a quasinormal proof with the same conclusion. Let Π be a CLL proof, according to theorem 5.2, we can also suppose Π without cuts. In order to normalize it, we can choose between different strategies. We can, for example, start with the forward movement of all concerned inferences and then move backward all the others. Of course, we must proceed methodically and carefully because every new movement does not have to destroy what has been realized before. Then, we proceed by structural induction on Π.

1) \underline{Π is an axiom.} In this case, Π is obviously normal and is the proof we search.

2) \underline{Π is not an axiom.} Let I be the last inference of Π. By the induction hypothesis, we can replace the subproofs of the I premises by quasi-normal proofs in Π. We obtain in this way a proof Π′ which is not necessarily quasi-normal. The conclusion ⊢ Δ of I is not always a normal intermediate conclusion of Π′. It depends on the type of I. 2.1) \underline{type(I) =!} It is immediate that ⊢ Δ is normal in Π′. 2.2) \underline{type(I) ∈ T_{↓}} Then ⊢ Δ is not of the form ⊢!F,?Δ′ and therefore it is normal in Π′.

2.3) \underline{type(I) ∈ T_{↑} \ \{?, w?, c?\}} According to the theorem 4.4, there exists a proof Π′′, obtained by backward movement of I in Π′, such that every inference I’ of Π′′ resulting from this movement is immediately preceded by an inference which introduces the active formula of I’ (if its top connective is not ?). This operation preserves the normality of the modified intermediate conclusions, except possibly the conclusions of the inferences I’. They can contain formulas which have been introduced by inferences of type ∈ T_{↓}. But we can modify this feature using theorem 4.5 which allow, for every inference I’, to move forward the problematic inferences just after I’. The proof we obtain is then quasi-normal. 2.4) \underline{type(I) ∈ \{?, w?, c?\}} We use the same process as in 2.3) but with variants due to particularities of these types. In its backward movement, I cannot be stopped by an inference of ! type and according to the theorem 4.1, I can be moved just after axioms if it is of w? type.

Remark 6.1 The concept of normal proof, because of its static character, does not emphasize the essential difference between the inferences of type ℘, &, ∀, ⊤ and the ones of type ⊕, ⊗, ∃,?. The first ones are completely concerned by a ”don’t care” non-determinism and the second ones are partially concerned by a ”don’t know” non-determinism.

Remark 6.2 Moreover, the existence of a part of ”don’t care” non-determinism leads to different normal proofs for a given sequent, each being equivalent modulo inference permutations. A possibility for handling this specific case of inference permutation could be to investigate a notion of proof net and proof net normalization. Proof net is a concept in proof theory firstly introduced by Girard for the multiplicative fragment of linear logic [12] from the fact that the sequential presentation of proofs with trees is inadequate and does not emphasize their meaning. In [11], we have investigated automatic proof net construction but the point is to be able to extend this notion to more important fragments of CLL [5] through a new appropriate representation and definition of proof nets. Having it, it would be interesting to apply the previous results on normalization directly on this concept with a view to reducing not useful redundancies.

As in [16] where the uniform proof notion is essential for proof construction, we have with the normal proof concept the possibility to found systems dependent from proof search in CLL on this concept defining sub-classes of proofs that are complete and tractable. It is important to note that this notion depends on the fragment we consider and also on the proof construction direction (bottom-up or top-down). In a general way, if we want to build normal proofs in CLL it is necessary to fix some constraints about choices, as mentioned above, with effect to mainly reduce non-determinism sources.

7 Application to linear logic programming

Until now, we have considered full linear logic and normalization aims to improve the efficiency of proof construction in a theorem prover for linear logic. Such a prover could be considered as a starting point for a based-on-linear-logic interpretor of logic programming. But it seems necessary to restrict the study to some fragments of CLL for efficiency purposes. Thus a crucial question arises: how can we determine an appropriate fragment ? . A first point to answer this question is to know the type of problems we want to specify with the help of linear logic. Commonly, it is well adapted to the specification of dynamic problems where we need a strict and explicit resource management as planning [23], natural languages analysis, Petri nets and more generally reactive systems. Thus, for a given problem, we can reduce the syntax to the one necessary for coding it as for Petri nets where only the {⊗,! —∘} fragment is involved. At this point, nothing tells us if the fragment determined by the problem involves efficient proof search procedures. The previous results will help us to analyze the adequacy between the fragment of logic and the possible proof search methods. To illustrate the application to the design of linear logic programming, including efficient proof search procedures, we consider the example of the representation of the standard Prolog in linear logic and the analysis of possible proof procedures. Let us note that this example is only significant for the illustration of the methodological point of view but applications of this approach to other logic programming proposals surely will emphasize its foundational character.

Let us consider the logical fragment of standard Prolog, i.e, Horn clauses. Basically, we have a program P and a goal G composed by clauses, each clause C_{i} of P being of the form A_{i} ⇐ B_{1}, B_{2}, .., B_{n}.

1) A first step is the translation of the program and goal clauses. each clause C_{i} is translated in CLL by the formula C_{i}^{L} ≡!(∀x_{1}, .., x_{m}(B_{1}&B_{2}&, ..&B_{n} —∘A)) where the x_{i}(1 ≤ i ≤ m) are the free variables of C_{i}. A goal G is translated by the formula G^{L} ≡ ∃y_{1}, .., y_{p}(G_{1}&G_{2}&...&G_{q}) where the y_{j}(1 ≤ j ≤ p) are free variables of G and G_{l} are subgoals of G. Thus the general query < P, G > will be represented by the following linear sequent

C_{1}^{L}, .., C_{k}^{L} ⊢ G^{L}.

To summarize we can say that the Prolog queries correspond to sequents in Linear Logic of the form !C_{1}, ..,!C_{k} ⊢ ∃x_{1}, .., x_{p}G where C_{1},..,C_{k} are particular formulas of CLL representing the clauses of the program and G is a formula representing the goal of the query, both being defined by the following grammar

C := X|G —∘X|∀xC.
G := X|G&G|∃xG.

where X represents a positive literal, C a definite clause and G a goal. Let us remark that here, we have translated a given logical framework to obtain the previous grammar about clauses and goals. That is because we have chosen standard Prolog as starting point, but a normal approach is to give directly such a grammar and to begin the study with it.

2) A second step consists in defining the CLL fragment involved by this sequent form. Thus, according to the subformula property we can deduce, from the previous syntax, the set of inference rules of CLL that will be concerned to prove the linear sequents deduced by the first step. For our example, this set of rules is R_{0} = { —∘_{L}, &_{R},!_{L}, w!_{L}, c!_{L}, ∀_{L}, ∃_{R}} and we have now determinated the logical fragment (denoted LF_{0}).

3) A third step consists in studying the logical foundations of this fragment, i.e., permutability properties in order to define proof search procedures. Let us remark that our results work on sequents without left-hand side part but we can transpose them without difficulty for application to classical sequents. The study of inference permutability, according to theorem 3.2, leads to the following results for LF_{0}, summarized in the array below.

\begin{matrix}t_{2}\t_{1} & —∘_{L} & &_{R} & !_{L} & w!_{L} & c!_{L} & ∀_{L} & ∃_{R} \\ —∘_{L} & p & p & p & p & p & p & p \\ &_{R} & np & × & np & np & np & p & × \\ !_{L} & p & p & p & p & p & p & p \\ w!_{L} & p & p & p & p & p & p & p \\ c!_{L} & np & p & p & p & p & p & p \\ ∀_{L} & p & p & p & p & p & p & p \\ ∃_{R} & p & × & p & p & p & p & × \end{matrix}

4) A fourth step consists in studying the possible inference movements in LF_{0}. To do that, we have first to fix a direction for proof strategy, i.e, bottom-up or top down, and according to our example, we choose a bottom-up proof search strategy and try to order inferences as in the general case presented section 4. For LF_{0}, the inferences of type &_{R} and ∃_{R} can be moved forward (or down) as far as possible in a proof and the inferences of type —∘_{L}, !_{L}, w!_{L} and c!_{L} can be moved forward (or up) as far as possible. Let us remark that ∀_{L} can be moved up or down and we decide here to move it backward.

5) A fifth step consists in defining, through inferences ordering, the form of bottom-up proof we can construct. From the previous step, a bottom-up proof will begin with the application of the ∃_{R} and &_{R} rules for decomposing the goal into subgoals. Then, we will apply the !_{L} or c!_{L} rules that correspond to the choice of a clause in a program. If we apply the !_{L} rule, we can always have a c!_{L} rule application preceding it and if it is useless we can cancel it by a weakening. It means that the set of resources of the program will be unchanged until the next step. The backward movement of c!_{L} inferences means that the application of such a rule will be immediately followed by !_{L} rule application (the application of the w!_{L} rule could introduce a redundancy that we can suppress). With a selected clause being usable through the application of !_{L} rule we can apply it the ∀-L rule because the !_{L} rules have been moved up at maximum. Then we consider the —∘_{L} because the ∀_{L} rules have been moved up at maximum and we have a goal of the form !Γ, G —∘X ⊢ Y. In the classical strategy of Prolog we have X and Y unifiable but here we have X and Y identical. Let us explain why. The inference to realize has the form

\frac{!Γ_{1} ⊢ G !Γ_{2}, X ⊢ Y}{!Γ_{1},!Γ_{2}, G —∘X ⊢ Y}

We know that it is moved up at maximum and thus the active formula X is also the principal formula of the inference just above, even it is an atom. X is an atom and this inference is an axiom and consequently X = Y and Γ_{2} = ∅ and the inference is

\frac{!Γ ⊢ G X ⊢ X}{!Γ, G —∘X ⊢ X}

Here, we have partially the Prolog mechanism without unification because the corresponding rules ∀-L and ∃-R have been applied. To obtain unification, it is sufficient to have a lazy application of these rules where the instantiation of the variables is stopped until the axioms application.

We have proposed a simple example, for which we have knowledge about expressiveness and proof search, but we can apply this analysis method to different fragments of linear logic as in [15, 16, 17], considered as basis for linear logic programming.

8 Related and further work

This work on proof normalization in linear logic presents similarities and differences with other works on various fragments of LL, mainly those focusing on extensions of logic programming. The study of permutability properties is significant for proof search and theorem proving for non classical logics in general [29]. Shankar has presented in [26] a proof search method for intuitionistic calculus, based on the permutability possibilities, that could be generalized for our purpose. We will investigate this point and the connections with our work. Our aim, here, consists in having a special proof form, called normal form, in the class of equivalent cut-free proofs. In a similar way, Andreoli emphasizes in [2] also a subclass of proofs, called ”focusing proofs”, which is complete. Let us recall that, in a normal proof, the weakenings (w?) are moved just after the axioms, the inferences of type ℘, &, ⊥, ∀ are moved forward as far as possible (until the principal formula becomes active or to the end of the proof), the inferences of type ⊗, ⊕,?, ∃, c? are moved backward as far as possible (until its active formulae are introduced). So we obtain a partition of inference types into two groups with the respect of the notion of movement of an inference in a proof. [2] proposes a similar partition of the connectives, consequently of the inference rules, that is based on notions of synchronization and determinism. It presents two main differences concerning the treatment of connectives ? and !. In [2] Andreoli considers the connective ? as synchronous, which seems justified by its triadic system. But, the syntax of this system masks the point that the three types of inferences introducing ?, w? and c? have no common behaviour which our study confirms. The difference about the treatment of ! is more important. He considers the connector ! as those he called ”synchronous” connectives (for example, ⊗) and does not reduce the non-determinism in this case. Then a principal formula !A is chosen with a non-determinism. But it is possible to suppress it because, as shown in the previous sections, in a sequent ⊢ !A,?Δ, the formula !A can always be selected as principal. For example, if we have to prove ⊢ !A,?(A^{⊥} ⊕ B),?B^{⊥} in [2] it is possible to choose ?(A^{⊥} ⊕ B) as principal formula, then ?B^{⊥} before the right one !A whereas in our system we choose immediately !A as principal formula. Tammet in [27] concentrates on problems of automated theorem proving in full linear logic and investigate general search strategies mainly for top-down direction with original proposals for resolution method in CLL. It appears that we might consider our approach to refine and define proof strategies for top-down direction. Keeping full linear logic for the proof normalization process, leads to some limits due to the impossibility to permute some inferences. A way to solve this problem is to consider an adequate CLL fragment to go further than in CLL in the inference movement in a proof and then in the normalization. For example, in a fragment without &, the inferences of type ⊕ can be moved forward as much as possible as those of type ℘. Of course, for the choice of the fragment, there is another important criterion to take into account: the ability to express problem specifications in such a fragment. Both requirements of expressiveness and efficiency can be contradictory and we have to find the best compromise between these aspects. In this way, we can mention the work of Hodas and Miller [16] and of Harland and Pym [14, 15]. The common objective is to extend the expressiveness capability in logic programming languages using linear logic and to efficiently construct proofs in the logical framework. They consider a two-sided linear sequent calculus without negation rule. But are, in such a framework, our permutability properties still available ? The answer is yes if we made a good translation of it. Then any property of an inference type (for sequents without left-hand side part) is transposed automatically to the corresponding inference type at righthand side and also to the dual inference type at left-hand side (see section 7). It results from the fact that any rule of the sequent calculus without left-hand side part leads to two rules when we consider a sequent calculus with it. Moreover, the connective —∘, more adequate for logic programming, replaces the connective ℘ but keeps the same properties of inference permutability (in fact A —∘B ≡ A^{⊥}℘B). Briefly, we can say that [16] considers two sorts of formulae (as goals and resources) and sequents (as queries) of a specific CLL fragment. The point is that such sequents can be proved using the notion of uniform proofs: in a bottom-up construction, the right rules are always applied before the left rules. It is the case because, in this fragment of LL, the inferences on right-hand side parts of sequents can be moved down as much as possible in a proof. This point is strongly connected to the previous results. A complete study could be done on the basis of the method proposed in section 7 to understand and justify the limits and the power of the fragment considered. Moreover, a similar study can be done with the approach of Harland and Pym [15]. They have proposed also a fragment of LL chosen so that uniform proofs remain complete but it presents more difficulty to treat right-hand sides including !, with difference of expressiveness in goals and contexts. These works refer to the resolution on CLL fragments which appears as a specific rule defined mainly from an analysis of the permutation properties as but with a bottom-up proof direction. Finally, we cannot forget to mention the relationship with the fundamental results about complexity and decidability in LL. Kanovich’s works [17] aim to develop a computational interpretation of the logic and to obtain efficient decision algorithms based on a bottom-up approach. To do it, he considers the Horn fragment of LL from a computational and a logical point of view and then generalizes the approach by introduction of the additives and !. Knowing that the propositional linear logic is not decidable [21], the main conclusions about this complexity analysis is that the multiplicative fragment is NP-complete and the additive multiplicative one is Pspace-complete. The connections between our based-on-permutability logical study and the various related work presented here are to be deeply analyzed with a view to mechanizing proof construction in fragments of linear logic.

9 Conclusion

We have considered the problem of proof normalization in full linear logic. The solution we propose results from a systematic study of inference permutabilities in this logic framework. An issue of them is the effective construction of a theorem prover for linear logic in which it is possible to reduce some sources of undeterminism during the proof construction. It would be necessary to consider other tactics or strategies for proof development based in addition on semantical results. Another issue consists in using the analysis on permutability of inferences in designing some logic programming languages in fragments of CLL with a compromise between the expressiveness of the language and the efficiency of the proof construction. This point is strongly connected to recent works on some extensions of logic programming [15, 16] and allows to understand or justify some choices in the language conception. Moreover, from this analysis of proof mechanization in linear logic and the better comprehension of CLL through this prooftheoretic foundation, we could consider the various applications of proof development in linear logic. In addition to logic programming, let us mention the connections with some dynamical problems as planning [22] and with the proofs as programs approach through adequate typed λ-calculi. In this latter case, a good knowledge about various aspects of proof construction and transformation would be necessary to use the algorithmic contents of proofs to prospect for example typed concurrent programming and program synthesis through program extraction from proofs in this logical framework.

References

[1] S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1-2):3–58, 1993.

[2] J.M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992.

[3] J.M. Andreoli and R. Pareschi. Logic programming with sequent systems: A linear logic approach. In Int. Workshop on Extensions of Logic Programming, LNCS 475, pages 1–30, Tübingen, Germany, December 1989.

[4] J.M. Andreoli and R. Pareschi. Linear objects: logical processes with built-in inheritance. In 7th Conference on Logic Programming, MIT Press, pages 495–510, Jerusalem, June 1990.

[5] G. Bellin. Proof nets for multiplicative and additive linear logic. Technical Report ECS-LFCS 91-161, Department of Computer Science, Edinburgh University, May 1991.

[6] S. Cerrito. A linear semantics for allowed logic programs. In 5th IEEE Symposium on Logic in Computer Science, pages 219–227, Philadelphia, June 1990.

[7] J. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. John Wiley & Sons, 1986.

[8] D. Galmiche. Constructive system for automatic program synthesis. Theoretical Computer Science, 71(2):227–239, 1990.

[9] D. Galmiche. Program development in constructive type theory. Theoretical Computer Science, 94(2):237–259, 1992.

[10] D. Galmiche and G. Perrier. Automated deduction in additive and multiplicative linear logic. In Logic at Tver ’92, Logical Foundations of Computer Science Symposium, LNCS 620, pages 151–162, Tver, Russia, July 1992.

[11] D. Galmiche and G. Perrier. A procedure for automatic proof nets construction. In LPAR’92, International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 42–53, St. Petersburg, Russia, July 1992.

[12] J.Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–102, 1987.

[13] J.Y. Girard. Towards a geometry of interaction. In J.W. Gray and A. Scedrov, editors, Conference on Categories in Computer Science and Logic, pages 69–108, Boulder, Colorado, June 1987.

[14] J. Harland and D. Pym. The uniform proof-theoretic foundation of linear logic programming. In International Symposium on Logic Programming, MIT Press, pages 304–318, San Diego, October 1991.

[15] J. Harland and D. Pym. On resolution in fragments of classical linear logic. In LPAR’92, International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 30–41, St. Petersburg, Russia, July 1992.

[16] J.S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In 6th IEEE Symposium on Logic in Computer Science, pages 32–42, Amsterdam, The Netherlands, July 1991.

[17] M.I. Kanovich. Horn programming in linear logic is NP-complete. In 7th IEEE Symposium on Logic in Computer Science, pages 200–210, Santa-Cruz, California, June 1992.

[18] N. Kobayashi and A. Yonezawa. ACL - a concurrent linear logic programming paradigm. In Int. Symposium on Logic Programming, pages 279–294, Vancouver, October 1993.

[19] Y. Lafont. Interaction nets. In 17th ACM Symposium on Principles of Programming Languages, pages 95–108, San Francisco, January 1990.

[20] P. Lincoln and J. Mitchell. Operational aspects of linear lambda calculus. In 7th IEEE Symposium on Logic in Computer Science, pages 235–246, Santa-Cruz, California, June 1992.

[21] P. Lincoln, J. Mitchell, A. Scedrov, and N. Schankar. Decision problems for propositional linear logic. In 31st IEEE Symposium on Foundations of Computer Science, pages 662–671, St. Louis, Missouri, October 1990.

[22] M. Masseron, C. Tollu, and J. Vauzeilles. Generating plans in linear logic. In Foundations of Software Technology and Theoretical Computer Science, LNCS 472, pages 63–75, Bangalore, India, December 1990.

[23] M. Masseron, C. Tollu, and J. Vauzeilles. Generating plans in linear logic I: Actions as proofs. Theoretical Computer Science, 113(2):349–371, 1993.

[24] J. Meseguer and N. Marti-Oliet. From petri nets to linear logic. In Category Theory and Computer Science, LNCS 389, pages 313–340, Manchester, September 1989.

[25] J. Mitchell. Introduction to linear logic. Sigact News, 23(2):29–37, 1992.

[26] N. Shankar. Proof search in the intuitionistic sequent calculus. In 11th Conference on Automated DEduction, LNAI 607, pages 522–536, Saratoga Springs, June 1992.

[27] T. Tammet. Proof search strategies in linear logic. Programming Methodology Group Report 70, Chalmers University Group, University of Göteborg, 1993.

[28] A.S. Troelstra. Lectures on Linear Logic, volume 29 of Lecture Notes. CSLI, 1992.

[29] L.A. Wallen. Automated Proof search in Non-Classical Logics. MIT Press, 1990.

A Proof of permutability theorem

Case by case analysis according to the partition of the inference rules into two groups: those depending on the context, i.e, of type &,!, ∀ and the others.

1) \underline{type(I_{2}) = &}. To have I_{1} permutable with I_{2}, we need in Π an inference J_{1} of the same type as I_{1} and the conclusion of which coincides with the premiss of I_{2} that is not the conclusion of I_{1}. For any type for I_{1}, we can find a counter-example that does not verify this condition. Then I_{1} is not always permutable with I_{2}.

2) \underline{type(I_{2}) =!}. If I_{1} is in permutation position with I_{2} the context of I_{2}, being under the form ?Δ, contains Δ_{p}(I_{1}) and then we have two possibilities: α) Δ_{p}(I_{1}) = ∅ and type(I_{1}) = cut, β) Δ_{p}(I_{1}) = {?A} and type(I_{1}) ∈ {?, w?, c?}. 2.1) \underline{type(I_{1}) = cut}. In this case, Π has the following form

\frac{\frac{\begin{matrix}: \\ ⊢ F, G,?Δ_{n}^{1} \end{matrix}  \begin{matrix}: \\ ⊢ F^{⊥},?Δ_{n}^{2} \end{matrix}}{⊢ G,?Δ_{n}^{1},?Δ_{n}^{2}} cut}{⊢!G,?Δ_{n}^{1},?Δ_{n}^{2}} !

Let us consider the proof

\frac{\frac{\begin{matrix}: \\ ⊢ F, G,?Δ_{n}^{1} \end{matrix}}{⊢ F,!G,?Δ_{n}^{1}} ! \frac{:}{⊢ F^{⊥},?Δ_{n}^{2}}}{⊢!G,?Δ_{n}^{1},?Δ_{n}^{2}}  cut

If F does not have the form ?F then this proof is not correct and I_{1} is not always permutable with I_{2}. Let us remark that if we extend the notion of inference permutability by adding the possibility of inserting new inferences in the resulting proof as in [10] then we can say that I_{1} is permutable with I_{2} in a certain sense. In this permutation, we add two inferences ? and ! to obtain the following proof

\frac{\frac{\frac{\begin{matrix}: \\ ⊢ F, G,?Δ_{n}^{1} \end{matrix}}{⊢?F, G,?Δ_{n}^{1}} ?}{⊢?F,!G,?Δ_{n}^{1}} ! \frac{\begin{matrix}: \\ ⊢ F^{⊥},?Δ_{n}^{2} \end{matrix}}{⊢!F^{⊥},?Δ_{n}^{2}} !}{⊢!G,?Δ_{n}^{1},?Δ_{n}^{2}} cut

2.2) \underline{type(I_{1}) =?}. The following counter-example shows that in general I_{1} is not permutable with I_{2}.

\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢?A, A^{⊥}} ?}{⊢?A,!A^{⊥}} !

2.3) \underline{type(I_{1}) = w?}. In this case, we have the transformation

\frac{\frac{\begin{matrix}: \\ ⊢ G,?Δ_{n} \end{matrix}}{⊢?F, G,?Δ_{n}} w?}{⊢?F,!G,?Δ_{n}} ! ⇝ \frac{\frac{\begin{matrix}: \\ ⊢ G,?Δ_{n} \end{matrix}}{⊢!G,?Δ_{n}} !}{⊢?F,!G,?Δ_{n}} w?

that is correct. Then I_{1} is permutable with I_{2}.

2.4) \underline{type(I_{1}) = c?}. In this case, we have the transformation

\frac{\frac{\begin{matrix}: \\ ⊢?F,?F, G,?Δ_{n} \end{matrix}}{⊢?F, G,?Δ_{n}} c?}{⊢?F,!G,?Δ_{n}} ! ⇝ \frac{\frac{\begin{matrix}: \\ ⊢?F,?F, G,?Δ_{n} \end{matrix}}{⊢?F,?F,!G,?Δ_{n}} !}{⊢?F,!G,?Δ_{n}} c?

that is correct. Then I_{1} is permutable with I_{2}.

3) \underline{type(I_{2}) = ∀}. Necessarily, the variable y quantified by I_{2} is not free in Δ_{p}. If I_{1} is not of type cut, ∀ or ∃ the variable y is not free also in Δ_{a} (or Δ_{a}^{1} and Δ_{a}^{2}). Moreover, if I_{1} is independent of the context then I_{1} is permutable with I_{2}. Let us analyze the cases with potential problems. 3.1) \underline{type(I_{1}) = cut}. The following counter-example shows that I_{1} is not in general permutable with I_{2}.

\frac{\frac{\overline{⊢ a(y), a(y)^{⊥}}  \frac{\overline{⊢ a(y), a(y)^{⊥}}}{⊢ ∃xa(x), a(y)^{⊥}} ∃}{⊢ a(y)^{⊥}, ∃xa(x)} cut}{⊢ ∀xa(x)^{⊥}, ∃xa(x)} ∀

3.2) \underline{type(I_{1}) = &}. In this case, we have the transformation

\frac{\frac{⊢ F, H[y/x], Δ_{n} ⊢ G, H[y/x], Δ_{n}}{⊢ F &G, H[y/x], Δ_{n}} &}{⊢ F &G, ∀xH, Δ_{n}} ∀ ⇝ \frac{\frac{⊢ F, H[y/x], Δ_{n}}{⊢ F, ∀xH, Δ_{n}} ∀ \frac{⊢ G, H[y/x], Δ_{n}}{⊢ G, ∀xH, Δ_{n}} ∀}{⊢ F &G, ∀xH, Δ_{n}} &

that is a correct proof. Then I_{1} is permutable with I_{2}. 3.3) \underline{type(I_{1}) = ∀}. In this case, we have the transformation

\frac{\frac{⊢ F [u/x], G[z/y], Δ_{n}}{⊢ ∀xF, G[z/y], Δ_{n}} ∀}{⊢ ∀xF, ∀yG, Δ_{n}} ∀ ⇝ \frac{\frac{⊢ F [u/x], G[z/y], Δ_{n}}{⊢ F [u/x], ∀yG, Δ_{n}} ∀}{⊢ ∀xF, ∀yG, Δ_{n}} ∀

If the left-hand side proof Π is correct, let us show that the resulting proof Π′ on the right-hand side is also correct. To do that, we have to prove that the two ∀ inferences of Π′ are correct. Let us begin with the second one. The first ∀ inference of Π being correct, u is not free in G[z/y], Δ_{n}. Then, a fortiori, u is not free in ∀yG, Δ_{n}. Let us examine now the first one. The second ∀ inference of Π being correct, z is not free in ∀xF, Δ_{n}. The only case in which z could be free in F [u/x], Δ_{n} is the one where z is identical to u. Then G[z/y] ≡ G[u/y]. Since u is not free in G[z/y], i.e in G[u/y], then G[z/y] ≡ G and y is not free in G. Thus, by association of any variable, that is neither free in G nor in F [u/x], with the first ∀ inference of Π′ we obtain a correct inference. In conclusion, Π′ is correct and I_{1} is permutable with I_{2}. 3.4) \underline{type(I_{1}) = ∃}. The following counter-example shows that I_{1} is not in general permutable with I_{2}.

\frac{\frac{\overline{⊢ a(y), a(y)^{⊥}}}{⊢ a(y), ∃xa(x)^{⊥}} ∃}{⊢ ∀xa(x), ∃xa(x)^{⊥}} ∀

3.5) \underline{type(I_{1}) =!}. The following counter-example shows that I_{1} is not in general permutable with I_{2}.

\frac{\frac{\frac{\overline{⊢ a, a^{⊥}}}{⊢?a, a^{⊥}} ?}{⊢?a,!a^{⊥}} !}{⊢ ∀x(?a),!a^{⊥}} ∀

4) \underline{type(I_{1}) =! and type(I_{2}) ∉ \{&,!, ∀\}}. 4.1) \underline{I_{2} has one premise}. Π has the following form

\frac{\frac{\begin{matrix}: \\ ⊢ F,?Δ′_{a},?Δ_{n} \end{matrix}}{⊢!F,?Δ′_{a},?Δ_{n}} !}{⊢!F, Δ′_{p},?Δ_{n}} I_{2}

Let us consider the following proof

\frac{\frac{\begin{matrix}: \\ ⊢ F,?Δ′_{a},?Δ_{n} \end{matrix}}{⊢ F, Δ′_{p},?Δ_{n}} I′_{2}}{⊢!F, Δ′_{p},?Δ_{n}} !.

It is correct iff Δ′_{p} is under the form ?Δ, i.e, iff I_{2} is of type ?, w? ou c?. In these three cases, I_{1} is always permutable with I_{2} but not in the other cases. 4.2) \underline{I_{2} has two premises}. Then I_{2} is of the cut or ⊗ type and Π has the form

\frac{\begin{matrix}: \\ ⊢ F,?Δ_{a}^{′1},?Δ_{n} \end{matrix}}{⊢!F,?Δ_{a}^{′1},?Δ_{n}} ! \frac{:}{⊢ Δ_{a}^{′2}, Δ′_{n}}

⊢!F, Δ′_{p},?Δ_{n}, Δ′_{n} I_{2}

Δ′_{n} not being necessarily of the form ?Δ, I_{1} is not always permutable with I_{2}.

5) \underline{type(I_{1}) = ∀ and type(I_{2}) ∉ \{&,!, ∀\}}. 5.1) \underline{I_{2} has one premise}. In this case, Π has the following form

\frac{\frac{Π_{1} \{ \begin{matrix}: \\ ⊢ F [y/x], Δ′_{a}, Δ_{n} \end{matrix}}{⊢ ∀xF, Δ′_{a}, Δ_{n}} ∀}{⊢ ∀xF, Δ′_{p}, Δ_{n}} I_{2}

Let z be a variable that is not free in all intermediate conclusions of Π over I_{2} included.

\frac{\frac{Π_{1}[z/y] \{ \begin{matrix}: \\ ⊢ F [z/x], Δ′_{a}, Δ_{n} \end{matrix}}{⊢ F [z/x], Δ′_{p}, Δ_{n}} I′_{2}}{⊢ ∀xF, Δ′_{p}, Δ_{n}} ∀

It is correct because I_{2} is of one type that does not depend on the context and z is not free in Δ′_{p}, Δ_{n}. Then I_{1} is always permutable with I_{2} (when I_{2} is not of type ⊕ or w? a renaming is not necessary). 5.2) \underline{I_{2} has two premises}. I_{2} is then of the cut or ⊗ type and Π has the form

\frac{\frac{Π_{1} \{ \begin{matrix}: \\ ⊢ F [y/x], Δ_{a}^{′1}, Δ_{n} \end{matrix}}{⊢ ∀xF, Δ_{a}^{′1}, Δ_{n}} ∀ Π_{2} \{ \begin{matrix}: \\ ⊢ Δ_{a}^{′2}, Δ′_{n} \end{matrix}}{⊢ ∀xF, Δ′_{p}, Δ_{n}, Δ′_{n}} I′_{2}

Let z be a variable that is not free in all intermediate conclusions of Π over I_{2} included.

\frac{\frac{Π_{1}[z/y] \{ \begin{matrix}: \\ ⊢ F [z/x], Δ_{a}^{′1}, Δ_{n} \end{matrix} Π_{1}[z/y] \{ \begin{matrix}: \\ ⊢ Δ_{a}^{′2}Δ′_{n} \end{matrix}}{⊢ F [z/x], Δ′_{p}, Δ_{n}, Δ′_{n}} I′_{2}}{⊢ ∀xF, Δ′_{p}, Δ_{n}, Δ′_{n}} ∀

Here y is not free in Δ_{a}^{′1} and Δ_{a}^{′2}. The proof is correct and then I_{1} is always permutable with I_{2}.

6) \underline{type(I_{1}) = & and type(I_{2}) ∉ \{&, ∀\}}. 6.1) \underline{I_{2} has one premise}. In this case, Π has the following form

\frac{\frac{\begin{matrix}: \\ ⊢ F, Δ′_{a}, Δ_{n} \end{matrix}  \begin{matrix}: \\ ⊢ G, Δ′_{a}, Δ_{n} \end{matrix}}{⊢ F &G, Δ′_{a}, Δ_{n}} &}{⊢ F &G, Δ′_{p}, Δ_{n}} I_{2}

Let us consider the proof

\frac{\frac{⊢ F, Δ′_{a}, Δ_{n}}{⊢ F, Δ′_{p}, Δ_{n}} I_{2} \frac{⊢ G, Δ′_{a}, Δ_{n}}{⊢ G, Δ′_{p}, Δ_{n}} I_{2}}{⊢ F &G, Δ′_{p}, Δ_{n}} &

It is correct because I_{2} does not depend on the context and then I_{1} is always permutable with I_{2}. 6.2) \underline{I_{2} has two premises}. I_{2} is then of the cut or ⊗ type and then Π has the form

\frac{\begin{matrix}: \\ ⊢ F, Δ_{a}^{′1}, Δ_{n} \end{matrix}  \begin{matrix}: \\ ⊢ G, Δ_{a}^{′1}, Δ_{n} \end{matrix}}{⊢ F &G, Δ_{a}^{′1}, Δ_{n}} & \begin{matrix}: \\ ⊢ Δ_{a}^{′2}, Δ′_{n} \end{matrix}

⊢ F &G, Δ′_{p}, Δ_{n}, Δ′_{n} I_{2}

Let us consider the proof

\frac{\frac{⊢ F, Δ_{a}^{′1}, Δ_{n} ⊢ Δ_{a}^{′2}, Δ′_{n}}{⊢ F, Δ′_{p}, Δ_{n}, Δ′_{n}} I′_{2} \frac{⊢ G, Δ_{a}^{′1}, Δ_{n} ⊢ Δ_{a}^{′2}, Δ′_{n}}{⊢ G, Δ′_{p}, Δ_{n}, Δ′_{n}} I′_{2}}{⊢ F &G, Δ′_{p}, Δ_{n}, Δ′_{n}} &

It is correct and then I_{1} is always permutable with I_{2}.

7) \underline{type(I_{i})_{i∈\{1,2\}} ∉ \{&,!, ∀\}}. 7.1) \underline{I_{1} and I_{2} have only one premise}. Π has the following form

\frac{\frac{\begin{matrix}: \\ ⊢ Δ_{a}, Δ′_{a}, Δ_{n} \end{matrix}}{⊢ Δ_{p}, Δ′_{a}, Δ_{n}} I_{1}}{⊢ Δ_{p}, Δ′_{p}, Δ_{n}} I_{2}

The following proof is correct (because I_{1} and I_{2} do not depend on the context).

\frac{\frac{\begin{matrix}: \\ ⊢ Δ_{a}, Δ′_{a}, Δ_{n} \end{matrix}}{⊢ Δ_{a}, Δ′_{p}, Δ_{n}} I′_{2}}{⊢ Δ_{p}, Δ′_{p}, Δ_{n}} I′_{1}

Then I_{1} is always permutable with I_{2}. 7.2) \underline{I_{1} has one premise and I_{2} has two premises}. I_{2} is of the cut or ⊗ type and then Π has the following form:

\frac{\begin{matrix}: \\ ⊢ Δ_{a}, Δ_{a}^{′1}, Δ_{n} \end{matrix}}{⊢ Δ_{p}, Δ_{a}^{′1}, Δ_{n}} I_{1} \begin{matrix}: \\ ⊢ Δ_{a}^{2}, Δ′_{n} \end{matrix}

⊢ Δ_{p}, Δ′_{p}, Δ_{n}, Δ′_{n} I_{2}

The following proof is correct (because I_{1} does not depend on the context).

\frac{\frac{⊢ Δ_{a}, Δ_{a}^{′1}, Δ_{n} ⊢ Δ_{a}^{′2}, Δ′_{n}}{⊢ Δ_{a}, Δ′_{p}, Δ_{n}, Δ′_{n}} I′_{2}}{⊢ Δ_{p}, Δ′_{p}, Δ_{n}, Δ′_{n}} I′_{1}

Then I_{1} is always permutable with I_{2}. 7.3) \underline{I_{1} has two premises and I_{2} has one premise}.

a) \underline{type(I_{2}) ∉ \{c?, ℘\}}. In this case, Δ′_{a} has at most one formula and then cannot be cut into two non-empty sets: it is completely included in one of the premises of I_{1} (for example, the left one).

\frac{\frac{\begin{matrix}: \\ ⊢ Δ_{a}^{1}, Δ′_{a}, Δ_{n} \end{matrix}  \begin{matrix}: \\ ⊢ Δ_{a}^{2}, Δ′_{n} \end{matrix}}{⊢ Δ_{p}, Δ′_{a}, Δ_{n}, Δ′_{n}} I_{1}}{⊢ Δ_{p}, Δ′_{p}, Δ_{n}, Δ′_{n}} I_{2}

The following proof is correct (because I_{1} does not depend on the context).

\frac{\begin{matrix}: \\ ⊢ Δ_{a}^{1}, Δ′_{a}, Δ_{n} \end{matrix}}{⊢ Δ_{a}^{1}, Δ′_{p}, Δ_{n}} I′_{2} \begin{matrix}: \\ ⊢ Δ_{a}^{2}, Δ′_{n} \end{matrix}

⊢ Δ_{p}, Δ′_{p}, Δ_{n}, Δ′_{n} I′_{1}

Then I_{1} is always permutable with I_{2}.

b) \underline{type(I_{2}) = ℘}. The following counter-examples show that, in this case, I_{1} is not always permutable with I_{2}.

\frac{\frac{_{\overline{⊢ A, A^{⊥}}  \overline{⊢ B, B^{⊥}}}}{⊢ A ⊗ B, A^{⊥}, B^{⊥}} ⊗}{⊢ A ⊗ B, A^{⊥}℘B^{⊥}} ℘  \frac{\frac{_{\overline{⊢ A, A^{⊥}}  \overline{⊢ B, B^{⊥}}}}{⊢ A, A^{⊥}} cut}{⊢ A℘A^{⊥}} ℘

c) \underline{type(I_{2}) = c?}. The following counter-examples show that, in this case, I_{1} is not always permutable with I_{2}.

\frac{\frac{\frac{\overline{⊢ A, A^{⊥}}}{⊢ A,?(A^{⊥})} ? \frac{\overline{⊢ A, A^{⊥}}}{⊢ A,?(A^{⊥})} ?}{⊢ A ⊗ A,?(A^{⊥}),?(A^{⊥})} ⊗}{⊢ A ⊗ A,?(A^{⊥})} c?

\frac{\frac{\frac{\frac{_{\overline{⊢ B, B^{⊥}}  \overline{⊢ A, A^{⊥}}}}{⊢ B^{⊥} ⊗ A^{⊥}, B, A} ⊗}{⊢ B^{⊥} ⊗ A^{⊥}, B,?A} d?  \frac{\frac{_{\overline{⊢ B, B^{⊥}}  \overline{⊢ A, A^{⊥}}}}{⊢ B ⊗ A^{⊥}, B^{⊥}, A} ⊗}{⊢ B ⊗ A^{⊥}, B^{⊥},?A} d?}{⊢ B^{⊥} ⊗ A^{⊥}, B ⊗ A^{⊥},?A,?A} cut}{⊢ B^{⊥} ⊗ A^{⊥}, B ⊗ A^{⊥},?A} c?

7.4) \underline{I_{1} and I_{2} have two premises}. I_{2} is of the cut or ⊗ type then Π has the following form:

\frac{\frac{\begin{matrix}: \\ ⊢ Δ_{a}^{1}, Δ_{a}^{′1}, Δ_{n} \end{matrix} \begin{matrix}: \\ ⊢ Δ_{a}^{2}, Δ′′_{n} \end{matrix}}{⊢ Δ_{p}, Δ_{a}^{′1}, Δ_{n}, Δ′_{n}} I_{1} \begin{matrix}: \\ ⊢ Δ_{a}^{2}, Δ′′_{n} \end{matrix}}{⊢ Δ_{p}, Δ′_{p}, Δ_{n}, Δ′_{n}, Δ′′_{n}} I_{2}.

The following proof is correct and then I_{1} is always permutable with I_{2}.

\frac{\frac{⊢ Δ_{a}^{1}, Δ_{a}^{′1}, Δ_{n} ⊢ Δ_{a}^{′2}, Δ′′_{n}}{⊢ Δ_{a}^{1}, Δ′_{p}, Δ_{n}, Δ′′_{n}} I′_{2} ⊢ Δ_{a}^{2}, Δ′′_{n}}{⊢ Δ_{p}, Δ′_{p}, Δ_{n}, Δ′_{n}, Δ′′_{n}} I′_{1}.

B Proof of theorem 5.1 (complexity reduction)

Theorem B.1 (complexity reduction) Let Π be a proof in LL of a sequent ⊢ Δ with only one cut, there exists a proof Π′ of ⊢ Δ such that c(Π′) < c(Π).

Proof B.1 Let I be the unique cut in Π. By theorem 4.3, there exists a proof Π′′, obtained by backward movement of I in Π, such that for any inference I’ resulting from this movement, I’ is immediately preceded by two inferences introducing the active formulae of I’. Thus, from definition 5.3, we have c(I’) which is equal to c(I). In fact, the problem is to reduce the complexity of each cut I’ considering the subproof Π_{1} of Π′′ ending with I’. Hence, Π_{1} has only one cut I’ and then c(Π_{1}) = c(I′) = c(Π). Let us consider such a cut I’, with several cases according to the form of the active formulae of I’.

1) \underline{The active formulae are atomic or constant}. Π_{1} can have three different forms:

a) \frac{_{\overline{⊢ ⊤, Δ} \overline{⊢ 0, ⊤, Δ′}}}{⊢ ⊤, Δ, Δ′}  b) \frac{\overline{⊢ 1}  \frac{\begin{matrix}: \\ ⊢ Δ \end{matrix} \}Π_{2}}{⊢ ⊥, Δ}}{⊢ Δ}  c) \frac{_{\overline{⊢ A, A^{⊥}}  \overline{⊢ A, A^{⊥}}}}{⊢ A, A^{⊥}}

In the case a), it can be replaced by the proof Π′_{1} ≡ \overline{⊢ ⊤, Δ, Δ′} with c(Π′_{1}) = 0 < c(Π_{1}). In the

case b), it can be replaced by the proof Π_{2} which contains no more cut and then c(Π_{2}) = 0 <

c(Π_{1}). Finally, in case c), it can be replaced by the proof Π′_{1} ≡ \overline{⊢ A, A^{⊥}} which contains no

more cut and then c(Π′_{1}) = 0 < c(Π_{1}).

2) \underline{The active formulae are of the ⊗ and ℘ type}. In this case, Π_{1} has the form

\frac{\frac{\begin{matrix}: \\ ⊢ F, Δ_{n} \end{matrix}  \begin{matrix}: \\ ⊢ G, Δ′_{n} \end{matrix}}{⊢ F ⊗ G, Δ_{n}, Δ′_{n}} ⊗ \frac{\begin{matrix}: \\ ⊢ F^{⊥}, G^{⊥}, Δ′′_{n} \end{matrix}}{⊢ F^{⊥}℘G^{⊥}, Δ′′_{n}} ℘}{⊢ Δ_{n}, Δ′_{n}, Δ′′_{n}} cut

and we can replace it by the following proof Π′_{1}

\frac{\begin{matrix}: \\ ⊢ F, Δ_{n} \end{matrix}  \begin{matrix}: \\ ⊢ F^{⊥}, G^{⊥}, Δ′′_{n} \end{matrix}}{⊢ G^{⊥}, Δ_{n}, Δ′_{n}} cut \begin{matrix}: \\ ⊢ G, Δ′_{n} \end{matrix}

⊢ Δ_{n}, Δ′_{n}, Δ′′_{n} cut

and we have c(Π′_{1}) = c(F) + c(F^{⊥}) and c(Π_{1}) = c(F ⊗ G) + c(F^{⊥}℘G^{⊥}) = sup{c(F), c(G)} + sup{c(F^{⊥}), c(G^{⊥})} +2. Then c(Π′_{1}) < c(Π_{1}).

3) \underline{The active formulae are of the ⊕ and & type}. In this case, Π_{1} has the form

\frac{\frac{\begin{matrix}: \\ ⊢ F, Δ_{n} \end{matrix}  \begin{matrix}: \\ ⊢ G, Δ_{n} \end{matrix}}{⊢ F &G, Δ_{n}} & \frac{\begin{matrix}: \\ ⊢ F^{⊥}, Δ′_{n} \end{matrix}}{⊢ F^{⊥} ⊕ G^{⊥}, Δ′_{n}} ⊕}{⊢ Δ_{n}, Δ′_{n}} cut

and we can replace it by the following proof Π′_{1}

\frac{\begin{matrix}: \\ ⊢ F, Δ_{n} \end{matrix}  \begin{matrix}: \\ ⊢ F^{⊥}, Δ′_{n} \end{matrix}}{⊢ Δ_{n}, Δ′_{n}} cut

and we have c(Π′_{1}) = c(F) + c(F^{⊥}) and c(Π_{1}) = c(F &G) + c(F^{⊥} ⊕ G^{⊥}) = sup{c(F), c(G)} + sup{c(F^{⊥}), c(G^{⊥})} +2. Then c(Π′_{1}) < c(Π_{1}).

4) \underline{The active formulae are of the ∀ and ∃ type}. In this case, Π_{1} has the form

\frac{\frac{Π_{2} \{ \begin{matrix}: \\ ⊢ F [y/x], Δ_{1} \end{matrix}}{⊢ ∀xF, Δ_{1}} w? \frac{\begin{matrix}: \\ ⊢ F^{⊥}[t/x], Δ_{2} \end{matrix}}{⊢ ∃xF^{⊥}, Δ_{2}} !}{⊢ Δ_{1},?Δ_{2}} cut

and we can replace it by the following proof Π′_{1}

\frac{Π′_{2} \{ \begin{matrix}: \\ ⊢ F [t/x], Δ_{1} \end{matrix} ⊢ F^{⊥}[t/x], Δ_{2}}{⊢ Δ_{1}, Δ_{2}}

when Π′_{2} is obtained from Π_{2} by substitution of F [t/x] to F [y/x] with a renaming of the variables that do not respect the condition on ∀ rule. Thus we have c(Π′_{1}) = c(F [t/x]) + c(F^{⊥}[t/x]) and c(Π_{1}) = c(F [t/x]) + c(F^{⊥}[t/x] + 2) and then c(Π′_{1}) < c(Π_{1}).

5) \underline{The active formulae are of the ! and ? type}. In this case, we have three subcases depending on the way the active formula of type ? has been introduced. 5.1) \underline{Introduction by an inference of the ? type}. In this case, Π_{1} has the form

\frac{\frac{\begin{matrix}: \\ ⊢ F, Δ_{n} \end{matrix}}{⊢?F, Δ_{n}} ? \frac{\begin{matrix}: \\ ⊢ F^{⊥},?Δ′_{n} \end{matrix}}{⊢!F^{⊥},?Δ′_{n}} !}{⊢ Δ_{n},?Δ′_{n}} cut

and we can replace it by the following proof Π′_{1}

\frac{\begin{matrix}: \\ ⊢ F, Δ_{n} \end{matrix}  \begin{matrix}: \\ ⊢ F^{⊥},?Δ′_{n} \end{matrix}}{⊢ Δ_{n},?Δ′_{n}} cut

and we have c(Π′_{1}) = c(F) + c(F^{⊥}) and c(Π_{1}) = c(F) + c(F^{⊥}) + 2. Then c(Π′_{1}) < c(Π_{1}). 5.2) \underline{Introduction by an inference of the w? type}. In this case, Π_{1} has the form

\frac{\frac{Π_{2} \{ \begin{matrix}: \\ ⊢ Δ_{n} \end{matrix}}{⊢?F, Δ_{n}} w? \frac{\begin{matrix}: \\ ⊢ F^{⊥},?Δ′_{n} \end{matrix}}{⊢!F^{⊥},?Δ′_{n}} !}{⊢ Δ_{n},?Δ′_{n}} cut

and we can replace it by the following proof Π′_{1}

\frac{Π_{2} \{ \begin{matrix}: \\ ⊢ Δ_{n} \end{matrix}}{\begin{matrix}: \\ ⊢ Δ_{n},?Δ′_{n} \end{matrix}}

and we have c(Π′_{1}) = 0 < c(Π_{1}). 5.3) \underline{Introduction by an inference of the c? type}. In this case, Π_{1} has the form

\frac{\frac{\begin{matrix}: \\ ⊢?F,?F, Δ_{n} \end{matrix}}{⊢?F, Δ_{n}} c? \frac{\begin{matrix}: \\ ⊢ F^{⊥},?Δ′_{n} \end{matrix}}{⊢!F^{⊥},?Δ′_{n}} !}{⊢ Δ_{n},?Δ′_{n}} cut

and we can replace it by the following proof Π′_{1}

\frac{\begin{matrix}: \\ ⊢?F,?F, Δ_{n} \end{matrix}  \begin{matrix}: \\ ⊢!F^{⊥},?Δ′_{n} \end{matrix}}{⊢?F, Δ_{n},?Δ′_{n}} cut \begin{matrix}: \\ ⊢!F^{⊥},?Δ′_{n} \end{matrix}

⊢ Δ_{n},?Δ′_{n},?Δ′_{n} cut

\begin{matrix}: \\ ⊢ Δ_{n},?Δ′_{n} \end{matrix} c?

and we have c(Π′_{1}) = c(?F) + c(!F^{⊥}) and c(Π_{1}) = 1 + c(Π′_{1}). Then c(Π′_{1}) < c(Π_{1}).