The algebraic $\lambda$-calculus is an extension of the ordinary $\lambda$-calculus with linear combinations of terms. We establish that two ordinary $\lambda$-terms are equivalent in the algebraic $\lambda$-calculus iff they are $\beta$-equal. Although this result was originally stated in the early 2000's (in the setting of Ehrhard and Regnier's differential $\lambda$-calculus), the previously proposed proofs were wrong: we explain why previous approaches failed and develop a new proof technique to establish conservativity.
翻译:代数$λ$-演算是普通$λ$-演算的保守扩展
翻译摘要:
代数$λ$-演算是普通$λ$-演算的扩展,其中包含术语的线性组合。我们证明,在代数$λ$-演算中,两个普通$λ$-术语是等价的,当且仅当它们是$\beta$-相等的。虽然这个结论最初在2000年代初期提出(在Ehrhard和Regnier的微分$λ$-演算的背景下),但以前提出的证明是错误的:我们解释为什么以前的方法失败了,并开发了一种新的证明技术来确立保守性。