Matthieu Perrinel | Search arXiv

arXiv2017

Paths-based criteria and application to linear logic subsystems characterizing polynomial time

Several variants of linear logic have been proposed to characterize complexity classes in the proofs-as-programs correspondence. Light linear logic (LLL) ensures a polynomial bound on reduction time, and characterizes in this way polynomial time (Ptime). In this paper we study the complexity of linear logic proof-nets and propose three semantic criteria based on context semantics: stratification, dependence control and nesting. Stratification alone entails an elementary time bound, the three criteria entail together a polynomial time bound. These criteria can be used to prove the complexity soundness of several existing variants of linear logic. We define a decidable syntactic subsystem of linear logic: SDNLL. We prove that the proof-nets of SDNLL satisfy the three criteria, which implies that SDNLL is sound for Ptime. Several previous subsystems of linear logic characterizing polynomial time (LLL, mL^4, maximal system of MS) are embedded in SDNLL, proving its Ptime completeness.

cs.LO↗

arXiv2012

On paths-based criteria for polynomial time complexity in proof-nets

Girard's Light linear logic (LLL) characterized polynomial time in the proof-as-program paradigm with a bound on cut elimination. This logic relied on a stratification principle and a "one-door" principle which were generalized later respectively in the systems L^4 and L^3a. Each system was brought with its own complex proof of Ptime soundness. In this paper we propose a broad sufficient criterion for Ptime soundness for linear logic subsystems, based on the study of paths inside the proof-nets, which factorizes proofs of soundness of existing systems and may be used for future systems. As an additional gain, our bound stands for any reduction strategy whereas most bounds in the literature only stand for a particular strategy.

cs.LO↗