Our present contribution is to show

Our present contribution is to show that in those various calculi, the finiteness results hold, up to a convenient definition of the resource calculi and to the choice of arguments depending on those calculi’s precise features. Call-By-Value Taylor expansion has already been defined by Ehrhard [9], and shown to be compatible with B¨ohm trees by Kerinec, Manzonetto and Pagani [17], but in a qualitative way (i.e. coefficients are not considered). We show in Section 2.1 that a parallel reduction is definable on Taylor expansion with coefficients, and this remains true if we provide an algebraic extension of Call-By-Value calculus, because the method used by Vaux-Auclair can be adapted to this setting. We also define in Section 2.2 a resource calculus adapted to Call-By-Need reduction, and observe that the specificities of its operational semantics implies that its Taylor expansion consists in the same set of resource terms as Call-By-Value one. For the two calculi of Section 2 and for the Bang calculus, the finiteness result is proven thanks to a combinatorial study of the parallel reduction and the size of resource terms in the Taylor expansion, following Vaux-Auclair’s method [29]. The key result is then about cardinalities of sets, size of terms, and concerns the sets J. Chouquet / Electronic Notes in Theoretical Computer Science 347 (2019) 65–85 67 underlying to Taylor expansion. This implies in particular that uniformity is not a necessary property for the proofs to be valid, and that algebraic extensions of the calculus would not interfere with the arguments.