关于$lambda$-项的泰勒展开和其刚性逼近的群结构
摘要：正规的Taylor展开形式与其B"ohm树同构，改进了Ehrhard和Regnier的原始证明的三个独立方向。首先，通过直接在资源计算中遵循左规约策略，简化了证明的最后一步，避免引入一种特定的抽象机。此外，我们引入了参数的副本的排列的群oid，在资源计算的刚性变体中与Taylor展开的系数相关联，而Ehrhard和Regnier是通过变量出现的排列群进行研究的。最后，我们将所有结果扩展到非确定性设置：与以前的尝试相比，我们展示了在这种设置中关键的一致性属性可以被保留下来。
作者：Federico Olimpieri and Lionel Vaux Auclair
论文ID：2008.02665
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22