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.

翻译：代数λ演算是普通λ演算的扩展，增加了项的线性组合。我们证明：两个普通λ项在代数λ演算中等价当且仅当它们β相等。尽管这一结果最初于21世纪初（在Ehrhard和Regnier的微分λ演算框架下）被提出，但此前给出的证明存在错误：我们解释了先前方法失败的原因，并发展了一种新的证明技术来建立保守性。