On the Computational Complexity of Cut-Elimination in Linear Logic

  • Harry G. Mairson
  • Kazushige Terui
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2841)


Given two proofs in a logical system with a confluent cut-elimination procedure, the cut-elimination problem (CEP) is to decide whether these proofs reduce to the same normal form. This decision problem has been shown to be ptime-complete for Multiplicative Linear Logic (Mairson 2003). The latter result depends upon a restricted simulation of weakening and contraction for boolean values in MLL; in this paper, we analyze how and when this technique can be generalized to other MLL formulas, and then consider CEPfor other subsystems of Linear Logic. We also show that while additives play the role of nondeterminism in cut-elimination, they are not needed to express deterministic ptime computation. As a consequence, affine features are irrelevant to expressing ptime computation. In particular, Multiplicative Light Linear Logic (MLLL) and Multiplicative Soft Linear Logic (MSLL) capture ptime even without additives nor unrestricted weakening. We establish hierarchical results on the cut-elimination problem for MLL (ptime-complete), MALL (coNP-complete), MLLL (EXPTIME-complete), and for MLLL (2EXPTIME-complete).


Normal Form Turing Machine Linear Logic Reduction Rule Boolean Circuit 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Asp98.
    Asperti, A.: Light affine logic. In: Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, pp. 300–308 (1998)Google Scholar
  2. AR02.
    Asperti, A., Roversi, L.: Intuitionistic light affine logic (proof-nets, normalization complexity, expressive power, programming notation). ACM Transactions on Computational Logic 3(1), 1–39 (2002)CrossRefMathSciNetGoogle Scholar
  3. dF03.
    Tortora de Falco, L.: The additive multiboxes. Annals of Pure and Applied Logic 120(1), 65–102 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  4. Gir87.
    Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  5. Gir98.
    Girard, J.-Y.: Light linear logic. Information and Computation 14(3), 175–204 (1998)CrossRefMathSciNetGoogle Scholar
  6. GJ78.
    Garey, M., Johnson, D.: Computers and Intractability: A Guide to the Theory of NP-completeness. Freeman, San Francisco (1978)Google Scholar
  7. Hin89.
    Hindley, J.R.: BCK-combinators and linear λ-terms have types. Theoretical Computer Science 64, 97–105 (1989)zbMATHCrossRefMathSciNetGoogle Scholar
  8. Lad75.
    Ladner, R.E.: The circuit value problem is logspace complete for P. SIGACT News 7(1), 18–20 (1975)CrossRefMathSciNetGoogle Scholar
  9. Laf01.
    Lafont, Y.: Soft linear logic and polynomial time. Theoretical Computer Science (to appear)Google Scholar
  10. Lin95.
    Lincoln, P.D.: Deciding provability of linear logic formulas. In: Advances in Linear Logic. London Mathematical Society Lecture Notes Series, vol. 222, pp. 109–122. Cambridge University Press, Cambridge (1995)CrossRefGoogle Scholar
  11. MR02.
    Mairson, H.G., Rival, X.: Proofnets and context semantics for the additives. Computer Science Logic (CSL), 151–166 (2002)Google Scholar
  12. Mai03.
    Mairson, H.G.: Linear lambda calculus and polynomial time. Journal of Functional Programming (to appear)Google Scholar
  13. NM02.
    Neergaard, P.M., Mairson, H.G.: LAL is square: representation and expressiveness in light affine logic. Presented at the Fourth International Workshop on Implicit Computational Complexity (2002)Google Scholar
  14. Sch01.
    Schubert, A.: The Complexity of β-Reduction in Low Orders. Typed Lambda Calculi and Applications (TLCA), 400–414 (2001)Google Scholar
  15. Sta79.
    Statman, R.: The typed λ-calculus is not elementary recursive. Theoretical Computer Science 9, 73–81 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  16. Ter01.
    Terui, K.: Light affine lambda calculus and polytime strong normalization. In: Proceedings of the sixteenth annual IEEE symposium on Logic in Computer Science, pp. 209–220 (2001), The full version is available at

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Harry G. Mairson
    • 1
  • Kazushige Terui
    • 2
  1. 1.Computer Science DepartmentBrandeis UniversityWalthamUSA
  2. 2.National Institute of InformaticsTokyoJapan

Personalised recommendations