nLab proof net

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products

Semisimplicity

Morphisms

Internal monoids

Examples

Theorems

In higher category theory

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 ¬AA\neg A \coloneqq A \multimap \bot, and the multiplicative disjunction by AB¬ABA \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 STS \otimes T have the same sign as STS \otimes T.

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

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

Definition

A (cut-free) proof structure of type ΓΔ\Gamma \to \Delta (in the language of MLL) is a directed graph whose vertices are subformulas of the formulas of Γ,Δ\Gamma, \Delta, and whose edges are either

  • “KM-links” (Kelly-Mac Lane links) which are of the form t t +t^- \to t^+ between two subformula occurrences of the same variable tTt \in \mathbf{T} but with opposite sign (always oriented from a negative occurrence to a positive occurrence);

  • Edges in binary construction trees of the formulas A i,B jA_i, B_j, oriented according to the following rules:

(ST) S + T + (ST) S T + S T (ST) + S + T (ST) +\array{ & & (S \otimes T)^- & & \qquad S^+ & & & & T^+ & & & & (S \multimap T)^- & & \qquad S^- & & & & T^+ \\ & \swarrow & & \searrow & \qquad & \searrow & & \swarrow & & & & \nearrow & & \searrow & \qquad & \nwarrow & & \swarrow & \\ S^- & & & & T^- \qquad & & (S \otimes T)^+ & & & S^+ & & & & & T^- \qquad & & (S \multimap T)^+ }

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 ABA \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 TStruct[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.

Definition

A proof net (in the language of MLL) of type ABA \to B is a proof structure π\pi of the form S(f)S(f), the graphical semantics of some arrow f:ABf: A \to B in F[T]F[\mathbf{T}].

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.

Theorem

The restriction of S:F[T]Struct[T]S: F[\mathbf{T}] \to Struct[\mathbf{T}] to the full subcategory consisting of objects isomorphic to formulas with no subformula occurrences of 1\mathbf{1} or \bot is faithful.

For a cedent of formulas Γ=A 1,,A n\Gamma = A_1, \ldots, A_n, let Γ\bigotimes \Gamma be the formula A 1A 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 1A 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.

Remark

By the Hauptsatz, i.e., cut-elimination theorem, we omit consideration of the cut rule. It is however interesting to consider the meaning of the cut-elimination algorithm in terms of proof nets; someone who is sufficiently savvy with graphics may wish to include material here.

  1. Axiom

    ttid,\frac{}{\displaystyle t \vdash t}\; id,

    where tTt \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,ΔΣΓ,AB,ΔΣ \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'.

    δ:Γ,AB,ΔΓAB,Δ +\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,ΩΓ,ΣΔ,AB,Ω +\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,ΔΣ,AB,ΓΩ,Δ \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 ABA \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.)

Definition

A par switch (a \parr-switch) in a proof structure is a subgraph of one of the two forms

(ST) S T + S T (ST) + \array{ & & (S \otimes T)^- & & & & S^- & & & & T^+ \\ & \swarrow & & \searrow & & & & \nwarrow & & \swarrow \\ S^- & & & & T^- & & & & (S \multimap T)^+ & & }

where (ST) (S \otimes T)^- or (ST) +(S \multimap T)^+ is a subformula node of the proof structure. (A \otimes switch in a proof structure is similarly a subgraph consisting of a subformula node (ST) +(S \otimes T)^+ or (ST) (S \multimap T)^- and its two children in the binary construction tree, and the edges connecting them.)

A network of a proof structure π\pi is obtained by removing exactly one of the two edges from each par switch of π\pi.

Theorem

(Girard, Danos-Regnier) A proof structure π\pi is a proof net if every network of π\pi is a connected acyclic graph (considered as an unoriented graph, forgetting edge orientations).

Remark

The proof is quite technical, but it is of fundamental importance in the analysis of proof nets. The method is to “sequentialize” a proof structure that satisfies this graphical criterion (i.e., provide a sequent deduction for it). This is by an inductive procedure which first removes consideration of outer par switches (replacing a proof structure of type Γ,AB,ΔΣ\Gamma, A \otimes B, \Delta \to \Sigma by an ‘equivalent’ structure of type Γ,A,B,ΔΣ\Gamma, A, B, \Delta \to \Sigma, and similarly a proof structure of type ΓAB,Δ\Gamma \to A \multimap B, \Delta by an equivalent one of type Γ,AB,Δ\Gamma, A \to B, \Delta). Once these have been removed, the hard part is to show there exists an outer \otimes switch with parent (AB) +(A \otimes B)^+ or (AB) (A \multimap B)^-, such that removal of the parent and edges to its children splits the graph cleanly into two connected components, each of which then satisfies the graphical criterion. The proof of existence is by a tricky combinatorial analysis on graphs. Once this is done, each of the two graph components is sequentializable by the inductive hypothesis, and the induction can then be pushed through.

Remark

François Métayer (1994) showed that the Danos-Regnier criterion on a proof structure’s ‘convergence to a proofnet’ can equivalently be expressed as a criterion on the homology of a suitable associated graph.

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.)

Description

Informally, what one does is draw an arc between the two edges of each par switch (in the manner of secondary school geometry, when one wishes to indicate an angle between two lines), and then applies a series of graph reductions:

  • At each step in the series, any un-arced edge between two distinct nodes may be contracted to a single node;

  • At each step of the series, any configuration consisting of two distinct nodes and a pair of arced edges between them may be contracted to a point,

  • A graph consisting of a single node and no edges reduces to itself.

Proposition

(Danos-Regnier) A proof structure is a proof net if and only if any series of graph reductions eventually reduces it to a graph with a single node and no edges.

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.

Definition

A unit-extended proof structure of type ΓΔ\Gamma \to \Delta is a proof structure π:ΓΔ\pi: \Gamma \to \Delta together with a function from the set of subformula occurrences of 1 \mathbf{1}^- to the set of subformulas, and a function from the set of subformula occurrences of +\bot^+ to the set of subformulas.

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 ttt \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.

Definition

A unit-extended proof net is a unit-extended proof structure that is associated with some MLL sequent deduction.

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:

Theorem

A unit-extended proof structure is a unit-extended proof net if and only if each of its networks is an acyclic connected graph (ignoring edge orientations).

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

Last revised on March 16, 2021 at 08:25:23. See the history of this page for a list of all contributions to it.