[Prev][Next][Index][Thread]
Complexity of ConstantOnly Fragments of LL

To: linear@cs.stanford.edu

Subject: Complexity of ConstantOnly Fragments of LL

From: bekl@log.mian.su (Lev D. Beklemishev)

Date: Sun, 10 Jan 93 17:13:13 +0300 (MSK)

Approved: types@dcs.gla.ac.uk
For ordinary logics (e.g. for classical or intuitionistic ones),
their oneliteral and, especially, constantonly fragments
are essentially simpler than the corresponding full
logics (with unrestricted number of literals.)
The point is that the simulating of PSPACEcomplete problems,
a priori, requires unrestricted number of variables.
For example, the proof of PSPACEcompleteness of the implicative
fragment of intuitionistic logic as well as of quantified Boolean
formulas essentially uses unrestricted number of variables.
Contrary to what might be expected, we prove that
oneliteral and even constantonly fragments of Linear
Logic are of the same expressive power as the corresponding
full parts of LL with infinite number of literals.
In abbreviations like
MLL, MALL, MELL, MAELL
LL indicates Propositional Linear Logic,
M indicates Multiplicatives: Tensor Product and Linear Implication,
A indicates Additives: & and \oplus,
E indicates the storage operator !.
Let us recall that
1. MLL is NPcomplete (Kanovich, 1991).
2. MALL is PSPACEcomplete
(Lincoln, Mitchell, Scedrov, and Shankar, 1990)
3. MELL can encode Petri Nets reachability.
4. MAELL is undecidable (Lincoln, Mitchell, Scedrov, and Shankar, 1990)
We consider Oneliteral parts of these fragments which contain
(a) the only one positive literal p,
(b) no other literals,
(c) neither negative literals, nor constants, nor negations,
(d) in the case E, the exponential ! is allowed to appear only
outside of formulas.
We proved the following results:
1. Oneliteral MLL is NPcomplete (Kanovich, 1992).
2. Oneliteral MALL is PSPACEcomplete (Kanovich, this message).
3. Oneliteral MELL can encode Petri Nets reachability.
(Kanovich, this message).
4. Oneliteral MAELL can directly simulate standard Minsky machines,
and, hence, it is undecidable (Kanovich, 1992, December).
We consider Constantonly parts of the fragments of LL in question
which contain
(a) no literals at all,
(b) the only constant \bottom,
(c) neither other constants, nor negations,
(d) only one multiplicative: linear implication,
(e) in the case E, the exponential ! is allowed to appear only
outside of formulas.
The following results are proved:
1. Constantonly MLL is NPcomplete (Lincoln and Winkler, 1992).
2. Constantonly MALL is PSPACEcomplete (Kanovich, this message).
3. Constantonly MELL can encode Petri Nets reachability.
(Kanovich, this message).
4. Constantonly MAELL can directly simulate standard Minsky machines,
and, hence, it is undecidable (Kanovich, 1992, December).
In order to establish PSPACEhardness, we prove that the purely
implicative fragment of intuitionistic logic can be directly
simulated in Oneliteral MALL, as well as in Constantonly MALL.
My best regards,
Max Kanovich.