We study parallel cut elimination in the connected, multiplicative fragment of linear logic proof nets, and provide a bound on the diminution of size, and on the length of switching paths under parallel reduction. We show that this combinatorial result applies to Taylor expansion of MELL proof nets, and allows to establish that coefficients keep finite under parallel reduction of infinite linear combination of resource nets, because they behave exactly like multiplicative nets.
We examine some recent methods introduced to extend Ehrhard and Regnier's result on Taylor expansion: infinite linear combinations of approximants of a lambda-term can be normalized while keeping all coefficients finite. The methods considered allow to extend this result to non-uniform calculi; we show that when focusing on precise reduction strategies, such as Call-By-Value, Call-By-Need, PCF or variants of Call-By-Push-Value, the extension of Ehrhard and Regnier's finiteness result can hold or not, depending on the structure of the original calculus. In particular, we introduce a resource calculus for Call-By-Need, and show that the finiteness result about its Taylor expansion can be derived from our Call-By-Value considerations. We also introduce a resource calculus for a presentation of PCF with an explicit fixpoint construction, and show how it interferes with the finiteness result. We examine then Ehrhard and Guerrieri's Bang Calculus which enjoys some Call-By-Push-Value features in a slightly different presentation.
We extend the results of our CSL paper, generalizing it to a larger fragment of linear logic, including weakenings and multiplicative units. It demands specific methods to deal with non connected structures, in particular because of cuts reducing to empty substructures.