规范化非确定性λ项的泰勒展开：通过资源向量的并行归约
Normalizing the Taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors
AI总结：
该研究将泰勒展开与规范化交换性推广至代数λ演算，通过资源向量归约解决非确定性难题，并识别可规范化项类以泛化Böhm树。
摘要：
自Ehrhard和Regnier关于λ项泰勒展开的开创性工作以来，已知该操作与规范化可交换：一个λ项的展开总是可规范化的，且其规范形式是该项的Böhm树的展开。我们将此结果推广到代数λ演算的非均匀设置，即扩展了项线性组合的λ演算。这要求我们解决两个困难：首先是Ehrhard和Regnier的技术严重依赖于普通λ演算的均匀、确定性本质，因此无法直接改编；其次是缺乏在定量非确定性存在下Böhm树概念的令人满意的通用扩展，这反映在代数λ项的泰勒展开并非总是可规范化这一事实上。我们的解决方案是提供对泰勒展开下β-归约动力学的细粒度研究，通过引入资源向量（即资源λ项的无限线性组合）上的归约概念。后者构成微分λ演算的多线性片段，而资源向量是λ项泰勒展开的目标。我们证明资源向量的归约包含任何β-归约步骤的像，由此推断泰勒展开与规范化精确交换。此外，我们识别了一类代数λ项，涵盖可规范化的代数λ项和任意普通λ项：这些项的展开总是可规范化的，这指导了Böhm树在此设置中泛化的定义。
英文摘要：
It has been known since Ehrhard and Regnier's seminal work on the Taylor expansion of $λ$-terms that this operation commutes with normalization: the expansion of a $λ$-term is always normalizable and its normal form is the expansion of the Böhm tree of the term. We generalize this result to the non-uniform setting of the algebraic $λ$-calculus, i.e. $λ$-calculus extended with linear combinations of terms. This requires us to tackle two difficulties: foremost is the fact that Ehrhard and Regnier's techniques rely heavily on the uniform, deterministic nature of the ordinary $λ$-calculus, and thus cannot be adapted; second is the absence of any satisfactory generic extension of the notion of Böhm tree in presence of quantitative non-determinism, which is reflected by the fact that the Taylor expansion of an algebraic $λ$-term is not always normalizable. Our solution is to provide a fine grained study of the dynamics of $β$-reduction under Taylor expansion, by introducing a notion of reduction on resource vectors, i.e. infinite linear combinations of resource $λ$-terms. The latter form the multilinear fragment of the differential $λ$-calculus, and resource vectors are the target of the Taylor expansion of $λ$-terms. We show the reduction of resource vectors contains the image of any $β$-reduction step, from which we deduce that Taylor expansion and normalization commute on the nose. We moreover identify a class of algebraic $λ$-terms, encompassing both normalizable algebraic $λ$-terms and arbitrary ordinary $λ$-terms: the expansion of these is always normalizable, which guides the definition of a generalization of Böhm trees to this setting.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
