How should I think about proof nets?

Question

In his answer to this question, Stephane Gimenez pointed me to a polynomial-time normalization algorithm for proofs in linear logic. The proof in Girard's paper uses proof nets, which are an aspect of linear logic I don't actually know very much about.

Now, I've tried to read papers on proof nets before (such as Pierre-Louis Curien's notes on them), but I have not really understood them. So my question is: how should I think about them? By "how to think about them", I mean both the informal intuition behind them (e.g., how they behave computationally, or how they are related to sequents), and also which theorems about them I should prove for myself to really get them.

In answering this question, you can assume (1) I know the proof theory of linear logic well (including things like how the cut-elimination proof goes, and in focalized form too), (2) their categorical semantics in terms of coherence spaces or via Day convolution, and (3) the very basic rudiments of the GoI construction.

Answer 1

Let us call a logic "symmetric" where a $-A$ ("not A") assumption means the same as proving $A$ and a proof of $-A$ means the same as an assumption of $A$. Classical logic and linear logic are symmetric in this sense. Intuitionistic logic is not.

Girard noticed that natural deduction is asymmetric in exactly this way. That is why it matches up with intuitionistic logic. Proof nets represent an attempt by Girard to invent a symmetric form of natural deduction.

The best introduction to these ideas is in Girard's "Proofs and Types". If you work through the natural deduction and sequent calculus system for the $\land\to$ fragment of intuitionistic logic, and closely read the sections 5.3 and 5.4 which establish a homomorphism from sequent calculus to natural deduction, you get an appreciation of what natural deduction is all about. Then Lafont's Appendix introduces proof nets in the same spirit. It is more or less straightforward to extend the homomorphism of sections 5.3-4 to one between linear logic sequent calculus and linear logic proof nets (at least for the multiplicative fragment).

One thing that is perhaps needlessly confusing about Girard's treatment is that he dispenses with two-sided sequents and uses one-sided sequents in the interest of economy. For sequent calculus this works more or less fine. But, when the same economy is applied to natural deduction, things look strange. A proof net is therefore a "natural deduction proof" of a disjunction of formulas, without any assumptions. A deduction of type $\Gamma \vdash A$ is turned into a proof net of type $\vdash \Gamma^\perp, A$. If this confuses you then you might want to write down for yourself a two sided sequent calculus and an assumption-conclusion form of proof nets. That might clarify things.

---

Something I missed out in my original answer: Proof nets are a way of writing proofs, and we know that proofs are programs. So, proof nets are also a way of writing programs.

The traditional functional notation for writing programs is asymmetric, just like natural deduction is. So, proof nets point to a way of writing programs in a symmetric form. That is how process calculi enter the picture.

Another way of representing the symmetry is through logic programming, which I have explored in two papers: A typed foundation for directional logic programs and Higher-order aspects of logic programming

Answer 2

Proof nets are interesting essentially for three reasons:

1) IDENTITY OF PROOFS. They provide an answer to the problem "when are two proofs the same"? In sequent calculus you may have many different proofs of the same proposition which differ only because sequent calculus forces an order among deduction rules even when this is not necessary. Of course, one can add an equivalence relation on sequent calculus proofs, but then one has to show that cut-elimination behaves properly on equivalence classes, and also it is necessary to turn to rewriting modulo, which is quite more technical than plain rewriting. Proof nets solve the problem of dealing with equivalence classes by providing a syntax where every equivalence class is collapsed on a single object. This situation is anyway a bit idealistic, as for many reasons proof nets are often extended with some form of equivalence.

2) NO COMMUTATIVE CUT-ELIMINATION STEPS. Cut-elimination on proof nets takes a quite different flavor than on sequent calculi because commutative cut-elimination steps disappear. The reason is that in proof nets the deduction rules are connected only by their causal relation. Commutative cases are generated by the fact that one rule can be hidden by another causally unrelated rule. This cannot happen in proof nets, where causally unrelated rules are far apart. Since most cases of cut-elimination are commutative one gets a striking simplification of cut-elimination. This has been particularly useful for studying lambda calculi with explicit substitutions (because exponentials = explicit substitutions). Again, this situation is idealized since some presentations of proof nets require commutative steps. However, their number is much smaller than in sequent calculus

3) CORRECTNESS CRITERIA. Proof nets can be defined by translation of sequent calculus proofs, but usually a system of proof nets is not accepted as such unless it is provided with a correctness criterion, i.e. a set of graph-theoretical principles characterizing the set of graphs obtained by translating a sequent calculus proof. The reason for requiring a correctness criterion is that the free graphical language generated by the set of proof net constructors (called links) contains "too many graphs", in the sense that some graphs do not correspond to any proof. The relevance of the correctness criteria approach is usually completely misunderstood. It is important because it gives non-inductive definitions of what is a proof, providing shockingly different perspectives on the nature of deductions. The fact that the characterization is non-inductive is usually criticized, while it is exactly what is interesting. Of course, it is not easily amenable to formalization, but, again, this is its strength: proof nets provide insights that are not available through the usual inductive perspective on proofs and terms. A fundamental theorem for proof nets is the sequentialization theorem, which says that any graph satisfying the correctness criterion can be inductively decomposed as a sequent calculus proof (translating back to the correct graph).

Let me conclude that it is not precise to say that proof nets are a classical and linear version of natural deduction. The point is that they solve (or attempt to solve) the problem of the identity of proofs and that natural deduction succesfully solve the same problem for minimal intuitionistic logic. But proof nets can be done also for intuitionistic systems and for non-linear systems. Actually, they work better for intuitionistic systems than for classical systems.

Answer 3

This relates mostly to the "how they behave computationally" part of your question. One way to understand proof nets well from the computational perspective is by looking at slightly more concrete interpretations (eg., process algebraic).

You might be interested in the following:

• The paper by Abramsky (the CLL section on Proof Expressions): Computational Interpretations of Linear Logic. This paper also presents some results that are close to the corresponding ones for proof nets, so might help in the second aspect of your question.

• The paper by Honda and Laurent which shows how a specific kind of Proof Nets, called Polarized Proof Nets, corresponds to Pi-calculus processes, and which is mentioned above by Martin Berger: An exact correspondence between a typed pi-calculus and polarised proof-nets

• (here i shamelessly advertise my own work) The draft: Proof Nets in Process Algebraic Form

There are also some works relating proof nets and lambda calculus, which also give substantial intuitions. For example, the following by Delia Kesner and Stéphane Lengrand:

• Resource Operators for λ-calculus

You might also be interested in this type of work (very oriented to theoretical aspects) which relies on Proof Structures to prove in detail the Strong Normalisation property of LL, by Michele Pagani and Lorenzo Tortora de Falco.

• Strong Normalisation Property for Second Order Linear Logic (this paper contains a nice map of important theorems).

In general, which theorems should one study? Well, I'm hardly an authority but you might want to look at "Sequentialisation" (relating Proof Nets and Sequent Proofs; see the original TCS paper on LL), and the strong normalisation proof (rather involved, as expected, but many important PN theorems are related to it [or, used to prove it]).

If you are familiar with focusing, you might also be interested in this paper by Andreoli:

• Focusing and Proof-Nets in Linear and Non-commutative Logic

Hope this helps. Again, these references are really non-exhaustive.

best, Dimitris

Answer 4

I focus on how proof nets are related to sequent calculus, leaving more dynamic stuff.

Proof nets abstract sequent calculus proofs: a proof net represents a set of sequent calculus proofs. Proof nets forget unimportant differences between sequent calculus proofs (like which formula is decomposed below which). The important theorem here is "sequentialization", which converts a proof net into a sequent calculus proof.

Answer 5

There has been interesting work recently on making the relation between proof net and focused calculi tighter, using "multi-focused" variants where you may have several simultaneous left holes, and studying "maximally focused" proofs. If you pick the calculus right, maximally-focused proofs can correspond to MLL proof nets or, in classical logic, to expansion proofs (The Isomorphism Between Expansion Proofs and Multi-Focused Sequent Proofs, Kaustuv Chaudhuri, Stefan Hetzl and Dale Miller, 2013)

Answer 6

You can check my paper "A survey of proof nets and matrices for substructural logics".

Abstract:

This paper is a survey of two kinds of "compressed" proof schemes, the \emph{matrix method} and \emph{proof nets}, as applied to a variety of logics ranging along the substructural hierarchy from classical all the way down to the nonassociative Lambek system. A novel treatment of proof nets for the latter is provided. Descriptions of proof nets and matrices are given in a uniform notation based on sequents, so that the properties of the schemes for the various logics can be easily compared.