Re: String diagrams, adjunction and autonomous categories.

["André Joyal" <joyal.andre@uqam.ca>]

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
>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]