代数λ演算是普通λ演算的保守扩展
摘要：代数λ-演算是普通λ-演算的一个扩展，它引入了项的线性组合。我们证明，在代数λ-演算中，两个普通λ-项等价当且仅当它们是η-等价的。虽然这个结果最早是在2000年左右提出的（在Ehrhard和Regnier的微分λ-演算中），但之前的证明方法是错误的：我们解释了之前的方法为什么失败，并开发了一种新的证明技巧来证明保守性。
作者：Axel Kerinec and Lionel Vaux Auclair
论文ID：2305.01067
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-16