Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Beniamino Accattoli

TL;DR

This work introduces the Exponential Substitution Calculus (ESC) as a new, substitution-based presentation of cut elimination for IMELL, building on ideas from the Linear Substitution Calculus to achieve a sub-term property and a polynomial-time cost model for unconstrained exponentials. By separating micro- and small-step rewriting, and enforcing term splitting and controlled meta-level substitutions, ESC provides a clock with regular ticks suitable for complexity analysis, while also proving untyped confluence and typed strong normalization. The paper further develops the sub-term strategy, culminating in a good strategy that generalizes linear head reduction to full IMELL and computes cut-free proofs within polynomial cost. Foundational results, including confluence, SN, and the preservation of the sub-term property under micro-steps, establish ESC as a robust alternative to proof nets for analyzing cut elimination in linear logic. Overall, ESC advances the understanding of complexity in linear logic by delivering a concrete, compositional framework for cost-modeling cut elimination with exponentials.

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 $λ$-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.

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

TL;DR

This work introduces the Exponential Substitution Calculus (ESC) as a new, substitution-based presentation of cut elimination for IMELL, building on ideas from the Linear Substitution Calculus to achieve a sub-term property and a polynomial-time cost model for unconstrained exponentials. By separating micro- and small-step rewriting, and enforcing term splitting and controlled meta-level substitutions, ESC provides a clock with regular ticks suitable for complexity analysis, while also proving untyped confluence and typed strong normalization. The paper further develops the sub-term strategy, culminating in a good strategy that generalizes linear head reduction to full IMELL and computes cut-free proofs within polynomial cost. Foundational results, including confluence, SN, and the preservation of the sub-term property under micro-steps, establish ESC as a robust alternative to proof nets for analyzing cut elimination in linear logic. Overall, ESC advances the understanding of complexity in linear logic by delivering a concrete, compositional framework for cost-modeling cut elimination with exponentials.

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 -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.
Paper Structure (40 sections, 5 theorems, 4 equations, 2 figures)

This paper contains 40 sections, 5 theorems, 4 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Linear Logic and Complexity Classes
  3. The Cut Elimination Clock
  4. The Linear Substitution Calculus
  5. The Sub-Term Property
  6. Linear Logic and the Sub-Term Property
  7. This Paper
  8. Related Work
  9. Journal Version and Proofs
  10. Overview of the Contributions
  11. Contribution 1: The Exponential Substitution Calculus
  12. Basics of Explicit Substitutions
  13. Design Principles
  14. Left Splitting
  15. Additives
  16. ...and 25 more sections

Key Result

Proposition 3.2

prop:abs-size-explosion Let $n \!>\! 0$. Then Moreover, $|t_n \mathtt{I}| = {\mathcal{O}}(n)$, $|r_n| = \Omega(2^n)$, $t_n \mathtt{I}$ is closed, and $r_n$ is a $\beta$ normal form.

Figures (2)

  • Figure 1: Untyped proof net of classical LL reducing to itself in 3 micro steps.
  • Figure 2: The two rewriting rules that are used in the discussions on the sub-term property and size explosion for proof nets.

Theorems & Definitions (9)

  • Definition 3.1: Sub-term property
  • Proposition 3.2: Closed and strategy-independent size explosion
  • proof
  • Proposition 3.3: Size explosion in MELL
  • proof
  • Proposition 4.1: Local termination, DBLP:conf/rta/Accattoli12
  • Definition 4.2: Structural equivalence
  • Proposition 4.3: $\equiv$ is a strong bisimulation wrt $\rightarrow_{LSC}$ DBLP:conf/popl/AccattoliBKL14
  • Theorem 4.4: Sub-term property for $\rightarrow_{\mathtt{lh}}$, DBLP:conf/rta/AccattoliL12