Taylor expansion in linear logic is invertible

Daniel de Carvalho

doi:10.23638/LMCS-14(4:21)2018

Daniel de Carvalho - Taylor expansion in linear logic is invertible

lmcs:4643 - Logical Methods in Computer Science, December 7, 2018, Volume 14, Issue 4 - https://doi.org/10.23638/LMCS-14(4:21)2018

Taylor expansion in linear logic is invertibleArticle

Authors: Daniel de Carvalho

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.

https://doi.org/10.23638/LMCS-14(4:21)2018

Source: arXiv.org:1712.05505

Volume: Volume 14, Issue 4

Secondary volumes: Selected Papers of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Published on: December 7, 2018

Accepted on: October 24, 2018

Submitted on: June 25, 2018

Keywords: Computer Science - Logic in Computer Science

Licence: Attribution 4.0 International (CC BY 4.0)