MobilityReadingGroup

Causality in Linear Logic
Full completeness and injectivity (unit-free multiplicative-additive fragment)

Simon CASTELLAN, Nobuko YOSHIDA

Commuting conversions of Linear Logic induce a notion of dependency between rules inside a proof derivation: a rule depends on a previous rule when they cannot be permuted using the conversions. We propose a new interpretation of proofs of Linear Logic as causal invariants which captures exactly this dependency.

We represent causal invariants using game semantics based on general event structures, carving out, inside a recent game semantics model based on general event structures, a submodel of causal invariants. This submodel supports an interpretation of unit-free Multiplicative Additive Linear Logic with MIX (MALL⁻) which is (1) fully complete: every element of the model is the denotation of a proof and (2) injective: equality in the model characterises exactly commuting conversions of MALL⁻. This improves over the standard fully complete game semantics model of MALL⁻.

@inproceedings{CY2019,
  author = {Simon Castellan and Nobuko Yoshida},
  title = {{Causality in Linear Logic}},
  booktitle = {22nd International Conference on Foundations of Software Science and Computation Structures},
  series = {LNCS},
  pages = {150--168},
  publisher = {Springer},
  year = 2019
}

@inproceedings{CY2019,
  author = {Simon Castellan and Nobuko Yoshida},
  title = {{Causality in Linear Logic}},
  booktitle = {22nd International Conference on Foundations of Software Science and Computation Structures},
  series = {LNCS},
  pages = {150--168},
  publisher = {Springer},
  doi = "10.1007/978-3-030-17127-8_9",
  year = 2019
}