一句话：改进 λ-项 Taylor 展开正规形与 Böhm 树同构的证明，引入刚性资源演算中的置换群胚并扩展到非确定性情形。
本文研究 λ-项 Taylor 展开与其 Böhm 树之间的关系，即 Taylor 展开的正规形是否同构于原项的 Böhm 树。Ehrhard 与 Regnier 原有证明依赖特定抽象机器，且仅处理变量出现置换的群结构。作者在资源演算中直接采用左归约策略，简化证明最后一步；进而定义刚性资源演算中参数副本置换的群胚，并用其刻画 Taylor 展开的系数。最后将全部结果推广到非确定性设定，证明此前关键的 uniformity 性质在该设定下仍可保持。该工作为 Taylor 展开、资源演算与 λ-演算语义提供了更统一的结构视角。
We show that the normal form of the Taylor expansion of a $\lambda$-term is isomorphic to its B\"ohm tree, improving Ehrhard and Regnier's original proof along three independent directions. First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad hoc. We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables. Finally, we extend all the results to a nondeterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier's approach can be preserved in this setting.
@article{paperbot1753,
title = {On the Taylor expansion of $\lambda$-terms and the groupoid structure of their rigid approximants},
author = {Federico Olimpieri and Lionel Vaux Auclair},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:1)2022}
}