指数作为代换与线性逻辑中割除消的成本
计算机科学中的逻辑
2024-02-14 v4 编程语言
摘要
本文引入指数代换演算（ESC），一种基于证明项、以指数为显式代换为思想的对 IMELL 割除消的新表述。该思想本身并不新颖，但本文受 Accattoli 与 Kesner 的线性代换演算（LSC）启发将其推至新高度。LSC 的关键性质之一是其自然建模抽象机的子项性质，此为研究 -演算合理时间成本模型的关键要素。新 ESC 随后被用于设计具有子项性质的割除消策略，提供了首个带无约束指数的割除消的多项式成本模型。对于 ESC，我们还证明了无类型合流与有类型强规范化，表明其可作为证明网的替代以深入研究割除消。
引用
@article{arxiv.2205.15203,
title = {Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic},
author = {Beniamino Accattoli},
journal= {arXiv preprint arXiv:2205.15203},
year = {2024}
}