Dear Peter, If I recall it right, string diagrams were first introduced by Kelly and MacLane as a visual device for analysing the structure of the arrows of a free monoidal closed category. The device was not perfect but was giving some real insights. Max Kelly showed later that it was a complete description in the compact case. I believe that Penrose was inspired by Feynman's diagrams when he introduced his graphical tensor calculus (sometimes later). I have first learned about Penrose's diagram from Max, in the late 70's. One of the best way to learn something is to reinvent it. Mathematics need to be constantly reinvented to stay alive and prosper. Every new generation is reinventing mathematics. Category theorists are permanently reinventing mathematics. I guess we also need to remember the past. Best, andre Le 10-09-05 à 22:05, Peter Selinger a écrit :
I agree that string diagrams for closed monoidal categories are quite a bit subtler than those for autonomous categories.
Of course, because of the forgetful functor from autonomous categories to closed monoidal categories, there's a unique functor from the free closed monoidal category (over some generators) to the free autonomous category (over the same generators), i.e., string diagrams. So one can say, without doing any technical work, that morphisms of the free closed monoidal category are "certain" string diagrams, possibly with additional structure.
The technical questions then are: which diagrams are "certain" ones (i.e., what's the image of this functor), and what, if anything, is the additional structure? One obvious piece of extra structure is that there are two binary connectives instead of one, namely, tensor and '-o'. In the Rosetta Stone paper (p.30), Baez and Stay use "clasps" to bind two strings together, to indicate an object A -o B. I am not sure how this will work for nested operations, such as (((A tensor B) -o C) tensor D) -o ((E -o F) tensor G). As John has already pointed out, the paper does not give details or theorems.
On the other hand, the question of such string diagrams has been very extensively studied by logicians under the name "proof nets for linear logic". It turns out that one usually needs a condition logicians call a "correctness criterion" (originally invented by Girard) to identify the string diagrams that actually correspond to legal morphisms. Alternatively, it is possible to just draw a box around every operation (as done by Baez and Stay), and say that the legal diagrams are those built up using the operations of closed monoidal categories. But that is really just a graphical way of displaying the original term, together with its forgetful image in string diagrams.
Most work on proof nets is for classical linear logic (corresponding to *-autonomous categories). Looking for the case of closed monoidal categories only, we need to look for intuitionistic linear logic. By googling "proof nets for intuitionistic linear logic", I found this 2008 paper by Lamarche (based on a 1994 technical report), which seems to contain the answer, with theorems:
http://hal.inria.fr/docs/00/34/73/36/PDF/prfnet1.pdf
That paper actually contains a bit more than just the monoidal closed case; it also shows how to extend the diagrams to cartesian product (in addition to tensor), and it adds the exponential operator "!" of linear logic, in the presence of which one can then have diagrams for *cartesian* closed categories as well. I think an even earlier version of such string diagrams may already appear in Regnier's 1992 thesis (http://iml.univ-mrs.fr/~regnier/articles/these.ps.gz).
So I guess the point is that one can save some time by exploiting what logicians have already done, using the connections between logic, category theory, and string diagrams, rather than re-inventing the wheel. Which is also precisely the point of the Baez/Stay "Rosetta Stone" paper.
-- Peter
John Baez wrote:
Mike Shulman wrote:
On the other hand, am I right that you (John) have also written about
string diagrams in closed (non-autonomous) monoidal categories?
Right.
Those are a bit subtler, and I don't recall them in the work of Joyal and Street (am I wrong?).
I think you're right - they're subtler, and I haven't seen anyone else using them. I never proved any *theorems* about them. But I used them extensively in my course on "Classical versus quantum computation", starting here:
http://math.ucr.edu/home/baez/qg-fall2006/index.html#computation
I wanted to explain how beta-reduction in the lambda calculus is like "straightening a zig-zag".
There's a quick summary of this material in that "Rosetta Stone" paper with Mike Stay, mentioned earlier:
http://arxiv.org/abs/0903.0340
The original question used the word "autonomous" but the notation used suggested a merely closed monoidal category, so perhaps that's what he had in mind.
Oh, okay. Yeah, I was sort of disappointed that Micah credited me for string diagrams in the autonomous case, where I didn't invent them, instead of the closed case, where maybe I did.
Best, jb
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]