zbMATH — the first resource for mathematics

On the dependencies of logical rules. (English) Zbl 1367.03109
Pitts, Andrew (ed.), Foundations of software science and computation structures. 18th international conference, FOSSACS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Berlin: Springer (ISBN 978-3-662-46677-3/pbk; 978-3-662-46678-0/ebook). Lecture Notes in Computer Science 9034, 436-450 (2015).
In the domain of proof theory, linear logic (LL) stands as a tool of main importance, for the fine-grained study of logical deductions it permits. One of the beauty of this proof system comes from proof nets: instead of conceiving proofs as being necessarily sequential deduction trees, it allows to represent proofs in a graphical way that makes it possible to manipulate proofs geometrically. This major discovery allows to reason about proofs using operator algebra, graph-theoretical arguments, and contributed to the study of the connexions between proofs and parallelism, proofs and complexity, and proofs and geometry.
Proof nets would not be without correction criteria, which separate “legitimate” graphs, i.e., one that stands for valid deductions, from illegitimate ones, i.e., one that does not have a corresponding sequenlization as a deduction tree. The most obvious correction criterion – “Is there a deduction tree that corresponds to this graph?” – is actually not the only one. Depending on the fragment of linear logic one consider (multiplicative, additive, with or without unit, with or without exponents), other criteria might be offered, sometimes varying greatly in the tools they use and their complexity.
The most well-studied substructural logic of linear logic is multiplicative linear logic (MLL), elegant and simple, and yet powerful enough to embed typed lambda-calculus. Several correction criteria were proposed for proof nets of this fragment (or slight variations of this fragment, e.g., without units or without the cut rule), even recently, when the Mogbil-Naurois criterion was used to prove that the correctness of proof nets for MLL was a non-deterministic logarithmic space (NL) complete problem. The paper presented here studies those various criteria, offers a new criteria, provides a tool to compare them, and gives precise references. It is at the same time an excellent introduction to the problem, one of the most complete summary of the current situation, and an interesting contribution to the problem.
The paper has a clear exposition, offers an unifying framework, and has a nice introduction that exposes clearly the problem and its interest. The concise reformulation of scattered correction criterion could be particularly useful to anyone willing to understand and compare them. The notion of dependency studied by the authors is a nice observation that is suitably used to compare (mainly three of) those criterion. The use of the Euler-Poincaré lemma is a nice contribution to strengthen the links between graph theory and proof theory.
Overall, this work should be the future point of entry for anyone willing to become familiar with MLL’s criterion correction. Anyone willing to understand the situation for additive proof nets should look at the works of Willem Heijltjes (https://www.cs.bath.ac.uk/~wbh22/). One could regret that this work wasn’t offer any follow-up (except maybe for the journal version of [V. M. Abrusci and R. Maieli, Lect. Notes Comput. Sci. 9160, 53–68 (2015; Zbl 1365.03039)]), for the future extensions sketched in the conclusion are of interest. The extended version is now hosted at http://dissem.in/p/17648/ .
For the entire collection see [Zbl 1320.68027].

03F52 Proof-theoretic aspects of linear logic and other substructural logics
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
Full Text: DOI