Gluing resource proof-structures: inhabitation and inverting the Taylor expansion

Giulio Guerrieri; Luc Pellissier; Lorenzo Tortora de Falco

doi:10.46298/lmcs-18(2:4)2022

Gluing resource proof-structures: inhabitation and inverting the Taylor expansion

Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco

Department of Computer Science

Research output: Contribution to journal › Article › peer-review

2 Citations (SciVal)

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 (and deciding in the finite case) 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. We also prove semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.

Original language	English
Pages (from-to)	4:1-4:46
Journal	Logical Methods in Computer Science
Volume	18
Issue number	2
DOIs	https://doi.org/10.46298/lmcs-18(2:4)2022
Publication status	Published - 22 Apr 2022

Bibliographical note

Publisher Copyright:
© G. Guerrieri, L. Pellissier, and L. Tortora de Falco.

Keywords

Taylor expansion
linear logic
natural transformation
proof-structure
pullback

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.46298/lmcs-18(2:4)2022Licence: CC BY

Cite this

@article{fd84abed618b45e48ff4c3bbc209ecf3,

title = "Gluing resource proof-structures: inhabitation and 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 (and deciding in the finite case) 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. We also prove semi-decidability of the type inhabitation problem for cut-free MELL proof-structures. ",

keywords = "Taylor expansion, linear logic, natural transformation, proof-structure, pullback",

author = "Giulio Guerrieri and Luc Pellissier and {Tortora de Falco}, Lorenzo",

note = "Publisher Copyright: {\textcopyright} G. Guerrieri, L. Pellissier, and L. Tortora de Falco.",

year = "2022",

month = apr,

day = "22",

doi = "10.46298/lmcs-18(2:4)2022",

language = "English",

volume = "18",

pages = "4:1--4:46",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Technischen Universitat Braunschweig",

number = "2",

}

TY - JOUR

T1 - Gluing resource proof-structures: inhabitation and inverting the Taylor expansion

AU - Guerrieri, Giulio

AU - Pellissier, Luc

AU - Tortora de Falco, Lorenzo

N1 - Publisher Copyright: © G. Guerrieri, L. Pellissier, and L. Tortora de Falco.

PY - 2022/4/22

Y1 - 2022/4/22

N2 - 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 (and deciding in the finite case) 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. We also prove semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.

AB - 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 (and deciding in the finite case) 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. We also prove semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.

KW - Taylor expansion

KW - linear logic

KW - natural transformation

KW - proof-structure

KW - pullback

UR - http://www.scopus.com/inward/record.url?scp=85130102287&partnerID=8YFLogxK

U2 - 10.46298/lmcs-18(2:4)2022

DO - 10.46298/lmcs-18(2:4)2022

M3 - Article

SN - 1860-5974

VL - 18

SP - 4:1-4:46

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 2

ER -

Gluing resource proof-structures: inhabitation and inverting the Taylor expansion

Abstract

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Typed Lambda-Calculi with Sharing and Unsharing

Cite this

Gluing resource proof-structures: inhabitation and inverting the Taylor expansion

Abstract

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Cite this