Appeared in FOCS 1990

Decision Problems for Propositional Linear Logic

Patrick Lincoln^{∗}  John Mitchell^{†}  Andre Scedrov^{‡}  Natarajan Shankar^{§}

Abstract

Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. We show that unlike most other propositional (quantifier-free) logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes pspace-complete. We also establish membership in np for the multiplicative fragment, np-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for certain fragments of noncommutative propositional linear logic.

1 Introduction

Linear logic, introduced by Girard [14, 18, 17], is a refinement of classical logic which may be derived from a Gentzen-style sequent calculus axiomatization of classical logic in three steps. The resulting sequent system is given in Appendix A, where some standard notation is also defined.

The first step in deriving linear logic from classical logic is to eliminate two structural rules, contraction and weakening. We view hypothesis as resources, and conclusions as requirements to be met using the resources. Therefore the formula A implies A means that the resource A can be use to meet the requirement A. Contraction allows any property which follows from two assumptions of a formula to be derived from a single assumption of that formula. For example the formula (A and A) implies A is derivable using contraction. Weakening allows deductions which do not use all of their hypotheses, e.g., the formula (A and B) implies A is derivable with weakening, but not without. Since contraction and weakening make it possible to use an assumption as little or as often as desired, these rules are responsible for what we see in hindsight as a loss of control over resources in both classical and intuitionistic logic. Excluding these rules produces a linear system in which each assumption must be used exactly once. In the resulting linear logic, formulas indicate bounded or finite resources which cannot necessarily be discarded or duplicated.

The second step in deriving linear logic involves the propositional connectives. Briefly, the change in structural rules leads naturally to two forms of conjunction, one called “multiplicative” and the other “additive”, and similarly two forms of disjunction. The multiplicative forms disallow sharing of resources, while the additive forms require resource sharing.

Finally, in order to recover the full deductive power of classical logic, a storage or reuse operator, ! , is added. Intuitively, the formula !A provides unlimited use of the resource A. Using a computational metaphor, the formula !A means that, “the datum A is stored in the memory and may be referenced an unlimited number of times.” There is also a dual modal operator ?, definable from ! using negation. The formula ?B allows the unlimited consumption of B.

∗Lincoln@CS.Stanford.EDU Department of Computer Science, Stanford University, Stanford, CA 94305, and the Computer Science Laboratory, SRI International, Menlo Park, CA 94025. Supported by AT&T Bell Laboratories Doctoral Scholarship, and SRI internal funding.

†JCM@CS.Stanford.EDU Department of Computer Science, Stanford University, Stanford, CA 94305. Supported in part by an NSF PYI Award, matching funds from Digital Equipment Corporation, the Powell Foundation, and Xerox Corporation; NSF grant CCR-8814921 and the Wallace F. and Lucille M. Davis Faculty Scholarship.

‡Andre@Saul.CIS.Upenn.EDU Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104. Partially supported by NSF Grant CCR-87-05596, by ONR Grant NOOO14-88-K-0635 and by the 1987 Young Scientist Award from the Natural Sciences Association of the University of Pennsylvania. Work completed while on sabbatical at the Computer Science Department and Center for the Study of Language and Information, Stanford University, Stanford, CA.

§Shankar@CSL.SRI.COM Computer Science Laboratory, SRI International, Menlo Park, CA 94025. Supported by SRI internal funding.

Since the basic framework remains linear, unbounded reuse or consumption is only allowed “locally”, at formulas specifically marked with ! or ? (respectively). The resulting logic is natural from both proof-theoretic and computational standpoints. In particular, Gentzenstyle cut-elimination, a central property in the prooftheoretic tradition (see [13, 18], for example), has been established for linear logic [14]. Cut elimination establishes consistency and provides a natural computational mechanism that resembles reduction in lambda calculus (e.g., [22, 18]).

An early application of the resource-sensitive aspect of the logic was the implementation of a functional programming language in which garbage collection was replaced by explicit duplication operations based on linear logic [25]. Further studies have demonstrated connections with Petri nets [3, 20, 30, 4, 12, 10] and other models of concurrency [26, 1]. With regard to concurrency, there is a similarity between proof nets, the inherent model of computation associated with cut-elimination in multiplicative linear logic (c.f. [14, 15, 9, 26]), and connection graphs, which were designed to model connection machine computation [5]. Other applications include optimization of copying in lazy functional programming language implementation [21] and the control structure of logic programs [7, 2]. A natural characterization of polynomial time computations can be given in a bounded version of linear logic [19] obtained by limiting reuse to specified bounds, i.e., by bounding the number of references to each datum in memory.

In this paper, we study the complexity of provability for several fragments of propositional (quantifier-free) linear logic. Perhaps our most notable result is that full propositional linear logic is undecidable. However, we begin the description of our results with the smallest fragment considered, the so-called multiplicative linear logic.

The multiplicative fragment contains only linear implication, negation, and forms of conjunction and disjunction which require the available resource to be partitioned among subformulas, rather than shared. We show that the decision problem for this fragment is in np. Moreover, if unrestricted weakening is allowed, then the multiplicative fragment becomes np-complete.

There are two natural fragments extending pure multiplicative linear logic. We show that the first extension, with additive and multiplicative connectives but not !, is pspace-complete.

We note in passing that the second extension, with only multiplicative connectives and storage (!), is at least as hard as the reachability problem for Petri nets (or, equivalently, commutative semi-Thue systems or vector addition systems). This follows from conservativity properties established in this paper and previous work relating linear logic and Petri nets. Although reachability is decidable [32, 24], the best known lower bound is expspace [29, 31]. A likely upper bound is primitive recursive in the Ackermann function [33, 8]. Finally, we show that provability in full propositional linear logic, with additive and multiplicative connectives and modal storage operator, is undecidable. (Provability is trivially r.e., since the proof system is effective.) We also establish the undecidability of a noncommutative variant of linear logic (even without additive connectives), a system that extends the calculus in [27], see [16, 34].

In the remainder of this paper we state the requisite lemmas and give a brief overview of the proofs of our theorems. Complete detailed proofs may be found in our technical report [28].

2 Multiplicative Additive Linear Logic is PSPACEcomplete

This section deals with the fragment of propositional linear logic, called mall, which contains the multiplicative connectives, ⊗ and ℘, the additive connectives, & and ⊕, the constants 0, 1, ⊤, and ⊥, but excludes the modal storage operators ! and ?. The proof rules of mall are all of the rules in the Appendix A that are associated with these connectives and constants. mall has been studied by Girard and Bellin, and used by Andreoli, Pareschi, and Cerrito [16, 6, 2, 7]. In contrast to classical propositional logic, which is co-NP-complete, we show below that provability for mall is pspace-complete.

The cut-elimination theorem for the mall fragment follows from the cut-elimination theorem and the subformula property for linear logic.

Lemma 2.1 The provability in mall of a given sequent can be decided by a polynomial space bounded Turing machine.

Proof. There is a linear bound on the depth of cut-free mall proofs so that an alternating Turing machine could generate and check all branches of a cutfree proof in parallel.

2.1 Informal Outline of PSPACE-hardness of mall

The pspace-hardness of mall provability is demonstrated by a reduction from the validity problem for quantified Boolean formulas (QBF). In this brief abstract, only the key intuitions are emphasized.

A quantified Boolean formula has the (prenex) form Q_{m}X_{m} … Q_{1}X_{1}: M, where M is a quantifier-free Boolean matrix and each Q_{i} is either ∀ or ∃ quantifying Boolean variables in M. The syntactic variable G ranges over QBFs, M ranges quantifier-free Boolean formulas, and X ranges over Boolean variables. An assignment I for G maps the free variables in G to truth values T or F. The validity of G under I is written as I ⊧ G. The QBF validity problem is: Given a closed QBF G, is ⊧ G?

We provide a succinct encoding of a closed QBF G as a mall sequent that is provable exactly when G is valid. One part encodes the Boolean matrix, and a second part encodes the quantifier prefix. The encoding is carried out in a one-sided formulation of the mall sequent calculus where, for example, the provable twosided sequent A, A−∘B ⊢ B is written as ⊢ A^{⊥}, A ⊗ B^{⊥}, B.

2.1.1 Encoding Boolean Evaluation.

The encoding of the Boolean connectives and quantifiers in mall is described by means of an example. Let G be the valid QBF

∀X_{2}∃X_{1}: ¬(¬X_{1} ∧ X_{2}) ∧ ¬(¬X_{2} ∧ X_{1})

G is a restatement of ∀X_{2}∃X_{1}: (X_{1} ⟺ X_{2}), so that with the quantifier reversed, ∃X_{1}∀X_{2}: (X_{1} ⟺ X_{2}) is falsifiable. The encoding of the Boolean matrix M of G describes the formula as a circuit with signals labeled by mall literals. If the assignment I is encoded by a sequence of mall formulas ⟨I⟩, and [M]_{a} is the mall formula encoding M with output labeled by the literal a, then I ⊧ M is encoded by the sequent ⊢ ⟨I⟩, [M]_{a}, a, whereas I |̸= M is encoded by ⊢ ⟨I⟩, [M]_{a}, a^{⊥}.

The assignment ⟨{X_{1} ← T, X_{2} ← F }⟩ is encoded by the sequence of formulas x_{1}^{⊥}, x_{2}. These literals are the input signals to the encoding of the Boolean formula.

The encoding [¬X_{1}]_{a} of ¬X_{1} with output labeled a is the formula not(x_{1}, a) expressing the truth table for negation within mall.

not(x_{1}, y) = (x_{1} ⊗ y) ⊕ (x_{1}^{⊥} ⊗ y^{⊥})  (1)

Which is the negation of the formula (x_{1}−∘a^{⊥}) & (x_{1}^{⊥}−∘a). The sequent

⊢ x_{1}, not(x_{1}, a), a  (2)

encodes the situation where the input X_{1} is F, and asserts (correctly) that the output ¬X_{1} is T. The sequent (2) is easily seen to have the proof

⊢ x_{1}, x_{1}^{⊥} ⊢ a^{⊥}, a
⊢ x_{1}, (x_{1}^{⊥} ⊗ a^{⊥}), a
⊢ x_{1}, (x_{1} ⊗ a) ⊕ (x_{1}^{⊥} ⊗ a^{⊥}), a

Similarly, the sequent (3) representing {X_{1} ← T } |̸= ¬X_{1} is also provable.

⊢ x_{1}^{⊥}, not(x_{1}, a), a^{⊥}  (3)

On the other hand, the sequent

⊢ x_{1}^{⊥}, not(x_{1}, a), a  (4)

asserts (falsely) that {X_{1} ← T } ⊧ ¬X_{1}. Sequent (4) is not provable because mall is a refinement of classical logic in which no falsifiable sequents of ordinary propositional logic are provable.

The truth tables for the other Boolean connectives can similarly be expressed as mall formulas and the entire matrix M encoded as above. The only subtlety is that when the fanout of a signal exceeds one, the encoding must provide an explicit means for duplicating the corresponding mall literal, since mall lacks a contraction rule.

2.1.2 Encoding Boolean Quantification

To encode Boolean quantification, we need to encode individual quantifiers as well as the dependencies between quantifiers. Given the above encoding for assignments and the Boolean connectives, an almost correct way to encode Boolean quantifiers would be to encode ∃X_{1} by the formula (x_{1} ⊕ x_{1}^{⊥}), and ∀X_{2} by (x_{2} & x_{2}^{⊥}). The reason the formula (x_{1} ⊕ x_{1}^{⊥}) behaves like existential quantification in proof search is that a nondeterministic choice can be made between

\frac{⊢ x_{1}^{⊥}, Γ}{⊢ (x_{1} ⊕ x_{1}^{⊥}), Γ}  and  \frac{⊢ x_{1}, Γ}{⊢ (x_{1} ⊕ x_{1}^{⊥}), Γ}

according to the assignment (T or F, respectively) to X_{1} which makes ∃X_{1}: M valid. Similarly, the formula of (x_{2} & x_{2}^{⊥}) in a sequent behaves like universal quantification requiring proofs of both ⊢ x_{2}^{⊥}, Γ and ⊢ x_{2}, Γ:

\frac{⊢ x_{2}^{⊥}, Γ ⊢ x_{2}, Γ}{⊢ (x_{2} & x_{2}^{⊥}), Γ}

However, with this representation of quantifiers, the mall encoding of ∃X_{1}∀X_{2}: M would be the same as that of ∀X_{2}∃X_{1}: M, but only the latter formula is valid since M expresses (X_{1} ⟺ X_{2}).

To guarantee that ∃X_{1}∀X_{2}: M has been correctly encoded, we need to ensure that if the encoding is provable, there is a proof in which the choice of witness for X_{1} does not depend on whether X_{2} is T or F. Such a dependency of X_{1} on X_{2} is shown in the proof below.

\frac{\begin{aligned}⊢ x_{1}, x_{2}, Γ & ⊢ x_{1}^{⊥}, x_{2}^{⊥}, Γ \\ ⊢ (x_{1} ⊕ x_{1}^{⊥}), x_{2}, Γ & ⊢ (x_{1} ⊕ x_{1}^{⊥}), x_{2}^{⊥}, Γ \end{aligned}}{⊢ (x_{1} ⊕ x_{1}^{⊥}), (x_{2} & x_{2}^{⊥}), Γ}

\begin{matrix}\underline{\underline{\overline{⊢ q_{2}, q_{2}^{⊥}}^{I} ? ; \overline{⊢ q_{1}^{⊥}, q_{1}, x_{1}} ; \overline{⊢ q_{1}^{⊥}, q_{1}℘x_{1}}^{℘} ; \overline{⊢ q_{1}^{⊥}, ((q_{1}℘x_{1}) ⊕ (q_{1}℘x_{1}^{⊥}))}^{⊕}}_{⊗} ; ⊢ q_{2}, q_{1}^{⊥}, q_{2}^{⊥} ⊗ ((q_{1}℘x_{1}) ⊕ (q_{1}℘x_{1}^{⊥})) ⋮ ; ⊢ (q_{0}℘x_{2}) & (q_{0}℘x_{2}^{⊥}), q_{0}^{⊥} ⊗ [M]_{g}, g} & ⊗ \\ ⊢ q_{2}, q_{2}^{⊥} ⊗ ((q_{1}℘x_{1}) ⊕ (q_{1}℘x_{1}^{⊥})), q_{1}^{⊥} ⊗ ((q_{0}℘x_{2}) & (q_{0}℘x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g \end{matrix}

Figure 1: A failed proof attempt

\underline{\overline{⊢ q_{2}, q_{2}^{⊥}}^{I} \begin{matrix}⊢ q_{1}, x_{1}, q_{1}^{⊥} ⊗ ((q_{0}℘x_{2}) & (q_{0}℘x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g \\ \overline{⊢ q_{1}℘x_{1}, q_{1}^{⊥} ⊗ ((q_{0}℘x_{2}) & (q_{0}℘x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g} & ℘ \\ \overline{⊢ ((q_{1}℘x_{1}) ⊕ (q_{1}℘x_{1}^{⊥})), q_{1}^{⊥} ⊗ ((q_{0}℘x_{2}) & (q_{0}℘x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g} & ⊕ \end{matrix}}_{⊗} ; ⊢ q_{2}, q_{2}^{⊥} ⊗ ((q_{1}℘x_{1}) ⊕ (q_{1}℘x_{1}^{⊥})), q_{1}^{⊥} ⊗ ((q_{0}℘x_{2}) & (q_{0}℘x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g

Figure 2: A correct deduction respecting quantifier order

The solution is to encode the quantifier order in a way that forces (x_{1} ⊕ x_{1}^{⊥}) to be introduced below (x_{2} & x_{2}^{⊥}) in any cut-free proof. For this we introduce new mall atoms q_{0}, q_{1}, q_{2}, and define the encoding [[∃X_{1}∀X_{2}: G]]_{g} as

⊢ q_{2},

q_{2}^{⊥} ⊗ ((q_{1}℘x_{1}) ⊕ (q_{1}℘x_{1}^{⊥})), q_{1}^{⊥} ⊗ ((q_{0}℘x_{2}) & (q_{0}℘x_{2}^{⊥})), q_{0}^{⊥} ⊗ [M]_{g}, g

The quantifier encoding for ∃X_{1} now hides the “key” q_{1} that is needed to unlock the quantifier encoding for ∀X_{2}. One attempt to violate the quantifier ordering as before, is shown in Figure 1, where the subgoal ⊢ q_{1}^{⊥}, q_{1}, x_{1} is unprovable in mall due to the absence of an applicable weakening rule.

All other attempts at violating the quantifier ordering also fail, but the deduction which does respect the quantifier order succeeds as shown in Figure 2.

2.2 Proof of pspace-hardness of mall

Lemma 2.2 Let M be a Boolean formula and I an assignment for the variables in M, then

1. I ⊧ M iff ⊢ ⟨I⟩, [M]_{g}, g

2. I |̸= M iff ⊢ ⟨I⟩, [M]_{g}, g^{⊥}

The next lemma establishes the correctness of the encoding of quantifiers.

Lemma 2.3 Let M be a Boolean formula in the variables X_{1}, …, X_{n}, then for any m, 0 ≤ m ≤ n, and assignment I for X_{m+1}, …, X_{n}, I ⊧ Q_{m}X_{m} … Q_{1}X_{1}: M iff ⊢ q_{m}, ⟨I⟩, [[Q_{m}X_{m} … Q_{1}X_{1}: M]]_{g}, g is provable.

Lemma 2.4 Given a closed QBF Q_{n}X_{n} … Q_{0}X_{0}: M, ⊧ Q_{n}X_{n} … Q_{0}X_{0}: M iff ⊢ q_{n}, [[Q_{n}X_{n} … Q_{0}X_{0}: M]]_{g}, g is provable in mall.

The size of the sequent encoding a QBF G is polynomial in G and the encoding takes place in polynomial time. Along with Lemmas 2.4 and 2.1 yields the final result.

Theorem 2.5 mall provability is pspace-complete.

With two-sided sequents, the intuitionistic fragment of mall constrains the right-hand side of the sequent to contain at most one formula. A two-sided reformulation of the above proof could be carried out entirely within the intuitionistic fragment of mall so that intuitionistic mall is also pspace-complete.

3 Propositional Linear Logic is Undecidable

We show that propositional linear logic is undecidable by reduction from the halting problem for a form of counter machine. More specifically, we begin by extending linear logic with theories whose axioms may be used any number of times in a proof. We then describe a form of and-branching two-counter machines with undecidable halting problem and show how to encode these machines in propositional linear logic with theories. Since the axioms of our theories must have a special form, we are able to show the faithfulness of this encoding using a natural form of cut-elimination with non-logical axioms. To illustrate the encoding of twocounter machines, we present an example simulation of a simple computation in Section 3.5. On first reading, the reader may wish to jump ahead to that section since it demonstrates the basic mechanism used in the undecidability proof.

3.1 Linear Logic Augmented With Theories

We begin by augmenting linear logic with a notion of theory. Essentially, a theory is a set of non-logical axioms (sequents) that may occur as leaves of a proof tree. The theories described here are an extension of earlier work on multiplicative theories [20, 30].

We define a positive literal as one of the given p_{i} propositions, a negative literal as one of the p_{i}^{⊥} propositions, and an atomic formula as any positive or negative literal.

For the theories of interest here, an axiom may be any linear logic sequent of the form ⊢ C, p_{i_{1}}^{⊥}, p_{i_{2}}^{⊥}, ..., p_{i_{n}}^{⊥}, where C is any linear logic formula, and the remainder of the sequent is made up of negative literals. For example, the sequents ⊢ p_{1}, p_{2}^{⊥}, ⊢ (p_{1} ⊗ p_{2}), p_{2}^{⊥}, ⊢ ?(p_{1}℘p_{1}), and ⊢ p_{1}^{⊥}, p_{2}^{⊥} may all be axioms. However, ⊢ p_{1}, p_{1} and ⊢ (p_{1}⊗p_{2}), p_{3} may not. We use this restriction on axioms to achieve strict control over the shape of a proof as provided by Lemma 3.1. Some of this control is lost if the definition of theory is generalized, although for some applications the weaker available results would be sufficient.

Any finite set of axioms is a theory. We consider only finite theories so that theories may be encoded as formulas of linear logic, which would be impossible if we allowed arbitrary sets of axioms. For any theory T, we say that a sequent ⊢ Γ is provable in T exactly when we are able to derive ⊢ Γ using the standard set of linear logic proof rules and axioms from T. Thus each axiom of T is treated as a reusable sequent which may occur as a leaf of a proof tree.

A directed cut is one where at least one premise is an axiom and where the cut formula is not a negative literal of the axiom. A cut between two axioms is therefore always directed. A directed or standardized proof where all the cuts are directed. With these definitions, we may obtain the following result.

Lemma 3.1 (Cut Standardization) If there is a proof of ⊢ Γ in theory T, then there is a directed proof of ⊢ Γ in theory T.

The proof of this lemma follows by induction on the length of proofs. At each step of the induction we appeal to a modified version of the usual cut-elimination procedure.

3.2 Coding Theories in Formulas

We define the translation [T] of a theory T with k axioms into a pure linear logic formula by

[{t_{1}, t_{2}, ⋯, t_{k}}] = ?[t_{1}],?[t_{2}], ⋯,?[t_{k}]

where [t_{i}] is defined for each axiom t_{i} as follows:

[ ⊢ C, p_{a}^{⊥}, p_{b}^{⊥}, ..., p_{z}^{⊥}] =^{Δ} (C^{⊥} ⊗ p_{a} ⊗ p_{b} ⊗ ⋯ ⊗ p_{z})

Thus each axiom becomes a reusable formula, where the parity of the subformulas of the axiom have been inverted in the formula.

With this translation we are able to achieve the following result.

Lemma 3.2 For any finite set of axioms T, the sequent ⊢ Γ is provable in theory T if and only if ⊢ [T], Γ is provable.

3.3 And-Branching Two Counter Machines Without Zero-Test

We introduce a nondeterministic two counter machine with and-branching but without a zero-test instruction. Intuitively, Q_{i} F ork Q_{j}, Q_{k} is an instruction which allows a machine in state Q_{i} to continue computation from both states Q_{j} and Q_{k}, each computation continuing with the current counter values. For brevity in the following proofs, we emphasize two counter machines. More formally, an And-Branching Two Counter Machine Without Zero-Test, or acm for short, is given by a finite set Q of states, a finite set δ of transitions, and distinguished initial and final states, Q_{I} and Q_{F}, as follows.

An instantaneous description, or ID, of an acm M is a list of ordered triples ⟨Q_{i}, A, B⟩, where Q_{i} ∈ Q, and A and B are natural numbers, each corresponding to a counter of the machine.

We define the accepting triple as ⟨Q_{F} , 0, 0⟩. We also define an accepting ID as any ID where every element of the ID is the accepting triple. That is, every andbranch of the computation has reached an accepting triple. We say that an acm accepts input n if and only if there is some computation from initial ID {⟨Q_{I}, n, 0⟩} to an accepting ID. It is essential for our undecidability result that both counters be zero in all elements of an accepting ID.

The set δ may contain transitions of the following form:

(Q_{i} Increment A Q_{j}) taking

⟨Q_{i}, A, B⟩ to ⟨Q_{j}, A + 1, B⟩

(Q_{i} Increment B Q_{j}) taking

⟨Q_{i}, A, B⟩ to ⟨Q_{j}, A, B + 1⟩

(Q_{i} Decrement A Q_{j}) taking

⟨Q_{i}, A + 1, B⟩ to ⟨Q_{j}, A, B⟩

(Q_{i} Decrement B Q_{j}) taking

⟨Q_{i}, A, B + 1⟩ to ⟨Q_{j}, A, B⟩

(Q_{i} Fork Q_{j}, Q_{k}) taking ⟨Q_{i}, A, B⟩ to (⟨Q_{j}, A, B⟩, ⟨Q_{k}, A, B⟩)

where the Q_{i}, Q_{j}, and Q_{k} are states in Q. Note that the Decrement instructions only apply if the appropriate counter is not zero.

Thus, for example, the single transition Q_{i} Increment Q_{j} takes an acm from ID: {⋯, ⟨Q_{i}, A, B⟩, ⋯} to ID: {⋯, ⟨Q_{j}, A + 1, B⟩, ⋯}

Since we may simulate a zero-test with andbranching, using the fact that all branches must terminate with counters set to zero, acceptance by an andbranching machines is undecidable.

Lemma 3.3 It is undecidable whether an andbranching two counter machine without zero-test accepts input 0. This remains so if the transition relation of the machine is restricted so that there are no outgoing transitions from the final state.

3.4 From Machines to Logic

We will write C^{n} to indicate a sequence of n C’s, separated by commas.

We have already seen how the linear connective & may be used to achieve and-branching in the proof of pspace-completeness of mall. We now make use of that, along with some other machinery, to simulate acm computation.

Given an acm M = ⟨Q, δ, Q_{I}, Q_{F} ⟩ we define a linear logic theory from the transition relation δ as follows:

Q_{i} Increment A Q_{j} ↦ ⊢ q_{i}^{⊥}, (q_{j} ⊗ a)
Q_{i} Increment B Q_{j} ↦ ⊢ q_{i}^{⊥}, (q_{j} ⊗ b)
Q_{i} Decrement A Q_{j} ↦ ⊢ q_{i}^{⊥}, a^{⊥}, q_{j}
Q_{i} Decrement B Q_{j} ↦ ⊢ q_{i}^{⊥}, b^{⊥}, q_{j}
Q_{i} Fork Q_{j}, Q_{k} ↦ ⊢ q_{i}^{⊥}, (q_{j} ⊕ q_{k})

Using linear implication, the “Q_{i} Increment B Q_{j}” transition may be viewed as ⊢ q_{i}−∘(q_{j} ⊗ b), i.e., from state Q_{i}, move to state Q_{j} and add one to B.

Given an element of an ID of an acm ⟨Q_{i}, x, y⟩, we define a translation θ:

θ(⟨Q_{i}, x, y⟩) =^{Δ} ⊢ q_{i}^{⊥}, (a^{⊥})^{x}, (b^{⊥})^{y}, q_{F}

Thus all sequents which correspond to elements of acm ID’s have exactly one positive literal, q_{F}, some number of a^{⊥}s, and b^{⊥}s, the multiplicity of which correspond to the values of the two counters of the acm, and exactly one other negative literal, which corresponds to the current state of the acm.

The translation of an acm ID is simply the set of translations of the elements of the ID. We claim that an acm M halts from ID if and only if every element of θ(ID) is provable in the theory corresponding to the transition relation of the machine.

Lemma 3.4 (Machine ⇒) An and-branching counter machine M accepts from ID only if θ(ID) is provable in the theory derived from M.

Given a halting computation of an ACM machine M from ID we must build a proof of θ(ID) in the theory derived from M. This may be accomplished by induction on the length of accepting acm computation.

Lemma 3.5 (Machine ⇐) An and-branching counter machine M accepts from ID if θ(ID) is provable in the theory derived from M.

Given a proof of θ(ID) in the theory derived from M, we must show that a halting computation of the acm M from state ID can be extracted from that proof. We achieve this with the aid of cut standardization, Lemma 3.1, which in this case leaves cuts in the proof only where they correspond to applications of acm instructions. We may thus simply read the description of the computation from the normalized proof. The formal proof of this lemma proceeds by induction on the length of the standardized proof, and depends on the particular encoding of the acm state.

3.5 Example Computation

This section is intended to give an overview of the mechanisms we have defined above, and lend some insight into our undecidability result, stated below. We present a simple computation of an ordinary two counter machine with zero-test instruction, a corresponding acm computation, and a corresponding linear logic proof. The overall structure is that searching for a proof of a sequent is analogous to searching for an accepting acm computation.

If the transition relation δ of a standard two counter machine with zero-test consists of the following:

δ_{1} : : = Q_{I} Increment A Q_{2}
δ_{2} : : = Q_{3} Decrement A Q_{F}
δ_{3} : : = Q_{2} ZeroTest B Q_{3}

then the machine may perform the following transitions, where an instantaneous description of a two

\overline{⊢ z_{B}^{⊥}, a^{⊥}, z_{B}}^{T4}  \underline{\overline{⊢ z_{B}^{⊥}, (q_{F} ⊕ q_{F})}^{T5}  \underline{\overline{⊢ q_{F}^{⊥}, q_{F}}^{I}  \overline{⊢ q_{F}^{⊥}, q_{F}}^{I}}_{&} ; ⊢ (q_{F}^{⊥} & q_{F}^{⊥}), q_{F}}_{Cut} ; ⊢ z_{B}^{⊥}, q_{F} Cut

⊢ z_{B}^{⊥}, a^{⊥}, q_{F}

Figure 3: Zero-test proof

⊢ q_{I}^{⊥}, (q_{2} ⊗ a) T1

\overline{⊢ q_{2}^{⊥}, (z_{B} ⊕ q_{3})}^{T3}  \underline{⋮ ; ⊢ z_{B}^{⊥}, a^{⊥}, q_{F}  \underline{\overline{⊢ q_{3}^{⊥}, a^{⊥}, q_{F}}^{T2} \overline{⊢ q_{F}^{⊥}, q_{F}}^{I}}_{Cut} ; ⊢ q_{3}^{⊥}, a^{⊥}, q_{F}}_{&} ; ⊢ (z_{B}^{⊥} & q_{3}^{⊥}), a^{⊥}, q_{F} Cut

⊢ q_{2}^{⊥}, a^{⊥}, q_{F}

\overline{⊢ (q_{2}^{⊥}℘a^{⊥}), q_{F}}^{℘} Cut

⊢ q_{I}^{⊥}, q_{F}

Figure 4: Proof corresponding to computation

counter machine is given by the triple consisting of Q_{j}, the current state, and the values of counters A and B.

⟨Q_{I}, 0, 0⟩ ⟶^{δ_{1}} ⟨Q_{2}, 1, 0⟩ ⟶^{δ_{3}} ⟨Q_{3}, 1, 0⟩ ⟶^{δ_{2}} ⟨Q_{F} , 0, 0⟩

This computation starts in state Q_{I}, increments the A counter and steps to state Q_{2}. Then it tests the B counter for zero, and moves to Q_{3}, where it then decrements the A counter, moves to Q_{F}, and accepts.

The transition relation δ may be translated into a transition relation δ′ for an and-branching two counter machine without zero-test. The modified relation δ′ (shown on the left below), may then be encoded as a linear logic theory (shown on the right):

Transitions

δ′_{1} : : = Q_{I} Increment A Q_{2}
δ′_{2} : : = Q_{3} Decrement A Q_{F}
δ′_{3} : : = Q_{2} Fork Z_{B}, Q_{3}
δ′_{4} : : = Z_{B} Decrement A Z_{B}
δ′_{5} : : = Z_{B} Fork Q_{F} , Q_{F}

Theory Axioms

⊢ q_{I}^{⊥}, (q_{2} ⊗ a) T_{1}
⊢ q_{3}^{⊥}, a^{⊥}, q_{F}  T_{2}
⊢ q_{2}^{⊥}, (z_{B} ⊕ q_{3}) T_{3}
⊢ z_{B}^{⊥}, a^{⊥}, z_{B}  T_{4}
⊢ z_{B}^{⊥}, (q_{F} ⊕ q_{F}) T_{5}

Notice how the first two transitions (δ_{1} and δ_{2}) of the standard two counter machine are preserved in the translation from δ to δ′. Also, the ZeroTest instruction δ_{3} is encoded as three acm transitions — δ′_{3}, δ′_{4}, and δ′_{5}. The transition δ′_{3} is a fork to a special state Z_{B}, and one other state, Q_{3}. The two extra transitions, δ′_{4} and δ′_{5}, embody the encoding of that special zero-testing state, Z_{B}, of the acm. Given the above transitions, the and-branching machine without zerotest may then perform these moves:

{⟨Q_{I}, 0, 0⟩} ⟶^{δ′_{1}} {⟨Q_{2}, 1, 0⟩} ⟶^{δ′_{3}} {⟨Z_{B}, 1, 0⟩, ⟨Q_{3}, 1, 0⟩}

⟶^{δ′_{4}} {⟨Z_{B}, 0, 0⟩, ⟨Q_{3}, 1, 0⟩} ⟶^{δ′_{5}}

{⟨Q_{F} , 0, 0⟩, ⟨Q_{F} , 0, 0⟩, ⟨Q_{3}, 1, 0⟩} ⟶^{δ′_{2}}

{⟨Q_{F} , 0, 0⟩, ⟨Q_{F} , 0, 0⟩, ⟨Q_{F} , 0, 0⟩}

Note that the instantaneous descriptions of this andbranching machine is a list of triples, and the machine accepts if and only if it is able to reach ⟨Q_{F} , 0, 0⟩ in all branches of its computation. This particular computation starts in state Q_{I}, increments the A counter and steps to state Q_{2}. Then it forks into two separate computations; one which verifies that the B counter is zero, and the other which proceeds to state Q_{3}. The B counter is zero, so the proof of that branch proceeds by decrementing the A counter to zero, and essentially jumping to the final state Q_{F}. The other branch from state Q_{3} simply decrements A and moves to Q_{F}. Thus all branches of the computation terminate in the final state with both counters at zero, resulting in an accepting computation.

The linear logic proof corresponding to this computation is displayed in Figures 3 and 4. In these proofs, each application of a theory axiom (T rule) corresponds to one step of acm computation. We represent the values of the acm counters in unary by copies of the formulas a^{⊥} and b^{⊥}. In this example the B counter is always zero, so there are no occurrences of b^{⊥}.

The proof shown in Figure 3 of ⊢ z_{B}^{⊥}, a^{⊥}, q_{F} in the above linear logic theory (T_{1} through T_{5}) corresponds to the acm verifying that the B counter is zero. Reading the proof bottom up, it begins by cutting against the theory axiom T_{4}, leaving the sequent ⊢ z_{B}^{⊥}, q_{F} as an intermediate step. Correlating with the acm computation, T_{4} corresponds to the Decrement A instruction δ′_{4}, and ⊢ z_{B}^{⊥}, q_{F} has exactly one less a^{⊥} than ⊢ z_{B}^{⊥}, a^{⊥}, q_{F}. The next step is to cut against axiom T_{5}, and after application of the & rule, we have two sequents left to prove — ⊢ q_{F}^{⊥}, q_{F} and ⊢ q_{F}^{⊥}, q_{F}. Both of these correspond to the acm triple ⟨Q_{F} , 0, 0⟩ which is the accepting triple, and are provable by the identity rule. If we had attempted to prove this sequent with some occurrences of b^{⊥}, we would be unable to complete the proof.

The proof shown in Figure 4 of ⊢ q_{I}^{⊥}, q_{F} in the same theory demonstrates the remainder of the acm machinery. The lowermost introduction of a theory axiom, T_{1}, cut, and ℘ together correspond to the application of the increment instruction δ′_{1}. That is, the q_{I}^{⊥} has been “traded in” for q_{2}^{⊥} along with a^{⊥}. The application of T_{3}, cut, and & correspond to the fork instruction, δ′_{3}, which requires that both branches of the proof be successful in the same way that and-branching machines require all branches to reach an accepting configuration. The elided proof of ⊢ z_{B}^{⊥}, a^{⊥}, q_{F} appears in Figure 3, and corresponds to the verification that the B counter is zero. The application of T_{2}, cut, and identity correspond to the final decrement instruction of the computation, and complete the proof.

From the earlier lemmas, our main result is provable.

Theorem 3.6 The provability problem for propositional linear logic is recursively unsolvable.

As mentioned earlier, linear logic, like classical logic, has an intuitionistic fragment. Briefly, the intuitionistic fragment is restricted so that there is only one positive formula in any sequent. In fact, the entire construction above was carried out in intuitionistic linear logic, and thus the undecidability result also holds for this logic.

4 Additional Results

The pure multiplicative fragment (without additive connectives or storage operator) is the simplest fragment of linear logic that we have investigated.

Theorem 4.1 !-free multiplicative linear logic is in np.

The proof is straightforward: Each connective in the conclusion sequent is the principle connective in exactly one proof step in any cut-free proof, thus giving a polynomial bound on the size of cut-free proofs. Thus the entire proof may be guessed in polynomial time.

We have been unable to prove this fragment npcomplete. We now believe that this may be very difficult, due to the lack of redundancy in this problem [11]. As part of our investigation of the need to discard arbitrary resources to achieve np-completeness, we studied propositional logic with weakening, but without contraction, which is sometimes called Direct Logic [23]. This is equivalent to linear logic with the structural modification of adding the weakening rule.

Weakening \frac{⊢ Σ}{⊢ A, Σ}

Theorem 4.2 !-free multiplicative linear logic with weakening is NP-Complete.

Provability in this logic is in np by the same reasoning as the previous fragment: multiplicative sequent proofs are polynomially short, and may be guessed. Provability is np-hard by reduction from Vertex Cover. In this reduction, weakening appears essential since an edge may be covered by selecting one endpoint or both. Finally, we investigate linear logic where we consider sequents to be cyclic lists of formula, instead of multisets, and add an explicit exchange rule limited to reusable formulas. We also add a Rotate rule which allows formulas to circulate, so that the proof rules in Appendix A are applicable to more than just the end formulas of a sequent. This logic has been called noncommutative linear logic, cyclic linear logic, but we call it circular logic [16, 34].

Exchange ? \frac{⊢ Σ, Γ,?A}{⊢ Σ,?A, Γ}

Rotate  \frac{⊢ Σ, A}{⊢ A, Σ}

Theorem 4.3 Noncommutative propositional multiplicative linear logic is undecidable, even without additives.

This result is obtained by reduction from semi-Thue systems. A rule such as “ABC → DE” is faithfully represented by the circular logic formula !(A ⊗ B ⊗ C −∘ D ⊗ E), since in this logic ⊗ is not commutative. Although the main idea behind this reduction is straightforward, substantial proof-theoretic machinery is required to demonstrate that the reduction is correct. An immediate corollary of this theorem is that full noncommutative propositional linear logic (with additives) is undecidable.

5 Conclusion

We have investigated the complexity of provability for several fragments of propositional linear logic. Our most significant results are that provability for full propositional linear logic is undecidable, but that provability becomes pspace complete when the modal storage operator is removed. This gives some interesting insight into the power of reuse when combined with linear propositional connectives. We have also shown that the decision problem for the multiplicative fragment is in np, and becomes np-complete in the presence of unrestricted weakening. Finally, we have shown that provability for circular logic (the noncommutative fragment of linear logic without additive connectives) is also undecidable.

A few open problems remain. We have been unable to establish tight bounds for the multiplicative fragment or settle the decidability of the multiplicatives with the storage operator. The latter seems particularly difficult, since a positive solution would involve an extension of the reachability algorithm for Petri nets. The final open problem, which may have logical interest, is the decidability of the !-free fragment, extended with propositional quantifiers.

References

[1] S. Abramsky and S. Vickers. Quantales, observational logic, and process semantics. Preprint, January 1990.

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

[3] A. Asperti. A logic for concurrency. Technical report, Dipartimento di Informatica, Universitá di Pisa, 1987.

[4] A. Asperti, G.-L. Ferrari, and R. Gorrieri. Implicative formulae in the ‘proofs as computations’ analogy. In Proc. 17-th ACM Symp. on Principles of Programming Languages, San Francisco, pages 59–71, January 1990.

[5] A. Bawden. Connection graphs. In Proc. ACM Symp. on Lisp and Functional Programming, pages 258–265, 1986.

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

[7] S. Cerrito. A linear semantics for allowed logic programs. In Proc. 5-th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990.

[8] P. Clote. On the finite containment problem for Petri nets. Theoretical Computer Science, 43:99–105, 1986.

[9] V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181–203, 1989.

[10] U. Engberg and G. Winskel. Petri nets as models of linear logic. In A. Arnold, editor, Proceedings of CAAP’90. Lecture Notes in Computer Science vol. 431, Springer, 1990.

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

[12] V. Gehlot and C.A. Gunter. Normal process representatives. In Proc. 5-th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990.

[13] G. Gentzen. Collected Works. Edited by M.E. Szabo. North-Holland, Amsterdam, 1969.

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

[15] J.-Y. Girard.  Multiplicatives.  Rendiconti del

Seminario Matematico dell’ Universitá e Politecnico Torino, Special Issue on Logic and Computer Science, pages 11–33, 1987.

[16] J.-Y. Girard. Towards a geometry of interaction. In: Contemporary Math. 92, Amer. Math. Soc., 1989. 69-108.

[17] J.-Y. Girard. La logique linéaire. Pour La Science, Édition Francaise de Scientific American, 150:74–85, April 1990.

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

[19] J.-Y. Girard, A. Scedrov, and P.J. Scott. Bounded linear logic: A modular approach to polynomial time computability. In Proc. Math. Sci. Institute Workshop on Feasible Mathematics, Cornell University, June, 1988. Birkhauser, 1990.

[20] C.A. Gunter and V. Gehlot. Nets as tensor theories. In G. De Michelis, editor, Proc. 10-th International Conference on Application and Theory of Petri Nets, Bonn, pages 174–191, 1989.

[21] J.C. Guzman and P. Hudak. Single-threaded polymorphic lambda calculus. In Proc. 5-th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990.

[22] J.R. Hindley and J.P. Seldin. Introduction to Combinators and Lambda Calculus. London Mathematical Society Student Texts, Cambridge University Press, 1986.

[23] J. Ketonen and R. Weyhrauch. A decidable fragment of predicate calculus. Theoretical Computer Science, 32, 1984.

[24] S.R. Kosaraju. Decidability of reachability in vector addition systems. In Proc. 14-th ACM Symp. on Theory of Computing, pages 267–281, 1982.

[25] Y. Lafont. The linear abstract machine. Theoretical Computer Science, 59:157–180, 1988.

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

[27] J. Lambek. The mathematics of sentence structure. Amer. Math. Monthly, 65:154–169, 1958.

[28] P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. Technical Report SRI-CSL-90-08, CSL, SRI International, 1990.

[29] R. Lipton. The reachability problem is exponentialspace hard. Technical Report 62, Department of Computer Science, Yale University, January 1976.

[30] N. Marti-Oliet and J. Meseguer. From Petri nets to linear logic. In: Springer LNCS 389, ed. by D.H. Pitt et al., 1989. 313-340.

[31] E. Mayr and A. Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46:305–329, 1982.

[32] E.W. Mayr. An algorithm for the general Petri net reachability problem. In Proc. 13-th ACM Symp. on Theory of Computing, Milwaukee, pages 238–246, 1981.

[33] K. McAloon. Petri nets and large sets. Theoretical Computer Science, 32:173–183, 1984.

[34] D.N. Yetter. Quantales and (noncommutative) linear logic. Journal of Symbolic Logic, 55:41–64, 1990.

A Propositional Linear Logic Proof Rules

A linear logic sequent is a ⊢ followed by a multiset of linear logic formulas. 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 identity, cut, tensor, par, plus, with, weakening, contraction, dereliction, storage, bottom, one, and top, respectively. Note that there is no rule for the 0 constant.

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

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

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

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

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

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

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

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

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

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

⊥  \frac{⊢ Σ}{⊢ Σ, ⊥}
1  \overline{⊢ 1}
⊤  \overline{⊢ Σ, ⊤}

Linear negation is defined as follows:

(p_{i})^{⊥} =^{Δ} p_{i}^{⊥}
(p_{i}^{⊥})^{⊥} =^{Δ} p_{i}
(A ⊗ B)^{⊥} =^{Δ} A^{⊥}℘B^{⊥}
(A℘B)^{⊥} =^{Δ} A^{⊥} ⊗ B^{⊥}
(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