A finiteness structure on resource terms

摘要

We study the Taylor expansion of lambda-terms in a non-deterministic or algebraic setting, where terms can be added. The target language is a resource lambda calculus based on a differential lambda-calculus that we introduced recently. This operation is not possible in the general untyped case where reduction can produce unbounded coefficients. We endow resource terms with a finiteness structure (in the sense of our earlier work on finiteness spaces) and show that the Taylor expansions of terms typ