Taylor expansion in linear logic is invertible
Logic in Computer Science
2023-06-22 v4
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.
Keywords
Cite
@article{arxiv.1712.05505,
title = {Taylor expansion in linear logic is invertible},
author = {Daniel de Carvalho},
journal= {arXiv preprint arXiv:1712.05505},
year = {2023}
}