Glueability of resource proof-structures: inverting the Taylor expansion (long version)
Giulio Guerrieri (1), Luc Pellissier (2), Lorenzo Tortora de Falco (3), ((1) University of Bath, Department of Computer Science, (2) Universit\'e de, Paris, IRIF, (3) Universit\`a Roma Tre, Dipartimento di Matematica e Fisica)
TL;DR
This paper introduces a new criterion for identifying sets of resource proof-structures that originate from a MELL proof-structure's Taylor expansion, using a rewriting system to characterize the expansion process.
Contribution
It provides a novel criterion and rewriting system to invert the Taylor expansion of MELL proof-structures, clarifying the relationship between resource and original proof-structures.
Findings
Characterizes resource proof-structures from Taylor expansion
Introduces a rewriting system for proof-structure analysis
Establishes conditions for inverting the Taylor expansion
Abstract
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.