First Order Linear Logic Without Modalities is NEXPTIME-Hard

Patrick Lincoln^{∗}  Andre Scedrov^{†}

Abstract

The decision problem is studied for the nonmodal or multiplicative-additive fragment of first order linear logic. This fragment is shown to be nexptimehard. The hardness proof combines Shapiro’s logic programming simulation of nondeterministic Turing machines with the standard proof of the pspacehardness of quantified boolean formula validity, utilizing some of the surprisingly powerful and expressive machinery of linear logic.

1 Introduction

Linear logic, introduced by Girard, is a resource-sensitive refinement of classical logic [10, 29]. Linear logic gains its expressive power by restricting the “structural” proof rules of contraction (copying) and weakening (erasing). The contraction rule makes it possible to reuse any stated assumption as often as desired. The weakening rule makes it possible to use dummy assumptions, i.e., it allows a deduction to be carried out without using all of the hypotheses. Because contraction and weakening together make it possible to use an assumption as often or as little as desired, these rules are responsible for what one may see in hindsight as a loss of control over resources in classical (and intuitionistic) logic. Without contraction or weakening, as in linear logic, propositions may be thought of as process states, events, or resources, which must be carefully accounted for. One may then isolate two distinct forms of conjunction and disjunction, one form called “multiplicative”, and the other “additive”. Viewing the hypotheses as resources, a proof of a multiplicative conjunction as a conclusion forbids any sharing between the resources used to establish each conjunct, whereas the additive conjunction requires the sharing of all of the resources. Full linear logic also involves a kind of modality: a “storage” or “reuse” operator, !. Intuitively, the hypothesis !A provides unlimited reuse of the resource A. The usual function type A ⇒ B can be recovered as !A−∘B , where −∘ is linear implication, which provides the type of functions that “use” their argument exactly once.

∗lincoln@cs.stanford.edu Computer Science Laboratory, SRI International, Menlo Park, CA 94025-3493. Initial results obtained during the visit to University of Pennsylvania in February 1992, supported by the Institute of Research in Cognitive Science.

†andre@cis.upenn.edu Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104-6395. Partially supported by NSF Grant CCR-91-02753 and by ONR Grants N00014-88-K-0635 and N00014-92-J-1916.

Basic constructions on vector spaces provide a first, naive interpretation of linear logic connectives, much as the basic operations on sets provide an interpretation of usual logical connectives. For instance, multiplicative conjunction is interpreted as tensor product. More subtle points of linear logic originate in so-called coherence spaces, which maintain a notion of finite basis and isomorphism with the double dual without imposing isomorphism with the dual. Similar phenomena have been observed in certain natural set-theoretic operations on infinite games [6, 7] and in so-called -autonomous categories [5]. Event spaces, which come about from semantics of concurrency, provide another semantic framework for linear logic [23]. A mathematical setting for dynamic aspects of cut elimination is provided by proof nets [10, 9] and in a deeper sense by Girard’s geometry of interaction [11, 12, 8, 24, 1, 13, 14].

Among the computer science ramifications of linear logic, the methods of this paper are closest to what may be broadly called logic programming ramifications, in which computation is expressed by cut-free proof search in certain linear logic theories. Recent topics in this direction include a treatment of object-style inheritance and linear logic programming [3, 4, 2, 15], a treatment of concurrent constraint programming [25], and a closely related treatment of Milner’s π-calculus [22].

The remarkable expressiveness of cut-free linear logic proof search as a computational paradigm is also indicated by the complexity and undecidability of provability in fragments of linear logic. These results are consequences of direct, lockstep simulations of computations on generic machines by cut-free proof search in fragments of linear logic. Provability in full propositional (i.e., quantifier-free) linear logic is undecidable [18]. However, even the fragment of linear logic that does not allow modalities is strikingly expressive: provability of multiplicative propositional formulas is np-complete [17]. In fact, the decision problem for constant-only formulas in multiplicative propositional linear logic is also np-complete [20]. If the additives are also allowed, provability for propositional formulas is pspace-complete [18], and in fact this fragment allows a structural embedding of a cut-free proof system for implicational propositional intuitionistic logic [19]. The decidability of second order propositional linear logic without modalities is an open problem.

In the remainder of the paper we shall restrict our attention to the nonmodal, or multiplicative-additive linear logic with first order quantifiers and function symbols, mall1. Because the depth of a cut-free proof tree is still linear in the size of the conclusion, as in the case of the propositional multiplicative-additive fragment, it can be seen that without function symbols, mall1 is still pspace-complete. However, in the presence of function symbols the complexity is different in spite of the same bound on the depth. It is shown that provability in mall1 is nexptime-hard (Theorem 5.4).

The hardness result is achieved through a direct encoding of Turing machine transitions, which are shared via the additives, and the existential quantification over intermediate Turing machine configurations. The linear depth bound on cut-free mall1 proofs gives an immediate single exponential upper bound on the number of Turing machine transitions that can be used in the entire proof using this encoding. In contrast to previous work on linear logic proof search as a computational paradigm (see above), in which a computation proceeds “upwards” along a proof tree, here the computation steps are applied “horizontally across” the leaves of a proof tree.

It is likely that the membership of mall1 in nexptime, and hence its nexptime-completeness, may be shown by a decision procedure based on dynamic skolemization. This technique, developed for theorem proving in intuitionistic logic [26], falls outside of the scope of this paper.

The precise descriptions of mall1 and of the particular version of nondeterministic (single) exponential time Turing machines are given in Section 2. An encoding of nondeterministic exponential time Turing machines by mall1 formulas is given in Section 3. This encoding is reminiscent of the standard proof of the pspace-hardness of quantified boolean formula validity [28, 16]. The encoding is also related to the logic programming simulation of Turing machines given in [27]. In Section 4 it is shown that whenever a nondeterministic exponential time Turing machine accepts, then the mall1 formula encoding the machine is provable. The converse is shown in Section 5.

We would like to thank Yuri Gurevich for suggesting that the logic programming simulation of Turing machines given in [27] may be a source of lower bounds for the complexity of mall1. This suggestion eventually led us to formulate the encoding given in Section 3. We would also like to thank Jean-Marc Andreoli, Jawahar Chirimar, Jean Gallier, Jean-Yves Girard, Carl Gunter, Joshua Hodas, Jim Lipton, Dale Miller, John Mitchell, Jon Riecke, Vijay Saraswat, Phil Scott, Natarajan Shankar, and Tim Winkler for interesting and inspiring discussions.

2 Preliminaries

Let us begin by specifying the logical framework and the particular version of nondeterministic Turing machines considered in this paper.

2.1 Logical Framework

Gentzen-style sequent calculus is the formal logical framework throughout the paper. For our purposes it is convenient to consider sequents of the form Γ ⊢ Δ where Γ, Δ are finite multisets of formulas. Note that in standard presentations of sequent calculi, sequents are often built from sets of formulas, where we use multisets here. This difference is crucial. We assume a set of function symbols and predicate symbols, along with their associated arities. Atomic formulas (other than constants 1, ⊥, ⊤, 0) are of the form P (t_{1}, …, t_{n}) where t_{1}, …, t_{n} are terms and P is a predicate symbol of arity n, as usual in first order predicate calculus. Note that there is no equality symbol. The inference rules for the mall1 sequent calculus are given in Figure 1.

The following notational conventions are observed throughout this paper:

H  Positive atomic formula P (t_{1}, …, t_{n})
H^{⊥}  Negated atomic formula P (t_{1}, …, t_{n})^{⊥}
A, B, C  Arbitrary formulas
Γ, Δ, Σ, Θ, Ξ  Arbitrary finite multisets of formulas

In the ∀R and ∃L rules in Figure 1 it is assumed that X is not free in Γ, Δ. The English names for the rules given in Figure 1 are identities, tensor, linear implication, plus, with, bottom, one, zero, top, universal, existential, and cut, respectively. ⊗, −∘, and ^{⊥} are multiplicative connectives; 1 and ⊥ are multiplicative propositional constants. ⊕ and & are additive connectives; 0 and ⊤ are additive propositional constants. Observe the “additive” nature of the quantifiers. For notational convenience, it is often assumed that −∘ and ⊗ associate to the right, and that ⊗ has higher precedence than −∘.

I+  \overline{H ⊢ H}  \overline{H^{⊥} ⊢ H^{⊥}}  I-
IL  \overline{H, H^{⊥} ⊢}  \overline{⊢ H, H^{⊥}}  IR

⊗L  \frac{Γ, A, B ⊢ Δ}{Γ, (A ⊗ B) ⊢ Δ}  \frac{Σ ⊢ A, Θ  Γ ⊢ B, Δ}{Σ, Γ ⊢ (A ⊗ B), Θ, Δ} ⊗R

−∘L \frac{Σ ⊢ A, Θ  Γ, B ⊢ Δ}{Σ, Γ, (A−∘B) ⊢ Θ, Δ}  \frac{Γ, A ⊢ B, Δ}{Γ ⊢ (A−∘B), Δ}  −∘R

⊕L \frac{Γ, A ⊢ Δ  Γ, B ⊢ Δ}{Γ, (A ⊕ B) ⊢ Δ}  \frac{Γ ⊢ A, Δ  Γ ⊢ B, Δ}{Γ ⊢ (A & B), Δ} & R

& L1  \frac{Γ, A ⊢ Δ}{Γ, (A & B) ⊢ Δ}  \frac{Γ ⊢ A, Δ}{Γ ⊢ (A ⊕ B), Δ}  ⊕R1

& L2  \frac{Γ, B ⊢ Δ}{Γ, (A & B) ⊢ Δ}  \frac{Γ ⊢ B, Δ}{Γ ⊢ (A ⊕ B), Δ}  ⊕R2

⊥L  \overline{⊥ ⊢}  \frac{Γ ⊢ Δ}{Γ ⊢ ⊥, Δ}  ⊥R

1L  \frac{Γ ⊢ Δ}{Γ, 1 ⊢ Δ}  \overline{⊢ 1}  1R
0L  \overline{Γ, 0 ⊢ Δ}  \overline{Γ ⊢ ⊤, Δ}  ⊤R

∀L  \frac{Γ, A[t/X] ⊢ Δ}{Γ, ∀X.A ⊢ Δ}  \frac{Γ ⊢ A, Δ}{Γ ⊢ ∀X.A, Δ}  ∀R

∃L  \frac{Γ, A ⊢ Δ}{Γ, ∃X.A ⊢ Δ}  \frac{Γ ⊢ A[t/X], Δ}{Γ ⊢ ∃X.A, Δ}  ∃R

\frac{Σ ⊢ A, Θ  A, Γ ⊢ Δ}{Σ, Γ ⊢ Θ, Δ} Cut

Figure 1: Rules for mall1

An analysis is the process of applying a rule to a sequent matching the conclusion of the rule in order to generate the corresponding premises. The principal formula of the rule is then said to be analyzed by the reduction. A mall1 proof is represented as a tree rooted at its conclusion sequent at the bottom and with the leaves at the top. Given this orientation, the notion of a rule occurring above or below another rule should be clear.

The reader will note that linear negation is a defined concept on composite formulas, not a basic connective. One may define negation by recursion on the structure of formulas: (H^{⊥})^{⊥} is H, (A ⊗ B)^{⊥} is A−∘B^{⊥}, (A−∘B)^{⊥} is A ⊗ B^{⊥}, (A & B)^{⊥} is A^{⊥} ⊕ B^{⊥}, (A ⊕ B)^{⊥} is A^{⊥} & B^{⊥}, (∀X.A)^{⊥} is ∃X.A^{⊥}, (∃X.A)^{⊥} is ∀X.A^{⊥}, 1^{⊥} is ⊥, ⊥^{⊥} is 1, ⊤^{⊥} is 0, and 0^{⊥} is ⊤. If Γ consists of A_{1}, …, A_{n}, then Γ^{⊥} denotes A_{1}^{⊥}, …, A_{n}^{⊥}.

Although the identity rules (i.e., the first four rules in Figure 1) are restricted to atomic formulas H, the analogous identity rules for arbitrary formula A instead of H are derivable. Negation rules are derivable as well, namely from Γ, A ⊢ Δ one can infer Γ ⊢ A^{⊥}, Δ, and from Γ ⊢ A, Δ one can infer Γ, A^{⊥} ⊢ Δ. The reader will also observe that the linear logic connective par may be defined by letting A℘B be A^{⊥}−∘B and that the par rule [10] is derivable. In fact, our sequent calculus presentation is equivalent to the first order sequent calculus in [10] without exponentials ! ,? . More precisely, a sequent Γ ⊢ Δ is provable in mall1 (without cut) iff the sequent ⊢ Γ^{⊥}, Δ is provable (without cut, respectively) in the first order sequent calculus in [10], excluding exponentials. In particular, cut-elimination for mall1 follows from the cut-elimination shown in [10], see also [18]. For the record:

Theorem 2.1 If a sequent is provable in mall1, then it is provable in mall1 without using the Cut rule.

We end this section by considering some technical properties of mall1, in particular so-called permutability properties, some of which have been discussed in several texts [2, 21].

The sign of a formula is defined using the transformations below:

\begin{aligned}[A−∘B]^{+} & = & [A]^{−}−∘[B]^{+} \\ [A ⊗ B]^{+} & = & [A]^{+} ⊗ [B]^{+} \\ [Σ, A]^{+} & = & [Σ]^{+}, [A]^{+} \\ [A^{⊥}]^{+} & = & ([A]^{−})^{⊥} \\ [A−∘B]^{−} & = & [A]^{+}−∘[B]^{−} \\ [A ⊗ B]^{−} & = & [A]^{−} ⊗ [B]^{−} \\ [Σ, A]^{−} & = & [Σ]^{−}, [A]^{−} \\ [A^{⊥}]^{−} & = & ([A]^{+})^{⊥} \end{aligned}

The sign of an instance of a formula A in a sequent Σ ⊢ Δ is given by the superscript on A in [Σ]^{−} or [Δ]^{+}. That is, if an instance of formula A ends up as [A]^{+}, then it is positive. If an instance of formula A ends up as [A]^{−}, then it is negative.

A sequent is said to be balanced if it has the same number of positive and negative occurrences of atoms other than constants. Otherwise, a sequent is said to be unbalanced. A sequent is said to be multiplicative if it contains only formulas built of atoms other than 0,⊤, of their negations, or of connectives ⊗ or −∘ . It is linear logic folklore that all provable multiplicative sequents are balanced, and therefore no unbalanced multiplicative sequents can be provable. This property is readily shown by induction on cut-free proofs.

Proposition 2.2 A multiplicative sequent is provable only if it is balanced.

Note that this property fails for full mall1 and other fragments of linear logic that include the additive connectives and constants.

The following properties all follow by induction on the height of cut-free proof. These are permutability properties, as they ensure that if a proof exists, then a proof of a certain permuted form exists. That is, one may permute the order of application of inferences in a proof to achieve a kind of normal form. These properties are used to give control over the shape of linear logic proofs, thus enabling a more direct computational reading.

Proposition 2.3 If a sequent Γ, A ⊕ B ⊢ Δ is provable in mall1, then so are Γ, A ⊢ Δ and Γ, B ⊢ Δ.

Proposition 2.4 If a sequent Γ ⊢ A&B, Δ is provable in mall1, then so are Γ ⊢ A, Δ and Γ ⊢ B, Δ.

Proposition 2.5 If a sequent Γ, A ⊗ B ⊢ Δ is provable in mall1, then so is Γ, A, B ⊢ Δ.

Proposition 2.6 If a sequent Γ ⊢ A−∘B, Δ is provable in mall1, then so is Γ, A ⊢ B, Δ.

Proposition 2.7 If a sequent Γ, ∃X.A ⊢ Δ is provable in mall1, then so is Γ, A[t/X] ⊢ Δ for any term t.

Proposition 2.8 If a sequent Γ ⊢ ∀X.A, Δ is provable in mall1, then so is Γ ⊢ A[t/X], Δ for any term t.

Proposition 2.9 If a sequent Γ, A&B ⊢ Δ is provable in mall1, where Γ, Δ contain only negative occurrences of & and positive occurrences of ⊕, then Γ, A ⊢ Δ or Γ, B ⊢ Δ is provable in mall1.

Proposition 2.10 If a sequent Γ ⊢ A ⊕ B, Δ is provable in mall1, where Γ, Δ contain only negative occurrences of & and positive occurrences of ⊕, then Γ ⊢ A, Δ or Γ ⊢ B, Δ is provable in mall1.

Proposition 2.11 If a sequent Γ, ∀X.A ⊢ Δ is provable in mall1, where Γ, Δ contain only positive occurrences of ⊕ and ∃ and only negative occurrences of & and ∀, then for some term t, Γ, A[t/X] ⊢ Δ is provable in mall1.

Proposition 2.12 If a sequent Γ ⊢ ∃X.A, Δ is provable in mall1, where Γ, Δ contain only positive occurrences of ⊕ and ∃ and only negative occurrences of & and ∀, then for some term t, Γ ⊢ A[t/X], Δ is provable in mall1.

2.2 nexptime Turing Machines

For definiteness, let us agree that “Turing machine” means the following kind of nondeterministic machine. These machines have one tape and no transitions are applicable in the final state. More precisely, such a machine is given by the tuple ⟨Q, S, T , δ, q_{0}, ♭, q_{F} ⟩, where:

• Q is a finite set of states,

• q_{0} ∈ Q is the (unique) initial state,

• q_{F} ∈ Q is the (unique) final state, • T is a finite set of allowable tape symbols, disjoint from Q,

• S ⊂ T is a finite set of input symbols,

• ♭ ∈ T \S is the blank symbol,

• δ is the next move relation, a relation from (Q \ {q_{F} }) × T to Q × T × {Left, Right},

For instance, if δ contains move instructions q_{5}, c ↦ q_{6}, d, Left and q_{5}, c ↦ q_{3}, d, Right, then one may informally say that the Turing machine M in state q_{5}, where the tape symbol c is currently under the read/write head, can make one of the following one-step moves: either it erases c, writes d, moves one square to the left, and passes to state q_{6}, or it erases c, writes d, moves one square to the right, and passes to state q_{3}.

A configuration or instantaneous description of a Turing machine, or briefly id, is given by a quadruple ⟨α_{1}, q, c, α_{2}⟩, where q ∈ Q is the current state, and α_{1}, α_{2} ∈ T^{∗} are the used part of the tape to the left and to the right of the Turing machine’s read/write head, respectively, and c is the symbol directly underneath the read/write head. Here and throughout the paper “the used portion of the tape” means the smallest contiguous portion of the tape that includes all tape cells with a symbol other than ♭ and all tape cells visited by the read/write head.

The machine is given input t ∈ S^{∗} by writing ♭t on the otherwise empty tape, one symbol per tape cell, with the read/write head scanning the first symbol before the beginning of t, and the state is q_{0}, forming the id ⟨ϵ, q_{0}, ♭, t⟩. M is said to accept input t in exactly n steps, n ≥ 1, if there exists a sequence of configurations v_{0}, …, v_{n}, each obtained from the previous by a one-step move, where v_{0} is the initial configuration just described and v_{n} = ⟨α_{1}, q_{F} , ♭, α_{2}⟩. Note that the state of v_{i} cannot be q_{F} whenever 0 ≤ i < n. M is said to accept input t if there exists n ≥ 1 such that M accepts t in exactly n steps. Let L(M), the language accepted by M, consist of all t ∈ S^{∗} accepted by M.

A Turing machine M is said to be exponential time if there exists a polynomial p(n) with nonnegative integer coefficients such that M ∈ ntime(2^{p(n)}), that is, for each t ∈ L(M), M accepts t in at most 2^{p(n)} steps, where n is the length of t. Let nexptime be the class of languages of the form L(M) for some exponential time Turing machine M [28].

3 Encoding nexptime in mall1

In this section we give an efficient encoding of any nondeterministic Turing machine and any input by a mall1 sequent, which also depends on a natural number n. In Sections 4 and 5 it will be shown that the mall1 sequent is provable if and only if the Turing machine accepts the input in at most 2^{n} steps.

We translate Turing machine instructions as follows, similarly to the logic programming simulation given in [27]. A left move Turing machine instruction is translated as:

\begin{aligned}[q_{i}, a ↦ q_{j}, d, Left] & = & &_{c∈T} ∀L∀R id(⟨[c|L], q_{i}, a, R⟩)−∘ id(⟨L, q_{j}, c, [d|R]⟩) \\ & & & ∀R id(⟨ϵ, q_{i}, a, R⟩)−∘ id(⟨ϵ, q_{j}, ♭, [d|R]⟩), \end{aligned}

where the first conjunct describes the behavior at the center and at the right end of the used portion of the tape, while the second conjunct describes the behavior at the left end of the used portion of the tape and the behavior if the tape has not been used yet.

A right move Turing machine instruction is translated as:

\begin{aligned}[q_{i}, a ↦ q_{j}, d, Right] & = & &_{c∈T} ∀L∀R id(⟨L, q_{i}, a, [c|R]⟩)−∘ id(⟨[d|L], q_{j}, c, R⟩) \\ & & & ∀L id(⟨L, q_{i}, a, ϵ⟩)−∘ id(⟨[d|L], q_{j}, ♭, ϵ⟩), \end{aligned}

where the first conjunct describes the behavior at the center and at the left end of the used portion of the tape, while the second conjunct describes the behavior at the right end of the used portion of the tape and the behavior if the tape has not been used yet.

Given a Turing machine program with m instructions δ = τ_{1}, τ_{2}, ⋯, τ_{m}, we construct the following formula:

[δ] = 1 & [τ_{1}] & [τ_{2}] & ⋯ & [τ_{m}].

In order to encode an exponential number of steps of execution we use a modification of the standard proof of the pspace-hardness of quantified boolean formula validity [16]. We develop an encoding function M, where M_{k}(V, V′) is meant to denote that from id V, one can reach id V′ in at most 2^{k} steps. A first attempt would be to use the encoding:

M_{k}(V, V′) = ∃W.M_{k−1}(V, W) and M_{k−1}(W, V′).

However, since M_{k−1} appears twice in the encoding of M_{k}, this encoding is itself exponential. Instead, let us use the following polynomial encoding, which achieves the same aim. Here and throughout P is a fixed unary predicate symbol distinct from id and A → B abbreviates 1&(A−∘B).

\begin{aligned}M_{0}(V, V′) & = & P (V)−∘ P (V′), \\ M_{k}(V, V′) & = & ∃W.∀Y.∀Z. [( \begin{matrix}(P (Y) → P (V)) ⊗ (id(W) → P (Z)) \\ ⊕ \\ (P (Y) → id(W)) ⊗ (P (V′) → P (Z)) \end{matrix} ) −∘ M_{k−1}(Y, Z)] . \end{aligned}

In this encoding, M_{k−1} only appears once in the encoding of M_{k}, thus enabling the encoding of an exponential number of steps of computation in a polynomially-sized formula.

Finally, we define the mall1 encoding of a Turing machine accepting an input in at most 2^{n} steps as follows. Let end be a fresh propositional symbol. Given a number n, a Turing machine M = ⟨Q, S, T , δ, q_{0}, ♭, q_{F} ⟩, and an input t, let v_{0} = ⟨ϵ, q_{0}, ♭, t⟩ and define the encoding [M(t)]_{n} as the mall1 sequent:

[δ], ∀L ∀R (((P (X) → id(v_{0}))−∘ ((id(⟨L, q_{F} , ♭, R⟩) → P (X′))−∘ M_{n}(X, X′)))−∘ end) ⊢ end.

Let k be the length of t. Observe that the sequent [M(t)]_{n} , fully written out, has length polynomial in n, k.

Discussion: Although the complexity class nexptime is defined to be the union of ntime(2^{p(n)}) taken over all polynomials p and the above encoding seemingly captures only ntime(2^{n}), it will nevertheless follow that mall1 is nexptime-hard once the soundness and faithfulness of the encoding has been established. Indeed, a polynomial p(n) may be fixed for our translation by choosing a particular nexptime-complete problem whose decision algorithm M_{0} is in ntime(2^{p(n)}). Hence it suffices to consider the encoding [M_{0}(t)]_{p(n)} on inputs t of size n.

3.1 Encoding logic programs in mall1

It follows from [27] that nondeterministic Turing machines can be simulated by logic programs with at most one formula in the body of each program clause, i.e., logic programs in which each program clause has one of the following two forms, where A, A′ are atomic formulas:

\begin{aligned}A & ← & A′ \\ A & ← \end{aligned}

so that the depth complexity of the logic program is the same as time complexity of the nondeterministic Turing machine. Such logic programs can be encoded in mall1 by a straightforward modification of the above encoding of nondeterministic Turing machines, namely:

\begin{aligned}[A_{i}(f⃗(X⃗)) ← A_{j}(h⃗(X⃗))] & = & ∀X⃗ id(⟨g_{i}, f⃗(X⃗)⟩)−∘ id(⟨g_{j}, h⃗(X⃗)⟩), \\ [A_{i}(f⃗(X⃗)) ← ] & = & ∀X⃗ id(⟨q_{i}, f⃗(X⃗)⟩)−∘ id(⟨g_{E}, ϵ⟩), \end{aligned}

where constant g_{E} is distinct from the constants g_{i}, g_{j} , f⃗ = f_{1}, … f_{k}, g⃗ = g_{1}, … g_{k}, X⃗ = X_{1}, … X_{k}, with k large enough, since a logic program consists of finitely many clauses. It is easy to see that the soundness and faithfulness of this encoding may be shown by a straightforward adaptation of the arguments given in Sections 4 and 5.

4 Soundness of the Encoding

In this section it is shown that the encoding given in Section 3 is sound, i.e., if a Turing machine M accepts an input t in at most 2^{n} steps, then the sequent [M(t)]_{n} is provable in mall1. The main technical point is given by

Lemma 4.1 If a Turing machine with program δ can pass from a id v to a id v′ in at most 2^{n} steps, then for any natural numbers j, k and any natural numbers i ≤ j and m ≤ k, the sequent

[δ], \begin{matrix}P (Y_{j}) → P (Y_{j−1}), \\ ⋯, \\ P (Y_{i}) → id(v), \\ id(v′) → P (Z_{m}), \\ ⋯, \\ P (Z_{k−1}) → P (Z_{k}) \end{matrix} ⊢ M_{n}(Y_{j}, Z_{k})

is provable in mall1.

Proof. Let Γ consist of P (Y_{j}) → P (Y_{j−1}), …, P (Y_{i}) → id(v) and let Δ consist of id(v′) → P (Z_{m}), …, P (Z_{k−1}) → P (Z_{k}). The argument is by induction on n. If n = 0, then M_{0}(Y_{j}, Z_{k}) = P (Y_{j})−∘ P (Z_{k}). There are two cases: either the Turing machine idles or it makes one step. If the machine makes one step from v to v′ by applying an instruction τ ∈ δ, then id(v)−∘id(v′) is an instance of a conjunct C in [τ] and thus a mall1 proof of the sequent

C, Γ, Δ, P (Y_{j}) ⊢ P (Z_{k})

is readily obtained by several instances of I+, −∘ L, and by ∀ L. Then a required mall1 proof follows by −∘ R and several instances of 1L and & L. If the machine idles, then v is the same as v′ and the argument is similar by using 1 instead of C.

Assume that the statement of the lemma holds for n. If the machine passes from id v to id v′ in at most 2^{n+1} steps, let w be an id such that the machine passes from v to w in at most 2^{n} steps and from w to v′ also in at most 2^{n} steps. Then let π be a mall1 proof of the sequent

[δ], Γ, P (Y_{j+1}) → P (Y_{j}), id(w) → P (Z_{k+1}) ⊢ M_{n}(Y_{j+1}, Z_{k+1})

and let π′ be a mall1 proof of the sequent

[δ], Δ, P (Y_{j+1}) → id(w), P (Z_{k}) → P (Z_{k+1}) ⊢ M_{n}(Y_{j+1}, Z_{k+1})

both of which exist by the induction hypothesis. Let ρ be the mall1 proof of

[δ], Γ, Δ, P (Y_{j+1}) → P (Y_{j}), id(w) → P (Z_{k+1}) ⊢ M_{n}(Y_{j+1}, Z_{k+1})

obtained from π by several instances of 1L and & L. Use ⊗ L to obtain the mall1 proof σ of

[δ], Γ, Δ, (P (Y_{j+1}) → P (Y_{j})) ⊗ (id(w) → P (Z_{k+1})) ⊢ M_{n}(Y_{j+1}, Z_{k+1})

Let σ′ be the mall1 proof of

[δ], Γ, Δ, (P (Y_{j+1}) → id(w)) ⊗ (P (Z_{k}) → P (Z_{k+1})) ⊢ M_{n}(Y_{j+1}, Z_{k+1})

obtained similarly from π′. Then the required mall1 proof of

[δ], Γ, Δ ⊢ M_{n+1}(Y_{j}, Z_{k})

can be obtained from σ, σ′ by ⊕ L, −∘ R, ∀ R, ∀ R, and ∃ R.

The soundness of the encoding now follows:

Theorem 4.2 For any natural number n, Turing machine M, and input t, if M accepts t in at most 2^{n} steps, then the sequent [M(t)]_{n} is provable in mall1.

Proof. Let M = ⟨Q, S, T , δ, q_{0}, ♭, q_{F} ⟩, v_{0} = ⟨ϵ, q_{0}, ♭, t⟩ be the initial id, and let v′ = ⟨ℓ, q_{F} , ♭, r⟩ be the final id in an accepting computation of M on t. By Lemma 4.1, let π be a mall1 proof of

[δ], P (X) → id(v_{0}), id(v′) → P (X′) ⊢ M_{n}(X, X′)

A mall1 proof of [M(t)]_{n} may then be constructed from π first by using two instances of −∘ R, then −∘ L whose other premise is the identity end ⊢ end , and finally two instances of ∀ L.

5 Faithfulness of the Encoding

This section is concerned with the faithfulness of the encoding given in Section 3. That is, given a Turing machine M, an input t , a natural number n, and a mall1 proof of [M(t)]_{n}, then M accepts t in at most 2^{n} steps.

First let us observe

Proposition 5.1 For any Turing Machine M = ⟨Q, S, T , δ, q_{0}, ♭, q_{F} ⟩ , wellformed Turing machine id v, instruction τ ∈ δ, and universally quantified conjunct C in the formula [τ] , if id(v)−∘id(v′) is an instance of C for some term v′ , then v′ is a well-formed Turing machine id and M can make a transition from id v to id v′ in one step.

Proof. By cases on the instruction τ and its translation [τ] given in Section 3.

Permutability properties discussed in Section 2 will now be used to show that without loss of generality, a cut-free proof of [M(t)]_{n} consists only of sub-proofs of sequents of the form [δ], Ξ ⊢ M_{k}(X, Y), where k < n and Ξ includes exactly two occurences of the predicate symbol id, one negative and one of positive. Informally, one may read such a sequent as asserting that the machine instructions δ can be used to move from the negative occurrence of id in Ξ to the positive occurrence of id in Ξ in at most 2^{n} steps. This informal reading is made formal below. The key point is that a cut-free proof of such a sequent can be read as a description of a Turing machine computation. Recall that A → B abbreviates 1&(A−∘B).

Lemma 5.2 Let M = ⟨Q, S, T , δ, q_{0}, ♭, q_{F} ⟩ be a Turing machine and n a natural number. For any well-formed Turing machine id v, for any natural numbers j, k and any natural numbers i ≤ j and m ≤ k, if a sequent

[δ], Σ, Θ, \begin{matrix}P (Y_{j}) → P (Y_{j−1}), \\ ⋯, \\ P (Y_{i}) → id(v), \\ id(v′) → P (Z_{m}), \\ ⋯, \\ P (Z_{k−1}) → P (Z_{k}), \end{matrix} ⊢ M_{n}(Y_{j}, Z_{k})

is provable in mall1 for some term v′, where Σ is a union of disjoint multisets of the form P (Y_{j′}) → P (Y_{j′−1}), …, P (Y_{i′}) → id(u) for some natural numbers i′ ≤ j′ < i and some term u, where Θ is a union of disjoint multisets of the form id(u′) → P (Z_{m′}), …, P (Z_{k′−1}) → P (Z_{k′}) for some natural numbers m′ ≤ k′ < m and some term u′, and where no atomic formula with predicate symbol P occurs as a subformula in two distinct multisets in Σ, Θ, then v′ is a well-formed Turing machine id, and M can make a transition from id v to id v′ in at most 2^{n} steps.

Proof. Let Γ consist of P (Y_{j}) → P (Y_{j−1}), …, P (Y_{i}) → id(v) and let Δ consist of id(v′) → P (Z_{m}), …, P (Z_{k−1}) → P (Z_{k}). Γ, Δ will be called the active assumptions, while Σ, Θ will be called the passive assumptions. The argument is by induction on n . If n = 0, then by Propositions 2.6 and 2.9 we may assume without loss of generality that the bottommost proof rules in the given cut-free proof are, in reverse order, −∘ R and a string of &L’s, the latter analyzing [δ], Γ, Δ, Σ, Θ. After this analysis, the provable premise must be of the form:

C, Γ′, Δ′, Σ′, Θ′, P (Y_{j}) ⊢ P (Z_{k}),

where C is a conjunct in [δ] and where Γ′, Δ′, Σ′, Θ′ consist of linear implications or of 1’s. If C is [τ] for some instruction τ ∈ δ, then by Proposition 2.11 we may assume that the next higher rule is ∀ L that analyzes C, hence that its provable premise is

A, Γ′, Δ′, Σ′, Θ′, P (Y_{j}) ⊢ P (Z_{k})

where A is a linear implication and an instance of C. This sequent is multiplicative and hence by Proposition 2.2 it must be balanced. Because of the conditions on Σ, Θ it follows that Σ′, Θ′ must consist entirely of 1’s, that Γ′, Δ′ must consist entirely of linear implications, and that A is in fact id(v)−∘id(v′). In other words, the only way to achieve a balanced sequent is to drop the passive assumptions and to instantiate C as id(v)−∘id(v′). By Proposition 5.1 it is then readily seen that v′ is a well-formed machine id and that M can make a transition from v to v′ in one step. By similar reasoning, if A is 1 , then v′ must be the same as v and the machine idles.

In the induction step, assume that the statement of the lemma holds for n and consider a cut-free mall1 proof of

A, Γ, Δ, Σ, Θ ⊢ M_{n+1}(Y_{j}, Z_{k}).

By Propositions 2.12, 2.8, 2.6, and 2.3 we may assume without loss of generality that the bottommost rules used are, in reverse order: ∃ R, ∀ R, ∀ R, −∘ R, and ⊕ L. This last step yields two branches, each of which may be assumed by Proposition 2.5 to have ⊗ L as the bottommost rule. The two branches are cut-free proofs of

[δ], Γ, Δ, Σ, Θ, P (Y_{j+1}) → P (Y_{j}), id(w) → P (Z_{k+1}) ⊢ M_{n}(Y_{j+1}, Z_{k+1})

and

[δ], Γ, Δ, Σ, Θ, P (Y_{j+1}) → id(w), P (Z_{k}) → P (Z_{k+1}) ⊢ M_{n}(Y_{j+1}, Z_{k+1}).

This is the key point of this proof. One reads the given cut-free proof as a description of Turing machine computation from id v to id v′ by normalizing the given cut-free proof by permutations, finding the two branches above, and reading them as Turing machine computations from id v to id w, and id w to id v′. The induction hypothesis applies to both branches. In the first branch, the active assumptions are P (Y_{j+1}) → P (Y_{j}), Γ, id(w) → P (Z_{k+1}) and the passive assumptions are Δ, Σ, Θ. In the second branch, the active assumptions are P (Y_{j+1}) → id(w), Δ, P (Z_{k}) → P (Z_{k+1}) and the passive assumptions are Γ, Σ, Θ. Utilizing these two instances of the induction hypothesis, we conclude that w and hence v′ are well-formed machine id’s and that M can make a transition from id v to id w in at most 2^{n} steps and also from id w to id v′ in at most 2^{n} steps. Therefore M can make a transition from id v to id v′ in at most 2^{n} + 2^{n} = 2^{n+1} steps.

Thus in the full proof tree, one reads the complete Turing machine computation across the top of the proof, with all the action happening at applications of −∘ L rule. The machinery utilized throughout the remainder of the proof tree exists to create an exponential number of copies of the instruction set, and provide the glue to hold the computation together. The application of this lemma to the initial id yields the faithfulness theorem:

Theorem 5.3 For any natural number n, Turing machine M, and input t, if the sequent [M(t)]_{n} is provable in mall1, then M accepts t in at most 2^{n} steps.

Proof. Let v_{0} = ⟨ϵ, q_{0}, ♭, t⟩ be the initial id. By Proposition 2.11 we may assume without loss of generality that the two bottommost rules in a cut-free mall1 proof of

[δ], ∀L ∀R (((P (X) → id(v_{0}))−∘ ((id(⟨L, q_{F} , ♭, R⟩) → P (X′))−∘ M_{n}(X, X′)))−∘ end) ⊢ end

are the instances of ∀ L. Therefore, we may consider a cut-free mall1 proof of

[δ], (((P (X) → id(v_{0}))−∘ ((id(⟨ℓ, q_{F} , ♭, r⟩) → P (X′))−∘ M_{n}(X, X′)))−∘ end) ⊢ end

for some terms ℓ, r. It may be readily seen that the analysis of [δ] in this cut-free proof may always be postponed above the instance of the −∘ L rule that analyzes the formula

((P (X) → id(v_{0}))−∘ ((id(⟨ℓ, q_{F} , ♭, r⟩) → P (X′))−∘ M_{n}(X, X′)))−∘ end.

Because end, 0, ⊤, ⊥ do not occur in [δ], M_{n}(X, X′), the left premise of this instance of −∘ L may not contain end, and thus we may consider a cut-free mall1 proof of

[δ] ⊢ (P (X) → id(v_{0}))−∘ ((id(⟨ℓ, q_{F} , ♭, r⟩) → P (X′))−∘ M_{n}(X, X′)).

By two applications of Proposition 2.6, we may consider a cut-free mall1 proof of

[δ], P (X) → id(v_{0}), id(⟨ℓ, q_{F} , ♭, r⟩) → P (X′) ⊢ M_{n}(X, X′).

Lemma 5.2 now applies with Σ, Θ empty. Hence ⟨ℓ, q_{F} , ♭, r⟩ is a well-formed id, in fact the final id, and M can reach it from v_{0} in at most 2^{n} steps.

Theorems 4.2 and 5.3 yield:

Theorem 5.4 Provability in mall1 is nexptime-hard.

References

[1] S. Abramsky and R. Jagadeesan. New foundations for the geometry of interaction. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 211–222. IEEE Computer Society Press, Los Alamitos, California, June 1992.

[2] J.-M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 1992.

[3] J.-M. Andreoli and R. Pareschi. Logic programming with sequent systems: a linear logic approach. In Proc. Workshop on Extensions of Logic Programming, Tuebingen. Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, 1990.

[4] J.-M. Andreoli and R. Pareschi. Linear objects: Logical processes with built-in inheritance. New Generation Computing, 9, 1991.

[5] M. Barr. *-Autonomous Categories, volume 752 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1979.

[6] A. Blass. Degrees of indeterminacy of games. Fundamenta Mathematicae, 77:151–166, 1972.

[7] A. Blass. A game semantics for linear logic. Annals Pure Appl. Logic, 56:183–220, 1992. Special Volume dedicated to the memory of John Myhill.

[8] V. Danos. La Logique Linéaire Appliquée à l’Étude de Divers Processus de Normalisation at Principalement du Lambda-Calcul. Thèse de Doctorat, Université de Paris VII, 1990.

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

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

[11] J.-Y. Girard. Geometry of interaction I: Interpretation of system F. In Logic Colloquium ’88, Amsterdam, 1989. North-Holland.

[12] J.-Y. Girard. Geometry of interaction II: Deadlock-free algorithms. In: Springer LNCS 417, 1990.

[13] G. Gonthier, M. Abadi, and J.-J. Levy. The geometry of optimal lambda reduction. In Proc. 19-th Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico. ACM Press, New York, NY, January 1992.

[14] G. Gonthier, M. Abadi, and J.-J. Levy. Linear logic without boxes. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 223–234. IEEE Computer Society Press, Los Alamitos, California, June 1992.

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

[16] J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley Publishing Company, 1979.

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

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

[19] P. Lincoln, A. Scedrov, and N. Shankar. Linearizing intuitionistic implication. In Proc. 6-th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 51–62. IEEE Computer Society Press, Los Alamitos, California, July 1991. Full paper to appear in Annals of Pure and Applied Logic.

[20] P. Lincoln and T. Winkler. Constant-Only Multiplicative Linear Logic is NP-Complete. Manuscript to be submitted to Proc. MFPS 8, Oxford, 1992.

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

[22] D. Miller. The π-calculus as a theory in linear logic: Preliminary results. Technical Report MS-CIS-92-48, Computer Science Department, University of Pennsylvania, June 1992. Submitted. Available using anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/miller/pic.dvi.Z.

[23] V.R. Pratt. Event spaces and their linear logic. In AMAST ’91: Algebraic Methodology and Software Technology, Iowa City, 1991, Workshops in Computing, pages 1–23. Springer-Verlag, 1992.

[24] L. Regnier. λ-calcul et Réseaux. Thèse de Doctorat, Université de Paris VII, 1992.

[25] V. Saraswat and P. Lincoln. Higher-order, linear, concurrent constraint programming. Draft, January 1993.

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

[27] E.Y. Shapiro. Alternation and the computational complexity of logic programs. Journal of Logic Programming, 1:19–33, 1984.

[28] L. Stockmeyer. Classifying the computational complexity of problems. Journal of Symbolic Logic, 52:1–43, 1987.

[29] A.S. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes No. 29. Center for the Study of Language and Information, Stanford University,