A semantic account of strong normalization in linear logic

DOI10.1016/J.IC.2015.12.010MaRDI QIDQ276260zbMATH OpenOpenAlexFDO

Authors Daniel de Carvalho, Lorenzo Tortora de Falco

Publication date 3 May 2016

Published in Information and Computation (Search for Journal in Brave)

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

zbMATH Keywords

computational complexitycut eliminationdenotational semanticslinear logicproof netsstrong normalization

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical semantics of formal languages (18C50)

Abstract: We prove that given two cut free nets of linear logic, by means of their relational interpretations one can: 1) first determine whether or not the net obtained by cutting the two nets is strongly normalizable 2) then (in case it is strongly normalizable) compute the maximal length of the reduction sequences starting from that net.

Review text

The present paper further explores the connection between linear logic proofs (proof-nets) and the multiset based relational model of linear logic [\textit{J.-Y. Girard}, Theor. Comput. Sci. 50, 1--102 (1987; Zbl 0625.03037); the first author et al., Theor. Comput. Sci. 412, No. 20, 1884--1902 (2011; Zbl 1222.03070)].NEWLINENEWLINEThe authors prove that it is possible to determine if the net obtained by cutting two cut-free nets is strongly normalizable, from the relational interpretations of the two cut-free nets. Moreover, being the former net strongly normalizable it is possible to determine the maximum length (i.e.\ the number of cut reduction steps) of its reduction sequences, once more by only referring to the interpretations of the two cut-free nets in the relational model.NEWLINENEWLINESimilar questions apropos \textit{weakly} normalization and the number of cut reduction steps leading to the normal form were answered in [the first author et al., loc. cit.]. The strongly normalization variant, not surprisingly, raises new challenges addressed in the present paper.NEWLINENEWLINEAs a consequence of the authors' semantic approach an alternative proof of strong normalization for Multiplicative Exponential Linear Logic (MELL) is presented. This alternative proof does not rely on confluence. In [``Linear logic and strong normalization, in: 24th international conference on rewriting techniques and applications (RTA 2013), Eindhoven, The Netherlands, June 24--26, 2013. Wadern: Schloss Dagstuhl -- Leibniz Zentrum für Informatik. 39--54 (2013; \url{doi:10.4230/LIPIcs.RTA.2013.39})], \textit{B. Accattoli} also gave a proof of strong normalization for MELL which does not use any form of confluence. The novelty of the present proof is that it keeps the structure `weak normalization + conservation theorem', being the conservation theorem an immediate consequence of the semantic approach not relying on the confluence result.

Recommendations

• Linear Logic and Strong Normalization
• scientific article; zbMATH DE number 937366
• A semantic measure of the execution time in linear logic
• Strong normalization property for second order linear logic
• The conservation theorem for differential nets

Cites work

• A semantic measure of the execution time in linear logic
• An extension of basic functionality theory for -calculus
• Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
• Differential interaction nets
• Execution time of λ-terms via denotational semantics and intersection types
• Filter models: non-idempotent intersection types, orthogonality and polymorphism
• scientific article; zbMATH DE number 786499 (Why is no real title available?)
• Light affine lambda calculus and polynomial time strong normalization
• Linear logic
• Linear Logic and Strong Normalization
• Logical Approaches to Computational Barriers
• Non-idempotent intersection types and strong normalisation
• Proving termination with multiset orderings
• Strong normalization property for second order linear logic
• The Inhabitation Problem for Non-idempotent Intersection Types
• The relational model is injective for multiplicative exponential linear logic
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• Uniformity and the Taylor expansion of ordinary lambda-terms

Cited in

(20)

• Strong normalization property for second order linear logic
• On proof normalization in linear logic
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• The bang calculus revisited
• From propositional to linear logic: An introduction. Decoration, simulation, normalization
• Context semantics, linear logic, and computational complexity
• Linear Logic and Strong Normalization
• A By-Level Analysis of Multiplicative Exponential Linear Logic
• The Cut-Elimination Theorem for Differential Nets with Promotion
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• scientific article; zbMATH DE number 7003195 (Why is no real title available?)
• scientific article; zbMATH DE number 1405619 (Why is no real title available?)
• Towards a semantic measure of the execution time in call-by-value lambda-calculus
• Tight typings and split bounds, fully developed
• A semantic measure of the execution time in linear logic
• The conservation theorem for differential nets
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)
• The bang calculus revisited
• Categorifying non-idempotent intersection types
• Semantic bounds and multi types, revisited

This page was built for publication: A semantic account of strong normalization in linear logic

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