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.
翻译:本文介绍了指数替代微积分(ESC),这是根据证据条款和指数可被视为明显替代的概念,对IMELL的削减去除的一个新表述。这个想法本身不是新的,但在这里它被推到了一个新的水平,受Accattoli和Kesner的线性替代微积分(LSC)的启发。 LSC的关键特性之一是它自然地模拟抽象机器的子术语属性,这是研究美元/升巴元计算的合理时间成本模型的关键成分。新的 ESC随后被用来设计一个与子术语属性的削减消除战略,为用未受限制的指数进行切除提供了第一个多元成本模型。对于 ESC,我们也证明了非型的组合和键入的强烈正常化,表明它是用于高级削减研究的验证网的替代。