Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeJan 24th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have split-off _[[Feynman diagram]]_ from _[[perturbation theory]]_, gave it a brief Idea-section and added a pointer to an insightful reference.

   I have split-off Feynman diagram from perturbation theory, gave it a brief Idea-section and added a pointer to an insightful reference.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeFeb 5th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexThere had long been missing the obvious cross-links between _[[Feynman diagram]]_ and _[[string diagram]]_ and now also _[[proof net]]_. I have now added [here](http://ncatlab.org/nlab/show/Feynman+diagram#AsStringDiagrams) the following paragraph: *** It has been observed that Feynman diagrams, notably in [[gauge theory]], are in particular [[string diagrams]] (in the sense of [[category theory]], not here in any sense of [[string theory]]!) in the given [[category of representations]]: the edges are labelled by [[particle]] [[species]], hence by [[Wigner classification]] by [[irreps]], and the vertices are labeled by representation [[homomorphisms]] ("[[intertwiners]]") which, indeed, label the [[interaction]] of particles in the Feynman diagram. A review of this formulation is in * [[John Baez]], [[Aaron Lauda]], _A Prehistory of n-Categorical Physics_, Deep beauty, 13-128, Cambridge Univ. Press, Cambridge, 2011 ([arXiv:0908.2469](http://arxiv.org/abs/0908.2469)) Moreover, one may think of [[string diagrams]] in [[monoidal categories]] as being the [[categorical semantics]] for [[proof nets]] (see there for more) in [[linear logic]]. Under this identification then Feynman diagrams are [[proof nets]]. This is discussed in * [[Richard Blute]], [[Prakash Panangaden]], _Proof nets as formal Feynman diagrams_ ([pdf](http://www.indiana.edu/~iulg/qliqc/phi.pdf))

   There had long been missing the obvious cross-links between Feynman diagram and string diagram and now also proof net.

   I have now added here the following paragraph:

   ---

   It has been observed that Feynman diagrams, notably in gauge theory, are in particular string diagrams (in the sense of category theory, not here in any sense of string theory!) in the given category of representations: the edges are labelled by particle species, hence by Wigner classification by irreps, and the vertices are labeled by representation homomorphisms (“intertwiners”) which, indeed, label the interaction of particles in the Feynman diagram.

   A review of this formulation is in

   • John Baez, Aaron Lauda, A Prehistory of n-Categorical Physics, Deep beauty, 13-128, Cambridge Univ. Press, Cambridge, 2011 (arXiv:0908.2469)

   Moreover, one may think of string diagrams in monoidal categories as being the categorical semantics for proof nets (see there for more) in linear logic. Under this identification then Feynman diagrams are proof nets. This is discussed in

   • Richard Blute, Prakash Panangaden, Proof nets as formal Feynman diagrams (pdf)
3. • CommentRowNumber3.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 5th 2014
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexTo say "string diagrams in monoidal categories are the categorical semantics for proof nets" actually sounds pretty confused to me. Maybe let's slow down a bit on proof nets. There are of course connections between string diagrams and proof nets and the graphical calculus of extranatural transformations (also sometimes called KM graphs, where KM stands for Kelly and Mac Lane, who used them in their paper on coherence in closed categories) introduced by Eilenberg and Kelly in the mid 60's. One may say that cut-free proof nets -- here I refer to proof nets for MLL -- are essentially the same as KM graphs associated with cut-free sequent deductions for MLL, except that normally when one draws KM graphs, one just draws those edges which indicate instances of naturality and dinaturality in diagrams (e.g., for the evaluation $ev_{x, y}: (x \multimap y) \otimes x \to y$, an edge connecting the two occurrences of $y$ to indicate naturality in that variable, and an edge between the two instances of $x$ to indicate dinaturality in that variable). In addition to these, proof nets also include the graphical binary tree structure of the formulas above (e.g., the tree for $(x \multimap y) \otimes x$ has a root labeled by that formula, with edges connecting it to its two subformula children $x \multimap y$ and $x$, and $x \multimap y$ has the two children $x$ and $y$). Of course this tree structure may be read off from the structure of the formula, and so this graphical information is usually left implicit in the KM graphs. [As an exercise, let $\delta_y: y \to (y \multimap x) \multimap x$ be the evident "double-dual embedding" definable in the language of symmetric monoidal closed categories. Part (a): draw the KM-graphs and proof nets of $\delta_{x \multimap x}$ and of $\delta_x \multimap x$. Part (b): what would it mean to compose the KM-graphs and proof nets?] One can picture KM-graphs as 1-dimensional cobordisms between signed sets, and they are composed just like cobordisms. To compose proof nets (say of type $A \vdash B$ and $B \vdash C$), one can do one of two things: (1) forget those binary trees for the formulas $A, B, C$, just compose the KM graphs, and then append the binary trees for $A$ and $C$ at the end, or (2) glue the outgoing edge of the net for $A \vdash B$ (an edge labeled $B$) to the incoming edge of $B \vdash C$, and then perform a series of graphical "cut-eliminations" (which are reminiscent of operations on Feynman diagrams: each step has the appearance of replacing two pairs of pants sewn at the waists by two cylinders). Going through all the bother of (2) may seem like a lot of hoo-haw since in the end we get the same result as (1), but to understand what proof nets really mean, it helps to consider (2) instead, particularly in connection with classical cut-elimination in sequent calculus, which proof nets are meant to improve upon. You could _very roughly_ say that KM graphs are special cases of string diagrams, insofar as KM graphs usually come up in connection with families of extranatural transformations like $ev_{x, y}$ above that in turn arise from the types of cup and cap diagrams one can built from counits and units of adjoint pairs such as $- \otimes x \dashv x \multimap -$. And to the extent that (MLL or MILL) proof nets are elaborations of KM graphs, you could likewise describe proof nets, _very roughly_, as special types of of string diagrams. But KM graphs as string diagrams don't really involve "particle interactions" one associates with general string diagrams (where the "interactions" are formally described by what Joyal and Street call tensor schemes, or by computads if one interprets string diagrams as something one can evaluate in more general 2-categories). In other words, KM graphs are more like diagrams of free (non-interacting) particles which can move forward and backward in time. Now what Melliès does, in his "proof nets as string diagrams with boxes", is different still. He is explicitly not just dealing with the classical MLL proof nets (which are "identified with" string diagrams in monoidal categories or 2-categories only after all the caveats listed above), but rather with proof nets for full LL, where the boxes themselves indicate applications of the exponential $!$. I might add, in connection with connectives and modalities and such in another thread, that the idea of representing unary connectives like negation by using boxes, or modalities like necessity using slightly different kinds of boxes, goes back to C.S. Peirce and keeps being rediscovered in one form or another. On a general level, such boxes can also be used wherever one is dealing with a tensorial strength: an arrow $T x \otimes y \to T(x \otimes y)$ can be pictured as moving a node labeled $y$ into a "$T$-box" which already contains a node labeled $x$. There are lots of unexplored applications of this idea.

   To say “string diagrams in monoidal categories are the categorical semantics for proof nets” actually sounds pretty confused to me. Maybe let’s slow down a bit on proof nets.

   There are of course connections between string diagrams and proof nets and the graphical calculus of extranatural transformations (also sometimes called KM graphs, where KM stands for Kelly and Mac Lane, who used them in their paper on coherence in closed categories) introduced by Eilenberg and Kelly in the mid 60’s. One may say that cut-free proof nets – here I refer to proof nets for MLL – are essentially the same as KM graphs associated with cut-free sequent deductions for MLL, except that normally when one draws KM graphs, one just draws those edges which indicate instances of naturality and dinaturality in diagrams (e.g., for the evaluation $ev_{x, y}: (x \multimap y) \otimes x \to y$, an edge connecting the two occurrences of $y$ to indicate naturality in that variable, and an edge between the two instances of $x$ to indicate dinaturality in that variable). In addition to these, proof nets also include the graphical binary tree structure of the formulas above (e.g., the tree for $(x \multimap y) \otimes x$ has a root labeled by that formula, with edges connecting it to its two subformula children $x \multimap y$ and $x$, and $x \multimap y$ has the two children $x$ and $y$). Of course this tree structure may be read off from the structure of the formula, and so this graphical information is usually left implicit in the KM graphs.

   [As an exercise, let $\delta_y: y \to (y \multimap x) \multimap x$ be the evident “double-dual embedding” definable in the language of symmetric monoidal closed categories. Part (a): draw the KM-graphs and proof nets of $\delta_{x \multimap x}$ and of $\delta_x \multimap x$. Part (b): what would it mean to compose the KM-graphs and proof nets?]

   One can picture KM-graphs as 1-dimensional cobordisms between signed sets, and they are composed just like cobordisms. To compose proof nets (say of type $A \vdash B$ and $B \vdash C$), one can do one of two things: (1) forget those binary trees for the formulas $A, B, C$, just compose the KM graphs, and then append the binary trees for $A$ and $C$ at the end, or (2) glue the outgoing edge of the net for $A \vdash B$ (an edge labeled $B$) to the incoming edge of $B \vdash C$, and then perform a series of graphical “cut-eliminations” (which are reminiscent of operations on Feynman diagrams: each step has the appearance of replacing two pairs of pants sewn at the waists by two cylinders). Going through all the bother of (2) may seem like a lot of hoo-haw since in the end we get the same result as (1), but to understand what proof nets really mean, it helps to consider (2) instead, particularly in connection with classical cut-elimination in sequent calculus, which proof nets are meant to improve upon.

   You could very roughly say that KM graphs are special cases of string diagrams, insofar as KM graphs usually come up in connection with families of extranatural transformations like $ev_{x, y}$ above that in turn arise from the types of cup and cap diagrams one can built from counits and units of adjoint pairs such as $- \otimes x \dashv x \multimap -$. And to the extent that (MLL or MILL) proof nets are elaborations of KM graphs, you could likewise describe proof nets, very roughly, as special types of of string diagrams. But KM graphs as string diagrams don’t really involve “particle interactions” one associates with general string diagrams (where the “interactions” are formally described by what Joyal and Street call tensor schemes, or by computads if one interprets string diagrams as something one can evaluate in more general 2-categories). In other words, KM graphs are more like diagrams of free (non-interacting) particles which can move forward and backward in time.

   Now what Melliès does, in his “proof nets as string diagrams with boxes”, is different still. He is explicitly not just dealing with the classical MLL proof nets (which are “identified with” string diagrams in monoidal categories or 2-categories only after all the caveats listed above), but rather with proof nets for full LL, where the boxes themselves indicate applications of the exponential $!$. I might add, in connection with connectives and modalities and such in another thread, that the idea of representing unary connectives like negation by using boxes, or modalities like necessity using slightly different kinds of boxes, goes back to C.S. Peirce and keeps being rediscovered in one form or another. On a general level, such boxes can also be used wherever one is dealing with a tensorial strength: an arrow $T x \otimes y \to T(x \otimes y)$ can be pictured as moving a node labeled $y$ into a “$T$-box” which already contains a node labeled $x$. There are lots of unexplored applications of this idea.

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 5th 2014
   • (edited Feb 5th 2014)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexBy the way, let's not copy and paste my last comment into the nLab. I'd prefer to work on the relevant articles myself, when I get a moment. But I do want to slow down the entries on proof nets.

   By the way, let’s not copy and paste my last comment into the nLab. I’d prefer to work on the relevant articles myself, when I get a moment. But I do want to slow down the entries on proof nets.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeFeb 5th 2014
   • (edited Feb 5th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHey, Todd. Don't worry, I won't copy your message to any nLab entry. (Even if I did, it would be little harm as one could simply remove it again.) Speaking of slowing down: last time that I did use one of your comments in an nLab entry you were so quick with complaining -- watching the logs I suppose -- that I didn't have a chance to even announce it and say "Look, Todd, I used your message like this, let me know if you agree, otherwise I can undo it." But in that case and now here again, I am delighted to see that I managed to trigger your expertise. You clearly have a whole lot to say about linear logic, much more than I was aware before that you did, and maybe even much more than one can actually (or at least easily) find in the literature. Therefore, while I will certainly stay clear of daring to interfere again, I will sincerely applaud and enjoy seeing you add more of this stuff, eventually, to the nLab. Speaking of expertise, reading your comment above makes me feel as if I wrote a detailed discussion of proof nets and got it all wrong. I wish I did. But actually I just equipped a hyperlink to a citation with a super-brief comment. I do like adding quick comments to citations on what they are about, because I find that makes lists of citations considerably more useful. In this case, might it have helped had I thrown in the adjective "multiplicative" in the brief comment? Melliès on [p. 5](http://www.pps.univ-paris-diderot.fr/~mellies/papers/functorial-boxes.pdf) of his nice text says > multiplicative proof-nets are instances of string diagrams... and looking through the text again it indeed seems to me that it's all about string diagrams. True, he focuses on adding those boxes to denote the action of functors in general and of the exponential modality in particular, but it's still what is called string diagrams, or else I am really missing something. In your comment you focus on the extra structure one has in string diagrams when in addition to monoidal structure there is star-autonomous or similar extra structure around. At least our nLab page _[[string diagram]]_ does count all that still as string diagrams, too! In conclusion, while I am not actually sure what you mean that my confusion is, I am glad to see that whatever it was it triggered you into writing something about proof nets! That would be nice if you would eventually put some paragraphs along these lines into the $n$Lab entry.

   Hey, Todd.

   Don’t worry, I won’t copy your message to any nLab entry. (Even if I did, it would be little harm as one could simply remove it again.) Speaking of slowing down: last time that I did use one of your comments in an nLab entry you were so quick with complaining – watching the logs I suppose – that I didn’t have a chance to even announce it and say “Look, Todd, I used your message like this, let me know if you agree, otherwise I can undo it.”

   But in that case and now here again, I am delighted to see that I managed to trigger your expertise. You clearly have a whole lot to say about linear logic, much more than I was aware before that you did, and maybe even much more than one can actually (or at least easily) find in the literature. Therefore, while I will certainly stay clear of daring to interfere again, I will sincerely applaud and enjoy seeing you add more of this stuff, eventually, to the nLab.

   Speaking of expertise, reading your comment above makes me feel as if I wrote a detailed discussion of proof nets and got it all wrong. I wish I did. But actually I just equipped a hyperlink to a citation with a super-brief comment. I do like adding quick comments to citations on what they are about, because I find that makes lists of citations considerably more useful.

   In this case, might it have helped had I thrown in the adjective “multiplicative” in the brief comment? Melliès on p. 5 of his nice text says

   multiplicative proof-nets are instances of string diagrams…

   and looking through the text again it indeed seems to me that it’s all about string diagrams. True, he focuses on adding those boxes to denote the action of functors in general and of the exponential modality in particular, but it’s still what is called string diagrams, or else I am really missing something.

   In your comment you focus on the extra structure one has in string diagrams when in addition to monoidal structure there is star-autonomous or similar extra structure around. At least our nLab page string diagram does count all that still as string diagrams, too!

   In conclusion, while I am not actually sure what you mean that my confusion is, I am glad to see that whatever it was it triggered you into writing something about proof nets! That would be nice if you would eventually put some paragraphs along these lines into the $n$Lab entry.

6. • CommentRowNumber6.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 5th 2014
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexSorry, I didn't mean to come off sounding as strongly (or offensively!) as it probably did. And I didn't really mean _you_ were confused -- only that what I saw _sounded_ confused (and maybe was just jotted down quickly, or whatever). I think what "triggered" me is that the phrase that I put in quotes, and perhaps that innocent little verb 'are' particularly, just came off sounding like such a bald assertion that felt badly in need of qualification. Yes, Melliè said "instances", and I wanted to make clearer what he must have meant. Anyway, sorry to have come off as such a meanie. :-(

   Sorry, I didn’t mean to come off sounding as strongly (or offensively!) as it probably did. And I didn’t really mean you were confused – only that what I saw sounded confused (and maybe was just jotted down quickly, or whatever). I think what “triggered” me is that the phrase that I put in quotes, and perhaps that innocent little verb ’are’ particularly, just came off sounding like such a bald assertion that felt badly in need of qualification.

   Yes, Melliè said “instances”, and I wanted to make clearer what he must have meant.

   Anyway, sorry to have come off as such a meanie. :-(

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeFeb 5th 2014
   • (edited Feb 5th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexNo problem, Todd. Let's just sort it out: So at _[[Feynman diagram]]_ I have changed the sentence > Moreover, one may think of [[string diagrams]] in [[monoidal categories]] as being the [[categorical semantics]] for [[proof nets]] (see there for more) in [[linear logic]]. to >Moreover, one may think of [[string diagrams]] in [[monoidal categories]] as providing [[categorical semantics]] for [[proof nets]] (see there for more) in multiplicative [[linear logic]]. Maybe that's better? Otherwise, please modify it. On the other hand, putting my physicists hat on and looking at [Blute & Panangaden](http://www.indiana.edu/~iulg/qliqc/phi.pdf), actually they do something much more ambitious and physically interesting than the basic statement "A Feynman diagram in gauge theory is a string diagram in a representation category". Instead, they actually look at Lagrangians and really derive their Feynman rules, it seems. That's rather more substantial. So it seems we easily agree that much more should be said here, eventually.

   No problem, Todd. Let’s just sort it out:

   So at Feynman diagram I have changed the sentence

   Moreover, one may think of string diagrams in monoidal categories as being the categorical semantics for proof nets (see there for more) in linear logic.

   to

   Moreover, one may think of string diagrams in monoidal categories as providing categorical semantics for proof nets (see there for more) in multiplicative linear logic.

   Maybe that’s better? Otherwise, please modify it.

   On the other hand, putting my physicists hat on and looking at Blute & Panangaden, actually they do something much more ambitious and physically interesting than the basic statement “A Feynman diagram in gauge theory is a string diagram in a representation category”. Instead, they actually look at Lagrangians and really derive their Feynman rules, it seems. That’s rather more substantial.

   So it seems we easily agree that much more should be said here, eventually.

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 6th 2014
   • (edited Feb 6th 2014)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexIt's still not how I'd put it, but let me try to put matters in a way that might bring us closer (see below). Proof nets are a "graphical semantics" of (certain fragments of) linear logic, in other words are a graphical way of interpreting deductions in linear sequent calculus (or terms in linear type theory, or what have you). They are not something one has to interpret a second time (i.e., provide a semantics for) in terms of another layer of graphical calculus (string diagrams). They already are a graphical calculus. So I myself would express the Idea slightly differently. Maybe like this: > Proof nets, in the original conception due to J.-Y. Girard, provide a graphical representation for deductions in [[linear logic]], particularly multiplicative linear logic or MLL. They are akin to (in fact, an elaborated form of) the extranaturality graphs developed by Eilenberg, Kelly, and Mac Lane for tracking compositions of [[extranatural transformations]] and for stating [[coherence theorems]]. As such, they can be viewed as a baseline for variants of [[string diagrams]], especially those variants that deal particularly with (symmetric) [[closed monoidal categories]] and [[star-autonomous categories]]. > "Baseline" here means that proof nets, at least in the form given by Girard, are graphical structures used particularly to visualize symmetric monoidal closed categories that are freely generated from [[computads]] or tensor schemes of the simplest kind: [[directed graphs]], usually just discrete directed graphs. This baseline concept of proof nets can be widened and developed further to take into account the structure of smc categories freely generated from more complicated tensor schemes (so that the calculus of proof nets, thus generalized, would be very closely akin to those variants of string diagram calculus that would apply particularly to smc or $\ast$-autonomous categories, although with a somewhat more proof-theoretic emphasis). > A more elaborate notion of proof net may be used to deal with full linear logic, including the exponential modalities used to mediate between the multiplicative and additive connectives. These may be conveniently packaged as (MLL) proof nets with boxes (see Melliès), where the contents of a box are arguments of an exponential that can be moved in and out according to certain rules. Of course, this way of putting it opens up further opportunities for creating grey links with question marks. ;-) I might even copy and paste the above, if it seems satisfactory.

   It’s still not how I’d put it, but let me try to put matters in a way that might bring us closer (see below).

   Proof nets are a “graphical semantics” of (certain fragments of) linear logic, in other words are a graphical way of interpreting deductions in linear sequent calculus (or terms in linear type theory, or what have you). They are not something one has to interpret a second time (i.e., provide a semantics for) in terms of another layer of graphical calculus (string diagrams). They already are a graphical calculus.

   So I myself would express the Idea slightly differently. Maybe like this:

   Proof nets, in the original conception due to J.-Y. Girard, provide a graphical representation for deductions in linear logic, particularly multiplicative linear logic or MLL. They are akin to (in fact, an elaborated form of) the extranaturality graphs developed by Eilenberg, Kelly, and Mac Lane for tracking compositions of extranatural transformations and for stating coherence theorems. As such, they can be viewed as a baseline for variants of string diagrams, especially those variants that deal particularly with (symmetric) closed monoidal categories and star-autonomous categories.

   “Baseline” here means that proof nets, at least in the form given by Girard, are graphical structures used particularly to visualize symmetric monoidal closed categories that are freely generated from computads or tensor schemes of the simplest kind: directed graphs, usually just discrete directed graphs. This baseline concept of proof nets can be widened and developed further to take into account the structure of smc categories freely generated from more complicated tensor schemes (so that the calculus of proof nets, thus generalized, would be very closely akin to those variants of string diagram calculus that would apply particularly to smc or $\ast$-autonomous categories, although with a somewhat more proof-theoretic emphasis).

   A more elaborate notion of proof net may be used to deal with full linear logic, including the exponential modalities used to mediate between the multiplicative and additive connectives. These may be conveniently packaged as (MLL) proof nets with boxes (see Melliès), where the contents of a box are arguments of an exponential that can be moved in and out according to certain rules.

   Of course, this way of putting it opens up further opportunities for creating grey links with question marks. ;-)

   I might even copy and paste the above, if it seems satisfactory.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 6th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexFWIW, #3 is already one of the best explanations of proof nets I've ever heard.

   FWIW, #3 is already one of the best explanations of proof nets I’ve ever heard.

10. • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 6th 2014
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexYeah, now I think that I might understand what they are! I need to go back and look at Girard\'s book again.

    Yeah, now I think that I might understand what they are! I need to go back and look at Girard's book again.

11. • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 6th 2014
    • (edited Feb 6th 2014)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexWell, I'm gratified to hear you say so Mike and Toby, because I didn't think I at all succeeded in saying it properly. :-) FWIW (and having been prompted by Urs), I am currently in the process of writing up a shortened account of my thesis -- which is how I learned most of what I understand of linear logic. While I am currently hammering it out on my non-public web at the nLab, it is meant to be eventually integrated into the nLab proper. Right now the idea is just to write up enough so that the main results are understandable and plausible-sounding, without getting into the nitty-gritty details of all the proofs. (But those might in time be made available on the nLab as well.)

    Well, I’m gratified to hear you say so Mike and Toby, because I didn’t think I at all succeeded in saying it properly. :-)

    FWIW (and having been prompted by Urs), I am currently in the process of writing up a shortened account of my thesis – which is how I learned most of what I understand of linear logic. While I am currently hammering it out on my non-public web at the nLab, it is meant to be eventually integrated into the nLab proper. Right now the idea is just to write up enough so that the main results are understandable and plausible-sounding, without getting into the nitty-gritty details of all the proofs. (But those might in time be made available on the nLab as well.)

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeFeb 6th 2014
    • (edited Feb 6th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> Proof nets are a “graphical semantics” of (certain fragments of) linear logic, in other words are a graphical way of interpreting deductions in linear sequent calculus (or terms in linear type theory, or what have you). They are not something one has to interpret a second time (i.e., provide a semantics for) in terms of another layer of graphical calculus (string diagrams). They already are a graphical calculus. Is "graphical" already "semantics"? How about graphical syntax? Syntax need not be 1-dimensional, does it? I was thinking: proof nets talk about linear logic before and independently of choosing any model, hence any semantics for the linear logic. The moment we choose a such-and-such-monoidal category as the semantics of our linear logic, then every proof net we may have considered before now gives rise to a string diagram in that monoidal category. Isn't that a reasonable perspective?

    Proof nets are a “graphical semantics” of (certain fragments of) linear logic, in other words are a graphical way of interpreting deductions in linear sequent calculus (or terms in linear type theory, or what have you). They are not something one has to interpret a second time (i.e., provide a semantics for) in terms of another layer of graphical calculus (string diagrams). They already are a graphical calculus.

    Is “graphical” already “semantics”? How about graphical syntax? Syntax need not be 1-dimensional, does it?

    I was thinking: proof nets talk about linear logic before and independently of choosing any model, hence any semantics for the linear logic. The moment we choose a such-and-such-monoidal category as the semantics of our linear logic, then every proof net we may have considered before now gives rise to a string diagram in that monoidal category.

    Isn’t that a reasonable perspective?

13. • CommentRowNumber13.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 6th 2014
    • (edited Feb 6th 2014)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexYeah, sure, you could say proof nets are a kind of graphical syntax. And that's a good way to think of them. But if you want to put it that way, I'd say that they are about as syntactic as string diagrams, which is also a graphical syntax. (So again I'm not quite sure why one would write that string diagrams are a "categorical semantics" of proof nets.) Let me give a quick tutorial, if you don't mind, to explain better what I had in mind when I wrote "graphical semantics". Before we (and by "we", you can consider that I actually mean Girard) talk of "proof nets", we talk of "proof structures". (Not a great term, but that's what "we" call them.) A _proof structure_ of type $A \to B$, where $A, B$ are formulas built from a set of propositional variables $T$ and a constant $I$ (for monoidal unit) by applying operations \otimes, \multimap$, is a graph consisting of * a KM-graph which pairs off variables (each pairing being an edge between a negatively signed variable and a positively signed variable, where $A$ is deemed negative and $B$ positive and subformulas acquire signs by declaring that the children $S, T$ of $S \otimes T$ acquire its parity, where $T$ has the same parity and $S$ has parity opposite to $S \multimap T$), and * the construction trees of the formulas $A$, $B$. So in other words a proof structure of this type is a graph whose vertices are subformulas of $A$ and $B$ and whose edges occur either as KM pairings between variable subformulas or as edges in the two construction trees. This is what I was explaining in #3. (You'll see that I'm actually working here in the context of smc categories, but it works essentially the same way for $\ast$-autonomous categories.) So, for example, if $x, y, z$ are distinct variables, there's a unique proof structure of the form $x \multimap (x \otimes y) \to y \otimes (z \multimap z)$. There are, I guess, $6 = 3!$ proof structures of type $x \multimap (x \otimes x) \to x \otimes (x \multimap x)$. Note by the way that this pairing off of variables in KM graphs echoes the idea of "conservation of resources" in linear deductions. For example, there's no KM graph of the form $x \to x \otimes x$ that we'd get via the contraction rule or diagonal map, and similarly there's no KM graph of the form $x \to I$ which would come from the weakening rule or projection map. The fact of the matter is that formulas and proof structures between them form an smc category, $Struct[T]$, where again $T$ is a set of propositional variables. Proof structures are composed in the manner I'd tried to explain in #3, and this composition (of what I'm calling KM graphs) was discussed long, long ago by Eilenberg and Kelly, probably around the same time as their big La Jolla paper on the notion of closed category. I'll leave to the imagination how $\otimes$ and $\multimap$ work on this category, but as functors, tensoring and internal homming is by juxtaposing proof structures, pretty much the way it works for string diagrams, and I'll leave to the imagination how one describes the evaluation morphism $(A \multimap B) \otimes A \to B$ and coevaluation morphism $B \to A \multimap (B \otimes A)$ as proof structures. There is an inclusion functor $T \to Struct[T]$ from the discrete category $T$, which takes $t$ to itself (as propositional formula). Letting $V[T]$ denote the free smc category on $T$, there is an inclusion $i: T \to Struct[T]$. By freeness, this extends to an smc functor $S: V[T] \to Struct[T]$. This smc functor $S$ is what I am calling the _graph semantics_. (Actually, it's one of several things one could mean by "graph semantics" -- maybe we interpret sequent proofs instead of arrows in $V[T]$, etc.) By definition, a _proof net_ is a proof structure of the form $S(f)$. In other words, a proof net is a "correct" or "valid" proof structure, if we use the language of Girard. Or, to put it differently, the smc category of proof nets is the essential image of $S$. An example of an invalid proof structure would be the unique one of type $x \multimap (x \otimes y) \to y \otimes (z \multimap z)$ that I wrote above. There is no morphism definable in the language of smc categories that produces this proof structure. Anyway, while in spirit you could say that proof structures or proof nets do form a kind of graphical syntax, in the set-up above they are described as a possible (categorical) semantics. It's perhaps admittedly silly, ever since Lawvere's thesis, to be dogmatic and draw an absolutely strict dividing line between "categorical syntax" (free models) and "categorical semantics", and it's hardly something I want to argue about here, but at least this explains or justifies why I had written "semantics" earlier. You would be entirely justified in according "full syntactic status" to the smc category of nets $Net[T]$ -- if the full essentially surjective functor $S: V[T] \to Net[T]$ were faithful as well. But it's not faithful. There is a famous example observed by Kelly and Mac Lane, involving "double dual embeddings" $\delta_A: A \to (A \multimap I) \multimap I$, which shows that $$\delta_{x \multimap I} \circ (\delta_x \multimap I): ((x \multimap I) \multimap I) \multimap I \to ((x \multimap I) \multimap I) \multimap I$$ and the identity map on $((x \multimap I) \multimap I) \multimap I$ are distinct in $V[T]$ but have the same graph semantics. This is a fun problem to think about: morally, yes, proof nets are a kind of graphical syntax -- they just happen not to be fully up to the job of carrying _all_ the relevant syntax, or at least not in this form. (Continued, since the software thinks my message is too long.)

    Yeah, sure, you could say proof nets are a kind of graphical syntax. And that’s a good way to think of them. But if you want to put it that way, I’d say that they are about as syntactic as string diagrams, which is also a graphical syntax. (So again I’m not quite sure why one would write that string diagrams are a “categorical semantics” of proof nets.)

    Let me give a quick tutorial, if you don’t mind, to explain better what I had in mind when I wrote “graphical semantics”. Before we (and by “we”, you can consider that I actually mean Girard) talk of “proof nets”, we talk of “proof structures”. (Not a great term, but that’s what “we” call them.) A proof structure of type $A \to B$, where $A, B$ are formulas built from a set of propositional variables $T$ and a constant $I$ (for monoidal unit) by applying operations \otimes, \multimap$, is a graph consisting of

    • a KM-graph which pairs off variables (each pairing being an edge between a negatively signed variable and a positively signed variable, where $A$ is deemed negative and $B$ positive and subformulas acquire signs by declaring that the children $S, T$ of $S \otimes T$ acquire its parity, where $T$ has the same parity and $S$ has parity opposite to $S \multimap T$), and

    • the construction trees of the formulas $A$, $B$.

    So in other words a proof structure of this type is a graph whose vertices are subformulas of $A$ and $B$ and whose edges occur either as KM pairings between variable subformulas or as edges in the two construction trees. This is what I was explaining in #3. (You’ll see that I’m actually working here in the context of smc categories, but it works essentially the same way for $\ast$-autonomous categories.)

    So, for example, if $x, y, z$ are distinct variables, there’s a unique proof structure of the form $x \multimap (x \otimes y) \to y \otimes (z \multimap z)$. There are, I guess, $6 = 3!$ proof structures of type $x \multimap (x \otimes x) \to x \otimes (x \multimap x)$. Note by the way that this pairing off of variables in KM graphs echoes the idea of “conservation of resources” in linear deductions. For example, there’s no KM graph of the form $x \to x \otimes x$ that we’d get via the contraction rule or diagonal map, and similarly there’s no KM graph of the form $x \to I$ which would come from the weakening rule or projection map.

    The fact of the matter is that formulas and proof structures between them form an smc category, $Struct[T]$, where again $T$ is a set of propositional variables. Proof structures are composed in the manner I’d tried to explain in #3, and this composition (of what I’m calling KM graphs) was discussed long, long ago by Eilenberg and Kelly, probably around the same time as their big La Jolla paper on the notion of closed category. I’ll leave to the imagination how $\otimes$ and $\multimap$ work on this category, but as functors, tensoring and internal homming is by juxtaposing proof structures, pretty much the way it works for string diagrams, and I’ll leave to the imagination how one describes the evaluation morphism $(A \multimap B) \otimes A \to B$ and coevaluation morphism $B \to A \multimap (B \otimes A)$ as proof structures.

    There is an inclusion functor $T \to Struct[T]$ from the discrete category $T$, which takes $t$ to itself (as propositional formula). Letting $V[T]$ denote the free smc category on $T$, there is an inclusion $i: T \to Struct[T]$. By freeness, this extends to an smc functor $S: V[T] \to Struct[T]$.

    This smc functor $S$ is what I am calling the graph semantics. (Actually, it’s one of several things one could mean by “graph semantics” – maybe we interpret sequent proofs instead of arrows in $V[T]$, etc.) By definition, a proof net is a proof structure of the form $S(f)$. In other words, a proof net is a “correct” or “valid” proof structure, if we use the language of Girard. Or, to put it differently, the smc category of proof nets is the essential image of $S$.

    An example of an invalid proof structure would be the unique one of type $x \multimap (x \otimes y) \to y \otimes (z \multimap z)$ that I wrote above. There is no morphism definable in the language of smc categories that produces this proof structure.

    Anyway, while in spirit you could say that proof structures or proof nets do form a kind of graphical syntax, in the set-up above they are described as a possible (categorical) semantics. It’s perhaps admittedly silly, ever since Lawvere’s thesis, to be dogmatic and draw an absolutely strict dividing line between “categorical syntax” (free models) and “categorical semantics”, and it’s hardly something I want to argue about here, but at least this explains or justifies why I had written “semantics” earlier.

    You would be entirely justified in according “full syntactic status” to the smc category of nets $Net[T]$ – if the full essentially surjective functor $S: V[T] \to Net[T]$ were faithful as well. But it’s not faithful. There is a famous example observed by Kelly and Mac Lane, involving “double dual embeddings” $\delta_A: A \to (A \multimap I) \multimap I$, which shows that

    $$\delta_{x \multimap I} \circ (\delta_x \multimap I): ((x \multimap I) \multimap I) \multimap I \to ((x \multimap I) \multimap I) \multimap I$$

    and the identity map on $((x \multimap I) \multimap I) \multimap I$ are distinct in $V[T]$ but have the same graph semantics. This is a fun problem to think about: morally, yes, proof nets are a kind of graphical syntax – they just happen not to be fully up to the job of carrying all the relevant syntax, or at least not in this form. (Continued, since the software thinks my message is too long.)

14. • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 6th 2014
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItex(Continued) And this is really what my thesis was about: giving a more refined calculus of "proof nets" (more refined than the Girard proof nets or KM graphs) where coherence really could be decided in terms of these improved proof nets. It's an interesting problem to think about. It's not hard to come up with proposals for these improved proof nets, involving KM linkages between occurrences of the unit $I$, but the plot thickens when one realizes that not only do you have to account for the Kelly-Mac Lane triple dual example above, but you also have to account for the fact that we should get the same proof net after substituting $I$ for $x$! So as I say, it's an interesting problem.

    (Continued) And this is really what my thesis was about: giving a more refined calculus of “proof nets” (more refined than the Girard proof nets or KM graphs) where coherence really could be decided in terms of these improved proof nets. It’s an interesting problem to think about. It’s not hard to come up with proposals for these improved proof nets, involving KM linkages between occurrences of the unit $I$, but the plot thickens when one realizes that not only do you have to account for the Kelly-Mac Lane triple dual example above, but you also have to account for the fact that we should get the same proof net after substituting $I$ for $x$! So as I say, it’s an interesting problem.

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeFeb 6th 2014
    • (edited Feb 6th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks for all the information Todd. On one point I am not sure what to do: while all this discussion is to explain your use of "semantics" as opposed to my half-sentence, you also say that you don't want to argue about it here ;-) So please feel free to ignore this one comment I might make if I were to react: I would have thought a string diagram is not syntax but (categorical) semantics, because a string diagram is by definition labelled in objects and morphisms of a given category. The choice of category is already semantics. To me a string diagram is just a graphical way of speaking of morphisms in a monoidal category. Above you first say that proof net semantics is in $Struct[T]$, but then you conclude that this is actually a bad idea which you fixed in your thesis. I gather there you replaced $S$ by something that is fully faithful after all? But then am I not entitled to "according full syntactic status" to them, _qua_ your very thesis? Possibly we are splitting hairs here, not sure. I would just like to understand and to know how I do have to speak in order not to raise the eyebrows of the logicians. (That of course turned out to be impossibe on another matter already, which we discussed recently...)

    Thanks for all the information Todd.

    On one point I am not sure what to do: while all this discussion is to explain your use of “semantics” as opposed to my half-sentence, you also say that you don’t want to argue about it here ;-) So please feel free to ignore this one comment I might make if I were to react:

    I would have thought a string diagram is not syntax but (categorical) semantics, because a string diagram is by definition labelled in objects and morphisms of a given category. The choice of category is already semantics. To me a string diagram is just a graphical way of speaking of morphisms in a monoidal category.

    Above you first say that proof net semantics is in $Struct[T]$, but then you conclude that this is actually a bad idea which you fixed in your thesis. I gather there you replaced $S$ by something that is fully faithful after all? But then am I not entitled to “according full syntactic status” to them, qua your very thesis?

    Possibly we are splitting hairs here, not sure. I would just like to understand and to know how I do have to speak in order not to raise the eyebrows of the logicians. (That of course turned out to be impossibe on another matter already, which we discussed recently…)

16. • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 6th 2014
    • (edited Feb 6th 2014)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexUrs, you seemed to be objecting to how I was using the word "semantics", so I gave you a long comment which explained why I used that word. So I don't understand why you think I'm arguing. I'm not. I am however trying to explain why the sentence that was there sounds strange to my ears, and I mean to be helpful in doing so. The precise sense in which I view string diagrams as "graphical syntax" is that (let's work just with progressive string diagrams for monoidal categories, to illustrate the idea) the monoidal category of deformation classes of string diagrams labeled in a tensor scheme is the _free_ (strict) monoidal category generated by the tensor scheme. In other words, there is a "forgetful" functor $U$ from (strict) monoidal categories to tensor schemes, taking a monoidal category $M$ to the tensor scheme whose objects are those of $M$, and whose poly-arrows $\Gamma = A_1, \ldots, A_m \to \Delta = B_1, \ldots, B_n$ are triples $(\Gamma, \Delta, f: A_1 \otimes \ldots \otimes A_m \to B_1 \otimes \ldots \otimes B_n)$ where $f$ is a morphism of $M$. So letting $F$ be the left adjoint (which produces the monoidal category of labeled string diagrams), the thing you just referred to is the construction $F(U(M))$, and there is a counit $F(U(M)) \to M$ which evaluates a string diagram labeled in $M$ as a morphism of $M$. Following Lawvere, and in agreement with how you'd like to view proof nets, I am willing to view the constituents of the free structure as 'syntactic' by nature. Another option is to consider the terminal tensor scheme $1$ and to construct the monoidal category $F(1)$ of (deformation classes of) unlabeled string diagrams, and then view a general $F(T)$ (where $T$ is a tensor scheme or computad) as a kind of wreath or club construction $F(1) \rtimes T^\bullet$, which is analogous to how one can construct other types of free categorical structures. > But then am I not entitled to “according full syntactic status” to them, qua your very thesis? Yes, certainly. You could say, with respect to my thesis, that the morphisms of the free smc category $V[T]$ are identified with normalized "unit-extended" (cut-free) proof nets with variables in $T$, where "normalization" refers to a rewriting scheme on unit-extended proof nets called "directed rewiring". The point that I'm trying to make more or less is that both string diagrams and proof nets are both graphical syntax or one form or another, both graphical semantics if you like of one form or another, they are "about equally syntactic and equally semantic" to one another, to put it humorously. We hopefully can begin to understand each other on this point. I would _not_ make a kind of statement that contrasts proof nets as being more on the syntactic side with string diagrams as being more on the semantic side, or that we particularly need to emphasize a step whereby one interprets proof nets in terms of a "categorical semantics of string diagrams". If anything, I would say that string diagrams are "more cleanly syntactic" than proof nets are, because they cleanly represent the arrows of appropriate free structures, whereas Girardian proof nets are not completely satisfactory in this respect (at least not without caveats). Am I making slightly better sense now?

    Urs, you seemed to be objecting to how I was using the word “semantics”, so I gave you a long comment which explained why I used that word. So I don’t understand why you think I’m arguing. I’m not. I am however trying to explain why the sentence that was there sounds strange to my ears, and I mean to be helpful in doing so.

    The precise sense in which I view string diagrams as “graphical syntax” is that (let’s work just with progressive string diagrams for monoidal categories, to illustrate the idea) the monoidal category of deformation classes of string diagrams labeled in a tensor scheme is the free (strict) monoidal category generated by the tensor scheme. In other words, there is a “forgetful” functor $U$ from (strict) monoidal categories to tensor schemes, taking a monoidal category $M$ to the tensor scheme whose objects are those of $M$, and whose poly-arrows $\Gamma = A_1, \ldots, A_m \to \Delta = B_1, \ldots, B_n$ are triples $(\Gamma, \Delta, f: A_1 \otimes \ldots \otimes A_m \to B_1 \otimes \ldots \otimes B_n)$ where $f$ is a morphism of $M$. So letting $F$ be the left adjoint (which produces the monoidal category of labeled string diagrams), the thing you just referred to is the construction $F(U(M))$, and there is a counit $F(U(M)) \to M$ which evaluates a string diagram labeled in $M$ as a morphism of $M$. Following Lawvere, and in agreement with how you’d like to view proof nets, I am willing to view the constituents of the free structure as ’syntactic’ by nature.

    Another option is to consider the terminal tensor scheme $1$ and to construct the monoidal category $F(1)$ of (deformation classes of) unlabeled string diagrams, and then view a general $F(T)$ (where $T$ is a tensor scheme or computad) as a kind of wreath or club construction $F(1) \rtimes T^\bullet$, which is analogous to how one can construct other types of free categorical structures.

    But then am I not entitled to “according full syntactic status” to them, qua your very thesis?

    Yes, certainly. You could say, with respect to my thesis, that the morphisms of the free smc category $V[T]$ are identified with normalized “unit-extended” (cut-free) proof nets with variables in $T$, where “normalization” refers to a rewriting scheme on unit-extended proof nets called “directed rewiring”.

    The point that I’m trying to make more or less is that both string diagrams and proof nets are both graphical syntax or one form or another, both graphical semantics if you like of one form or another, they are “about equally syntactic and equally semantic” to one another, to put it humorously. We hopefully can begin to understand each other on this point. I would not make a kind of statement that contrasts proof nets as being more on the syntactic side with string diagrams as being more on the semantic side, or that we particularly need to emphasize a step whereby one interprets proof nets in terms of a “categorical semantics of string diagrams”. If anything, I would say that string diagrams are “more cleanly syntactic” than proof nets are, because they cleanly represent the arrows of appropriate free structures, whereas Girardian proof nets are not completely satisfactory in this respect (at least not without caveats).

    Am I making slightly better sense now?

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 6th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> I would have thought a string diagram is not syntax but (categorical) semantics, because a string diagram is by definition labelled in objects and morphisms of a given category. The choice of category is already semantics. To me a string diagram is just a graphical way of speaking of morphisms in a monoidal category. One might argue that anything which is described as a "way of speaking" should be considered syntax. (-: More precisely, I would say that a *syntax* (whether graphical, type-theoretic, $n$-dimensional, or whatever) is a way of presenting a free structure of some sort, and the unique maps *out of* that free structure into some other given structure $C$ (determined by interpreting the generators in $C$) are what provide a *semantics* of that syntax in $C$. This is true even when the syntax is the "internal logic" of a given structure $C$, with axioms (= generators) corresponding to all the elements of $C$. So a string diagram itself, even if it is labeled by objects and morphisms in a fixed category $C$, is still syntax --- the semantics comes when you "compose up" that diagram and interpret it as a single morphism of $C$.

    I would have thought a string diagram is not syntax but (categorical) semantics, because a string diagram is by definition labelled in objects and morphisms of a given category. The choice of category is already semantics. To me a string diagram is just a graphical way of speaking of morphisms in a monoidal category.

    One might argue that anything which is described as a “way of speaking” should be considered syntax. (-:

    More precisely, I would say that a syntax (whether graphical, type-theoretic, $n$-dimensional, or whatever) is a way of presenting a free structure of some sort, and the unique maps out of that free structure into some other given structure $C$ (determined by interpreting the generators in $C$) are what provide a semantics of that syntax in $C$. This is true even when the syntax is the “internal logic” of a given structure $C$, with axioms (= generators) corresponding to all the elements of $C$. So a string diagram itself, even if it is labeled by objects and morphisms in a fixed category $C$, is still syntax — the semantics comes when you “compose up” that diagram and interpret it as a single morphism of $C$.

18. • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeFeb 7th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, I get it. Thanks.

    Okay, I get it. Thanks.

19. • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have briefly spelled out how Feynman diagrams arise [For finitely many degrees of freedom](http://ncatlab.org/nlab/show/Feynman+diagram#ForFinitelyManyDegreesOfFreedom).

    I have briefly spelled out how Feynman diagrams arise For finitely many degrees of freedom.

20. • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 17th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexDid all that was good in the discussion above end up appearing on the pages of $n$Lab?

    Did all that was good in the discussion above end up appearing on the pages of $n$Lab?

21. • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2015
    • (edited Nov 17th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI don't think so. See [this paragraph](http://ncatlab.org/nlab/revision/diff/proof+net/16#comparison_to_string_diagrams). In any case, this ought to be discussed in a thread on proof nets, not in a thread on Feynman diagrams.

    I don’t think so. See this paragraph. In any case, this ought to be discussed in a thread on proof nets, not in a thread on Feynman diagrams.

22. • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 17th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItex$$ \langle V(\phi)^2 \rangle = prefactor \; A^{-1}_{x_1 x_1} A^{-1}_{x_1 x_2} A^{-1}_{x_2 x_2} + prefactor \; A^{-1}_{x_1 x_2} A^{-1}_{x_1 x_2} A^{-1}_{x_1 x_2} $$ So it's been specified that there are just two points $x_1$ and $x_2$? And won't there be a contribution from $\langle \phi^6_{x_1} \rangle$, or is this zero?

    $$\langle V(\phi)^2 \rangle = prefactor \; A^{-1}_{x_1 x_1} A^{-1}_{x_1 x_2} A^{-1}_{x_2 x_2} + prefactor \; A^{-1}_{x_1 x_2} A^{-1}_{x_1 x_2} A^{-1}_{x_1 x_2}$$

    So it’s been specified that there are just two points $x_1$ and $x_2$?

    And won’t there be a contribution from $\langle \phi^6_{x_1} \rangle$, or is this zero?

23. • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2015
    • (edited Nov 17th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, there was the sum-sign missing. I have added it now. $$ \begin{aligned} \langle (\sum_{x} \phi_x^3)^2 \rangle & = \sum_{x_1,x_2} \langle \phi_{x_1} \phi_{x_1}\phi_{x_1} \phi_{x_2}\phi_{x_2} \phi_{x_2} \rangle \\ &= prefactor \; \sum_{x_1,x_2 = 1}^k A^{-1}_{x_1 x_1} A^{-1}_{x_1 x_2} A^{-1}_{x_2 x_2} + prefactor \; \sum_{x_1, x_2 = 1}^k A^{-1}_{x_1 x_2} A^{-1}_{x_1 x_2} A^{-1}_{x_1 x_2} \end{aligned} $$

    Okay, there was the sum-sign missing. I have added it now.

    $$\begin{aligned} \langle (\sum_{x} \phi_x^3)^2 \rangle & = \sum_{x_1,x_2} \langle \phi_{x_1} \phi_{x_1}\phi_{x_1} \phi_{x_2}\phi_{x_2} \phi_{x_2} \rangle \\ &= prefactor \; \sum_{x_1,x_2 = 1}^k A^{-1}_{x_1 x_1} A^{-1}_{x_1 x_2} A^{-1}_{x_2 x_2} + prefactor \; \sum_{x_1, x_2 = 1}^k A^{-1}_{x_1 x_2} A^{-1}_{x_1 x_2} A^{-1}_{x_1 x_2} \end{aligned}$$
24. • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 17th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexOh I see, thanks. There's something about physics that makes me more dim than usual. Maybe it's the knowledge that the hope that physical interpretation will be helpful is often misplaced. Take >Notice that in "[[Schwinger parameterization]]" $A^{-1}_{x,y} = \int_0^\infty \exp(- \tau A_{x,y}) d\tau$ and we may think of $\exp(-\tau A_{x,y})$ is the propagator for a scalar along its [[worldline]] of length $\tau$ from $x$ to $y$ ("[[worldline formalism]]"). One might imagine that integrating over $\tau$ means that we have a pair of points, $x, y$, such that the worldline length between them can vary. But how then to think of such points? Especially as $x$ and $y$ might be the same point. Presumably this finite version is building up to the some fuller account of all points in a region?

    Oh I see, thanks. There’s something about physics that makes me more dim than usual. Maybe it’s the knowledge that the hope that physical interpretation will be helpful is often misplaced.

    Take

    Notice that in “Schwinger parameterization” $A^{-1}_{x,y} = \int_0^\infty \exp(- \tau A_{x,y}) d\tau$ and we may think of $\exp(-\tau A_{x,y})$ is the propagator for a scalar along its worldline of length $\tau$ from $x$ to $y$ (“worldline formalism”).

    One might imagine that integrating over $\tau$ means that we have a pair of points, $x, y$, such that the worldline length between them can vary. But how then to think of such points? Especially as $x$ and $y$ might be the same point.

    Presumably this finite version is building up to the some fuller account of all points in a region?

25. • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2015
    • (edited Nov 17th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexAh, don't worry, that was an annoying typo of mine. I am glad that you spotted it. > One might imagine that integrating over $\tau$ means that we have a pair of points, $x, y$, such that the worldline length between them can vary. Yes, the particle may travel from $x$ to $y$ taking any "time" $\tau$. The integral over $\tau$ accounts for the superposition of all contributions of particles taking any positive time to get from $x$ to $y$. Here you ought to think of $\tau$ not as physical time, but as wordline parameter length. It may be helpful to think of this when generalizing from poing particles to strings, then $\tau$ becomes complex, parameterizing the length and diameter of a torus (a string worldsheet) and the integral over $\tau$ is now over the moduli space of complex elliptic curves. > Presumably this finite version is building up to the some fuller account of all points in a region? All the appearance and role of the diagrams is fully visible in the finite version. Passing to infinite-dimensional "path integrals" only adds the complication of how to interpret (by renormalization) the contribution of each diagram to the total sum. For the time being I am too lazy to write more on that.

    Ah, don’t worry, that was an annoying typo of mine. I am glad that you spotted it.

    One might imagine that integrating over $\tau$ means that we have a pair of points, $x, y$, such that the worldline length between them can vary.

    Yes, the particle may travel from $x$ to $y$ taking any “time” $\tau$. The integral over $\tau$ accounts for the superposition of all contributions of particles taking any positive time to get from $x$ to $y$. Here you ought to think of $\tau$ not as physical time, but as wordline parameter length. It may be helpful to think of this when generalizing from poing particles to strings, then $\tau$ becomes complex, parameterizing the length and diameter of a torus (a string worldsheet) and the integral over $\tau$ is now over the moduli space of complex elliptic curves.

    Presumably this finite version is building up to the some fuller account of all points in a region?

    All the appearance and role of the diagrams is fully visible in the finite version. Passing to infinite-dimensional “path integrals” only adds the complication of how to interpret (by renormalization) the contribution of each diagram to the total sum. For the time being I am too lazy to write more on that.

26. • CommentRowNumber26.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 18th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexIt seems we start off there just with a "discrete space of $k \in \mathbb{N}$ points". As yet, there is no further structure on these points? But then how do I think of worldlines of different lengths between two points? Does this not suggest paths in a space in which the $k$ points sit?

    It seems we start off there just with a “discrete space of $k \in \mathbb{N}$ points”. As yet, there is no further structure on these points?

    But then how do I think of worldlines of different lengths between two points? Does this not suggest paths in a space in which the $k$ points sit?

27. • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeNov 18th 2015
    • (edited Nov 18th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, that's interesting about this explicit deduction of the whole story, one sees which piece of the physics picture really comes from which bit of mathematics. We see here that the wordline exists quite independently of the target spacetime. Again this is a phenomenon that is more familiar (to some people) in the higher dimensional case of strings. Here the worldline is replaced by the worldsheet, and it is a famous fact that there are situations where it is impossible to interpret the propagators as exhibiting propagation through anything like a continuous space. The famous example are [[Gepner models]]. In this stringy version of the Feynman diagram story, there is a priori no spacetime, defined. What in the entry appears as sums $\sum_{x = 1}^k$ over points in spacetime is all absorbed in the worldsheet correlators. All one has then in the end is a sum over Riemann surfaces (the higher dimensional version of Feynman graphs) and each contribution in the sum looks like the propability amplitude for some objects zipping around in some "space" in some way, but that "space" is a priori not defined, we see it only indirectly via those probability amplitudes.

    Yes, that’s interesting about this explicit deduction of the whole story, one sees which piece of the physics picture really comes from which bit of mathematics. We see here that the wordline exists quite independently of the target spacetime.

    Again this is a phenomenon that is more familiar (to some people) in the higher dimensional case of strings. Here the worldline is replaced by the worldsheet, and it is a famous fact that there are situations where it is impossible to interpret the propagators as exhibiting propagation through anything like a continuous space. The famous example are Gepner models.

    In this stringy version of the Feynman diagram story, there is a priori no spacetime, defined. What in the entry appears as sums $\sum_{x = 1}^k$ over points in spacetime is all absorbed in the worldsheet correlators. All one has then in the end is a sum over Riemann surfaces (the higher dimensional version of Feynman graphs) and each contribution in the sum looks like the propability amplitude for some objects zipping around in some “space” in some way, but that “space” is a priori not defined, we see it only indirectly via those probability amplitudes.

28. • CommentRowNumber28.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 18th 2015
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexPerhaps a silly question, but I know that one thing that is liked about string worldsheets is that they do not have the deficiencies vis a vis singularities that the underlying graphs of Feynman diagrs have. But why can't we consider foams as well as Riemann surfaces? Sure, the theory works nice with only the latter, but so do non-interacting particles. Or did I just reinvent branes?

    Perhaps a silly question, but I know that one thing that is liked about string worldsheets is that they do not have the deficiencies vis a vis singularities that the underlying graphs of Feynman diagrs have. But why can’t we consider foams as well as Riemann surfaces? Sure, the theory works nice with only the latter, but so do non-interacting particles. Or did I just reinvent branes?

29. • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeNov 19th 2015
    • (edited Nov 19th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexIs your question why one does not consider S-matrices built out of sums of correlators of $p+1$-dimensional field theories on diagrams of dimension $p+1 \gt 1+1$? Hence why not use $p$-branes for $p \gt 1$ to define a perturbation theory? The reason is that it is hard and seems impossible to make sense of this. There are two problems: a) for $p \gt 1$ then the standard worldvolume action functionals, which are really worldvolume gravity coupled to "matter" (the sigma-model fields) are not renormalizable; b) for $p \gt 1$ the moduli spaces of $p+1$-manifolds are not controllable. So for $p \gt 1$ one a) does not know how to define the "Feynman amplitudes" and b) even if one did, one does not know how against what to integrate them. Each of these two problems in itself makes a $p$-brane perturbation theory for $p \gt 1$ be hard to come by. That is, by the way, the reason for the term "M-theory". First there had been the observation that the super 1-brane in 10d target spacetimes is accompanied by a 2-brane in 11d target spacetimes. This suggested the evident idea that there ought to be perturbation theory for 2-branes -- called membranes, hence that there ought to be _membrane theory_ in direct analogy with _string theory_. But the above two problems make a direct such analogy unlikely. But since there might be a less obvious, more sophisticated kind of analogy, Witten started saying "M-theory" as an abbreviation, not tocommit himself to what exactly might be really going on, and leaving open for the future if "M" is for "membrane" or for something else: > As it has been proposed that the eleven-dimensional theory is a supermembrane theory but there are some reasons to doubt that interpretation, we will non-committally call it the M-theory, leaving to the future the relation of M to membranes. ([Hořava-Witten 95](http://ncatlab.org/nlab/show/M-theory#HoravaWitten95))

    Is your question why one does not consider S-matrices built out of sums of correlators of $p+1$-dimensional field theories on diagrams of dimension $p+1 \gt 1+1$? Hence why not use $p$-branes for $p \gt 1$ to define a perturbation theory?

    The reason is that it is hard and seems impossible to make sense of this. There are two problems:

    a) for $p \gt 1$ then the standard worldvolume action functionals, which are really worldvolume gravity coupled to “matter” (the sigma-model fields) are not renormalizable;

    b) for $p \gt 1$ the moduli spaces of $p+1$-manifolds are not controllable.

    So for $p \gt 1$ one a) does not know how to define the “Feynman amplitudes” and b) even if one did, one does not know how against what to integrate them.

    Each of these two problems in itself makes a $p$-brane perturbation theory for $p \gt 1$ be hard to come by.

    That is, by the way, the reason for the term “M-theory”. First there had been the observation that the super 1-brane in 10d target spacetimes is accompanied by a 2-brane in 11d target spacetimes. This suggested the evident idea that there ought to be perturbation theory for 2-branes – called membranes, hence that there ought to be membrane theory in direct analogy with string theory. But the above two problems make a direct such analogy unlikely. But since there might be a less obvious, more sophisticated kind of analogy, Witten started saying “M-theory” as an abbreviation, not tocommit himself to what exactly might be really going on, and leaving open for the future if “M” is for “membrane” or for something else:

    As it has been proposed that the eleven-dimensional theory is a supermembrane theory but there are some reasons to doubt that interpretation, we will non-committally call it the M-theory, leaving to the future the relation of M to membranes. (Hořava-Witten 95)

30. • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeNov 19th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have turned the above answer into a further item in the [[string theory FAQ]], _[Why not consider perturbative p-brane scattering for any p?](https://ncatlab.org/nlab/show/string+theory+FAQ#WhyNopBranePerturbationTheory)_

    I have turned the above answer into a further item in the string theory FAQ, Why not consider perturbative p-brane scattering for any p?

31. • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeJun 15th 2022
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded these two pointers: * [[Stefan Weinzierl]], *Introduction to Feynman Integrals* $[$[arXiv:1005.1855](https://arxiv.org/abs/1005.1855)$]$ * [[Stefan Weinzierl]], *Feynman Integrals*, UNITEXT for Physics, Springer (2022) $[$[arXiv:2201.03593](https://arxiv.org/abs/2201.03593), [doi:10.1007/978-3-030-99558-4](https://doi.org/10.1007/978-3-030-99558-4)$]$ (816 pages) <a href="https://ncatlab.org/nlab/revision/diff/Feynman+diagram/43">diff</a>, <a href="https://ncatlab.org/nlab/revision/Feynman+diagram/43">v43</a>, <a href="https://ncatlab.org/nlab/show/Feynman+diagram">current</a>

    added these two pointers:

    • Stefan Weinzierl, Introduction to Feynman Integrals $[$arXiv:1005.1855$]$

    • Stefan Weinzierl, Feynman Integrals, UNITEXT for Physics, Springer (2022) $[$arXiv:2201.03593, doi:10.1007/978-3-030-99558-4$]$ (816 pages)

    diff, v43, current

32. • CommentRowNumber32.
    • CommentAuthornLab edit announcer
    • CommentTimeJan 8th 2023
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdded reference * Zhi-Feng Liu, Yan-Qing Ma, *Determining Feynman Integrals with Only Input from Linear Algebra*, Physical Review Letters, Volume 129, Issue 22, 23 November 2022 ([doi:10.1103/PhysRevLett.129.222001](Zhi-Feng Liu, Yan-Qing Ma), [arXiv:2201.11637](https://arxiv.org/abs/2201.11637)) Anonymous <a href="https://ncatlab.org/nlab/revision/diff/Feynman+diagram/45">diff</a>, <a href="https://ncatlab.org/nlab/revision/Feynman+diagram/45">v45</a>, <a href="https://ncatlab.org/nlab/show/Feynman+diagram">current</a>

    Added reference

    • Zhi-Feng Liu, Yan-Qing Ma, Determining Feynman Integrals with Only Input from Linear Algebra, Physical Review Letters, Volume 129, Issue 22, 23 November 2022 ([doi:10.1103/PhysRevLett.129.222001](Zhi-Feng Liu, Yan-Qing Ma), arXiv:2201.11637)

    Anonymous

    diff, v45, current

33. • CommentRowNumber33.
    • CommentAuthornLab edit announcer
    • CommentTimeJan 8th 2023
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexfixing doi link in reference Anonymous <a href="https://ncatlab.org/nlab/revision/diff/Feynman+diagram/45">diff</a>, <a href="https://ncatlab.org/nlab/revision/Feynman+diagram/45">v45</a>, <a href="https://ncatlab.org/nlab/show/Feynman+diagram">current</a>

    fixing doi link in reference

    Anonymous

    diff, v45, current

34. • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeMar 21st 2023
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded pointer to today's * Johannes Henn, Elizabeth Pratt, Anna-Laura Sattelberger, Simone Zoia, *$D$-Module Techniques for Solving Differential Equations in the Context of Feynman Integrals* &lbrack;[arXiv:2303.11105](https://arxiv.org/abs/2303.11105)&rbrack; <a href="https://ncatlab.org/nlab/revision/diff/Feynman+diagram/46">diff</a>, <a href="https://ncatlab.org/nlab/revision/Feynman+diagram/46">v46</a>, <a href="https://ncatlab.org/nlab/show/Feynman+diagram">current</a>

    added pointer to today’s

    • Johannes Henn, Elizabeth Pratt, Anna-Laura Sattelberger, Simone Zoia, $D$-Module Techniques for Solving Differential Equations in the Context of Feynman Integrals [arXiv:2303.11105]

    diff, v46, current