[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")