[Prev][Next][Index][Thread]
MALL1 is NEXPTIME-hard
Date: Thu, 2 Apr 92 11:21:06 -0800
To: linear@cs.stanford.edu
First Order Linear Logic Without Modalities is NEXPTIME-hard
Patrick Lincoln and Andre Scedrov
In previous joint work with J. Mitchell and N. Shankar (FOCS '90) we
have shown that MALL, the multiplicative additive fragment of
propositional (i.e., quantifier-free) linear logic, is PSPACE-complete.
Here we consider multiplicatives, additives, and first order
quantifiers, MALL1. Because the depth of a cut-free proof tree is
still linear in the size of the conclusion, as in the case of MALL, 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. We
show that MALL1 with function symbols is NEXPTIME-hard.
This result is achieved through the direct encoding of Turing machine
transitions, which are shared via the additives, and the existential
quantification over intermediate Turing machine states. The linear
depth bound on MALL1 proofs gives an immediate single exponential
upper bound on the number of Turing machine transitions which can be
used in the entire proof using this encoding. This encoding uses one
binary and one nullary function symbol, and differs from some of our
earlier encodings of computations in linear logic in that here the
Turing machine transitions are applied "across the top" of the proof
tree, with existential quantification providing the glue between
steps. In earlier encodings, one read a computation "up" a proof
along its spine.
MALL1 is decidable. It is likely to be in NEXPTIME, using dynamic
skolemization to produce an exponential number of small (polynomial)
unification problems. Solving all unification problems simultaneously
would yield a single exponential time decision procedure.