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

DOI10.1007/978-3-319-12466-7_8MaRDI QIDQ3460508zbMATH OpenOpenAlexFDO

Authors Matthieu Perrinel

Publication date 7 January 2016

Published in Foundational and Practical Aspects of Resource Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1201.2956

Mathematics Subject Classification ID

Logic in computer science (03B70) Complexity of proofs (03F20) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Abstract: 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.

Recommendations

• Paths-based criteria and application to linear logic subsystems characterizing polynomial time
• Linear logic by levels and bounded time complexity
• Linear logic and polynomial time
• Light linear logic
• On the computational complexity of cut-elimination in linear logic.

Cites work

• Context semantics, linear logic, and computational complexity
• Elementary complexity and geometry of interaction
• scientific article; zbMATH DE number 786499 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• Light linear logic
• Light types for polynomial time computation in lambda calculus
• Linear dependent types and relative completeness
• Linear logic
• Linear logic and elementary time
• Linear logic by levels and bounded time complexity
• On paths-based criteria for polynomial time complexity in proof-nets
• Soft linear logic and polynomial time

Cited in

(2)

• Paths-based criteria and application to linear logic subsystems characterizing polynomial time
• On paths-based criteria for polynomial time complexity in proof-nets

This page was built for publication: On paths-based criteria for polynomial time complexity in proof-nets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460508)