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

TL;DR

This paper introduces a general path-based criterion for ensuring polynomial time complexity in proof-net systems, simplifying proofs of soundness and applicable across various reduction strategies.

Contribution

It proposes a broad, path-based criterion for polynomial time soundness in linear logic subsystems, unifying and extending previous stratification-based approaches.

Findings

Provides a unified criterion for Ptime soundness

Applies to multiple reduction strategies

Simplifies proofs of polynomial bounds

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.