Constant-Only Multiplicative Linear Logic is NP-Complete

Patrick Lincoln^{∗}  Timothy Winkler
Computer Science Department Computer Science Laboratory
Stanford University  SRI International
Stanford, CA, 94305  Menlo Park, CA

       lincoln@cs.stanford.edu           winkler@csl.sri.com

August 31, 1992

Abstract

Linear logic is a resource-aware logic that is based on an analysis of the classical proof rules of contraction (copying) and weakening (throwing away). In this paper we study the decision problem for the multiplicative fragment of linear logic without quantifiers or propositions: the constant-only case. We show that this fragment is np-complete. Earlier work by Max Kanovich showed that propositional multiplicative linear logic is np-complete. With Natarajan Shankar, the first author developed a simplified proof for the propositional case. The structure of this simplified proof is utilized here with a new encoding which uses only constants. The end product is the somewhat surprising result that simply evaluating expressions in true, false, and, and or in multiplicative linear logic (⊗, ℘, 1, and ⊥) is np-complete. By conservativity results not proven here, the np-hardness of larger fragments of linear logic follows.

1 Introduction

When Girard introduced linear logic [7], he brought to light the expressive power which can be gained by restricting the structural rules of contraction (copying) and weakening (throwing away) for propositions. Without contraction or weakening, propositions may be thought of as resources, which must be carefully accounted for. When propositions are treated as resources, as they are in linear logic, one is naturally led to consider two different forms of conjunction and disjunction. Girard named the two kinds of connectives “additive” and “multiplicative”, and focussed his attention on the multiplicative fragment by giving proof nets (a version of natural deduction tailored for linear logic) for this fragment. Since then much of the interest in linear logic has revolved around this fragment and small extensions to this fragment.

∗Supported by AT&T Doctoral Scholarship and SRI.

In order to explain the intuitive difference between additive and multiplicative connectives, consider the conjunctive goal Σ ⊢ A and B. In all sequent calculi, one must prove Δ ⊢ A and one must also prove Γ ⊢ B, for some Δ and Γ in order to prove this goal. Various sequent calculi place different requirements on the relationship between Σ, Δ, and Γ. For example, in classical logic the latter two are required to be subsets of the first (Δ ⊆ Σ and Γ ⊆ Σ). This may be seen as implicitly allowing copying of some propositions, (those which appear in all three contexts), and throwing away others (those which appear in the conclusion Σ, but not in either hypothesis). The multiplicative conjunction ⊗ of linear logic requires that the context Σ be divided between its hypotheses (Δ ⋃ Γ = Σ and Δ ⋂ Γ = ∅). The additive conjunction &, on the other hand, requires that the context be duplicated in both hypotheses (Δ = Γ = Σ). This critical difference is also reflected in the two forms of disjunction, which are the De Morgan duals of the two forms of conjunction.

Girard also added “exponential” unary connectives to linear logic, increasing the expressive power of the logic greatly. In fact, propositional linear logic with exponentials is undecidable [15]. Without exponentials, Multiplicative-Additive Linear Logic (mall) is decidable, and is pspacecomplete [15].

In this paper we focus on the smaller fragment with only the multiplicative connectives and constants, Constant-Only Multiplicative Linear Logic. In an earlier paper, the first author showed that the decision problem for Multiplicative Linear Logic (with propositions) mll is in np, by giving (a sketch of) an np algorithm [15]. However, the np-hardness of this problem was left open.

Here we show that not only is mll np-complete, but the fragment containing no propostions, comll is np-complete as well. Note that this fragment contains no quantifiers or propositions, and thus one may view this decision problem as simply evaluating expressions in true, false, and, and or in multiplicative linear logic (⊗, ℘, 1, and ⊥).

1.1 Propositional Linear Logic

The formal framework we will work with throughout this paper is a Gentzenstyle sequent calculus. We discuss three independent logics here: ll (full propositional linear logic), mll (ll restricted to multiplicative connectives and constants), and comll (The constant-only fragment of mll). We begin with a definition of ll.

A linear logic sequent is a ⊢ followed by a multiset of linear logic formulas. Note that in standard presentations of sequent calculi, sequents are often built from sets of formulas, where here we use multisets. This difference is crucial. We assume a set of propositions p_{i} given, along with their associated negations, p_{i}^{⊥}. Below we give the inference rules for the linear sequent calculus, along with the definition of negation and implication. The reader should note that negation is a defined concept, not an operator.

The following notational conventions are followed throughout this paper:

p_{i}  Positive propositional literal
p_{i}^{⊥}  Negative propositional literal
A, B, C  Arbitrary formulas
Σ, Γ, Δ  Arbitrary multisets of formulas

Thus the identity rule (I below) is restricted to atomic formulas, although in fact the identity rule for arbitrary formulas (⊢ A, A^{⊥}) is derivable in this system. For notational convenience, it is usually assumed that −∘ and ⊗ associate to the right, and that ⊗ has higher precedence than −∘. The notation ?Σ is used to denote a multiset of formulas which all begin with ?. The English names for the rules given below are are shown on the right. Note that there is no rule for the 0 constant.

I  \overline{⊢ p_{i}, p_{i}^{⊥}}  identity

Cut  \frac{⊢ Σ, A  ⊢ Γ, A^{⊥}}{⊢ Σ, Γ}  cut

⊗  \frac{⊢ Σ, A  ⊢ B, Γ}{⊢ Σ, (A ⊗ B), Γ}  tensor

℘  \frac{⊢ Σ, A, B}{⊢ Σ, (A℘B)}  par

⊕ \begin{aligned}⊢ Σ, A & ⊢ Σ, B \\ ⊢ Σ, (A ⊕ B) & ⊢ Σ, (A ⊕ B) \end{aligned} plus

&  \frac{⊢ Σ, A  ⊢ Σ, B}{⊢ Σ, (A & B)}  with

?W  \frac{⊢ Σ}{⊢ Σ,?A}  weakening

?C  \frac{⊢ Σ,?A,?A}{⊢ Σ,?A}  contraction

?D  \frac{⊢ Σ, A}{⊢ Σ,?A}  dereliction

!S  \frac{⊢?Σ, A}{⊢?Σ,!A}  storage

⊥  \frac{⊢ Σ}{⊢ Σ, ⊥}  bottom
1  \overline{⊢ 1}  one
⊤  \overline{⊢ Σ, ⊤}  top

Linear negation is defined as follows:

(p_{i})^{⊥} =^{Δ} p_{i}^{⊥}
(p_{i}^{⊥})^{⊥} =^{Δ} p_{i}
(A ⊗ B)^{⊥} =^{Δ} B^{⊥}℘A^{⊥}
(A℘B)^{⊥} =^{Δ} B^{⊥} ⊗ A^{⊥}
(A ⊕ B)^{⊥} =^{Δ} A^{⊥} & B^{⊥}
(A & B)^{⊥} =^{Δ} A^{⊥} ⊕ B^{⊥}
(!A)^{⊥} =^{Δ} ?A^{⊥}
(?A)^{⊥} =^{Δ} !A^{⊥}
(1)^{⊥} =^{Δ} ⊥
(⊥)^{⊥} =^{Δ} 1
(0)^{⊥} =^{Δ} ⊤
(⊤)^{⊥} =^{Δ} 0

Linear implication, −∘, is defined as follows:

A−∘B =^{Δ} A^{⊥}℘B

1.2 Multiplicative Linear Logic

The multiplicative fragment of linear logic mll is defined as follows. The sequent rules for mll are the same as those for ll except that the rules for the additive connectives, additive constants, and exponentials are thrown out: ⊕, & , ?W, ?C, ?D, !S, and ⊤. This leaves only the rules I, Cut, ⊗, ℘, ⊥, and 1.

1.3 Constant-Only Multiplicative Linear Logic

In this paper, we are concerned with the constant-only multiplicative fragment of linear logic comll. The sequent rules for comll are those of mll except I. Thus no formulas containing any propositional symbols are provable in comll.

1.4 Multiplicative Linear Logic is np-Complete

In this section we summarize results about the decision problem for propositional multiplicative linear logic which is known to be np-complete. An argument for the np-hardness of this fragment was first sketched by Max Kanovich in electronic mail [10]. Together with the earlier result [15] that the multiplicatives are in np, Kanovich’s result showed that this decision problem is np-complete. Kanovich later updated his argument to show that the “Horn fragment” of the multiplicatives is also np-complete [11, 12], using a novel computational interpretation of this fragment of linear logic. This paper continues this trend by providing a proof that evaluating expressions in true, false, and, and or in multiplicative linear logic is np-complete. That is, even without propositions, multiplicative linear logic is np-complete.

mll and comll are in np. Informally, the argument showing membership in np is simply that every connective in a multiplicative linear logic formula is analyzed exactly once in any cut-free proof. Thus an entire proof, if one exists, can be guessed and checked in nondeterministic polynomial time.

Formally, we first state a fundamental theorem originally due to Girard [7], but proven in complete gory detail in [15].

Theorem 1.1 (Cut Elimination) If a sequent is provable in mll, then it is provable in mll without using the Cut rule.

The above references actually prove this theorem for full linear logic, but the results for the fragments in question here follow immediately. Without cut, multiplicative proofs are quite concise.

Theorem 1.2 (Small-Proofs) Every connective is analyzed exactly once in any cut-free mll or comll proof.

From Theorem 1.1 and Theorem 1.2, we know that given a mll or comll sequent of size n, if there is any proof of this sequent, then there is a proof with exactly n total applications of inference rules. Since each application of an inference rule may be represented in space linear in n, we may simply guess and check an entire n^{2} representation of a proof tree in nondeterministic polynomial time.

The following is one of a large family of permutabilities of inferences. Propositional classical logic allows all possible permutabilities (that is, it never matters which formula one choses to break first in a classical proof), and intuitionistic logic exhibits a few impermutabilities [13]. The following permutability of (multiplicative) disjunction holds in linear logic.

Lemma 1.3 (Permutability of ℘) If there is a proof of ⊢ Γ, (A℘B), then there is a proof of ⊢ Γ, A, B.

The corresponding fact for ⊗ does not hold, as demonstrated by the following example ⊢ (1℘1), (⊥ ⊗ ⊥).

2 comll is np-complete

Some time ago, Girard [8] developed a necessary condition for the provability of constant multiplicative linear expressions:

Lemma 2.1 (Girard) Define a function M from constant multiplicative linear expressions to the integers as follows:

\begin{aligned}M(1) & = & 1 \\ M(⊥) & = & 0 \\ M(A ℘ B) & = & M(A) + M(B) \\ M(A ⊗ B) & = & M(A) + M(B) − 1 \end{aligned}

If a formula A is provable in multiplicative linear logic and contains no propositions, then M(A) = 1.

In other words, the number of tensors is one less than the number of ones in any provable comll formula. Avron (and others) have studied generalizations of this “semantic” measure to include propositions (where a proposition p is given value 1, and p^{⊥} is given value 0) yielding a necessary condition for mll provability. One may go even further, achieving a necessary condition for mall provability, using min for & and max for ⊕, and plus and minus infinity for the additive constants. For the latter case, the condition becomes: if a formula A is provable in mall, then M(A) ≥ 1. Also, one may generalize these conditions somewhat, replacing all instances of 1 with any arbitrary constant c, and allowing propositions to have different (although fixed) values, where p has value v_{p}, and p^{⊥} has value c−v_{p} [3]. Other related work is given in [17] and [4].

Since the above is only a necessary condition, there has been a question as to whether some form of simple “truth table” or numerical evaluation function like the above could yield a necessary and sufficient condition for provability of constant multiplicative (comll) expressions. The main result of this paper shows that even this multiplicative constant evaluation or circuit evaluation problem is np-complete.

We will encode 432-Partition, an np-complete problem which is a variant of 3-Partition, in mll, and show that our encoding is sound and complete.

The main idea is that the small-proof property of mll allows us to encode “resource distribution” problems naturally. Since linear logic treats propositions as resources natively, it has been called “resource-consciousness” [5]. Note that since full linear logic is conservative over mll, our encoding remains sound and complete even in larger fragments. This does not lead to new results, however, since the complexity of most larger linear logics have already been completely characterized [15].

2.1 3-Partition

We use the np-completeness of 3-Partition: (as stated in Garey+Johnson [6] page 224)

Instance: Set A of 3m elements, a bound B ∈ Z^{+}, and a size s(a) ∈ Z^{+} for each a ∈ A such that

B/4 < s(a) < B/2 and such that ∑_{a∈A} s(a) = mB

Question: Can A be partitioned into m disjoint sets A_{1}, A_{2}, ⋯, A_{m} such that, for 1 ≤ i ≤ m, ∑_{a∈A_{i}} s(a) = B (note that each A_{i} must therefore contain exactly 3 elements from A)?

Reference: [Garey+Johnson [6], 1975].
Comment: NP-complete in the strong sense.

Note that 3-Partition is np-complete in the strong sense, which implies that even when the input is represented in unary, the problem is np-hard. This property of 3-Partition is essential for our application, since we represent the input problem in unary by multiplicities of linear formulas.

To simplify later arguments we will want to assume that B > 8. However there is no loss of complexity with this assumption. One may consider only those instances of 3-Partition where B > 8. One may show this by cases. If B = 0, or B = 1, B = 2, or B = 4 there are no possible problem instances satisfying B/4 < s(a) < B/2. For B = 5, all elements must be equal to 2, and thus there are no possible solutions. For B = 8, all elements must be equal to 3, and thus there are also no possible solutions in this case. For B = 3, all allowable problem instances have all elements equal to 1, and thus this case is solvable in polynomial (constant) time (report “YES”). For B = 6, similarly, all elements have size 2, and the answer is trivially “YES”. For B = 7, all elements have size 2 or 3, and thus all partitions must be made up of two elements of size 2 and one element of size 3. The obvious counting algorithm thus solves this case in polynomial time. Thus for all cases where B is less than or equal to 8 the 3-Partition problem is solvable in polynomial time, and thus 3-Partition remains np-complete with the further constraint that B > 8.

2.2 432-Partition

We introduce a new np-complete problem, a variant of 3-Partition, which we call 432-Partition:

Instance: Set A of 3m elements, a bound B ∈ Z^{+}, and a size s(a) ∈ Z^{+} for each a ∈ A such that

B/4 < s(a) < B/2 and such that ∑_{a∈A} s(a) = mB

Question: Can A be partitioned into m disjoint sets A_{1}, A_{2}, ⋯, A_{m} such that, for 1 ≤ i ≤ m,

∑_{a∈A_{i}} s(a) = B + |A_{i}| − 3?
Comment: NP-complete in the strong sense.

We will write S1 for s(a_{1}) to improve readability of the following discussion.

We will show that solutions of 432-Partition correspond to solutions of 3-Partition for the same problem instance, under the assumption that B > 8. There is a very strong equivalence between these two problems: the instances are the same, instances are solvable in one case exactly when they are solvable in the other, and solutions in one case directly correspond to solutions in the other case. It is clear that solutions to 3-Partition are solutions for the same instance of 432-Partition.

For an arbitrary A_{i}, let A_{i} consist of X1, … Xn.

If n = 0, we have 0 = B−3, which is false by our assumption that B > 8. If n = 1, we have X1 = B − 2, but the sizes are bounded above by B/2, and with the assumption that B > 8, there is a contradiction. Also, considering cases of n > 4, we have ∑_{1≤i≤n} Xi = B + n − 3, and the assumptions that B > 8 and X_{i} > B/4, thus we have n(B/4) < B + n − 3, which implies that n − 3 > B((n/4) − 1) and from this and B > 8, we have n < 5. This leaves the n = 2, n = 3, and n = 4 cases.

Thus we have a partition each element of which consists of either two, three, or four elements.

In the case that n = 3, we have ∑_{1≤i≤3} Xi = B, and thus this set identifies a partition which directly satisfies the requirement for 3-Partition, that is, the sum is equal to B.

Note that if n = 2, we have by the above constraint that X1+X2 = B−1, and if n = 4, then X1 + X2 + X3 + X4 = B + 1. Since there are exactly 3m elements, and ∑_{a∈A} s(a) = mB, there are exactly the same number of groups with four elements as there are groups with two elements.

Further, we may analyze by cases to show that if there are any groups of four, then B = 4C + 3 for some integer C. If there are any groups of four, and B = 4C for some C, then the smallest allowable element is C + 1, since the size of each element must strictly dominate B/4. However, taking four elements of size C + 1, the constraint X1 + X2 + X3 + X4 = B + 1 is violated. Similarly for B = 4C + 1 and B = 4C + 2. Thus if there is a group of four elements, then B = 4C + 3 for some C, and by simple algebra, the elements of any group of four elements all have size C + 1, and the elements of any group of two elements both have size 2C + 1. Noting that there are exactly as many groups of two as groups of four, we may rearrange the elements of a group of four and a group of two into two groups of three by taking two elements from the group of four and one element from the group of two to form each group of three. Both resulting groups of three have total size 4C + 3, which happily is equal to B. This “reshuffling” will result in a solution to the 3-Partition problem with the same instance. Therefore 3-Partition and 432-Partition are equivalent problems.

Note that since 432-Partition and 3-Partition are equivalent, 432-Partition is np-complete in the strong sense. Thus 432-Partition is np-complete even in unary notation. This is important, since we utilize a unary representation of instances in our linear encoding.

2.3 Encoding with Propositions

We use the notation, for k and c propositions, x^{Y} = \overbrace{x ⊗ x ⊗ ⋯ ⊗ x ⊗ x}^{Y copies}.

Given an instance of 3-Partition equipped with a set A = {a_{1}, ⋯, a_{3m}}, an integer B, and a unary function S, presented as a tuple ⟨A, m, B, S⟩, we define the encoding function θ as θ(⟨A, m, B, S⟩) =

[(k−∘c^{S1}) ⊗ ⋯ ⊗ (k−∘c^{S3m})]−∘(k^{3}−∘c^{B})^{m}

As before, we are writing S1 for s(a_{1}) to improve readability.

It has been show that this formula is provable in the multiplicative fragment of linear logic if and only if the 3-Partition problem is solvable [16].

The encoding using only constants can be generated from this one by replacing k and c by ⊥.

2.4 Constant-only Encoding

We will now describe how 432-Partition instances (which are at the same time 3-Partition instances) can be encoded in comll.

We will use the following notation: x^{Y} = \overbrace{x ⊗ x ⊗ ⋯ ⊗ x ⊗ x}^{Y copies}, as before,

and x^{⟨Y ⟩} = \overbrace{x℘x℘ ⋯ ℘x℘x}^{Y copies}. Note that (x^{Y})^{⊥} = (x^{⊥})^{⟨Y ⟩} and (x^{⟨Y ⟩})^{⊥} = (x^{⊥})^{Y}.

Given an instance of 432-Partition equipped with a set A = {a_{1}, ⋯, a_{3m}}, an integer B, and a unary function S, presented as a tuple ⟨A, m, B, S⟩, we define the encoding function Θ as Θ(⟨A, m, B, S⟩) =

[(⊥−∘⊥^{S1}) ⊗ ⋯ ⊗ (⊥−∘⊥^{S3m})]−∘[(⊥^{3}−∘⊥^{B})^{m}]

Using the contrapositive (A−∘B ≡ B^{⊥}−∘A^{⊥}), we can develop a “1 only” encoding:

[(1^{⟨S1⟩}−∘1) ⊗ (1^{⟨S2⟩}−∘1) ⊗ ⋯ ⊗ (1^{⟨S3m⟩}−∘1)]−∘[(1^{⟨B⟩}−∘1^{⟨3⟩})^{m}]

Eliminating the linear implication in favor of ℘ these formulas both become:

(1^{⟨S1⟩} ⊗ ⊥)℘(1^{⟨S2⟩} ⊗ ⊥)℘ ⋯ ℘(1^{⟨S3m⟩} ⊗ ⊥)℘(⊥^{B}℘1^{⟨3⟩})^{m}

We will use the last form of this formula, since it contains no implicit negations (linear implication). One may see this formula satisfies Girard’s measure condition, Lemma 2.1, if there are 3m elements, and the sum of the sizes equals mB, side conditions on the statement of 432-Partition (and 3-Partition).

The claim is that these formulas are provable in the multiplicative fragment of linear logic if and only if the 432-Partition problem is solvable.

2.5 Soundness

Lemma 2.2 (Soundness) If a 432-Partition problem ⟨A, m, B, S⟩ is solvable, then we are able to find a proof of the comll formula Θ(⟨A, m, B, S⟩).

Proof.

The proof is straightforward. For each group of three elements in the assumed solution to the 432-Partition problem, one forms the following subproof, assuming the elements of the group are numbered x, y, and z.

\underline{\begin{matrix}\underline{\begin{matrix}\underline{⋮ ; ⊢ 1^{⟨Sx⟩}, 1^{⟨Sy⟩}, 1^{⟨Sz⟩}, ⊥^{B}  \begin{matrix}\overline{⊢ 1} & 1 \\ \overline{⊢ 1, ⊥} & ⊥ \end{matrix}} & ⊗ \\ ⊢ (1^{⟨Sx⟩} ⊗ ⊥), 1^{⟨Sy⟩}, 1^{⟨Sz⟩}, 1, ⊥^{B} \end{matrix}  \begin{matrix}\overline{⊢ 1} & 1 \\ \overline{⊢ 1, ⊥} & ⊥ \end{matrix}} & ⊗ \\ ⊢ (1^{⟨Sx⟩} ⊗ ⊥), (1^{⟨Sy⟩} ⊗ ⊥), 1^{⟨Sz⟩}, 1, 1, ⊥^{B} \end{matrix}  \begin{matrix}\overline{⊢ 1} & 1 \\ \overline{⊢ 1, ⊥} & ⊥ \end{matrix}} _{⊗}
\underline{⊢ (1^{⟨Sx⟩} ⊗ ⊥), (1^{⟨Sy⟩} ⊗ ⊥), (1^{⟨Sz⟩} ⊗ ⊥), 1, 1, 1, ⊥^{B}}_{℘}
\underline{⊢ (1^{⟨Sx⟩} ⊗ ⊥), (1^{⟨Sy⟩} ⊗ ⊥), (1^{⟨Sz⟩} ⊗ ⊥), 1^{⟨2⟩}, 1, ⊥^{B}}_{℘}
⊢ (1^{⟨Sx⟩} ⊗ ⊥), (1^{⟨Sy⟩} ⊗ ⊥), (1^{⟨Sz⟩} ⊗ ⊥), 1^{⟨3⟩}, ⊥^{B}
\overline{⊢ (1^{⟨Sx⟩} ⊗ ⊥), (1^{⟨Sy⟩} ⊗ ⊥), (1^{⟨Sz⟩} ⊗ ⊥), (1^{⟨3⟩}℘⊥^{B})}^{℘}

The elided proof of ⊢ 1^{⟨Sx⟩}, 1^{⟨Sy⟩}, 1^{⟨Sz⟩}, ⊥^{B} is guaranteed to exist by the conditions on the solution to 432-Partition. That is, since x, y, and z are from the same partition, the sum of Sx, Sy, and Sz must be equal to B.

Given the m proofs constructed as above from each of the m groups of elements, one combines them with ⊗ into a proof of

⊢ (1^{⟨S1⟩} ⊗ ⊥), ⋯, (1^{⟨S3m⟩} ⊗ ⊥), (1^{3}℘⊥^{B})^{m}

The proof can then be completed with 3m applications of ℘.

2.6 Completeness

Lemma 2.3 (Completeness) For A, m, B, and S satisfying the constraints of 432-Partition, if there is a proof of the comll formula Θ(⟨A, m, B, S⟩), then the 432-Partition problem ⟨A, m, B, S⟩ is solvable.

Proof.

To simplify this direction of the proof, we use the extra assumption that the “bin size” B is greater than 8. For a justification of this assumption, see Section 2.1. The following makes heavy use of Lemma 2.1.

Assuming we have a proof of

⊢ (1^{⟨S1⟩} ⊗ ⊥)℘(1^{⟨S2⟩} ⊗ ⊥)℘ ⋯ ℘(1^{⟨S3m⟩} ⊗ ⊥)℘(⊥^{B}℘1^{⟨3⟩})^{m}

we show that the corresponding 432-Partition problem is solvable.

If there is a proof of this sequent, then there is a cut-free proof, by the cut elimination theorem (Theorem 1.1). By repeated applications of Lemma 1.3, if there is a proof of this sequent, then there is a proof of ⊢ (1^{⟨S1⟩} ⊗ ⊥), (1^{⟨S2⟩} ⊗ ⊥), ⋯, (1^{⟨S3m⟩} ⊗ ⊥), (⊥^{B}℘1^{⟨3⟩})^{m}

We then perform complete induction on m.

If m > 1, the proof of this sequent must end in ⊗, since all formulas have main connective ⊗. We next show that the principal formula of that rule application must be (⊥^{B}℘1^{⟨3⟩})^{m}.

First, we note that each formula (1^{⟨Sj⟩} ⊗ ⊥) has measure Sj − 1. Since we are assuming B > 8, the initial conditions of the 432-Partition problem ensure that for all j, Sj > 2, and therefore Sj − 1 > 1. There is only one formula, (⊥^{B}℘1^{⟨3⟩})^{m}, with negative measure.

If we assume that one of the (1^{⟨Si⟩} ⊗ ⊥) formulas is principal in an application of ⊗, by Lemma 2.1, each hypothesis sequent must have measure one. In this case we have the following supposed proof for some Σ and Δ with the multiset union Σ ⋃ Δ ⋃(1^{⟨Si⟩} ⊗ ⊥) being equal to the conclusion:

\begin{matrix}⋮ ; ⊢ Σ, ⊥ & ⋮ ; ⊢ Δ, 1^{⟨Si⟩} \\ \overline{⊢ (1^{⟨S1⟩} ⊗ ⊥), (1^{⟨S2⟩} ⊗ ⊥), ⋯, (1^{⟨S3m⟩} ⊗ ⊥), (⊥^{B}℘1^{⟨3⟩})^{m}} & ⊗ \end{matrix}

But 1^{⟨Si⟩}, which occurs in one hypothesis, has measure > 2. Therefore, the formula with negative measure, (⊥^{B}℘1^{⟨3⟩})^{m}, must occur in Δ. Now consider the other hypothesis, which must contain ⊥, and other formulas Σ from the conclusion sequent. If any formulas of the form (1^{⟨Sj⟩} ⊗ ⊥) are included in Σ, the measure of that hypothesis is greater than 1. If no such formulas are included, then the sequent has measure 0. In either case, by Lemma 2.1, that sequent is not provable. Thus the assumption that one of the (1^{⟨Sj⟩}⊗⊥) formulas is principal must be in error, and (⊥^{B}℘1^{⟨3⟩})^{m} must be principal.

Thus if m > 1, the only possible next proof step is ⊗, with principal formula (⊥^{B}℘1^{⟨3⟩})^{m}. We may then focus on the case when m = 1. We claim that each such branch in the proof corresponds to one partition in the solution of the original 432-Partition problem. That is, we claim that when m = 1, we must be left with a sequent of the form:

⊢ (1^{⟨X1⟩} ⊗ ⊥), (1^{⟨X2⟩} ⊗ ⊥), ⋯, (1^{⟨Xn⟩} ⊗ ⊥), (⊥^{B}℘1^{⟨3⟩})

Where the Xi are a subset of the Si. There are exactly B+n−1 occurrences of ⊗ in this sequent, and ∑_{1≤i≤n} Xi+3 ones in this sequent. By Lemma 2.1, (∑_{1≤i≤n} Xi + 3) − (B + n − 1) = 1, or equivalently ∑_{1≤i≤n} Xi = B + n − 3. This gives rise to an instance of 432-Partition.

Thus, given any proof of Θ(⟨A, m, B, S⟩), we first see that one may identify m branches, each of which is of the form ⊢ (1^{⟨X1⟩} ⊗ ⊥), (1^{⟨X2⟩} ⊗ ⊥), ⋯, (1^{⟨Xn⟩} ⊗ ⊥), (⊥^{B}℘1^{⟨3⟩}). From these m branches, we may identify m partitions of 4,3, or 2 elements of the associated 432-Partition problem. In other words, from any proof of the given sequent, one may construct a solution to the 432-partition problem.

2.7 Main Result

From the preceding, we immediately achieve our stated result.

Theorem 2.4 (COMLL NP-COMPLETE) The decision problem for constant-only multiplicative linear logic is np-complete.

Also, with an easy conservativity result, we find that this np-Hardness proof suffices for multiplicative linear logic as well.

Theorem 2.5 (Conservativity) Multiplicative linear logic is conservative over constant-only multiplicative linear logic.

Proof. By induction on cut-free mll proofs.

2.8 Using 3-Partition Directly

Instead of using 432-Partition one could use 3-Partition directly with some simplifying assumptions.

One may also consider the following looser specification of 3-Partition, which we will call Generalized-3-Partition.

Instance: Set A′ of 3m elements, a bound B′ ∈ Z^{+}, and a size

s(a′) ∈ Z^{+} for each a′ ∈ A′

Question: Can A′ be partitioned into m disjoint sets A′_{1}, A′_{2}, ⋯, A′_{m} such that, for 1 ≤ i ≤ m, ∑_{a′∈A′_{i}} s(a′) = B′ such that each set contains exactly 3 elements from A′?

Generalized-3-Partition does not have a priori restrictions on the sizes of elements, but instead has an explicit specification that only partitions of three elements are allowed. One can immediately restrict s(a′) for all a′ ∈ A′ to be ≤ B′, for otherwise there is no solution, since all sizes are nonnegative.

From an instance of Generalized-3-Partition, one may generate an instance of 3-Partition by adding B′ + 1 to the size of each element of A′. The instance of 3-Partition then is asked with B = 4B′ + 3, and the size of each element satisfies the condition B/4 ≤ s(a) ≤ B/2, since B = 4B′ + 3, s(a′) < B′, and s(a) = s(a′) + B′ + 1. By adding more than B′ + 1 to the size each element, one can create instances of 3-Partition where elements are as close to B/3 as desired. Thus one could avoid the complications involved in “reshuffling” the groups of four and two elements above that arise with 432-Partition by using a properly restricted 3-Partition problem. The reshuffling only occurs for a with s(a) very close to B/4 or B/2.

Another type of simplification can be achieved with other encodings of a 3-Partition problem. Consider the earlier encoding of 3-Partition in full multiplicative linear logic:

[(k−∘c^{s(A_{1})}) ⊗ ⋯ ⊗ (k−∘c^{s(A_{3m})}) ⊗ (c^{B}−∘j)^{m}]−∘(k^{3}−∘j)^{m}

Constant-only encodings can be generated by replacing c by bottom, and k by 1^{⟨C⟩} for some integer C. A value of C that is particularly interesting is C = ∑_{a∈A} s(a). Although they are still polynomial, such encodings tend to be larger than the one advocated above, but result in somewhat less complicated proofs of soundness. The case of C = 1 is an incorrect encoding, and one may consider the “bottom only” encoding proved sound and complete above to be generated from the case C = 0.

3 Conclusion

We have demonstrated that simply evaluating expressions in true, false, and, and or in multiplicative linear logic (⊗, ℘, 1, and ⊥) is np-complete. By conservativity results the np-hardness of larger fragments of linear logic follow, although some of these results were known previously. These results comprise further dramatic evidence of the extreme expressive power of linear logic. Other results along these lines have previously shown that full propositional linear logic is undecidable, and there are natural fragments which are pspace-complete, exptime-complete, and np-complete.

Complexity results for fragments of linear logic indicate the difficulty of constructing efficient decision procedures for large fragments of linear logic. It may have been hoped previously that some “semantic” measure condition could be used to immediately decide constant-only expressions in linear logic. When constructing theorem provers for linear logic, one must consider carefully the sources of exponential blowup identified by these suites of results (in this case, the splitting of contexts in applications of the ⊗ rule).

However, it is still essentially unknown how to harness the evident power of linear logic for useful purposes. Several interesting attempts have been made, including using linear logic as the basis for a logic programming language [9, 2], and as the basis for a functional programming language [1, 14]. The results given here have more direct impact on the logic programming approach, which is still in its infancy.

References

[1] S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 1991. Special Issue on the 1990 Workshop on Math. Found. Prog. Semantics. To appear.

[2] J.-M. Andreoli and R. Pareschi. Linear objects: Logical processes with built-in inheritance. In Proc. 7-th International Conference on Logic Programming, Jerusalem, May 1990.

[3] A. Avron. Some properties of linear logic proved by semantic methods. Technical Report 260/92, Eskenasy Institute of Computer Science, Tel-Aviv University, 1992.

[4] M. Barr. *-autonomous categories. In: Lecture Notes in Mathematics 752, Springer, 1979.

[5] G. Bellin. Mechanizing Proof Theory: Resource-Aware Logics and Proof-Transformations to Extract Implicit Information. PhD thesis, Stanford University, 1990.

[6] M.R. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Co., 1979.

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

[8] Jean-Yves Girard. Personal communication. April 1990.

[9] J.S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In Proc. 6-th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 32–42. IEEE Computer Society Press, Los Alamitos, California, July 1991. Full paper to appear in Information and Computation.

[10] M. Kanovich. The multiplicative fragment of linear logic is np-complete. Email Message, 1991.

[11] M. Kanovich. The multiplicative fragment of linear logic is np-complete. Technical Report X-91-13, Institute for Language, Logic, and Information, June 1991.

[12] M. Kanovich. Horn programming in linear logic is np-complete. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, pages 200–210. IEEE Computer Society Press, Los Alamitos, California, June 1992.

[13] S.C. Kleene. Permutability of inferences in Gentzen’s calculi LK and LJ. Memoirs of the AMS, 1952.

[14] P. Lincoln and J. Mitchell. Operational aspects of linear lambda calculus. In Proc. 7th IEEE Symp. on Logic in Computer Science, 1992.

[15] P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. Annals Pure Appl. Logic, 56:239–311, 1992. Special Volume dedicated to the memory of John Myhill abstract appeared in Proc. 31st IEEE Symp. on Foundations of Computer Science, 1990.

[16] P.D. Lincoln. Computational Aspects of Linear Logic. PhD thesis, Stanford University, 1992.

[17] R.A.G. Seely. Linear logic, *-autonomous categories, and cofree coalgebras. In: Categories in Computer Science and Logic, June 1989, 1989.