The relational model is injective for multiplicative exponential linear logic (without weakenings) (Q435194): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(5 intermediate revisions by 5 users not shown) | |||
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 | |||
Property / Wikidata QID | |||
Property / Wikidata QID: Q114209365 / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.apal.2012.01.004 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1623703906 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Full abstraction for PCF / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4842980 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: λμ-calculus and Böhm's theorem / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A semantic measure of the execution time in linear logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Execution time of λ-terms via denotational semantics and intersection types / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Obsessional experiments for linear logic proof-nets / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The Typed Böhm Theorem / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Differential interaction nets / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linear logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Locus Solum: From the rules of logic to the logic of rules / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4838155 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On full abstraction for PCF: I, II and III / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4842976 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Syntax vs. semantics: A polarized approach / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Head linear reduction and pure proof net extraction / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Weak typed Böhm theorem on IMLL / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linear logic and polynomial time / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The Separation Theorem for Differential Interaction Nets / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A semantic characterisation of the correctness of a proof net / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: λ-definable functionals andβη conversion / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 11:33, 5 July 2024
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
0 references
0 references