Light linear logics with controlled weakening: expressibility, confluent strong normalization
elementary linear logicimplicit computational complexitylight linear logicpolynomial-time strong normalizationproofs-as-programs paradigm
Logic in computer science (03B70) Complexity of computation (including implicit computational complexity) (03D15) Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)
Light linear logic (LLL) was introduced by \textit{J.-Y. Girard} [Inf. Comput. 143, No. 2, 175--204 (1998; Zbl 0912.03025)] in order to capture polytime in the proofs-as-programs paradigm with a complexity bound on cut elimination. Subsequent works proposed simplifications as well as refinements of this seminal LLL. Nevertheless, most of these systems dealing with light logics do not behave well with respect to any choice of cut-reduction strategies.NEWLINENEWLINEThis paper proposes, in a traditional sequent calculus style, a new system of LLL, called Easy-LLL, which is powerful enough to represent any deterministic polynomial-time computations and, unlike the original LLL, admits a cut-elimination process which terminates in a unique way in polytime for any choice of cut-reduction strategies.NEWLINENEWLINEThe main novelty of Easy-LLL is the introduction of a pair of dual ``nabla modalities. This realizes a further step in the refinement of the resource control in linear logic. The old pairs of dual modalities (the exponentials) enabled to deal with any number of copies of resources in a sufficiently controlled way to have a deterministic cut elimination. The modality ``paragraph enabled to ``stratify the exponential nesting levels, such that cut elimination is polytime for at least one cut-reduction strategy. The modalities ``nabla help to go further in this direction. Two weakenings are distinguished: one for nabla formulas and one for exponential formulas. The author speaks of a weakening control \textit{at the current step} for the modality nabla versus a weakening control \textit{at the next step} for the modality exponential. A system is then defined using these new modalities, in which the cut elimination is polytime for any choice of cut-reduction strategies.NEWLINENEWLINEEasy-LLL is obtained in several steps. At first the author defines some nabla-versions of, respectively, LLL and ELL. The modalities nabla replace the too complex notion of ``blocks of formulas, which enabled in LLL to deal with several formulas in the context of a promotion rule as if they were a sole additive formula. At the same time, the additive rules also disappear since the additive connectives may be decomposed by means of second-order quantification and modalities nabla. A fibred phase semantics is introduced, and strong completeness is obtained for the two nabla-versions of light logics. Lastly, Easy-LLL is presented as a fragment of the nabla-version of LLL: the one in which the promotion rule is allowed only in the unary case. The main results are then proved. In Easy-LLL ``any proof is normalizable in \(s^d\) steps with one and the same result regardless of which sequence of cut reductions we take (here \(s\) is the size of the proof, and the degree \(d\) is determined only by the nesting depth of exponentials in the proof). The proof makes use of a proofnet representation of Easy-LLL proofs. One of its main ingredients is that, inside Easy-LLL proofnets, contraction nodes form a forest structure which is stable under cut reductions. The proof of the other main result, ``any polytime computable function is representable as a proof within Intuitionistic Easy-LLL, is an easy consequence of already known results.
- Bounded linear logic: A modular approach to polynomial-time computability
- scientific article; zbMATH DE number 786485 (Why is no real title available?)
- scientific article; zbMATH DE number 1392281 (Why is no real title available?)
- scientific article; zbMATH DE number 1424054 (Why is no real title available?)
- Intuitionistic light affine logic
- Light linear logic
- Light Linear Logic with Controlled Weakening
- Light types for polynomial time computation in lambda calculus
- Linear logic
- Linear logic and polynomial time
- On an interpretation of safe recursion in light affine logic
- On the computational complexity of cut-elimination in linear logic.
- Phase semantics for light linear logic
- Soft linear logic and polynomial time
- Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic
- Linear logic by levels and bounded time complexity
- Light linear logic
- Paths-based criteria and application to linear logic subsystems characterizing polynomial time
- Soft subexponentials and multiplexing
- An abstract approach to stratification in linear logic
- Linear logic and polynomial time
- Light Linear Logic with Controlled Weakening
- An analysis of (linear) exponentials based on extended sequents
- Free-cut elimination in linear logic and an application to a feasible arithmetic
- On the computational complexity of cut-elimination in linear logic.
- Parallelism in soft linear logic
- Light affine lambda calculus and polynomial time strong normalization
This page was built for publication: Light linear logics with controlled weakening: expressibility, confluent strong normalization
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q408540)
