The inverse taylor expansion problem in linear logic

Linear Logic is based on the analogy between algebraic linearity (i.e. commutation with sums and with products with scalars) and the computer science linearity (i.e. call-ing inputs only once). Keeping on this analogy, Ehrhard and Regnier introduced Differential Linear Logic (DILL) — an extension of Multiplicative Exponential Linear Logic with differential constructions. In this setting, promotion (the logical exponentiation) can be approximated by a sum of promotion-free proofs of DILL, via Taylor expansion. We present a constructive way to revert Taylor expan-sion. Precisely, we define merging reduction — a rewriting system which merges a finite sum of DILL proofs into a proof with promotion whenever the sum is an approxima-tion of the Taylor expansion of this proof. We prove that this algorithm is sound, complete and can be run in non-deterministic polynomial time