On the Computational Complexity of Cut-Elimination in Linear Logic
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).
KeywordsNormal Form Turing Machine Linear Logic Reduction Rule Boolean Circuit
Unable to display preview. Download preview PDF.
- 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
- GJ78.Garey, M., Johnson, D.: Computers and Intractability: A Guide to the Theory of NP-completeness. Freeman, San Francisco (1978)Google Scholar
- Laf01.Lafont, Y.: Soft linear logic and polynomial time. Theoretical Computer Science (to appear)Google Scholar
- MR02.Mairson, H.G., Rival, X.: Proofnets and context semantics for the additives. Computer Science Logic (CSL), 151–166 (2002)Google Scholar
- Mai03.Mairson, H.G.: Linear lambda calculus and polynomial time. Journal of Functional Programming (to appear)Google Scholar
- 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
- Sch01.Schubert, A.: The Complexity of β-Reduction in Low Orders. Typed Lambda Calculi and Applications (TLCA), 400–414 (2001)Google Scholar
- 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 http://research.nii.ac.jp/~terui