一句话：提出指数替换演算 ESC，为 IMELL 切消去给出具子项性质的多项式代价模型，并证明合流与强规范化。
本文研究线性逻辑 IMELL 中切消去的代价模型，尤其针对无约束指数难以获得多项式代价的问题。作者提出指数替换演算（ESC），以证明项为基础，将指数视为显式替换，并借鉴线替换演算（LSC）建模子项性质的思想。基于 ESC，作者设计了一种具有子项性质的切消去策略，首次为无约束指数的切消去给出多项式代价模型；同时证明该演算的无类型合流性与带类型强规范化性。结果表明 ESC 可作为证明网之外研究切消去的替代框架。
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.
@article{paperbot2171,
title = {Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic},
author = {Beniamino Accattoli},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:23)2023}
}