You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Evan Patterson (May 05 2023 at 00:41):Is there a graphical language in the style of string diagrams for (non-compact) closed monoidal categories or cartesian closed categories?
Last time I checked there seemed to be many informal/semi-formal such languages, but none that came with any coherence theorems. I am imagining something in vein of Jeffrey's classic graphical view of programs but with a mathematical result connecting it to closed monoidal categories. Also, I am not looking for clasp notation, which is farther away from the sort of informal pictures people often draw in graphical programming languages.
John Baez (May 05 2023 at 00:59):Do you know Mike Shulman's ideas?
John Baez (May 05 2023 at 00:59):Symmetric monoidal categories with duals, a.k.a. compact monoidal categories, have a pleasing string diagram calculus. In particular, any compact monoidal category is closed with [A,B] = (A* ⊗ B), and the transpose of A ⊗ B → C to A → [B,C] is represented by simply bending a string. Unfortunately, a closed symmetric monoidal category cannot even be embedded fully-faithfully into a compact one unless it is traced; and while string diagram calculi for closed monoidal categories have been proposed, they are more complicated, e.g. with “clasps” and “bubbles”. In this talk we obtain a string diagram calculus for closed symmetric monoidal categories that looks almost like the compact case, by fully embedding any such category in a star-autonomous one (via a functor that preserves the closed structure) and using the known string diagram calculus for star-autonomous categories. No knowledge of star-autonomous categories will be assumed.
Ryan Wisnesky (May 05 2023 at 03:45):there's this for untyped lambda calculus https://tromp.github.io/cl/diagrams.html
Cole Comfort (May 05 2023 at 09:21):As @John Baez mentioned, by the conservativity result of @Mike Shulman, proof nets for *-autonomous categories can be regarded as the graphical calculus for monoidal closed categories when the domain and codomain are the right types. However, as @Robin Piedeleu points out in his blog, to obtain a graphical calculus for Cartesian closed categories is not necessarily so easy as to take the pushout of the graphical calculi for monoidal closed and Cartesian categories
Cole Comfort (May 05 2023 at 14:22):I think it is kind of crazy how the graphical calculus for cartesian closed categories is not figured out, despite the fundamental importance of cartesian closed categories in computer science. If anyone has any ideas I would love to know.
John Baez (May 05 2023 at 14:28):Me too! Mike Stay and I tried, in a kind of rough-and-ready way, but as everyone in this area knows, we didn't really figure it out.
Cole Comfort (May 05 2023 at 14:32):John Baez said:
Me too! Mike Stay and I tried, in a kind of rough-and-ready way, but as everyone in this area knows, we didn't really figure it out.
Do you know if any other groups are still working on this sort of thing, I know that @Fabio Zanasi and Dan Ghica are working on things adjacent to this, but are there any others? If I continue in academia, then I would like to work with people who are still doing this kind of stuff, as there seems to be lots of unexplored territory.
Simon Willerton (May 05 2023 at 14:35):I learnt the clasp notation from John and Mike, I made it a bit more 3-d and find it a useful way to write it.
Screenshot-2023-05-05-at-15.32.54.png
John Baez (May 05 2023 at 14:36):I don't know anyone actually working on the cartesian closed case, @Cole Comfort.
John Baez (May 05 2023 at 14:39):But I didn't even know Simon had done this 3d notation! So I am apparently not the right one to ask about people working on a complete string diagram calculus for cartesian closed categories. @Mike Shulman might be a better person to ask.
Simon Willerton (May 05 2023 at 14:40):For example, the proof that the composition of internal homs -- -- is associative becomes the following. (Not that I expect anyone to immediately understand the picture!)
Screenshot-2023-05-05-at-15.38.34.png
Simon Willerton (May 05 2023 at 14:46):John Baez said:
But I didn't even know Simon had done this 3d notation!
I've been using in notebooks for years - like in my unfinished introduction to enriched categories - but it's not made it out into the public world. These snaps are from something I've been writing recently.
Simon Willerton (May 05 2023 at 14:53):Maybe I should add that you read the diagrams upwards, so the diagrammatic proof is showing that the composition maps
and
are equal.
John Baez (May 05 2023 at 14:53):Your notation reminds me visually of Jamie Vicary et al's notation for 3d extended TQFT using Feynman diagrams drawn inside cobordisms:
Simon Willerton (May 05 2023 at 14:56):In some sense they're not really 3d, the clasps are just a visual way of bracketing terms in the line.
Mike Shulman (May 05 2023 at 15:07):I've thought about this too, but haven't really gotten anywhere either.
Cole Comfort (May 05 2023 at 15:35):Simon Willerton said:
In some sense they're not really 3d, the clasps are just a visual way of bracketing terms in the line.
In some sense Jamie et al's diagrams are also a formal way of bracketing things. If you take a monoidal category, you can regard it as both a representable pseudomonoid and corepresentable pseudocomonoid in Prof. And if you take the elements of this pseudomonoid and pseudocomonoid, then these can be regarded as 1-cells in the symmetric monoidal bicategory of pointed profunctors. This is what Jamie et als string diagrams are representing, albeit in the vect-enriched setting, but it works just as well in the Set-enriched setting. So the way in which the the tubes are connected together expresses the order in which things are bracketed together. However, the category of pointed profunctors is a monoidal bicategory, and not a monoidal category, so to reassociate the bracketing, for example, is to apply a 2-cell. Therefore, asking that two diagrams in pointed profunctors are equal is too strict to determine if the diagrams obtained by dropping the tubes are equal.
Moreover, they don't talk about cartesian closedness at all, but there is probably a characterization of cartesian closed categories as some sort of object in Prof. And with such a characterization, then I imagine that these tube diagrams could easily be extended.
I suspect that it may be possible to take some sort of Grothendieck construction to produce a cartesian closed category from such data in Prof, getting rid of the 2-cells, in a way similar to the "coherence via universality" approach of Hermida, but I am not sure exactly how it would work.
John Baez (May 05 2023 at 15:40):This is cool, Cole! I'm so glad I let myself free-associate.
John Baez (May 05 2023 at 15:42):Moreover, they don't talk about cartesian closedness at all...
Right, they are trying to describe modular tensor categories, which are particularly nice Vect-enriched braided monoidal closed categories.
John Baez (May 05 2023 at 15:42):So it would be great if some of their ideas could be extended to handle other cases, e.g. Set-enriched cartesian closed categories.
John Baez (May 05 2023 at 15:48):Maybe in this case they would turn into something like what Simon is doing.
Cole Comfort (May 05 2023 at 15:50):John Baez said:
So it would be great if some of their ideas could be extended to handle other cases, e.g. Set-enriched cartesian closed categories.
I don't think that think that the major difficulty would be to figure out what set-enriched cartesian closed categories look like as data in prof/pointed prof, but rather the difficulty would be to produce a 1-category from this data. Because usually when people ask what the "graphical language for X" is they don't expect to have to apply a bunch of coherent 2-cells to the diagrams to prove that they are equal.
Jules Hedges (May 05 2023 at 18:05):Cole Comfort said:
I think it is kind of crazy how the graphical calculus for cartesian closed categories is not figured out, despite the fundamental importance of cartesian closed categories in computer science. If anyone has any ideas I would love to know.
What goes wrong if you take your favourite graphical calculus for monoidal closed categories, say the bubble-and-clasp calculus, and then add a supply of comonoids and the axiom that they commute with everything, to make your monoidal product cartesian?
Jules Hedges (May 05 2023 at 18:06):In private I always do this by pretending my category is compact closed and then, like, just don't make any mistakes
Evan Patterson (May 05 2023 at 18:09):Thanks for the responses everyone. To amplify Cole's comment: quantum computing is cool and it's great that we have rigorous graphical languages for it. But classical computing is kind of important too :)
I think of cartesian closed categories, and thus general closed monoidal categories, as being significantly different than compact closed categories, where you are allowed to bend wires. (As a point in favor of this view, any category that is both cartiesan closed and compact closed is trivial.) So I'd like to have graphical language for the former that is "native" to those structures rather than adapted from the compact setting.
Jules Hedges (May 05 2023 at 18:12):I guess a major reason nobody really knows about this is that we have an extremely effective 1-dimensional syntax for cartesian closed categories, namely simply typed lambda calculus
Jules Hedges (May 05 2023 at 18:14):The way I think about this: string diagrams are inherently linear due to conservation of string number: any piece of string that has 1 end must have exactly 1 other end. Using string diagrams in a cartesian setting requires encoding (eg. via comonoids) to allow you to draw "hyper-strings". Meanwhile in the more traditional world of variable-binding syntax you're cartesian by default (you can write a variable as many times as you like), and linearity requires encoding (eg. via a linear type theory)
Antonin Delpeuch (May 05 2023 at 19:30):I have the fuzzy intuition that there cannot be a 2D graphical calculus for monoidal closed categories that is "local", in the sense that the diagram is built out of blocks and the validity of a diagram can be checked locally, on each boundary between blocks. It would be nice if we could have a result of this sort, similar to the fact that the language of well-bracketed strings of brackets is not regular.
Robin Piedeleu (May 05 2023 at 19:36):Cole Comfort said:
Moreover, they don't talk about cartesian closedness at all, but there is probably a characterization of cartesian closed categories as some sort of object in Prof. And with such a characterization, then I imagine that these tube diagrams could easily be extended.
I think that should not be too difficult: cartesianess is given by the existence of an adjoint to the monoidal product profunctor, and exponentials by an adjoint to the same profunctor with one leg bent up (i.e. a categorified version of what's in my blog post that you've mentioned above). That should be enough as long as everything is representable etc., no?
Robin Piedeleu (May 05 2023 at 19:40):Jules Hedges said:
The way I think about this: string diagrams are inherently linear due to conservation of string number: any piece of string that has 1 end must have exactly 1 other end. Using string diagrams in a cartesian setting requires encoding (eg. via comonoids) to allow you to draw "hyper-strings". Meanwhile in the more traditional world of variable-binding syntax you're cartesian by default (you can write a variable as many times as you like), and linearity requires encoding (eg. via a linear type theory)
This is a great summary. I would also add that, in addition to the encoding of copying & discarding with explicit comonoids, you also need to enforce their naturality, which is what becomes difficult in the closed setting.
Fabio Zanasi (May 16 2023 at 13:33):Hi @Evan Patterson we give an introduction to string diagrams in monoidal closed categories (including cartesian) at the beginning of this paper:
https://drops.dagstuhl.de/opus/volltexte/2023/17467/pdf/LIPIcs-CSL-2023-6.pdf
I don't think there is anything strikingly 'new' here, but since we could not find a systematic source we summarised it ourselves.
Btw a more structured approach (a book actually) by Dan Ghica and me is coming out sometimes soon. It is about hierarchical string diagrams and applications in programming language theory.
Evan Patterson (May 16 2023 at 17:58):Thanks, I'm glad to hear that you're working on this!
Fabio Zanasi (Jun 01 2023 at 14:44):@Evan Patterson It came out:
https://arxiv.org/abs/2305.18945