论文标题
指数为替代和线性逻辑中的削减成本
Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
论文作者
论文摘要
本文介绍了指数替代计算（ESC），这是基于证明术语和基于指数可将指数视为显式替代的想法的基础的新的消除裁缝的介绍。这个想法本身并不是什么新鲜事物，但是在这里，它的灵感来自Accattoli和Kesner的线性替代演算（LSC）。 LSC的关键特性之一是它自然地建模了抽象机器的次级属性，这是研究$λ$ -calculus合理时间成本模型的关键要素。然后，新的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 $λ$-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.
