IMELL Cut Elimination with Linear Overhead
Beniamino Accattoli, Claudio Sacerdoti Coen
TL;DR
This work addresses the time-cost modeling of cut-elimination in IMELL by building on the Exponential Substitution Calculus (ESC) and its good strategy. The authors design SESAME, an environment-based abstract machine that implements the good strategy with linear overhead, and provide an OCaml implementation to validate the theoretical bounds. They establish key invariants (sub-term property, diamond property, contextual decoding) and prove that SESAME, together with a final garbage-collection pass, yields cut-free terms in a bi-linear overhead relative to the initial term and reduction length. The approach advances the explicit-management of duplication and garbage collection in a strong-evaluation setting for linear logic, with potential implications for implicit computational complexity within IMELL-based formalisms.
Abstract
Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination. He also introduced a new cut elimination strategy, dubbed the good strategy, and showed that its number of steps is a time cost model with polynomial overhead for the ESC/IMELL, and the first such one. Here, we refine Accattoli's result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead.