从泰勒展开看传值调用Böhm树
计算机科学中的逻辑
2023-06-22 v4
摘要
传值调用(lambda calculus) lambda演算可以赋予来自线性逻辑证明网的置换规则，其优点在于解除一些在归约过程中会被卡住的 redex。我们表明，这样的扩展允许在传值调用设定下定义令人满意的Böhm（类）树概念和程序逼近理论。我们证明所有具有相同Böhm树的lambda项在观测上等价，并刻画了那些作为lambda项实际Böhm树出现的类Böhm树。我们还将此方法与被Ehrhard基于lambda项泰勒展开的程序逼近理论相比较，后者将每个lambda项翻译成一个可能无限的所谓资源项集合。我们给出了一个资源项集合成为某lambda项泰勒展开的充分必要条件。最后，我们表明lambda项的泰勒展开范式可通过对其Böhm树执行归一化泰勒展开来计算。由此得出，两个lambda项具有相同的Böhm树当且仅当它们泰勒展开的范式一致。
引用
@article{arxiv.1809.02659,
title = {Revisiting Call-by-value B\"ohm trees in light of their Taylor expansion},
author = {Emma Kerinec and Giulio Manzonetto and Michele Pagani},
journal= {arXiv preprint arXiv:1809.02659},
year = {2023}
}