Paths-based criteria and application to linear logic subsystems characterizing polynomial time
Abstract
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.
Cite
@article{arxiv.1701.01413,
title = {Paths-based criteria and application to linear logic subsystems characterizing polynomial time},
author = {Matthieu Perrinel},
journal= {arXiv preprint arXiv:1701.01413},
year = {2017}
}