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.

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.

This special issue is devoted to some aspects of the new ideas that recently arose from the work of Thomas Ehrhard on the models of linear logic (LL) and of the λ-calculus. In some sense, the very origin of these ideas dates back to the introduction of LL in the 80s by Jean-Yves Girard. An obvious remark is that LL yielded a first logical quantitative account of the use of resources: the logical distinction between linear and non-linear formulas through the introduction of the exponential connectives. As explicitly mentioned by Girard in his first paper on the subject, the quantitative approach, to which he refers as ‘quantitative semantics,’ had a crucial influence on the birth of LL. And even though, at that time, it was given up for lack of ‘any logical justification’ (quoting the author), it contained rough versions of many concepts that were better understood, precisely introduced and developed much later, like differentiation and Taylor expansion for proofs. Around 2003, and thanks to the developments of LL and of the whole research area between logic and theoretical computer science, Ehrhard could come back to these fundamental intuitions and introduce the structure of finiteness space, allowing to reformulate this quantitative approach in a standard algebraic setting. The interpretation of LL in the category Fin of finiteness spaces and finitary relations suggested to Ehrhard and Regnier the differential extensions of LL and of the simply typed λ-calculus: Differential Linear Logic (DiLL) and the differential λ-calculus. The theory of LL proof-nets could be straightforwardly extended to DiLL, and a very natural notion of Taylor expansion of a proof-net (and of a λ-term) was introduced: an element of the Taylor expansion of the proof-net/term α is itself a (differential) proof-net/term and an approximation of α.

We give a semantic characterization of bounded complexity proofs. We introduce the notion of obsessional clique in the relational model of linear logic and show that restricting the morphisms of the category REL to obsessional cliques yields models of ELL and SLL. Conversely, we prove that these models are relatively complete: an LL proof whose interpretation is an obsessional clique is always an ELL/SLL proof. These results are achieved by introducing a system of ELL/SLL untyped proof-nets, which is both correct and complete with respect to elementary/ polynomial time

We address the question of injectivity of coherent semantics of linear logic proof-nets. Starting from Girard's definition of experiment, we introduce the key-notion of ‘injective obsessional experiment’, which allows us to give a positive answer to our question for certain fragments of linear logic, and to build counter-examples to the injectivity of coherent semantics in the general case.

Abstract The present report is a, somewhat lengthy, addendum to [4], where the elimination of cuts from derivations in sequent calculus for classical logic was studied ‘from the point of view of linear logic’. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives. The main novelty here is the observation that this type-distinction is not essential: we can allow classical sequent derivations to use any combination of additive and multiplicative introduction rules for each of the connectives, and still have strong normalization and confluence of tq-reductions. We give a detailed description of the simulation of tq-reductions by means of reductions of the interpretation of any given classical proof as a proof net of PN2 (the system of second order proof nets for linear logic), in which moreover all connectives can be taken to be of one type, e.g., multiplicative. We finally observe that dynamically the different logical cuts, as determined by the four possible combinations of introduction rules, are independent: it is not possible to simulate them internally, i.e.. by only one specific combination, and structural rules.