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

TL;DR

This paper characterizes and decides which sets of resource proof-structures can be derived from a MELL proof-structure's Taylor expansion, introducing a rewriting system and exploring type inhabitation semi-decidability.

Contribution

It introduces a new criterion and rewriting system to identify sets of resource proof-structures in the Taylor expansion of MELL proof-structures, and proves semi-decidability of type inhabitation.

Findings

Characterization of resource proof-structures in Taylor expansion

Decidability criterion for finite cases

Semi-decidability of type inhabitation in MELL

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.