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 $λ$-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.