Conflict nets: Locally canonical MALL proof nets

Proof nets capture the semantic and/or computational content of linear logic in a clean graphical representation. They are perfect for the multiplicative fragment without units, and for the additive fragment with or without units. Beyond these fragments, the multiplicative units and the weakening rule of the exponentials make canonical proof nets impossible.

In-between, the multiplicative-additive fragment without units (MALL) occupies an interesting space where the interplay between canonicity and complexity is subtle. Canonical proof nets exist, in Hughes and Van Glabbeek’s Slice Nets, but they are exponential-sized. Monomial proof nets (by Girard, Laurent and Maieli) have interesting computational properties, but not canonicity.

In this talk I will discuss Conflict Nets, a notion of proof net that combines several good properties:

• Conservativity over MLL and ALL proof nets
• Linear size compared to sequent proofs
• Canonicity for all local rule permutations

Here, local permutations are those that do not duplicate or erase entire subproofs. In MALL, only a the permutation of a tensor-rule and a with-rule is non-local; all other permutations are factored out in conflict nets. By isolating this one rule permutation, conflict nets give a very sharp picture of where complexity resides.

This is joint work with Dominic Hughes.