A Correctness Criterion Free from Switchings

ABSTRACT. We present a new correctness criterion for Multiplicative Linear Logic (MLL) proof nets. Our criterion generalizes a criterion recently introduced by Mogbil and Jacobé de Naurois in order to characterize the space complexity of the correctness problem for M(E)LL: while the Mogbil-Naurois criterion relies on a single switching, our criterion completely abstracts from the notion of switchings.

This is done in two steps. First we define dependency graphs on proof nets rather than correction graphs, as in Mogbil-Naurois, making them switching-independent. Then, we partition our criterion in two parts: one part deals exclusively with tensor, axiom and cut inferences while the other one deals with the structure of par inferences by requiring dependency graphs to be acyclic flowgraphs (or SDAG). We finally compare both notions of dependency graphs.