The Inverse Taylor Expansion Problem in Linear Logic

Linear Logic is based on the analogy between algebraic linearity (i.e. commutation with sums and scalar products) and the computer science linearity (i.e. calling 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 expansion. 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 approximation of the Taylor expansion of this proof. We prove that this algorithm is sound, complete and can be run in nondeterministic polynomial time.

• Type: Conference
• Year: 2009
• Where: LICS
• Authors: Michele Pagani, Christine Tasson
• Keywords: Computer Science, LICS 2009, Linear Logic, Multiplicative Exponential Linear, Taylor Expansion