Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic

DOI10.46298/LMCS-19(4:23)2023arXiv2205.15203OpenAlexW4389732286MaRDI QIDQ6137846FDOQ6137846

Authors: Beniamino Accattoli 

Publication date: 16 January 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: This paper introduces the exponential substitution calculus (ESC), a new presentation of cut elimination for IMELL, based on proof terms and building on the idea that exponentials can be seen as explicit substitutions. The idea in itself is not new, but here it is pushed to a new level, inspired by Accattoli and Kesner's linear substitution calculus (LSC). One of the key properties of the LSC is that it naturally models the sub-term property of abstract machines, that is the key ingredient for the study of reasonable time cost models for the $lambda$-calculus. The new ESC is then used to design a cut elimination strategy with the sub-term property, providing the first polynomial cost model for cut elimination with unconstrained exponentials. For the ESC, we also prove untyped confluence and typed strong normalization, showing that it is an alternative to proof nets for an advanced study of cut elimination.

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

zbMATH Keywords

linear logiccut eliminationcost modelsexplicit substitutions

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Linear logic
• Strong normalization property for second order linear logic
• Bounded linear logic: A modular approach to polynomial-time computability
• Light linear logic
• Linear logic and elementary time
• Soft linear logic and polynomial time
• On constructor rewrite systems and the lambda calculus
• Linear Logic and Strong Normalization
• A semantic measure of the execution time in linear logic
• On the computational complexity of cut-elimination in linear logic.
• Computational interpretations of linear logic
• Differential interaction nets
• Call-by-Value Solvability, Revisited
• Title not available (Why is that?)
• Term Rewriting and Applications
• Session types as intuitionistic linear propositions
• Title not available (Why is that?)
• The duality of computation
• Title not available (Why is that?)
• On the Relations between the Syntactic Theories of λμ-Calculi
• Head linear reduction and pure proof net extraction
• Linear logical relations and observational equivalences for session-based concurrency
• Propositions as sessions
• Title not available (Why is that?)
• Explicit substitutions
• On the \(\pi\)-calculus and linear logic
• (Optimal) duplication is not elementary recursive
• A Terminating and Confluent Linear Lambda Calculus
• Local bigraphs and confluence: two conjectures (extended abstract)
• Title not available (Why is that?)
• The structural \(\lambda \)-calculus
• The Theory of Calculi with Explicit Substitutions Revisited
• Resource operators for \(\lambda\)-calculus
• Title not available (Why is that?)
• A nonstandard standardization theorem
• Title not available (Why is that?)
• Lambda calculus and intuitionistic linear logic
• Linear explicit substitutions
• A syntax for linear logic
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• Distilling abstract machines
• Confluence of Pure Differential Nets with Promotion
• Title not available (Why is that?)
• A Semantical and Operational Account of Call-by-Value Solvability
• Title not available (Why is that?)
• A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem
• Proof nets and the linear substitution calculus
• Title not available (Why is that?)
• A Local Criterion for Polynomial-Time Stratified Computations
• Strong normalisation for the linear term calculus
• A new correctness criterion for MLL proof nets
• Bounding linear head reduction and visible interaction through skeletons
• Title not available (Why is that?)
• A theory of effects and resources: adjunction models and polarised calculi
• A Theory of Explicit Substitutions with Safe and Full Composition
• A Strong Distillery
• (Leftmost-outermost) beta reduction is invariant, indeed
• A calculus for interaction nets based on the linear chemical abstract machine
• Labelled calculi of resources
• Title not available (Why is that?)
• Title not available (Why is that?)
• Useful Open Call-By-Need

This page was built for publication: Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic

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