The relational model is injective for multiplicative exponential linear logic (without weakenings) (Q435194): Difference between revisions

This paper is motivated by a long line of research developed around the question of whether the relational semantics of multiplicative exponential linear logic (MELL) is injective, i.e., fully abstract. The main result of the paper is a great improvement of the state of the art and says that for MELL, without neither weakenings nor the multiplicative unit bottom, the relational semantics is injective. This is obtained from a much stronger result: in the full MELL fragment (with units) two proof-nets with the same interpretation are the same ``up to the connections between the doors of exponential boxes'', i.e., they have the same linear proof structure (LPS) in the authors' terminology. In the style of the work of \textit{D. de Carvalho}, \textit{M. Pagani} and \textit{L. Tortora de Falco} [Theor. Comput. Sci. 412, No. 20, 1884--1902 (2011; Zbl 1222.03070)], the authors work in an untyped framework; they neither define proof-nets nor cut elimination but only cut-free proof structures (PS): they prove that two PS with the same interpretation have the same LPS. A proof-net (as defined in [loc. cit.]) is a particular case of PS so that the result holds for untyped (so as for typed) MELL proof-nets. The notion of LPS, which comes from [\textit{L. Tortora de Falco}, Math. Struct. Comput. Sci. 13, No. 6, 799--855 (2003; Zbl 1049.03043)], is the main syntactical tool: with every proof-net R an LPS is associated which is obtained from R by forgetting some information about R's exponential boxes, namely which auxiliary doors correspond to which !-link (using standard LL's terminology). A PS is then an LPS and a function allowing to recover boxes. It is proved that this function can be recovered from the LPS when the PS is a connected graph: this yields injectivity for MELL without weakenings and bottom. The results of this paper build on some remarkable technical novelties introduced by the authors, among them a new use of ``injective experiments'' and ``injective \(k\)-points''. Summing up, it is shown that if the interpretation of a PS R contains an atomic injective \(k\)-point, then every PS R\('\) with the same interpretation as R, also has the same LPS as R.