Causality in Linear Logic Full Completeness and Injectivity (Unit-Free Multiplicative-Additive Fragment)

摘要

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 the model of [6], 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~-.