Linear Logic by Levels and Bounded Time Complexity

Abstract

We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard's seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratification, based on inducing levels in proof nets by means of indexes, which allows us to extend Girard's systems while keeping the same complexity properties. In particular, it turns out that Girard's systems can be recovered by forcing depth and level to coincide. A consequence of the higher flexibility of levels with respect to depth is the absence of boxes for handling the paragraph modality. We use this fact to propose a variant of our polytime system in which the paragraph modality is only allowed on atoms, and which may thus serve as a basis for developing lambda-calculus type assignment systems with more efficient typing algorithms than existing ones.

63 pages. To appear in Theoretical Computer Science. This version corrects minor fonts problems from v2

References in corpus (3)

• Algorithms for Omega-Regular Games with Imperfect Information
• Light types for polynomial time computation in lambda-calculus
• Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine Logic

Cited by in corpus (9)

• Unification and Logarithmic Space
• Safe Recursion on Notation into a Light Logic by Levels
• On the complexity of stratified logics
• An Abstract Approach to Stratification in Linear Logic
• Proceedings International Workshop on Developments in Implicit Computational complExity
• A tier-based typed programming language characterizing Feasible Functionals
• Super Exponentials in Linear Logic
• Implicit automata in typed $\lambda$-calculi II: streaming transducers vs categorical semantics
• Complete and tractable machine-independent characterizations of second-order polytime