[Prev][Next][Index][Thread]
Complexity of LL Decision Problems
Date: Tue, 12 Nov 91 16:44:16 -0800
Several people have asked for a summary of complexity results for
various fragments of linear and affine logic. Here is what I know.
I would be very happy to hear about any results filling in the blanks.
In my view, the key open problem here is the decidability of M E LL
(Propositional Multiplicative-Exponential Linear Logic).
Patrick Lincoln
P.S. Is "Affine Logic" the accepted name for LL with weakening?
----------------------------------------------------------------------
Survey of Results: Decision Problems for Fragments
of Linear and Affine Logic Containing the Multiplicatives:
M=multiplicative, A=additive, E=Exponential, FO=first order,
LL=linear logic, AL=affine logic (linear logic with weakening)
MAE LL is Undecidable, r.e. (LMSS 90)
M E LL ???????? Known EXP-SPACE-Hard
MA LL is PSPACE-Complete (LMSS 90)
M LL is NP-Complete (Kanovich 91)
FO MAE LL is Undecidable, r.e. (Girard's TCS Translation of FO LK)
FO M E LL is Undecidable, r.e. (Girard's TCS Translation of FO LJ =>)
FO MA LL is PSPACE-Complete (corollary of MALL result)
FO M LL is NP-Complete (corollary of MLL result)
MAE AL ????????
M E AL ????????
MA AL is PSPACE-Complete (corollary of MA LL result)
M AL is NP-Complete (LMSS 90)
FO MAE AL is Undecidable, r.e. (corollary of FO MAE LL result)
FO M E AL is Undecidable, r.e. (corollary of FO M E LL result)
FO MA AL is PSPACE-Complete (corollary of MA AL result)
FO M AL is NP-Complete (corollary of M AL result)
In all cases I know, the intuitionistic restriction
(at most one formula on right) does NOT effect the complexity
of the decision problem for a fragment.
Two surprises to me are how little first order quantifiers and
unrestricted weakening effect the expressiveness of fragments
of linear logic.
------------------------------------------------------------------
Other Interesting Results Along These Lines:
* (Asperti, Gunter and Gehlot, Marti-Oliet and Meseguer, Brown)
ME LL can encode Petri net reachability.
Horn fragment of ME LL can encode Petri net reachability.
MLL with tensor theories encodes Petri net reachability.
(Horn = !Gamma, X |- Y, where all formulas in Gamma are of form (X -o Y),
and X,Y are tensor of propositions). (tensor theory = set of
nonlogical axioms X |- Y, where X,Y are tensor of propositions).
Petri net reachability is EXP-SPACE hard, but decidable.
* Amiot, (reference?)
"Decision Problems for Second Order Linear Logic Without Exponentials"
FO MLL + 2nd order quantifiers + one (binary function) constant is undecidable.
(with or without additives)
* Chirimar and Lipton "Decidability and Filtration for !*"
UPenn CS tech report to appear in Dec. 91
("A decision procedure for the Tensor-Bang fragment of linear logic")
The (two sided) !,* Fragment of ME LL is decidable.
* Tammet (in preparation) "Proof Search in Linear Logic"
The fragment of MAE LL where no ! nor * appears inside a ? is decidable.
* (LMSS 90) Noncommutative Linear Logic NCL (LL without unrestricted
exchange, but ? formulas commute freely) ME NCLL is Undecidable.
(as are fragments with or without first order quantifiers,
with or without additives)
------------------------------------------------------------------
References
@techreport(
Asperti87TR,Author="Asperti, A.",
Title="A Logic for Concurrency",
Institution="{Dipartimento di Informatica, Universit\'a di Pisa}",
Year="1987")
@inproceedings( % POPL 90
Asperti90,Author="Asperti, A. and G.-L. Ferrari and R. Gorrieri",
Title="Implicative Formulae in the `Proofs as Computations'
Analogy",
Booktitle="Proc. 17-th {ACM} Symp. on Principles of
Programming Languages, San Francisco",
Month="January",
Year="1990",
pages="59-71")
@techreport(
Brown89TR,Author="Brown, C.",
Title="Relating Petri Nets to Formulae of Linear Logic",
Institution="LFCS, Edinburgh"
Year="1989")
@inproceedings( % LICS 90
BrownGurr90,Author="Brown, C. and D. Gurr",
Title="A Categorical Linear Framework for {Petri} Nets",
Booktitle="Proc. 5-th {IEEE} Symp. on Logic in Computer Science,
Philadelphia",
Month="June",
Year="1990")
@inproceedings(
GunterGehlot89,Author="Gunter, C.A. and V. Gehlot",
Title="Nets as Tensor Theories",
Booktitle="Proc. 10-th International Conference on Application and
Theory of Petri Nets, Bonn",
Editor="G. De Michelis",
Year="1989",
pages="174-191")
@techreport(
Kanovich91TR,Author="Kanovich, Max I. ",
Title="The Multiplicative Fragment of Linear Logic is NP-Compete",
Institution="University of Amsterdam",
Number="ITLI-X-91-13",
Year="1991")
@inproceedings( % FOCS 90
LincolnMSS90,author="Lincoln,P.and Mitchell,J.and Scedrov,A.and Shankar,N.",
Title="Decision Problems for Propositional Linear Logic",
Booktitle="Proc. 31st {IEEE} Symp. on Foundations of Computer Science",
pages="662--671",
Year="1990")
@techreport(
LincolnMSS90TR,Author="Lincoln,P.and Mitchell,J.and Scedrov,A.and Shankar,N.",
Title="Decision Problems for Propositional Linear Logic",
Institution="CSL, SRI International",
Number="SRI-CSL-90-08", % 76 pages
Year="1990")
@article( % TCS 87
Girard87,Author="Girard, J.-Y.",
Title="Linear Logic",
Journal="Theoretical Computer Science",
Volume="50",
Year="1987",
pages="1-102")
@misc(
MartiOlietMeseguer89,Author="Mart\'i-Oliet, N. and J. Meseguer",
Title="From {Petri} Nets to Linear Logic",
HowPublished="{In: Springer LNCS 389, ed. by D.H. Pitt et al.}",
Year="1989",
Note="313-340")