Light linear logics with controlled weakening: expressibility, confluent strong normalization (Q408540): Difference between revisions

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. This 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. The 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. Easy-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.