Lionel Vaux (I2M, Aix-Marseille), Taylor expansion, β-reduction and normalization

Schedule

Abstract

We introduce 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 introduced by Ehrhard and Regnier, and resource vectors are the target of the Taylor expansion of λ-terms. We show that the reduction of resource vectors contains the image, through Taylor expansion, of β-reduction in the algebraic λ-calculus, i.e. λ-calculus extended with weighted sums. We moreover exhibit a class of algebraic λ-terms, having a normalizable Taylor expansion: this subsumes both arbitrary pure λ-terms, and normalizable algebraic λ-terms. We then show that Taylor expansion and normalization commute.