关于 λ-项的泰勒展开及其刚性近似项的群oid结构
计算机科学中的逻辑
2023-06-22 v4
摘要
我们证明了 λ-项的泰勒展开的正规形同构于其Böhm树，沿三个独立方向改进了Ehrhard和Regnier的原始证明。首先，我们通过在资源演算中直接遵循左归约策略简化了证明的最后一步，避免了引入专门的抽象机。我们还在资源演算的刚性变体中引入了参数副本置换的群oid，并将泰勒展开的系数与该结构相关联，而Ehrhard和Regnier使用的是变量出现置换的群。最后，我们将所有结果推广到非确定性设定：与先前尝试相反，我们证明了在Ehrhard和Regnier方法中至关重要的均匀性性质在该设定下得以保持。
引用
@article{arxiv.2008.02665,
title = {On the Taylor expansion of $\lambda$-terms and the groupoid structure of their rigid approximants},
author = {Federico Olimpieri and Lionel Vaux Auclair},
journal= {arXiv preprint arXiv:2008.02665},
year = {2023}
}