Title: Normalizing the Taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors,
Abstract: 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öhm 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öhm 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öhm trees to this setting.