一句话：将 Taylor 展开与归一化交换的经典结果推广到代数 λ-演算，并引入资源向量并行归约证明该性质。
Ehrhard 与 Regnier 证明普通 λ-项的 Taylor 展开与归一化交换，其范式为 Böhm 树的展开。本文推广到含项线性组合的代数 λ-演算。难点在于原技术依赖确定性，且非确定性下缺少通用 Böhm 树，使展开未必可归一化。作者研究 Taylor 展开下 β-归约的动力学，在资源向量（资源 λ-项的无穷线性组合，即微分 λ-演算多线性片段）上引入归约，并证明其包含任意 β-归约步的像。由此得到 Taylor 展开与归一化严格交换，并刻画一类展开总可归一化的代数 λ-项，涵盖可归一化代数项与任意普通 λ-项，为推广 Böhm 树奠定基础。
It has been known since Ehrhard and Regnier's seminal work on the Taylor expansion of $\lambda$-terms that this operation commutes with normalization: the expansion of a $\lambda$-term is always normalizable and its normal form is the expansion of the B\"ohm tree of the term. We generalize this result to the non-uniform setting of the algebraic $\lambda$-calculus, i.e. $\lambda$-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 $\lambda$-calculus, and thus cannot be adapted; second is the absence of any satisfactory generic extension of the notion of B\"ohm tree in presence of quantitative non-determinism, which is reflected by the fact that the Taylor expansion of an algebraic $\lambda$-term is not always normalizable. Our solution is to provide a fine grained study of the dynamics of $\beta$-reduction under Taylor expansion, by introducing a notion of reduction on resource vectors, i.e. infinite linear combinations of resource $\lambda$-terms. The latter form the multilinear fragment of the differential $\lambda$-calculus, and resource vectors are the target of the Taylor expansion of $\lambda$-terms. We show the reduction of resource vectors contains the image of any $\beta$-reduction step, from which we deduce that Taylor expansion and normalization commute on the nose. We moreover identify a class of algebraic $\lambda$-terms, encompassing both normalizable algebraic $\lambda$-terms and arbitrary ordinary $\lambda$-terms: the expansion of these is always normalizable, which guides the definition of a generalization of B\"ohm trees to this setting.
@article{paperbot776,
title = {Normalizing the Taylor expansion of non-deterministic {\lambda}-terms, via parallel reduction of resource vectors},
author = {Lionel Vaux},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 3},
year = {2019},
doi = {10.23638/lmcs-15(3:9)2019}
}