Taylor expansion in linear logic is invertible

TL;DR

This paper proves that the Taylor expansion of MELL proof-nets is invertible, establishing a one-to-one correspondence between proof-nets and their differential expansions, and demonstrating the relational model's injectivity for MELL.

Contribution

It introduces a proof of invertibility of Taylor expansion in MELL proof-nets and shows the relational model's injectivity, providing a new completeness result.

Findings

Different MELL proof-nets have distinct Taylor expansions.

The relational model is injective for MELL proof-nets.

Equality in the relational model corresponds exactly to cut-elimination.

Abstract

Each Multiplicative Exponential Linear Logic (MELL) proof-net can be expanded into a differential net, which is its Taylor expansion. We prove that two different MELL proof-nets have two different Taylor expansions. As a corollary, we prove a completeness result for MELL: We show that the relational model is injective for MELL proof-nets, i.e. the equality between MELL proof-nets in the relational model is exactly axiomatized by cut-elimination.