基于路径的判定准则及其在描述多项式时间的线性逻辑子系统中的应用
Paths-based criteria and application to linear logic subsystems characterizing polynomial time
摘要：
线性逻辑的几种变体已经被提出来描述证明-程序对应中的复杂性类。轻线性逻辑（LLL）确保了约简时间的多项式界限，并且以这种方式表征多项式时间（Ptime）。本文研究了线性逻辑证明网的复杂性，提出了基于上下文语义的三个语义准则：分层、依赖控制和嵌套。分层本身需要一个基本的时间界限，这三个标准一起需要一个多项式时间界限。这些准则可以用来证明线性逻辑的几个现有变体的复杂性可靠性。我们定义了线性逻辑的一个可判定语法子系统：SDNLL。我们证明了SDNLL的证明网满足这三个标准，这意味着SDNLL是健全的Ptime。将线性逻辑中表征多项式时间的几个子系统（LLL，mL^4，MS的极大系统）嵌入SDNLL中，证明了SDNLL的Ptime完备性.
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
