关于 $\lambda$-项的泰勒展开及其刚性逼近的群胚结构
On the Taylor expansion of $λ$-terms and the groupoid structure of their rigid approximants
AI总结：
本文改进了泰勒展开范式与Böhm树同构的证明，简化步骤、引入群胚结构并扩展至非确定性设置，保留均匀性。
摘要：
我们证明了 $\lambda$-项的泰勒展开的范式与其 Böhm 树同构，沿着三个独立方向改进了 Ehrhard 和 Regnier 的原始证明。首先，我们通过直接在资源演算中遵循左归约策略来简化证明的最后一步，避免了引入专门的抽象机器。我们还引入了资源演算刚性变体中参数副本置换的群胚，并将泰勒展开的系数与此结构联系起来，而 Ehrhard 和 Regnier 使用的是变量出现置换的群。最后，我们将所有结果扩展到非确定性设置：与之前的尝试相反，我们表明在 Ehrhard 和 Regnier 方法中至关重要的均匀性属性可以在该设置中得以保留。
英文摘要：
We show that the normal form of the Taylor expansion of a $λ$-term is isomorphic to its Böhm 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
