The relational model is injective for multiplicative exponential linear logic (without weakenings) (Q435194): Difference between revisions
From MaRDI portal
Created a new Item |
Changed an Item |
||
Property / review text | |||
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. | |||
Property / review text: 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. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Alberto Carraro / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F52 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B40 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B47 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B70 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F03 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F05 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F07 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q55 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6054358 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
linear logic | |||
Property / zbMATH Keywords: linear logic / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
MELL proof-nets | |||
Property / zbMATH Keywords: MELL proof-nets / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
denotational semantics | |||
Property / zbMATH Keywords: denotational semantics / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
relational model | |||
Property / zbMATH Keywords: relational model / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
injectivity | |||
Property / zbMATH Keywords: injectivity / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
full abstraction | |||
Property / zbMATH Keywords: full abstraction / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
relational semantics | |||
Property / zbMATH Keywords: relational semantics / rank | |||
Normal rank |
Revision as of 00:48, 30 June 2023
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The relational model is injective for multiplicative exponential linear logic (without weakenings) |
scientific article |
Statements
The relational model is injective for multiplicative exponential linear logic (without weakenings) (English)
0 references
11 July 2012
0 references
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.
0 references
linear logic
0 references
MELL proof-nets
0 references
denotational semantics
0 references
relational model
0 references
injectivity
0 references
full abstraction
0 references
relational semantics
0 references