[Prev][Next][Index][Thread]

Decision problems for propositional linear logic

Date: Wed, 21 Mar 90 12:16:28 -0800

	     Decision problems for propositional linear logic
	     P. Lincoln, J. Mitchell, A. Scedrov, N. Shankar

We have been investigating several fragments of propositional linear
logic. Our main result is

1. Any fragment conservative over the intuitionistic linear logic
of tensor, plus, implication and ! (of course) is undecidable.

In particular, full propositional linear logic is conservative 
over this fragment, and therefore undecidable. We know of at least
one prior claim of decidability.

The undecidability proof is by reduction from a form of alternating
counter machines. Our machines differ from the usual counter machines
in that we do not have an atomic "zero test" instruction. However,
these machines may simulate ordinary counter machines using "and"
branching to verify that a counter value is zero. We reduce these
machines to a form of "tensor, plus theory" (similar to the
tensor theories used by Gunter and Gehlot) and show that in the
intuitionistic linear logic of tensor, plus, implication and ! 
we may faithfully axiomatize a finite tensor, plus theory by
a single formula. The insight of using plus to express a form
of "and" branching is due to Pat Lincoln.

Although the proper formulation of full non-commutative linear logic
is not completely clear, we have considered  the decision problem  for
a seemingly natural formulation and obtained the following:

2. Noncommutative linear logic of tensor, implication and !
is undecidable.

This proof is a straightforward encoding of the word problem for
semigroups, although the soundness of this encoding is not completely 
trivial. We also  observe that the (commutative)  linear logic of
implication, ! and second-order quantification is undecidable.
This follows from Girard's embedding of intuitionistic logic 
into linear logic, and the Gabbay/Lob undecidability result for
quantified positive intuitionistic propositional logic.

We also have some complexity results for more limited
fragments of propositional linear logic. (All of these fragments
are quantifier-free.) For example:

3. Linear logic of tensor, par and negation is in NP.

4. Linear logic with all  connectives (tensor, plus, par, with,
implies, negation) and logical constants (bottom, 0, top)
but without ! or ? is decidable in PSPACE.

We also remark that the fragment of tensor, implication and !
is EXP-space hard. This follows from the Asperti, Gunter,
Gehlot, Meseguer and Marti-Oliet correspondence between this
fragment and Petri nets, and the Mayr/Meyer result for nets.

Acknowledgement: We thank Alasdair Urquhart for communicating
prior results on the complexity of relevant implication (R ->),
and his recent Co-NP lower bound for propositional linear logic of
tensor, plus, negation, bottom, 0, 1  and top, and his
independent proof of the EXP-space lower bound for tensor, 
implication and !. Thanks also to Carl Gunter for pointing 
out the connection to Petri nets and to others who helpfully
responsed to our inquiry on this mailing list.