Causality in Linear Logic: full completeness and injectivity (unit-free multiplicative-additive fragment)
File(s)
Published version
Author(s)
Castellan, Simon
Yoshida, Nobuko
Type
Conference Paper
Abstract
Commuting conversions of Linear Logic induce a notion of dependencybetween rules inside a proof derivation: a rule depends on a previous rule whenthey cannot be permuted using the conversions. We propose a new interpretation ofproofs of Linear Logic ascausal invariantswhich capturesexactlythis dependency.We represent causal invariants using game semantics based on general eventstructures, carving out, inside the model of [6], a submodel of causal invariants.This submodel supports an interpretation of unit-free Multiplicative AdditiveLinear Logic with MIX (MALL−) which is (1)fully complete: every element ofthe model is the denotation of a proof and (2)injective: equality in the modelcharacterises exactly commuting conversions of MALL−. This improves over thestandard fully complete game semantics model of MALL−.
Date Issued
2019-04
Date Acceptance
2019-01-25
Citation
Lecture Notes in Computer Science, 2019, 11425, pp.150-168
ISBN
9783030171261
ISSN
0302-9743
Publisher
Springer Verlag
Start Page
150
End Page
168
Journal / Book Title
Lecture Notes in Computer Science
Volume
11425
Copyright Statement
© The Author(s) 2019. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
ERI 025567 (EP/K034413/1)
PO 20131167
EP/K011715/1
EP/N027833/1
20103649
Source
22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)
Subjects
Artificial Intelligence & Image Processing
Publication Status
Published
Start Date
2019-04-06
Finish Date
2019-04-11
Coverage Spatial
Prague, Czech Republic
Date Publish Online
2019-04-05