A Finiteness Structure on Resource Terms
Thomas Ehrhard · 2010
We study the Taylor expansion of lambda-terms in a on-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 typeable in Girard's system F are finitary by a reducibility method.