如何演奏手风琴。泰勒级数逼近引发的约化的（非）保守性。
摘要：泰勒展开源于线性逻辑及其微分扩展，是一种适用于λ-演算（及其许多变种）的近似框架。λ-项的近似项的约简会导致λ-项本身的约简，从而具有模拟特性：无论何时一个项约简到另一个项，近似项都会相应地约简。在最近的工作中，我们将这个结果扩展到了无穷λ-演算（即$Lambda\_{infty}^{001}$）。这篇简短的论文解决了一个问题：如果某个项的近似项约简到了另一个项的近似项，那么这两个项之间是否存在右简化？我们证明了这在λ-演算中成立，但我们的证明在无穷情况下失败了。我们展示了一个反例，驳斥了$Lambda\_{infty}^{001}$的保守性。
作者：R''emy Cerda, Lionel Vaux Auclair
论文ID：2305.02785
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-19