de Mathématiques de Luminy
Ehrhard Thomas, Regnier Laurent.
Uniformity and the Taylor expansion of ordinary lambda-terms.
We define the complete Taylor expansion of an ordinary lambda-terms as an infinite linear combination with rational coefficients of terms of a resource calculus similar to Boudol's resource lambda-calculus. In this calculus, all applications are (multi-)linear in the algebraic sense, that is commute withe linear combination of the function or the argument. We study the beta-reduction of the linear combination of resource terms associated to a lambda-term by Taylor expansion, using a uniformity property that they enjoy.