Strong polynomial bound for light linear logic by levels
Matthieu Perrinel · arXiv (Cornell University) · 2012
Girard's LLL characterized Ptime in the proof-as-program paradigm with a complexity bound on cut elimination. This logic relied on a stratification principle which Baillot and Mazza generalized by defining two variants L^4 and L^4_0 referred to as light linear logic by levels. However, for L^4, a polynomial bound was given on cut elimination only for a specific reduction strategy. L^4_0 only enjoyed a complexity soundness result without an explicit bound on cut elimination. These limitations are a problem for defining a proper type system out of theses logics. In this paper we overcome these problems by proving a polynomial time bound for cut elimination under any strategy(strong bound) both for L^4 and L^4_0. The proof is based on an extension of Dal Lago's context semantics, illustrating once again the usefullness of this tool.