On MALL proof nets

  (Willem Heijltjes)


Proof nets are geometric linear logic proofs. They are part of a long
tradition in mathematics where pictorial representations are used to
strip away distractions and get to the heart of the matter. In the
case of proof nets, the distractions are rule permutations in the
sequent calculus, and the "matter" is linear logic proof.

For the multiplicative fragment of linear logic, without units, proof
nets are in many ways perfect. They are canonical: two proofs
translate to the same proof net if and only if they are equal up to
permutations. They are small (the same size or smaller than a proof),
translating back and forth between proofs and nets is efficient
(linear-time), and cut-elimination is simple (path composition through
the graph). The additive fragment, even with units, is similarly
well-behaved.

Beyond these two fragments, the picture starts to fray. With the
multiplicative units, proof equivalence (deciding whether two proofs
are equal up to permutations) becomes PSPACE-complete - too much for
proof nets to be possible.

For the multiplicative-additive fragment without units (MALL) the
situation is subtle. Various notions of proof net, such as Girards
Monomial Nets, are small but not canonical, while Hughes and Van
Glabbeek's Slice Nets, are canonical but exponential-sized relative to
proofs. Recent work with Dominic Hughes proposes a new notion of proof
net for MALL, Conflict Nets, that is small, but as close to canonical
as we think possible. It factors out all permutations except one,
which would otherwise give exponential growth.

In this talk I will give an overview of recent and some less recent
work on proof nets, and discuss Conflict Nets in detail.