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

TL;DR

This paper introduces semantic criteria for linear logic proof-nets that ensure polynomial time complexity, and defines a new subsystem SDNLL that is sound and complete for polynomial time computations.

Contribution

It proposes three semantic criteria for linear logic proof-nets, introduces the SDNLL subsystem satisfying these criteria, and demonstrates its polynomial time soundness and completeness.

Findings

SDNLL proof-nets satisfy stratification, dependence control, and nesting criteria.

SDNLL is sound for polynomial time complexity.

Existing polynomial time linear logic subsystems are embedded in SDNLL.

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.