proof net (changes) in nLab

Showing changes from revision #24 to #25: Added | Removed | Changed

Contents

Idea

Proof nets are a graphical way to denote proofs in linear logic.

They were introduced by J.-Y. Girard in 1987 in order to remove spurious notational redundancies introduced by sequential rule application or indeterminacy of cut elimination and can be viewed as graphical normal forms of proofs freed from ‘the bureaucracy of syntax’ (Girard).

Bearing in mind the categorical semantics of (multiplicative intuitionistic) linear logic in (closed) monoidal categories, proof nets are closely related to Kelly-Mac Lane graphs that are used to track compositions of extranatural transformations definable in such categorical structures. More generally they may be compared to string diagrams that are evaluated in these categories (with various ways of making the comparison more precise). Proof nets for full linear logic have been thus described by Melliès 06 as string diagrams equipped with “boxes” to account for the exponential modality.

With linear logic/linear type theory interpreted as quantum logic/quantum computation, proof nets correspond to quantum circuits or Feynman diagrams (Blute-Panangaden).

Definition

We begin by describing proof nets for multiplicative linear logic (MLL), which is interpretable in *\ast-autonomous categories. Similar proof nets may be given for other forms of linear type theory such as multiplicative intuitionistic linear logic, which is interpretable in symmetric closed monoidal categories.

Proof structures

Before describing proof nets, we start with Girard’s notion of proof structure. It is simplest to describe the cut-free version, as this is closely connected with the notion of Kelly-Mac Lane graph, or KM-graph for short. We need just a few preliminaries.

Formulas in MLL may be built from an alphabet T\mathbf{T} of propositional variables and two constants 1\mathbf{1}, ⊥\bot by applying operations ⊗\otimes and ⊸\multimap. (Negation may be defined by ¬A≔A⊸⊥\neg A \coloneqq A \multimap \bot, and the multiplicative disjunction by A⅋B≔¬A⊸BA \parr B \coloneqq \neg A \multimap B. To get formulas in MILL, simply drop ⊥\bot.) The construction of a formula may be displayed as a binary planar tree.

We consider two-sided sequents Γ=A 1,…,A m⊢Δ=B 1,…,B n\Gamma = A_1, \ldots, A_m \vdash \Delta = B_1, \ldots, B_n, wherein the formulas of Γ\Gamma to the left of the turnstyle are called negative and the formulas of Δ\Delta are called positive. Subformulas of these formulas acquire signs according to the following rules:

• The subformulas S,TS, T of S⊗TS \otimes T have the same sign as S⊗TS \otimes T.

• The subformula TT of S⊸TS \multimap T has the same sign as S⊸TS \multimap T, while SS has the opposite sign.

We indicate the sign of a subformula using a superscript, e.g., S +S^+.

For a proof structure of type Γ→Δ\Gamma \to \Delta, it is clear that the only information not determined from Γ\Gamma and Δ\Delta are the KM-links. These KM-links give a KM-graph.

MLL formulas AA and proof structures of type A→BA \to B form a category Struct[T]Struct[\mathbf{T}]. Composition of proof structures is given by composing the underlying KM-graphs; identity proof structures are given by identity KM-graphs.

In fact this category of proof structures is a *\ast-autonomous category. As objects are MLL formulas, it is clear how ⊗\otimes and ⊸\multimap are defined on objects.

Proof nets

Proof nets are those proof structures that arise by taking the KM-graphs of morphisms that are definable in the language of *\ast-autonomous categories. Or, in the language of Girard, proof nets are those proof structures which are “correct” or “valid” (i.e., derivable from a sequent deduction, in a sense explained below).

More exactly, let F[T]F[\mathbf{T}] be the free *\ast-autonomous category on T\mathbf{T} (as discrete category), viewing *\ast-autonomous categories and functors that preserve *\ast-autonomous structure strictly as a 1-category that is 1-monadic over CatCat, the category of small categories and functors. Observe that the objects of F[T]F[\mathbf{T}] may be identified with MLL formulas. We view the morphisms of F[T]F[\mathbf{T}] as representing morphisms that are definable (starting with the datum T\mathbf{T}).

As Struct[T]Struct[\mathbf{T}] is *\ast-autonomous, the obvious inclusion T↪Struct[T]\mathbf{T} \hookrightarrow Struct[\mathbf{T}] induces a unique strict *\ast-autonomous functor S:F[T]→Struct[T]S: F[\mathbf{T}] \to Struct[\mathbf{T}], which may be called the graphical semantics functor.

The following theorem for MLL proof nets, proved by Richard Blute in his thesis, is similar in content to the coherence theorem for symmetric closed monoidal categories proved by Kelly-Mac Lane.

For a cedent of formulas Γ=A 1,…,A n\Gamma = A_1, \ldots, A_n, let ⨂Γ\bigotimes \Gamma be the formula A 1⊗…⊗A nA_1 \otimes \ldots \otimes A_n (associated to the left, say, if one is to be persnickety), and let ⅋Γ\parr \Gamma be the formula A 1⅋…⅋A nA_1 \parr \ldots \parr A_n. Each proof structure π:Γ→Δ\pi: \Gamma \to \Delta determines (and is determined by) a unique proof structure |π|:⨂Γ→⅋Δ{|\pi|}: \bigotimes \Gamma \to \parr \Delta with the same underlying KM-graph as π\pi.

Then, more generally we may define a proof net of type Γ→Δ\Gamma \to \Delta to be a proof structure π:Γ→Δ\pi: \Gamma \to \Delta such that |π|{|\pi|} is a proof net according to the definition above.

Alternatively, we may define proof nets by reference to MLL sequent calculus, as follows.

Nets of sequent deductions

To each deduction or derivation tree in MLL sequent calculus, one may give an associated proof net. This is by induction; one considers the last step of a deduction δ\delta whose premises have given derivations δ i:Γ i→Δ i\delta_i: \Gamma_i \to \Delta_i, which have been given assigned proof nets N(δ i)N(\delta_i), and uses this to assign a net to the full deduction δ\delta.

We recall the rules for MLL over a list of variable types T\mathbf{T}, and associated rules for forming nets. As remarked above, for a deduction δ\delta of a given sequent Γ→Δ\Gamma \to \Delta, the net N(δ)N(\delta) is determined up to its KM-links, and so we will give just the rules for computing the KM-graph.

The rules for forming KM-graphs will sound pretty repetitive! But don’t worry; that just means they’re really easy. In summary, all we do for each rule besides the axioms is take the disjoint union of the KM-graphs occurring for the (derivations of the) premises, to get the KM-graph of the conclusion.

1. Axiom

   t⊢tid,\frac{}{\displaystyle t \vdash t}\; id,

   where t∈Tt \in \mathbf{T}. Here the net of the conclusion consists of the KM-graph t −→t +t^- \to t^+.

2. Structural rule

   δ′:Γ,A,B,Δ⊢ΣΓ,B,A,Δ⊢Σexchange\frac{\displaystyle \delta': \Gamma, A, B, \Delta \vdash \Sigma}{\displaystyle \Gamma, B, A, \Delta \vdash \Sigma}\; exchange

   Here there is an identification between the sets of subformula occurrences for the premise and conclusion, and under this identification the proof net for δ\delta is the same as the proof net for δ′\delta'.

3. Unit rules (logical rules for units). There are four of these:

   ⊢11 +\frac{}{\displaystyle \; \vdash \mathbf{1}}\; \mathbf{1}_+

   For 1 +\mathbf{1}_+, the KM-graph of the conclusion is empty.

   ⊥⊢⊥ −\frac{}{\displaystyle \bot \vdash \; }\; \bot_{-}

   For ⊥ −\bot_{-}, the KM-graph of the conclusion is empty.

   δ′:Γ,Δ⊢ΣΓ,1,Δ⊢Σ1 −\frac{\displaystyle \delta': \Gamma, \Delta \vdash \Sigma}{\displaystyle \Gamma, \mathbf{1}, \Delta \vdash \Sigma}\; \mathbf{1}_{-}

   For 1 −\mathbf{1}_{-}, there is an identification between the variable subformula occurrences in the premise and in the conclusion. Under this identification, the KM-graph for δ\delta is the same as for δ′\delta'.

   δ′:Γ⊢Δ,ΣΓ⊢Δ,⊥,Σ⊥ +\frac{\displaystyle \delta': \Gamma \vdash \Delta, \Sigma}{\displaystyle \Gamma \vdash \Delta, \bot, \Sigma}\; \bot_+

   For ⊥ +\bot_+, there is an identification between the variable subformula occurrences in the premise and in the conclusion. Under this identification, the KM-graph for δ\delta is the same as for δ′\delta'.

4. Logical rules for ⊗\otimes and ⊸\multimap. There are four of these.

   δ′:Γ,A,B,Δ⊢ΣΓ,A⊗B,Δ⊢Σ⊗ −\frac{\displaystyle \delta': \Gamma, A, B, \Delta \vdash \Sigma}{\displaystyle \Gamma, A \otimes B, \Delta \vdash \Sigma}\; \otimes_{-}

   For ⊗ −\otimes_{-}, there is an identification between the variable subformula occurrences in the premise and in the conclusion. Under this identification, the KM-graph for δ\delta is the same as for δ′\delta'.

   δ′:Γ,A⊢B,ΔΓ⊢A⊸B,Δ⊸ +\frac{\displaystyle \delta': \Gamma, A \vdash B, \Delta}{\displaystyle \Gamma \vdash A \multimap B, \Delta}\; \multimap_+

   For ⊸ +\multimap_+, there is an identification between the variable subformula occurrences in the premise and in the conclusion. Under this identification, the KM-graph for δ\delta is the same as for δ′\delta'.

   δ 1:Γ⊢Δ,Aδ 2:Σ⊢B,ΩΓ,Σ⊢Δ,A⊗B,Ω⊗ +\frac{\displaystyle \delta_1: \Gamma \vdash \Delta, A \qquad \delta_2: \Sigma \vdash B, \Omega}{\Gamma, \Sigma \vdash \Delta, A \otimes B, \Omega}\; \otimes_+

   In the case ⊗ +\otimes_+, the set of variable subformula occurrences in the conclusion is identified with the disjoint union of those for the premises, and under this identification the KM-graph of δ\delta is the disjoint union of the KM-graphs for δ 1\delta_1 and δ 2\delta_2.

   δ 1:Σ,B⊢Ωδ 2:Γ⊢A,ΔΣ,A⊸B,Γ⊢Ω,Δ⊸ −\frac{\displaystyle \delta_1: \Sigma, B \vdash \Omega \qquad \delta_2: \Gamma \vdash A, \Delta \qquad }{\Sigma, A \multimap B, \Gamma \vdash \Omega, \Delta}\; \multimap_{-}

   In the case ⊸ −\multimap_{-}, the set of variable subformula occurrences in the conclusion is identified with the disjoint union of those for the premises, and under this ientification the KM-graph of δ\delta is the disjoint union of the KM-graphs for δ 1\delta_1 and δ 2\delta_2.

Graphical criterion for validity

In his original Linear Logic paper, Girard gave an interesting purely graphical criterion for a proof structure to be a proof net (i.e., “valid”), based on his so-called “cyclic trips” and “longtrip criterion”. Later this criterion was simplified and improved by Danos and Regnier, who at the same time showed that validity of a proof structure could be decided in polynomial time. We give this criterion below. (N.B. this criterion as given by them works for proof structures of type A→BA \to B where there are no subformula occurrences of 1\mathbf{1} and ⊥\bot. It may be extended to work for all formulas if we use a more refined notion of proof structure, called a unit-extended proof structure, as described below.)

The Danos-Regnier criterion, stated according to the definition above, might appear exponential in complexity since it appears to involve checking that every one of the 2 p2^p networks, where pp is the number of par switches, is connected and acyclic. However, Danos and Regnier gave a beautiful simplification which in fact gives an algorithm for deciding validity of a proof structure in polynomial time. (More recently, the problem has actually been shown to be complete for non-deterministic log space JdNM08.)

Unit-extended proof nets

In his thesis, Trimble introduced a refinement of proof structures, designed to take the units 1\mathbf{1} and ⊥\bot, particularly their actions and co-actions on other objects, more explicitly into account.

Unit-extended proof structures are considered as graphs, by adjoining to π\pi an edge 1 −→S\mathbf{1}^- \to S for each subformula occurrence 1 −\mathbf{1}^- that maps to SS under the first function, and another edge T→⊥ +T \to \bot^+ for each subformula occurrence ⊥ +\bot^+ that maps to TT under the second function. This means for instance that for the sequent 1⊢⊥\mathbf{1} \vdash \bot, there is just one unit-extended proof structure of type 1→⊥\mathbf{1} \to \bot, and it consists of a pair of edges from 1 −\mathbf{1}^- to ⊥ +\bot^+.

To each MLL sequent deduction, one can associate a unit-extended proof structure, or rather a set of proof structures.

• For the axioms t⊢tt \vdash t, the associated unit-extended proof structure is of course the KM-graph t −→t +t^- \to t^+.

• For each of the rules exchangeexchange, 1 +\mathbf{1}_+, ⊥ −\bot_{-}, ⊗ −\otimes_{-}, ⊗ +\otimes_+, ⊸ −\multimap_{-}, ⊸ +\multimap_+, if unit-extended proof structures γ i\gamma_i (i.e., sets of unit edges and KM-links) have been associated to derivations of the premises, then associated to the final deduction (obtained by applying that rule) is the proof structure obtained by taking the disjoint union of the γ i\gamma_i.

• This leaves the two unit rules 1 −\mathbf{1}_{-}, ⊥ +\bot_+. For the rule

  δ′:Γ,Δ⊢ΣΓ,1,Δ⊢Σ1 −,\frac{\displaystyle \delta': \Gamma, \Delta \vdash \Sigma}{\displaystyle \Gamma, \mathbf{1}, \Delta \vdash \Sigma}\; \mathbf{1}_{-},

  if γ′\gamma' is a unit-extended proof structure for δ′\delta', then associated to the final deduction δ\delta is any unit-extended proof structure obtained by adjoining to γ′\gamma' a unit edge from the occurrence of 1 −\mathbf{1}^- introduced in the conclusion, to any subformula node occurring in γ′:Γ,Δ→Σ\gamma': \Gamma, \Delta \to \Sigma. Similarly, for the rule

  δ′:Γ⊢Δ,ΣΓ⊢Δ,⊥,Σ⊥ +,\frac{\displaystyle \delta': \Gamma \vdash \Delta, \Sigma}{\displaystyle \Gamma \vdash \Delta, \bot, \Sigma}\; \bot_+,

  if γ′\gamma' is a unit-extended proof structure for δ′\delta', then associated to the final deduction δ\delta is any unit-extended proof structure obtained by adjoining to γ′\gamma' a unit edge going to the occurrence of ⊥ +\bot_+ introduced in the conclusion, from any subformula node occurring in γ′:Γ,Δ→Σ\gamma': \Gamma, \Delta \to \Sigma.

The notion of network for unit-extended proof structures is the same as for ordinary proof structures: a network is obtained by removing just one edge from each par-switch. The Danos-Regnier criterion for validity goes through without modification:

The simplified algorithm for deciding validity, in terms of a series of graph reductions, also goes through for unit-extended proof structures without any modification.

Comparison to string diagrams

There are various possibilities for translating the language of proof nets into a language of string diagrams. Some of these possibilities are subject to a debate on how liberally one would like to understand “string diagrams”, but the idea that both proof nets and string diagrams open possibilities for rapid-fire graphical calculations in similar-looking ways should be taken seriously.

(I’ll come back to this. I want to think some more on how I want to say it.)

References

Proofnets originated with Girard’s seminal paper introducing linear logic:

• Jean-Yves Girard , Linear Logic , Theor. Comp. Sci. 50 (1987) pp. 1-102. (draft)

• Todd Trimble, Linear Logic, Bimodules, and Full Coherence for Autonomous Categories, Rutgers 1994

• Richard Blute, J.R.B. Cockett, R. A. G. Seely, Todd Trimble, Natural deduction and coherence for weakly distributive categories, JPAA 113 (1996), 229-296. (web)

• Paulin Jacobé de Naurois and Virgile Mogbil, Correctness of Linear Logic Proof Structures is NL-Complete (pdf)

• François Lamarche, Proof nets for intuitionistic linear logic: Essential nets (pdf)

• Paul-André Melliès, A topological correctness criterion for non-commutative logic , London Mathematical Society Lecture Notes Series 316, 2004. (pdf)

• Paul-André Melliès, Functorial boxes in string diagrams, Proceedings of Computer Science Logic 2006 in Szeged, Hungary. 2006 (pdf)

• Paul-André Melliès, Categorical semantics of linear logic (pdf)

• François Métayer, Homology of proofnets ,Arch. Math. Logic 33 (1994) pp.169-188. (draft)

• Dominic J. D. Hughes, Unification nets: canonical proof net quantifiers arxiv

Relation to Feynman diagrams is discussed in

• Richard Blute, Prakash Panangaden, Proof nets as formal Feynman diagrams (pdf)