论文标题
关于$λ$ terms及其刚性近似值的taylor扩展
On the Taylor expansion of $λ$-terms and the groupoid structure of their rigid approximants
论文作者
论文摘要
我们表明，$λ$ term的泰勒膨胀的正常形式与其böhm树是同构的，从而改善了Ehrhard和Regnier的原始证明，并沿着三个独立的方向进行了原始证明。首先，我们通过直接在资源演算中遵循左减少策略来简化证明的最后一步，避免引入抽象机临时。我们还将参数副本的置换置于资源微积分的刚性变体中，并将泰勒扩展系数与该结构相关联，而Ehrhard和Regnier则与变量发生的置换库一起工作。最后，我们将所有结果扩展到非确定的环境：与以前的尝试相比，我们表明在Ehrhard中至关重要的统一属性可以在此环境中保留。
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.
