\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{proof net} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory} [[!include type theory - contents]] \hypertarget{monoidal_categories}{}\paragraph*{{Monoidal categories}}\label{monoidal_categories} [[!include monoidal categories - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{proof_structures}{Proof structures}\dotfill \pageref*{proof_structures} \linebreak \noindent\hyperlink{proof_nets}{Proof nets}\dotfill \pageref*{proof_nets} \linebreak \noindent\hyperlink{NetDeductions}{Nets of sequent deductions}\dotfill \pageref*{NetDeductions} \linebreak \noindent\hyperlink{graphical_criterion_for_validity}{Graphical criterion for validity}\dotfill \pageref*{graphical_criterion_for_validity} \linebreak \noindent\hyperlink{unitextended_proof_nets}{Unit-extended proof nets}\dotfill \pageref*{unitextended_proof_nets} \linebreak \noindent\hyperlink{comparison_to_string_diagrams}{Comparison to string diagrams}\dotfill \pageref*{comparison_to_string_diagrams} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} \emph{Proof nets} are a graphical way to denote [[proofs]] in [[linear logic]]. They were introduced by [[Jean-Yves Girard|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 \hyperlink{Mellies06}{Melli\`e{}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]] (\hyperlink{BlutePanangaden}{Blute-Panangaden}). \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} We begin by describing proof nets for multiplicative linear logic (MLL), which is interpretable in $\ast$-[[star-autonomous category|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 monoidal category|symmetric]] [[closed monoidal categories]]. \hypertarget{proof_structures}{}\subsubsection*{{Proof structures}}\label{proof_structures} Before describing proof nets, we start with Girard's notion of \emph{proof structure}. It is simplest to describe the [[cut rule|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. [[formula|Formulas]] in MLL may be built from an alphabet $\mathbf{T}$ of propositional variables and two constants $\mathbf{1}$, $\bot$ by applying operations $\otimes$ and $\multimap$. (Negation may be defined by $\neg A \coloneqq A \multimap \bot$, and the multiplicative disjunction by $A \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]] $\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 \emph{negative} and the formulas of $\Delta$ are called \emph{positive}. Subformulas of these formulas acquire signs according to the following rules: \begin{itemize}% \item The subformulas $S, T$ of $S \otimes T$ have the same sign as $S \otimes T$. \item The subformula $T$ of $S \multimap T$ has the same sign as $S \multimap T$, while $S$ has the opposite sign. \end{itemize} We indicate the sign of a subformula using a superscript, e.g., $S^+$. \begin{defn} \label{}\hypertarget{}{} A (cut-free) \emph{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 \begin{itemize}% \item ``KM-links'' (Kelly-Mac Lane links) which are of the form $t^- \to t^+$ between two subformula occurrences of the same variable $t \in \mathbf{T}$ but with opposite sign (always oriented from a negative occurrence to a positive occurrence); \item Edges in binary construction trees of the formulas $A_i, B_j$, oriented according to the following rules: \end{itemize} \begin{displaymath} \itexarray{ & & (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)^+ } \end{displaymath} \end{defn} 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 $A$ and proof structures of type $A \to B$ form a category $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. \hypertarget{proof_nets}{}\subsubsection*{{Proof nets}}\label{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[\mathbf{T}]$ be the free $\ast$-autonomous category on $\mathbf{T}$ (as discrete category), viewing $\ast$-autonomous categories and functors that preserve $\ast$-autonomous structure \emph{strictly} as a 1-category that is 1-monadic over $Cat$, the category of small categories and functors. Observe that the objects of $F[\mathbf{T}]$ may be identified with MLL formulas. We view the morphisms of $F[\mathbf{T}]$ as representing morphisms that are definable (starting with the datum $\mathbf{T}$). As $Struct[\mathbf{T}]$ is $\ast$-autonomous, the obvious inclusion $\mathbf{T} \hookrightarrow Struct[\mathbf{T}]$ induces a unique strict $\ast$-autonomous functor $S: F[\mathbf{T}] \to Struct[\mathbf{T}]$, which may be called the \emph{graphical semantics} functor. \begin{defn} \label{}\hypertarget{}{} A \textbf{proof net} (in the language of MLL) of type $A \to B$ is a proof structure $\pi$ of the form $S(f)$, the graphical semantics of some arrow $f: A \to B$ in $F[\mathbf{T}]$. \end{defn} The following theorem for MLL proof nets, proved by Richard Blute in his thesis, is similar in content to the [[coherence theorem]] for [[symmetric monoidal category|symmetric]] [[closed monoidal categories]] proved by Kelly-Mac Lane. \begin{theorem} \label{}\hypertarget{}{} The restriction of $S: F[\mathbf{T}] \to Struct[\mathbf{T}]$ to the full subcategory consisting of objects isomorphic to formulas with no subformula occurrences of $\mathbf{1}$ or $\bot$ is faithful. \end{theorem} For a cedent of formulas $\Gamma = A_1, \ldots, A_n$, let $\bigotimes \Gamma$ be the formula $A_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 \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. \hypertarget{NetDeductions}{}\subsubsection*{{Nets of sequent deductions}}\label{NetDeductions} 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 $\delta_i: \Gamma_i \to \Delta_i$, which have been given assigned proof nets $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 $\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(\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. \begin{remark} \label{}\hypertarget{}{} By the \emph{[[cut rule|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. \end{remark} \begin{enumerate}% \item Axiom \begin{displaymath} \frac{}{\displaystyle t \vdash t}\; id, \end{displaymath} where $t \in \mathbf{T}$. Here the net of the conclusion consists of the KM-graph $t^- \to t^+$. \item Structural rule \begin{displaymath} \frac{\displaystyle \delta': \Gamma, A, B, \Delta \vdash \Sigma}{\displaystyle \Gamma, B, A, \Delta \vdash \Sigma}\; exchange \end{displaymath} 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'$. \item Unit rules (logical rules for units). There are four of these: \begin{displaymath} \frac{}{\displaystyle \; \vdash \mathbf{1}}\; \mathbf{1}_+ \end{displaymath} For $\mathbf{1}_+$, the KM-graph of the conclusion is empty. \begin{displaymath} \frac{}{\displaystyle \bot \vdash \; }\; \bot_{-} \end{displaymath} For $\bot_{-}$, the KM-graph of the conclusion is empty. \begin{displaymath} \frac{\displaystyle \delta': \Gamma, \Delta \vdash \Sigma}{\displaystyle \Gamma, \mathbf{1}, \Delta \vdash \Sigma}\; \mathbf{1}_{-} \end{displaymath} For $\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'$. \begin{displaymath} \frac{\displaystyle \delta': \Gamma \vdash \Delta, \Sigma}{\displaystyle \Gamma \vdash \Delta, \bot, \Sigma}\; \bot_+ \end{displaymath} 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'$. \item Logical rules for $\otimes$ and $\multimap$. There are four of these. \begin{displaymath} \frac{\displaystyle \delta': \Gamma, A, B, \Delta \vdash \Sigma}{\displaystyle \Gamma, A \otimes B, \Delta \vdash \Sigma}\; \otimes_{-} \end{displaymath} 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'$. \begin{displaymath} \frac{\displaystyle \delta': \Gamma, A \vdash B, \Delta}{\displaystyle \Gamma \vdash A \multimap B, \Delta}\; \multimap_+ \end{displaymath} 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'$. \begin{displaymath} \frac{\displaystyle \delta_1: \Gamma \vdash \Delta, A \qquad \delta_2: \Sigma \vdash B, \Omega}{\Gamma, \Sigma \vdash \Delta, A \otimes B, \Omega}\; \otimes_+ \end{displaymath} 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 $\delta_1$ and $\delta_2$. \begin{displaymath} \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_{-} \end{displaymath} 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 $\delta_1$ and $\delta_2$. \end{enumerate} \hypertarget{graphical_criterion_for_validity}{}\subsection*{{Graphical criterion for validity}}\label{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. (\textbf{N.B.} this criterion as given by them works for proof structures of type $A \to B$ where there are no subformula occurrences of $\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.) \begin{defn} \label{}\hypertarget{}{} A \textbf{par switch} (a $\parr$-switch) in a proof structure is a subgraph of one of the two forms \begin{displaymath} \itexarray{ & & (S \otimes T)^- & & & & S^- & & & & T^+ \\ & \swarrow & & \searrow & & & & \nwarrow & & \swarrow \\ S^- & & & & T^- & & & & (S \multimap T)^+ & & } \end{displaymath} where $(S \otimes T)^-$ or $(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 $(S \otimes T)^+$ or $(S \multimap T)^-$ and its two children in the binary construction tree, and the edges connecting them.) A \textbf{network} of a proof structure $\pi$ is obtained by removing exactly one of the two edges from each par switch of $\pi$. \end{defn} \begin{theorem} \label{}\hypertarget{}{} \textbf{(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). \end{theorem} \begin{remark} \label{}\hypertarget{}{} 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 $\Gamma, A \otimes B, \Delta \to \Sigma$ by an `equivalent' structure of type $\Gamma, A, B, \Delta \to \Sigma$, and similarly a proof structure of type $\Gamma \to A \multimap B, \Delta$ by an equivalent one of type $\Gamma, A \to B, \Delta$). Once these have been removed, the hard part is to show there exists an outer $\otimes$ switch with parent $(A \otimes B)^+$ or $(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. \end{remark} \begin{remark} \label{}\hypertarget{}{} [[François Métayer]] (\hyperlink{Metayer94}{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. \end{remark} 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^p$ networks, where $p$ 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 \hyperlink{JdNM08}{JdNM08}.) \begin{remark} \label{DR}\hypertarget{DR}{} 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: \begin{itemize}% \item At each step in the series, any un-arced edge between two distinct nodes may be contracted to a single node; \item 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, \item A graph consisting of a single node and no edges reduces to itself. \end{itemize} \end{remark} \begin{prop} \label{}\hypertarget{}{} \textbf{(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. \end{prop} \hypertarget{unitextended_proof_nets}{}\subsection*{{Unit-extended proof nets}}\label{unitextended_proof_nets} In his thesis, Trimble introduced a refinement of proof structures, designed to take the units $\mathbf{1}$ and $\bot$, particularly their actions and co-actions on other objects, more explicitly into account. \begin{defn} \label{}\hypertarget{}{} A \textbf{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 $\mathbf{1}^-$ to the set of subformulas, and a function from the set of subformula occurrences of $\bot^+$ to the set of subformulas. \end{defn} Unit-extended proof structures are considered as graphs, by adjoining to $\pi$ an edge $\mathbf{1}^- \to S$ for each subformula occurrence $\mathbf{1}^-$ that maps to $S$ under the first function, and another edge $T \to \bot^+$ for each subformula occurrence $\bot^+$ that maps to $T$ under the second function. This means for instance that for the sequent $\mathbf{1} \vdash \bot$, there is just one unit-extended proof structure of type $\mathbf{1} \to \bot$, and it consists of a \emph{pair} of edges from $\mathbf{1}^-$ to $\bot^+$. To each MLL sequent deduction, one can associate a unit-extended proof structure, or rather a set of proof structures. \begin{itemize}% \item For the axioms $t \vdash t$, the associated unit-extended proof structure is of course the KM-graph $t^- \to t^+$. \item For each of the rules $exchange$, $\mathbf{1}_+$, $\bot_{-}$, $\otimes_{-}$, $\otimes_+$, $\multimap_{-}$, $\multimap_+$, if unit-extended proof structures $\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 $\gamma_i$. \item This leaves the two unit rules $\mathbf{1}_{-}$, $\bot_+$. For the rule \begin{displaymath} \frac{\displaystyle \delta': \Gamma, \Delta \vdash \Sigma}{\displaystyle \Gamma, \mathbf{1}, \Delta \vdash \Sigma}\; \mathbf{1}_{-}, \end{displaymath} 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 $\mathbf{1}^-$ introduced in the conclusion, to any subformula node occurring in $\gamma': \Gamma, \Delta \to \Sigma$. Similarly, for the rule \begin{displaymath} \frac{\displaystyle \delta': \Gamma \vdash \Delta, \Sigma}{\displaystyle \Gamma \vdash \Delta, \bot, \Sigma}\; \bot_+, \end{displaymath} 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$. \end{itemize} \begin{defn} \label{}\hypertarget{}{} A \textbf{unit-extended proof net} is a unit-extended proof structure that is associated with some MLL sequent deduction. \end{defn} 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: \begin{theorem} \label{}\hypertarget{}{} 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). \end{theorem} The simplified algorithm for deciding validity, in terms of a series of \hyperlink{DR}{graph reductions}, also goes through for unit-extended proof structures without any modification. \hypertarget{comparison_to_string_diagrams}{}\subsection*{{Comparison to string diagrams}}\label{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.) \hypertarget{references}{}\subsection*{{References}}\label{references} Proofnets originated with Girard's seminal paper introducing linear logic: \begin{itemize}% \item [[Jean-Yves Girard]] , \emph{Linear Logic} , Theor. Comp. Sci. \textbf{50} (1987) pp. 1-102. (\href{http://iml.univ-mrs.fr/~girard/Synsem.pdf.gz}{draft}) \item [[Todd Trimble]], \emph{Linear Logic, Bimodules, and Full Coherence for Autonomous Categories}, Rutgers 1994 \item [[Richard Blute]], [[J.R.B. Cockett]], [[R. A. G. Seely]], [[Todd Trimble]], \emph{Natural deduction and coherence for weakly distributive categories}, JPAA 113 (1996), 229-296. (\href{http://www.sciencedirect.com/science/article/pii/002240499500159X}{web}) \item Paulin Jacob\'e{} de Naurois and Virgile Mogbil, \emph{Correctness of Linear Logic Proof Structures is NL-Complete} (\href{https://hal.archives-ouvertes.fr/hal-00360894/document}{pdf}) \item Fran\c{c}ois Lamarche, \emph{Proof nets for intuitionistic linear logic: Essential nets} (\href{http://hal.inria.fr/docs/00/34/73/36/PDF/prfnet1.pdf}{pdf}) \item [[Paul-André Melliès]], \emph{A topological correctness criterion for non-commutative logic} , London Mathematical Society Lecture Notes Series 316, 2004. (\href{https://hal.inria.fr/hal-00154204/document}{pdf}) \item [[Paul-André Melliès]], \emph{Functorial boxes in string diagrams}, Proceedings of \emph{Computer Science Logic 2006} in Szeged, Hungary. 2006 (\href{http://www.pps.univ-paris-diderot.fr/~mellies/papers/functorial-boxes.pdf}{pdf}) \item [[Paul-André Melliès]], \emph{Categorical semantics of linear logic} (\href{http://profs.sci.univr.it/~bellin/panorama.pdf}{pdf}) \item [[François Métayer]], \emph{Homology of proofnets} ,Arch. Math. Logic \textbf{33} (1994) pp.169-188. (\href{http://www.pps.univ-paris-diderot.fr/~metayer/PDF/hpn.pdf}{draft}) \item Dominic J. D. Hughes, \emph{Unification nets: canonical proof net quantifiers} \href{https://arxiv.org/abs/1802.03224}{arxiv} \end{itemize} Relation to [[Feynman diagrams]] is discussed in \begin{itemize}% \item [[Richard Blute]], [[Prakash Panangaden]], \emph{Proof nets as formal Feynman diagrams} (\href{http://www.indiana.edu/~iulg/qliqc/phi.pdf}{pdf}) \end{itemize} [[!redirects proof nets]] \end{document}