Provability in TBLL: A Decision Procedure ^{∗}

Jawahar Chirimar CIS University of Pennsylvania and James Lipton Dept. of Mathematics Wesleyan University

Abstract

We prove the decidability of the Tensor-Bang fragment of linear logic and establish upper (doubly exponential) and lower (NP-hard) bounds.

1 Introduction

Since Lincoln et al. [9] discovered in 1990 that propositional linear logic is undecidable, there has been a great deal of interest in determining the complexity of different fragments. Gehlot and Gunter [2, 5] established in 1991 that provability in the tensor fragment of linear logic with proper axioms (PrTLL) was equivalent to the reachability problem for Petri nets, whose decidability was established in 1982 in a difficult paper [8] by Kosaraju. It follows easily that the multiplicative-bang ( ⊗,−∘, !) fragment, MBLL (also called MELL) can encode Petri Net reachability. On the other hand it is known that MALL (the exponent-free or multiplicative-additive fragment of linear logic) is decidable (and PSPACE-complete) and that MLL is NP-complete [7] (see also below). It is thus of great interest to understand the “boundary” region (TBLL, PrTLL, MBLL) both to pin down as much as possible where undecidability happens as possibly to shed more light on the complexity of Petri Net reachability from a linear logic perspective.

Here we investigate the first such fragment, using a direct analysis of deduction somewhat in the spirit of formal language theory. We begin with the ground rules. The tensor-bang fragment of linear logic (TBLL) is comprised of the following symbols and rules of inference. The language consists of a (linearly ordered) set Σ of propositional letters {A_{1}, …, A_{n}}. The logical constants are the binary connective tensor (⊗) and the unary (prefix) connective bang^{1} (!).

∗An abbreviated version appeared in the proceedings of Computer Science Logic (CSL) ’91, LNCS 626, Springer, 1992.

1also called “of course”

Rules of Inference: Sequents Γ ⊢ θ consist of finite sequences Γ of propositions (separated by commas) and single propositions θ. In the rule called “axiom”, only propositional letters occur.

A ⊢ A “axiom”
\frac{Γ, φ, ψ, Λ ⊢ φ}{Γ, φ ⊗ ψ, Λ ⊢ φ}  ⊗ intro-left (⊗L)  \frac{Γ ⊢ φ  Λ ⊢ ψ}{Γ, Λ ⊢ φ ⊗ ψ}  ⊗ intro-right (⊗R)

\frac{Γ, θ ⊢ φ}{Γ,!θ ⊢ φ}  Dereliction (D)  \frac{Γ,!θ,!θ ⊢ φ}{Γ,!θ ⊢ φ}  Contraction (C)

\frac{Γ ⊢ φ}{Γ,!θ ⊢ φ}  Weakening (W)  \frac{!Γ ⊢ φ}{!Γ ⊢!φ}  ! -introduction (!I)

The only structural rules are exchange (×):

\frac{Γ, φ, ψ, Δ ⊢ θ}{Γ, ψ, φ, Δ ⊢ θ}

and cut

\frac{Γ ⊢ θ Δ, θ ⊢ φ}{Γ, Δ ⊢ φ}.

The following result will simplify our work below.

Theorem 1.1 TBLL admits cut-elimination.

The proof is almost identical to that for the full propositional logic. See e.g. [4].

2 A decision algorithm for deducibility in TBLL

To begin with we will need a series of translations and technical lemmas to define our main algorithm.

Definition 2.1 A formula α is in TLL (tensor-linear logic) if it is built up from propositional letters using only the connective ⊗.

Definition 2.2 A formula in TBLL is called banged if it is of the form !α where α is any TBLLformula, or if it is of the form α⊗β where α and β are banged^{2}. For a multiset Γ, ⊗Γ is the tensor product of all the formulas in Γ. A multiset Γ is banged if ⊗Γ is.

The following properties of banged formulas will be useful.

Lemma 2.3 The weakening and contraction rules of inference remain valid for arbitrary banged formulas β in place of !θ above. We can also replace the premiss in the rule of !-introduction by any banged formula.

2This agrees with Girard’s recent definition of positive polarity of a formula

The proof is immediate by structural induction.

We define a canonical form which will be repeatedly used in the sequel.

Lemma 2.4 (decomposition lemma) Every TBLL formula α is either

1. in TLL or

2. banged or

3. equivalent (with respect to TBLL-deducibility) to a formula of the form α_{0} ⊗ α_{1} where α_{0} is in TLL and α_{1} is banged.

proof: If (1) and (2) do not hold, then α is of the form γ ⊗ δ where not both γ and δ are in TLL. Inducting on length of formulas, and applying the tensoring rules of inference, there is a formula γ_{0} ⊗ γ_{1} ⊗ δ_{0} ⊗ δ_{1}, with γ_{0} and δ_{0} in TLL, γ_{1} and δ_{1} banged, which is equivalent to α (the cases γ in TLL, δ in TLL are left to the reader). Therefore α ≡ (γ_{0} ⊗ δ_{0}) ⊗ (γ_{1} ⊗ δ_{1}).

We will call case (3) in the statement of the previous lemma a decomposition of a TBLL formula α. The first formula will be called the unbanged or pure tensor part of the decomposition. Formulas in case (3) are said to be nontrivial, or to have a nontrivial decomposition.

We first tackle the problem of deciding when one can deduce sequents of the form Γ ⊢ α with Γ in TBLL and α in TLL. The number of occurrences of each letter of Σ in α will help determine the possible replications (contractions) of banged formulas in the antecedent required in the associated deduction we are trying to reconstruct. In order to make this precise we define the notion of an instance of a TBLL formula, namely a certain expression obtained by “decorating” the ! symbols with natural numbers.

Definition 2.5 (instances) Let γ be a TBLL formula.

1. If γ is an atom A, then A is the sole instance of γ.

2. \frac{!}{0}(δ′) is an instance of !δ if and only if (δ′) is an instance of δ and every ! in the subexpression (δ′) is instantiated to 0.

3. \frac{!}{m}(δ′) (m > 0) is an instance of !δ if δ′ is an instance of δ and m is a natural number.

4. δ′ ⊗ γ′ is an instance of δ ⊗ γ if δ′ (resp. γ′) is an instance of δ (resp. γ).

It will also be convenient to define a symbolic version of an instance.

Definition 2.6 A symbolic instance of a TBLL formula is an indexing of every ! with a fresh variable.

Note that if we pick a standard list of variables, and demand that consecutive variables be used as we proceed along the formula from left to right, a symbolic instance of a formula is unique. We now define a translation from TBLL formulas to a “polynomial expression” in the propositional letters of the language.

Definition 2.7 Σ-polynomial expressions are (ordered) expressions of the form

A_{1}^{e_{1}}A_{2}^{e_{2}} ⋯ A_{n}^{e_{n}}

where A_{i} ∈ Σ, A_{i} < A_{i+1} in the Σ-order, and each e_{i} is a sum ∑_{ij} e_{ij} of terms of the form k_{ij} or k_{ij}x_{ij} where k_{ij} is a natural number and x_{ij} a variable. The product of two such expressions A_{1}^{i_{1}}A_{2}^{i_{2}} ⋯ A_{n}^{i_{n}} and A_{1}^{j_{1}}A_{2}^{j_{2}} ⋯ A_{n}^{j_{n}} is A_{1}^{i_{1}+j_{1}}A_{2}^{i_{2}+j_{2}} ⋯ A_{n}^{i_{n}+j_{n}}.

Let θ′ be a symbolic instance of a proposition of TBLL. We define the polynomial form of θ′ to be the following Σ-polynomial expression p(θ′), by induction on the structure of θ′:

1. p(A) ≡^{def} A for A ∈ Σ.

2. p(β′ ⊗ γ′) ≡^{def} p(β′)p(γ′)

3. p(\frac{!}{x}γ′) ≡^{def} p(γ′)^{(x)} where we define the exponent (θ′)^{(x)} as follows:

• A^{(x)} ≡^{def} A^{x}

• (uv)^{(x)} ≡^{def} u^{(x)}v^{(x)}

• (u^{(y)})^{(x)} ≡^{def} u^{(y)}

We will also call such an expression a polynomial form of the original TBLL-formula θ itself.

Note in the preceding definition that p and the exponent are defined via a series of rewrite rules. Strictly speaking p(θ) is the polynomial obtained by applying the above rewritings until a polynomial expression results (which is unique, once Σ is ordered, up to the names of the variables). Also note that the translation proceeds somewhat like an instantiation of regular expressions (with ! taking the place of ∗) except for the unusual iterated exponentiation “law” (u^{(y)})^{(x)} ≡^{def} u^{(y)} Note also that for α in TLL, p(α) has no variables, and is essentially a lexicographical re-ordering of α. When instantiated with natural numbers, the exponents of the polynomials just defined will correspond to certain choices of instantiations (copies) of banged formulas in the proof theory.

We are now in a position to define a string test which will be repeatedly used in our decision procedure, and which is, as we shall see below, sufficient to decide the special case Γ ⊢ α when α is in TLL.

Definition 2.8 Let Γ and α be propositions in TBLL and TLL respectively. Then the pair ⟨Γ, α⟩ is said to satisfy the string test (in symbols Γ ⊧_{s} α) if 1. There are natural number values for the variables in the polynomials p(⊗(Γ)), p(α) such that

the following equation has a solution:

p(⊗(Γ)) = p(α)  (1)

and

2. These numerical values for the variables in p(⊗(Γ)) correspond to a legal instance (in the sense of definition 2.5) of the original formula (multiset) Γ when substituted for the same variables in the corresponding symbolic instance of θ. In particular any solution to 1 that results in the assignment of a nonzero decoration to a bang within the scope of a \frac{!}{0} does not qualify.

We remark that certain variables from the symbolic instance of θ may not occur in p(θ) because of the collapse of exponents. This is always the case when there is a subformula of θ of the form !α where α is banged. In this case, our notion of “checking the legality” of a solution to equation (1) requires comment. We first replace those variables which occur in the polynomial equation with their numerical values. Then all uninstantiated variables in the scope of a \frac{!}{0} are set equal to 0. All the remaining ones are set equal to 1.

We will call an instantiation of the variables in p(θ) a polynomial instance for θ. If α is in TLL, Γ is in TBLL, and Γ ⊧_{s} α, we call the corresponding instance of Γ the one “induced by the string test” Γ ⊧_{s} α.

In the next definition and the lemma that follows it, it will be convenient to introduce the TLLunit 1. For the purposes of the lemma we add the axiom ⊢ 1 as a legal proof rule to the rules of TBLL. We call the resulting fragments T(B)LL1.

Definition 2.9 Every instance θ has an associated TLL-normal form, namely the TLL1 formula obtained as follows.

1. T (A) ≡^{def} A for A ∈ Σ.

2. T (β ⊗ γ) ≡^{def} T (β) ⊗ T (γ)

3. T (\frac{!}{0}γ) ≡^{def} 1

4. T (\frac{!}{m}γ) (0 < m) ≡^{def} \underbrace{α ⊗ ⋯ ⊗ α}_{m times} ⊗T (β) where α ⊗ β is the canonical decomposition of γ (i.e.

α in TLL and β banged).

We lift the definition of instances to multisets of formulas in the obvious way.

Lemma 2.10 Let γ be in TBLL. Then for any instance γ′ of γ. the following sequent is derivable in TBLL1: γ ⊢ T (γ′).

proof: The proof is by induction on the structure of γ 1. If γ is an atom A then its instance is A. The conclusion is immediate.

2. Suppose γ is ϕ ⊗ δ. By definition we have that T (ϕ′ ⊗ δ′) = T (ϕ′) ⊗ T (δ′). The result is thus obtained by induction hypothesis and ⊗ − R.

3. Suppose γ is !ϕ. By definition we have that T (\frac{!}{0}ϕ′) = 1. But then we have the deduction

\frac{⊢ 1}{!ϕ ⊢ 1}w

If m > 0 we have

T (\frac{!}{m}ϕ′) = \underbrace{α ⊗ ⋯ ⊗ α}_{m times} ⊗T (β′)

where α ⊗ β is a canonical decomposition of ϕ, and β′ is an instance of β. We take m to be 2 for ease of notation below. The induction hypothesis β ⊢ T (β′) along with uses of ⊗ − R and the derived rule of weakening for banged formulas completes the proof shown below.

\frac{\frac{\frac{α, β, α, β ⊢ α ⊗ α ⊗ T (β′)}{ϕ, ϕ ⊢ α ⊗ α ⊗ T (β′)}^{(⊗−L)}}{!ϕ,!ϕ ⊢ α ⊗ α ⊗ T (β′)}^{(D)}}{!ϕ ⊢ α ⊗ α ⊗ T (β′)}^{(C)}

We give an example:

p(A⊗!(B⊗!A) ⊗ (!(A⊗!B ⊗ B))) = p(A ⊗ \frac{!}{x}(B ⊗ \frac{!}{y}A) ⊗ (\frac{!}{z}(A ⊗ \frac{!}{u}B ⊗ B))) = A^{1+y+z}B^{x+u+z}. (2)

If we take, e.g., x = 2, y = 2, z = 0 and u = 0 we obtain the instance

A ⊗ \frac{!}{2}(B ⊗ \frac{!}{2}A) ⊗ (\frac{!}{0}(A ⊗ \frac{!}{0}B ⊗ B))

The corresponding polynomial instance is A^{3}B^{2} and the associated tensor normal form is

A ⊗ A ⊗ A ⊗ B ⊗ B.

We consider a join operation on instances.

Definition 2.11 (join) Let C′, C′′ be instances of the TBLL-formula C. We define the join C′⋈C′′ as follows:

• If C is an atom A, C⋈C = C • If C is of the form !θ, with C′ = \frac{!}{m}θ′ and C′′ = \frac{!}{n}θ′′ then

\frac{!}{m}θ′⋈\frac{!}{n}θ′′ = \frac{!}{m+n}θ′⋈θ′′

• If C is of the form α ⊗ β, and C′ = α′ ⊗ β′ and C′′ = α′′ ⊗ β′′ then

(α′ ⊗ β′)⋈(α′′ ⊗ β′′) = (α′⋈α′′) ⊗ (β′⋈β′′)

Observe that if α is in TLL then α⋈α is α.

Lemma 2.12 (TLL-join lemma) Let γ′and γ′′ be instances of the same banged formula γ

T (γ′⋈γ′′) ⊢ T (γ′) ⊗ T (γ′′)

proof: Suppose γ =!φ. Then γ′, γ′′ are of the form \frac{!}{m}φ′ and \frac{!}{n}φ′′ for some m and n. Then we have

T (γ′⋈γ′′) = T (\frac{!}{m}φ′⋈\frac{!}{n}φ′′) = T (\frac{!}{n+m}φ′⋈φ′′)  (3)

Let α⊗β be the canonical decomposition of φ. Then φ′⋈φ′′ must be equivalent to α⊗(β′⋈β′′) where β′, β′′ are the instances of β occurring in the instances φ′, φ′′. By definition of T, the expressions in (3) are equivalent to

\underbrace{α ⊗ ⋯ ⊗ α}_{m + n times} ⊗T (β′⋈β′′).

This is easily shown equivalent to T (\frac{!}{m}φ′) ⊗ T (\frac{!}{n}φ′′) once we apply the definition of T and the induction hypothesis to β′ and β′′. The case θ = δ ⊗ γ is a straightforward induction and rearrangement of tensorands. The reader can easily check that in the \frac{!}{0} cases the appropriate TBLL1 sequent is provable. In particular if the left hand side is 1 or a tensor of 1’s, the right hand side must also be of this form.

Theorem 2.13 Let α be a proposition in TLL logic, and Γ a formula in TBLL. Then

Γ ⊢ α  iff  Γ ⊧_{s} α.

proof: We establish “soundness” ( Γ ⊢ α ⇒ Γ ⊧_{s} α) by induction on the length of proofs. If Γ ⊢ α is a one step proof by “axiom”: A ⊢ A then the polynomials are identical. Now suppose that Γ ⊢ α is a proof with n + 1 steps and inductively assume soundness holds

for all proofs of shorter length. We consider the possible cases for the last step of the proof.

case ⊗R The last step in the proof is an inference of the form

\frac{Δ ⊢ β Λ ⊢ γ}{Δ, Λ ⊢ β ⊗ γ} .

By the induction hypothesis and the definition of p the result is immediate. case ⊗ − L Soundness for tensor left is built into the definition of the string-test.

case D The last step is an inference using dereliction:

\frac{Δ, θ ⊢ α}{Δ,!θ ⊢ α}.

we can obtain a solution to p(Δ⊗!θ) = p(α) by using the instantiations obtained by inductive hypothesis, extended to the new premiss by taking the variable corresponding to the introduced ! to be 1 (assuming it is not eliminated due to collapse of exponents).

case C Suppose the last step in the proof is an instance of the rule of contraction:

\frac{Γ,!θ,!θ ⊢ α}{Γ,!θ ⊢ α}

By induction there is a polynomial instance of the left hand side of the sequent Γ,!θ,!θ ⊢ α agreeing with p(α) and satisfying the legality criterion of the string test. Note that the polynomial instances u and v corresponding to the first and second indicated occurrences of !θ may be different. Let i_{1} …, i_{n} and j_{1} …, j_{n} be the corresponding instantiations of exponents in u and v. Observe that the sequence of natural numbers i_{1} + j_{1}, …, i_{n} + j_{n} instantiating the polynomial associated with the indicated occurrence of !θ in the sequent Γ,!θ ⊢ α, satisfies

p(Γ,!θ) = p(α).

The instance is legal, since, if some \frac{!}{i_{r} + j_{r}} occurs on the scope of a \frac{!}{i_{s} + j_{s}} where i_{s} + j_{s} = 0 then i_{s} = j_{s} = 0 so by legality of the original solutions, i_{r} = j_{r} = 0.

case W Suppose the last rule used was weakening:

\frac{Γ, ⊢ α}{Γ,!θ ⊢ α}

by inductive hypothesis we have a solution to

p(Γ) = p(α)

By instantiating all the variables associated with the indicated !θ to 0 we get a solution for

p(Γ⊗!θ) = p(α)

case × This is true by induction hypothesis and the fact that the polynomials are unaffected by exchange.

Now we prove the other direction: “completeness” (Γ ⊧_{s} α ⇒ Γ ⊢ α), i.e., if there is a solution to p(Γ) = p(α) then Γ ⊢ α. Lemma 2.10 gives us that Γ ⊢ T (Γ′), for any instance Γ′ of Γ. It is easy to show that the instance obtained by the String Test is some permutation of α, thus Γ proves T (Γ′) and T (Γ′) proves α. Hence by Cut we are done.

The string test algorithm

The string test problem, and hence the decidability of the TBLL-TLL -fragment is NP-Complete.

Lemma 2.14 (NP-hardness) Provability in the TBLL/TLL-fragment is NP-hard.

proof: The set cover decision problem is a well known NP-complete problem (see e.g. [1, 6]). We give a brief description here. Let F = {S_{j}} be a finite family of finite sets. Let T be a subset of F. We say T is a cover of F if

⋃_{S_{i}∈T} S_{i} = ⋃_{S_{i}∈F} S_{i}.

Let k be a natural number. The set cover decision problem is, given inputs ⟨F, k⟩, to determine if there is a cover of F containing k sets.

We now show that this problem can be reduced to provability in TBLL/TLL. Suppose F = {S_{j} : 1 ≤ j ≤ n} and

S_{j} = {s_{j1}, …, s_{jt_{j}}} (1 ≤ j ≤ n)

and define Σ = ⋃_{1}^{n} S_{j}. Suppose Σ = {a_{1}, …, a_{l}}. Introduce propositional letters A_{1}, …, A_{l} (one for each of the elements a_{i}), B_{1}, …, B_{n} (one for each of the members of F) and an additional letter Z. Then we claim that the set-cover problem ⟨F, k⟩ has a positive solution if and only if the following sequent is derivable in TBLL:

(!B_{1} ⊗ ⋯ ⊗!B_{n})⊗
! [(!s_{11} ⊗ ⋯ ⊗!s_{1t_{1}}) ⊗ Z ⊗ B_{1}] ⊗ ⋯ ⊗! [(!s_{n1} ⊗ ⋯ ⊗!s_{nt_{n}}) ⊗ Z ⊗ B_{n}]
⊢
(A_{1} ⊗ A_{2} ⊗ ⋯ ⊗ A_{l}) ⊗ Z^{k} ⊗ (B_{1} ⊗ ⋯ ⊗ B_{n}).  (4)

In order to discuss our claim it will be convenient to selectively instantiate certain of the ! symbols in (4). Consider

(!B_{1} ⊗ ⋯ ⊗!B_{n})⊗

\frac{!}{ξ_{1}} [(!s_{11} ⊗ ⋯ ⊗!s_{1t_{1}}) ⊗ Z ⊗ B_{1}] ⊗ ⋯ ⊗ \frac{!}{ξ_{n}} [(!s_{n1} ⊗ ⋯ ⊗!s_{nt_{n}}) ⊗ Z ⊗ B_{n}]

⊢
(A_{1} ⊗ A_{2} ⊗ ⋯ ⊗ A_{l}) ⊗ Z^{k} ⊗ (B_{1} ⊗ ⋯ ⊗ B_{n}).  (5)

Observe that if the sequent is provable, only instantiations of 0 or 1 for the ξ_{i} could have occurred in the string test. Otherwise one of the B_{i} would occur more than once on the left and only once on the right. Observe that the presence of (!B_{1} ⊗ ⋯ ⊗!B_{n}) in the top row of the sequent is to supply one copy of B_{i} if the instantiation of ξ_{i} induced by the string test is 0. An instantiation of ξ_{i} to 1 corresponds to the inclusion of the ith set in the cover. We also note that the letters A_{1}, …, A_{l} each occur only once on the right hand side of the sequent, but may occur more than once (as one of the s_{ij}) on the left. This is the reason each s_{ij} occurs with a ! in each of the tensorands [(!s_{i1} ⊗ ⋯!s_{it_{i}}) ⊗ Z ⊗ B_{i}], so that it may be instantiated to 0 if the letter has already occurred as s_{uv} for some u < i. We illustrate with an example and leave the details to the reader. Let

F = \{ \begin{matrix}\{1, 2, 4, 7\} \\ \{2, 6, 7, 8\} \\ \{1, 3, 6\} \\ \{1, 2, 3, 4\} \\ \{2, 6, 8\} \end{matrix} \}

and let k= 3. The set-cover problem for ⟨F, 3⟩ has the positive solution {1, 2, 4, 7}{2, 6, 7, 8}{1, 3, 6}, the union of which is the set {1, 2, 3, 4, 6, 7, 8}. The test-sequent for this problem is produced as follows. We introduce letters A_{1}, A_{2}, A_{3}, A_{4}, A_{6}, A_{7}, A_{8} corresponding to the members of ⋃ F, as well as B_{1}, …, B_{5} and Z as described above. The associated sequent, then, is

(!B_{1} ⊗ ⋯ ⊗!B_{5})⊗
! [(!A_{1}⊗!A_{2}⊗!A_{4}⊗!A_{7}) ⊗ Z ⊗ B_{1}] ⊗! [(!A_{2}⊗!A_{6}⊗!A_{7}⊗!A_{8}) ⊗ Z ⊗ B_{2}] ⊗
! [(!A_{1}⊗!A_{3}⊗!A_{6}⊗) ⊗ Z ⊗ B_{3}] ⊗  (6)
[(!A_{1}⊗!A_{2}⊗!A_{3}⊗!A_{4}) ⊗ Z ⊗ B_{4}] ⊗! [(!A_{2}⊗!A_{6}⊗!A_{8}⊗) ⊗ Z ⊗ B_{5}]
⊢
(A_{1} ⊗ A_{2} ⊗ A_{3} ⊗ A_{4} ⊗ A_{6} ⊗ A_{7} ⊗ A_{8}) ⊗ Z^{3} ⊗ (B_{1} ⊗ ⋯ ⊗ B_{5}).  (7)

It is easy to check that the following instantiations, which reflect the set-cover solution given above satisfy the string test:

(\frac{!}{0}B_{1} ⊗ \frac{!}{0}B_{2} ⊗ \frac{!}{0}B_{3} ⊗ \frac{!}{1}B_{4} ⊗ \frac{!}{1}B_{5})⊗

\frac{!}{1} [(\frac{!}{1}A_{1} ⊗ \frac{!}{1}A_{2} ⊗ \frac{!}{1}A_{4} ⊗ \frac{!}{1}A_{7}) ⊗ Z ⊗ B_{1}] ⊗ \frac{!}{1} [(\frac{!}{0}A_{2} ⊗ \frac{!}{1}A_{6} ⊗ \frac{!}{0}A_{7} ⊗ \frac{!}{1}A_{8}) ⊗ Z ⊗ B_{2}] ⊗

\frac{!}{1} [(\frac{!}{0}A_{1} ⊗ \frac{!}{1}A_{3} ⊗ \frac{!}{0}A_{6}⊗) ⊗ Z ⊗ B_{3}] ⊗  (8)

\frac{!}{0} [(!A_{1}⊗!A_{2}⊗!A_{3}⊗!A_{4}) ⊗ Z ⊗ B_{4}] ⊗ \frac{!}{0} [(!A_{2}⊗!A_{6}⊗!A_{8}⊗) ⊗ Z ⊗ B_{5}]

⊢

(A_{1} ⊗ A_{2} ⊗ A_{3} ⊗ A_{4} ⊗ A_{6} ⊗ A_{7} ⊗ A_{8}) ⊗ Z^{3} ⊗ (B_{1} ⊗ ⋯ ⊗ B_{5}).  (9)

Lemma 2.15 (NP-completeness) Provability in the TBLL/TLL-fragment is NP-complete.

proof: This is almost immediate from the discussion of the deterministic string-algorithm in the next paragraph. To show a test sequent Γ ⊢ α derivable one has to guess the value (in the equations (10) below) of as many variables as there are ! symbols in the sequent. Each value is bounded by the number of occurrences of letters in α hence both the number of guesses and the values are bounded by the length of the test sequent.

We can describe a deterministic string test algorithm informally as follows. The input is an ordered pair ⟨Γ, α⟩ with Γ in TBLL and α in TLL. We then compute the polynomial forms p(α) and p(⊗Γ) associated with these formulas (see definition 2.7). For α in TLL, p(α) is an expression of the form

A_{1}^{f_{1}}A_{2}^{f_{2}} ⋯ A_{n}^{f_{n}}

and p(Γ) is of the form

B_{1}^{e_{1}}B_{2}^{e_{2}} ⋯ B_{m}^{e_{m}}

where the f_{i} > 0 are natural numbers and the e_{j} are sums of terms of the form k_{ij} or k_{ij}x_{ij}.

The string test algorithm checks that every A_{i} is among the B_{j}. If A_{i} matches B_{j} then we get an equation f_{i} = e_{j} else it fails as f_{i} = 0 has no solution. If all letters in A_{i}’s are found among the B_{j}’s then we get a set of equations of the following kind.

f_{1} = e_{i_{1}}  (10)
⋮
f_{n} = e_{i_{n}}
⋮
0 = e_{i_{m}}  (11)

Then it tries to solve these equations using bounded search, the bound being given by f_{j} for the variables in e_{i_{j}}. Moreover the algorithm checks that the solution corresponds to a legal instantiation of Γ (in the sense of definition 2.5).

The number of variables in e_{i} is bounded by b_{Γ}, the number of bangs in Γ and f_{i} are bounded by l_{α}, the length of α. Thus the search is bounded by O(l_{α}^{b_{Γ}}).

An Example

Consider the candidate sequent “A⊗!(B⊗!A) ⊗ (!(A⊗!B ⊗ B)) ⊢ A ⊗ (B ⊗ A).” Applying the string test reduces to finding if there are x, y, z, u ∈ N for which

2 = 1 + y + z
1 = x + u + z

x = 1, y = 1, u = z = 0 is a solution, and a legal instance, so the test succeeds, showing that the sequent is in fact derivable. Of course, the test can always be performed by a bounded search. Each equation generated is of the form

k = a_{1}x_{1} + a_{2}x_{2} + ⋯ + a_{m}x_{m}

where each a_{i} on the right is a natural number, and each x_{i} on the right satisfies 0 ≤ x_{i} ≤ k.

The following example suggests that there is no immediate generalization of the string test to deal with the general case of TBLL-sequents. Consider Γ :=!(A ⊗ A ⊗ A)⊗!(A ⊗ A) and θ := A ⊗ A⊗!A.

The set of polynomial instances of Γ is {A^{3x+2y} : x, y ∈ N} which is precisely the same set {A^{x+2z} : z ∈ N} of instances associated with θ (Using a little algebra: the set {3x + 2y : x, y ∈ N} is the (semi)- ideal of N generated by gcd(3,2) intersected with the set of numbers greater than (3-1)(2-1) = 2). However Γ ⊬ θ and θ ⊬ Γ, as can be checked using the algorithm described next.

Now we are ready to deal with general TBLL-sequents.

Definition 2.16 (reductions) Let θ′ be an instance of a TBLL-formula φ (i.e. a decoration of every ! in the original formula with a numerical subscript, as in definition 2.5). We abuse language and define a decomposition of the instance θ′ to be the “decorated” decomposition of the original formula φ in which we retain the subscripts of the instance θ′. Let the reduced form r(θ′) be the following associated TBLL-formula defined by induction on the structure of θ′. Primed formulas denote instances, and are dropped for TLL-formulas, (whose sole instances are themselves).

1. r(a) = a (a an atom).

2. r(φ′ ⊗ ψ′) = r(φ′) ⊗ r(ψ′)

3. r(\frac{!}{0}φ′) =!φ.

4. r(\frac{!}{k}φ′) (k > 0) =!φ ⊗ α^{k} ⊗ r(β′), where α ⊗ β′ is a decomposition of φ′.

We establish a few properties of the reduction r.

Lemma 2.17 Let φ be any TBLL-formula, with instance φ′. Then

φ ⊢ r(φ′)

proof: By structural induction. The atomic case is axiom. In the case that φ′ is a tensor, the result is immediate from the induction hypothesis. Suppose φ′ is \frac{!}{m}ψ′. Then use the induction hypothesis on ψ′ together and the derived rules of weakening and contraction on banged formulas (2.3) to obtain the proof.

Lemma 2.18 Let α ⊗ β be a decomposition of a nontrivial TBLL-formula. Then

Γ ⊢ α ⊗ β  ⇒  Γ ⊧_{s} α.

proof: It is clear that α ⊗ β ⊢ α, by weakening on β which is banged (2.3). By the cut rule Γ ⊢ α. Now by the Soundness of the String Test we get the result.

Lemma 2.19 Suppose α is in TBLL and it is banged. If Γ ⊢ α then Γ is banged.

proof: The lemma is shown by an easy induction on proofs. The only rule to check is that of ⊗ − R, as in all other rules if the context Γ is banged prior to the application of the rule then it remains so after the application.

\frac{Γ_{0} ⊢ β Γ_{1} ⊢ δ}{Γ_{0}, Γ_{1} ⊢ β ⊗ δ} .

then Γ_{0} and Γ_{1} are banged by induction hypothesis, hence so is Γ ≡ Γ_{0}, Γ_{1}.

Definition 2.20 Let γ′ be an instance of the TBLL formula γ. The !-closure γ̂′ of γ′ is a banged formula (or the empty multiset) defined inductively as follows.

• If a is an atom â is the empty multiset.

• ˆ \frac{!}{0}θ′ is !θ.

• ˆ \frac{!}{m}θ′ is !θ ⊗ θ̂′ (m > 0).

• θ̂′ ⊗ γ′ is θ̂′ ⊗ γ̂′

Lemma 2.21 (TBLL-join lemma) Let γ′and γ′′ be instances of the same banged formula γ

γ̂′⋈γ′′ ⊢ γ̂′ ⊗ γ̂′′

The proof of this is a straight forward induction on the structure of the formula, and is quite similar to the proof of TLL-join lemma.

Theorem 2.22 (bang-closure theorem) Let α ⊗β be a decomposition of a TBLL-formula, and suppose

Λ ⊢ α ⊗ β.

Then there is an instance Λ′ of Λ such that

T (Λ′) ⊢ α

and

Λ̂′ ⊢ β.

Conversely, suppose α is in TLL, β is a banged formula, and Λ ⊧_{s} α, inducing an instance Λ′. Then

Λ̂′ ⊢ β ⇒ Λ ⊢ α ⊗ β

proof: ( ⇒ ) Suppose Λ ⊢ α ⊗ β. By the preceding lemma Λ ⊧_{s} α, i.e., we have solution to p(Λ) = p(α) which yields an instance Λ′. Now by lemma 2.10 we have that T (Λ′) ⊢ α.

Now we show Λ̂′ ⊢ β. By the cut elimination theorem, there is a proof of Λ ⊢ α ⊗ β whose last right-introduction is (⊗ − R) resulting in the formation of α ⊗ β, i.e., there is a proof of the form:

\frac{\frac{\frac{Δ_{0} ⊢ α  Δ_{1} ⊢ β}{Δ_{0}, Δ_{1} ⊢ α ⊗ β}}{⋮  \} (∗)}}{Λ ⊢ α ⊗ β}  (12)

where the final steps are left introductions. Our proof that Λ̂′ ⊢ β will be by induction on the length of the displayed proof of Λ ⊢ α ⊗ β starting from Δ_{0}, Δ_{1} ⊢ α ⊗ β, in particular on the length n of the “mid-section” (*). Our induction hypothesis is that if the proof above has length n then Λ ⊧_{s} α and for the instance Λ′ induced by the string test, Λ̂′ ⊢ β.

Base case: If n = 0 then Λ is Δ_{0}, Δ_{1} and we must show that Δ̂_{0}′, Δ̂_{1}′ ⊢ β. Since the bangclosure of a formula is banged, it suffices to notice that for banged formulas φ, φ̂′ ⊢ φ (almost immediate from the definition). As Λ_{1} is banged as β is, then we have Δ̂_{1}′ ⊢ Δ_{1} and Δ_{1} ⊢ β, which, by the cut rule gives Δ̂_{1}′ ⊢ β, whence by the derived rule of weakening for banged formulas (see 2.3), we obtain Δ̂_{0}′, Δ̂_{1}′ ⊢ β.

Inductive case: suppose the induction hypothesis true for all shorter derivations than the one displayed above in (12). We consider all possible rules used in the last step.

\underline{D:}: Suppose that the last step of (12) is a dereliction:

\frac{\frac{⋮}{Γ, C ⊢ α ⊗ β}}{Γ,!C ⊢ α ⊗ β} .

By our induction hypothesis, Γ, C ⊧_{s} α and the instance Γ′, C′ induced by the string test satisfies Γ̂ ⊗ C′ ⊢ β. It is easy to see that Γ,!C ⊧_{s} α with the following instantiation

Γ′, \frac{!}{1}C′

By decorating the outermost ! of !C with a 1, we preserve precisely the same instance we had before. Now by the definition of !-closure

Γ̂′, \frac{!}{1}C′ = Γ̂′, ˆ \frac{!}{1}C′ = Γ̂′,!C, Ĉ′.

But we have Γ̂′, Ĉ′ ⊢ β by the induction hypothesis, hence, by weakening Γ̂′,!C, Ĉ′ ⊢ β.

\underline{⊗-L}: This is immediate: the string test and the definition of instance and !-closure remain unchanged when a subformula of a premiss C, D is rewritten as C ⊗ D.

\underline{W}: Suppose the last step of the proof (12) is weakening:

\frac{\frac{⋮}{Γ ⊢ α ⊗ β}}{Γ,!C ⊢ α ⊗ β} .

We take the zero instance \frac{!}{0}C for !C, and use the same instance of Γ. Then note that ˆ \frac{!}{0}C′ =!C

By induction hypothesis Γ̂′ ⊢ β and so Γ̂′,!C ⊢ β as well.

\underline{C}: We are left with the only slightly delicate case, namely where the last step in the proof (12) is contraction:

\frac{\frac{⋮}{Γ,!C,!C ⊢ α ⊗ β}}{Γ,!C ⊢ α ⊗ β} .

and the induction hypothesis that there are instances Γ′,!C′,!C′′ induced by the string-test, for which Γ̂′, ˆ!C′, ˆ!C′′ ⊢ β. Now !C′⋈!C′′ provides us an instantiation such that the instantiation of the conclusion is the same as that of the premiss. Now use TBLL-join lemma along with the Induction hypothesis to get Γ̂′, ˆ !C′⋈!C′′ ⊢ β.

( ⇐) Suppose that Λ ⊧_{s} α. Let Λ′ be the instance of Λ induced by the string test as defined in definition (2.5). Now by (lemma 2.17) we get that

Λ ⊢ r(Λ′)

Notice that r(Λ′) is (equivalent to) Λ̂′, T (Λ′). This gives us the result.

We are now ready to describe a decision procedure for TBLL.

The Algorithm: “decide TBLL”

Input: An ordered pair ⟨Γ, θ⟩ where Γ is a multiset of TBLL formulas, and θ is a formula in TBLL.

begin

1. if θ ∈ TLL then execute string-test for ⟨Γ, θ⟩, else

2. if θ is banged then check Γ is banged and

case 1: θ is !φ. Then apply decide TBLL to ⟨Γ, φ⟩

case 2: θ is σ ⊗ τ, (where σ and τ are banged): then apply decide TBLL to ⟨Γ, σ⟩ and ⟨Γ, τ⟩.

3. else let α ⊗ φ be a nontrivial decomposition of θ (α in TLL, φ banged). Then do:

3.1 apply string-test to ⟨Γ, α⟩. If it fails then fail. If it succeeds, let Γ′ := an instance induced by the string test not already used up. If all are used up then fail.

3.2 let Γ̂′ be the bang-closure of Γ′

3.3 apply decide TBLL to ⟨Γ̂′, φ⟩. If it fails, then call this instance Γ′ used up, and goto 3.1.

end

Remark on the algorithm Note that in step 3. we backtrack through all instantiations produced by the string test.

We briefly reconsider the example discussed following the string test algorithm, above.

We claimed that

Γ ⊬ θ  and  θ ⊬ Γ

where Γ :=!(A ⊗ A ⊗ A)⊗!(A ⊗ A) and θ := A ⊗ A⊗!A.

As our algorithm shows in two cycles, Γ ⊢ θ is not a theorem of TBLL: (A ⊗ A)⊗!A is a decomposition of θ, so we apply decide TBLL to ⟨Γ, A ⊗ A⟩ and ⟨Γ,!A⟩. The first input yields “yes” (by the string-test) but the second one yields the application of decide TBLL to ⟨Γ, A⟩ which fails the string-test. The failure of θ ⊢ Γ is immediate: θ is not banged.

2.1 Correctness and complexity of the algorithm

The correctness of the algorithm decide TBLL is essentially the content of lemma 2.13 (which justifies step 1.), the decomposition lemma 2.4, lemma 2.4, lemma 2.19 on banged formulas, and the bang-closure theorem 2.22. The complexity is bounded by the complexity of the string test times number of calls to the string test on the pair ⟨Γ̂, α⟩ where Γ̂ is the bang-closure of Γ. Γ̂ is bounded by the “full” bang-closure obtained by the taking the multiset of all banged subformulas of Γ whose length is bounded by lth(Γ^{2}). The number of calls is bounded by the 2^{(⊗α)} where (⊗α) = number of tensors in α, which is bounded by l. Letting l = lth(α) + lth(Γ),!!l = lth(Γ̂) ≤ l^{2}, This gives a bound of (!!l)^{l^{2}} · 2^{l} steps. We state this bound as a theorem and leave the details of formalizing this argument to the reader. We also recall that an NP lower bound for just the TBLL/TLL-fragment was established in lemma 2.14 above.

Theorem 2.23 There is an o(l^{2l^{2}}) algorithm for deciding the derivability of sequents in TBLL. The problem is NP-hard.

The authors would like to thank Andre Scedrov and Ramesh Subrahmanyam for comments and suggestions, and Dirk Roorda for pointing out errors in earlier drafts and for helpful suggestions.

References

[1] Garey, Michael R. and Johnson, Davis S.[1979] Computers and intractability : a guide to the theory of NP-completeness San Francisco : W. H. Freeman.

[2] Gehlot, V.[1991] A proof-theoretic approach to semantics of concurrency, Dissertation, University of Pennsylvania.

[3] Girard, Lafont, Taylor [1989] Proofs and Types, Cambridge University Press (Cambridge Tracts in Theoretical Computer Science 7), Cambridge.

[4] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[5] Gunter, C.A. and V. Gehlot [1989] “Nets as Tensor Theories” in Proc. 10-th International Conference on Application and Theory of Petri Nets, Bonn, G. De Michelis, ed.

[6] Horowitz, E. and Sahni S. [1978] Fundamentals of Computer Algorithms, Computer Science Press.

[7] Kanovich, M. [1992] “Horn Programming in Linear Logic is NP-Complete” in Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pp. 200-210, IEEE Computer Society Press, Los Alamitos, California.

[8] Kosaraju, S.R. [1982], “Decidability of Reachability in Vector Addition Systems”, Proc. 14-th ACM Symp. on Theory of Computing, pp. 267-281.

[9] Lincoln, P. Mitchell, J., Scedrov, A. and Shankar, N. [1990] ”Decision Problems for Propositional Linear Logic”, proc. 31st IEEE symp. on Foundations of Computer Science.

[10] Stockmeyer, L. [1987] “Classifying the computational complexity of problems”, Journal of Symbolic Logic, volume 52, pp. 1-43.

[11] Troelstra, A. S. [1991], Lectures on Linear Logic and Lectures on Linear Logic: errata and Supplement, lecture notes, Institute for Language, logic and information, Department of mathematics and Computer Science, University of Amsterdam. To appear as a book in the CSLI- Stanford series.