Category Theory
Zulip Server
Archive

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.

Stream: event: ACT20

Topic: Tutorial: String Diagrams (Fabrizio Genovese)

Paolo Perrone (Jun 16 2020 at 14:00):

Hi all! This is the thread of discussion for Fabrizio's tutorial, "An introduction to string diagrams."

Paolo Perrone (Jun 16 2020 at 14:00):

Abstract:
We will introduce the basic concepts of surface diagrams for 1-, 2- and n- categories. From there, we will introduce string diagrams for various flavors of monoidal categories (monoidal, compact closed, traced, ...). There are no prerequisites.

eric brunner (Jun 29 2020 at 14:37):

still, a pre-talk reading would be useful. thanks in advance.

Paolo Perrone (Jul 02 2020 at 02:46):

When and where: Sunday July 5, 15:00 UTC (11 am EDT)
Zoom meeting: https://mit.zoom.us/j/7055345747
See also the main website.

Paolo Perrone (Jul 05 2020 at 14:55):

We start in 5 min!

Paolo Perrone (Jul 05 2020 at 15:10):

Here are the links given by Fabrizio.
Marsden: Category Theory using string diagrams https://arxiv.org/abs/1401.7220
Selinger: A survey of graphical languages for mon cat https://arxiv.org/abs/0908.3347

Joe Moeller (Jul 05 2020 at 15:11):

He also mentioned this paper by Joyal and Street, where they essentially prove that using string diagrams is valid.
https://www.sciencedirect.com/science/article/pii/000187089190003P

Daniel Plácido (Jul 05 2020 at 15:30):

How does one draw a parallel pair $A\rightrightarrows B$ (no 2-morphisms between them) with this graphical representation of 2-categories?

Paolo Perrone (Jul 05 2020 at 15:31):

Let's ask this question at the end :)

Joe Moeller (Jul 05 2020 at 15:32):

A single string diagram only depicts a single morphism. What I mean is that you can have many morphisms depicted, but they must be composed somehow to get it all down to a single (composite) morphism.

Joe Moeller (Jul 05 2020 at 15:33):

So if you want two different morphisms, but you don't want to talk about composing them, you just have to draw two different diagrams.

Daniel Plácido (Jul 05 2020 at 15:33):

Paolo Perrone said:

Let's ask this question at the end :)

Ok, thanks! I wrote it here because the Zoom chat is flowing too fast. I'll save my questions for later.

Daniel Plácido (Jul 05 2020 at 15:34):

Joe Moeller said:

So if you want two different morphisms, but you don't want to talk about composing them, you just have to draw two different diagrams.

That makes sense. Thanks.

Kartik (Jul 05 2020 at 16:29):

Someone took notes here, that also includes a bunch of links: https://codi.lassul.us/HqlF3K2CR0eYcpUbiOnneA

Fabrizio Genovese (Jul 05 2020 at 16:52):

I'm still around if there are more questions btw :slight_smile:

Yuri de Wit (Jul 05 2020 at 17:01):

@Fabrizio Genovese , from the different 'extensions' of SMC (braided, traced, etc) where does Petri Nets fall?

Fabrizio Genovese (Jul 05 2020 at 17:02):

Heh! It turns out that Petri nets can be thought of as presentations of monoidal categories

Fabrizio Genovese (Jul 05 2020 at 17:02):

There are many different flavors of petri nets and many different flavors of monoidal categories, but roughly:

Fabrizio Genovese (Jul 05 2020 at 17:04):

Petri nets can be linked to commutative and symmetric monoidal categories, depending who you ask to. Relevan papers are:
https://arxiv.org/abs/1808.05415
https://link.springer.com/chapter/10.1007/3-540-59293-8_205

Fabrizio Genovese (Jul 05 2020 at 17:04):

Then there are generalizations, such as:
https://arxiv.org/abs/1805.05988
https://www.researchgate.net/publication/221138189_Pre-nets_Read_Arcs_and_Unfolding_A_Functorial_Presentation/link/09e41511e079fab475000000/download

Paolo Perrone (Jul 06 2020 at 01:58):

Hey all! Here's the video.
https://www.youtube.com/watch?v=LY5H9uY7Gns&list=PLCOXjXDLt3pYPE63bVbsVfA41_wa3sZOh

David Tanzer (Jul 06 2020 at 23:16):

Given a string diagram in an SMC, I'm trying to picture algorithms for converting them into expressions involving tensoring, composition and identities. Let's assume there are no loops. Then the process nodes are partially ordered by the relation where A <= B means that A outputs to wire X, and X inputs to B. Then form a topological sort of the process nodes. We can use this to get an expression for the whole diagram, which is a sequential composition of expressions, one per process node. This corresponds to morphing the diagram by sliding the process nodes around, so that in the result, no two process nodes are drawn concurrently. Then every intermediate stage in the sequential pipeline is a tensoring of all the parallel wires that go from one stage to the next. Each node inputs some wires from the outputs of its predecessor node, and some wires which are "carried over" from earlier stages in the chain. So the expression for that node is the tensoring of the morphism associated with that node, with identities for all of the wires which are carrried over.

David Tanzer (Jul 06 2020 at 23:17):

This construction seems to work, but it involves what looks like an artificial sequentialization of the diagram.

David Tanzer (Jul 06 2020 at 23:26):

Maybe this is just one of those things, stemming ultimately from the fact that whereas the string diagram involves a DAG-like structure, any representing expression must be a tree.

Fabrizio Genovese (Jul 07 2020 at 00:16):

You are tapping into a very complicated problem. It seems to me that you want to find a data structure that represents well a string diagram, that is, a data structure which is invariant wrt the topological deformations you do with diagrams.

Fabrizio Genovese (Jul 07 2020 at 00:17):

This is pretty much what we tried to do at Statebox for one year. We absolutely needed such a data structure to get a formally verified implementation of free SMCs in Idris

Fabrizio Genovese (Jul 07 2020 at 00:18):

Then this paper came out: http://cartographer.id/cartographer-calco-2019.pdf

Fabrizio Genovese (Jul 07 2020 at 00:19):

Pawel, Paul and Fabio worked out a data structure that is not quite what we want, but very very close to it. From there, we were able to edit it here and there to finally obtain a data structure that represents string diagrams invariantly

Fabrizio Genovese (Jul 07 2020 at 00:20):

In general, for some "easier" stuff (e.g. manipulating string diagrams in the graphical interface) we just store the diagram as a tree. This is what we do in edit.statebox.cloud, and you can see the tree corresponding to a diagram in the bottom part of the window.

Fabrizio Genovese (Jul 07 2020 at 00:21):

Clearly, there are many different trees depicting the same diagram. We do not pick any particular normal form, the tree you get depends on how you specify the morphisms. This is ok because then we convert such a tree into our invariant data structure in the formally verified idris "core", where the actual computations are carried out

Fabrizio Genovese (Jul 07 2020 at 00:23):

Maybe all this is a bit handwavy, but long story short: Representing string diagrams in a computationally satisfying way is not easy, nor intuitive. This is very similar to what happens with graphs. Mathematicians working with graphs may think "well it's just a graph" but there are many different ways of storing a graph as data, which have absolutely inequivalent properties. Simply put, rivers of words have been written on the problem of computing with graphs, and with string diagrams the situation is similar if not worse :grinning:

James Fairbanks (Jul 07 2020 at 00:44):

Maybe this is just one of those things, stemming ultimately from the fact that whereas the string diagram involves a DAG-like structure, any representing expression must be a tree.

@Evan Patterson implemented a function from StringDiagrams to Expressions in Catlab. It does require arbitrary choices about ordering the diagram in order to force a DAG into a tree. Different choices yield different properties of the resulting trees. That is part of the motivation for unbiased languages for SMCs based on Operads of Wiring Diagrams, which is an ongoing development topic in Catlab.

Evan Patterson (Jul 07 2020 at 01:32):

Thanks James, Catlab does have an algorithm for converting wiring diagrams into expression trees. It is inspired by known algorithms for decomposing series-parallel digraphs (graphs that really wish they were SMCs). The algorithm prefers parallelism, i.e., it favors $(f \cdot g) \otimes (h \cdot k)$ over $(f \otimes h)\cdot (g \otimes k)$ in the interchange law. To deal with the arbitrariness of order in tensor products (think $f \otimes g$ vs $g \otimes f$) simple heuristics for minimizing edge crossings are used.

That said, I do not understand the mathematical properties of the algorithm. I do not know whether it is "optimal" in finding parallelism or even that it works in all cases, as tricky special cases have a habit of cropping up. So, as Fabrizio said, it is a hard problem.

Personally, I find myself moving away from this approach towards working in fully unbiased structures like wiring diagrams. However, as the Cartographer paper illustrates, the problem of extracting expressions is closely related to the layout of diagrams for drawing, and it is used for that purpose in Catlab, being one of two layout algorithms supported. (The other layout algorithm is Graphviz dot, a layered graph drawing algorithm.) So there will always be uses for such techniques.

David Tanzer (Jul 07 2020 at 03:46):

Thanks @Fabrizio Genovese , @James Fairbanks and @Evan Patterson for your informative replies!

Aleks Kissinger (Jul 07 2020 at 10:13):

Fabrizio Genovese said:

Pawel, Paul and Fabio worked out a data structure that is not quite what we want, but very very close to it. From there, we were able to edit it here and there to finally obtain a data structure that represents string diagrams invariantly

I'm interested in what you mean by "invariant" here. One of the things that was always a pain Quantomatic was dealing concretely with graphs and graph rewriting, which are iso-invariant. This involves lots of fiddling with "names" of vertices and edges, with much of the code devoted to renaming and finding fresh names e.g to do direct sums and the like. Does your implementation get around those problems?

Fabrizio Genovese (Jul 07 2020 at 11:09):

Aleks Kissinger said:

Fabrizio Genovese said:

Pawel, Paul and Fabio worked out a data structure that is not quite what we want, but very very close to it. From there, we were able to edit it here and there to finally obtain a data structure that represents string diagrams invariantly

I'm interested in what you mean by "invariant" here. One of the things that was always a pain Quantomatic was dealing concretely with graphs and graph rewriting, which are iso-invariant. This involves lots of fiddling with "names" of vertices and edges, with much of the code devoted to renaming and finding fresh names e.g to do direct sums and the like. Does your implementation get around those problems?

What i mean is that, for instance, you can write the same string diagram as $(f;g) \otimes (h;k)$ and as $(f \otimes h);(g \otimes k)$. If you write a string diagram as a tree of tensors and compositions, those two things will be different trees. Instead, you want a data structure where those are literally the same thing.

Fabrizio Genovese (Jul 07 2020 at 11:10):

E.g, lists are naturally associative: If I denote a composition of morphisms as a list, then [f,g,h] both stands for $(f;g);h$ and $f;(g;h)$. In this sense, the list is naturally invariant wrt associativity

Aleks Kissinger (Jul 07 2020 at 11:26):

So, in your data structure, are any two descriptions of the same string diagram literally equal? Or are they equal upto some equivalence (e.g. alpha-conversion)?

Fabrizio Genovese (Jul 07 2020 at 12:29):

Aleks Kissinger said:

So, in your data structure, are any two descriptions of the same string diagram literally equal? Or are they equal upto some equivalence (e.g. alpha-conversion)?

Literally equal would be the dream. Actually the cartographer data structure goes very close to this modulo some slight reindexing

Fabrizio Genovese (Jul 07 2020 at 12:30):

So what we did is implementing everything in idris, and then we postulated that two terms are equal modulo reindexing

Alexis Toumi (Jul 07 2020 at 12:30):

@Fabrizio Genovese I'd be interested to know how things developed since the last time we had a chat about this in Tallinn!
Did you have a chance to get into nominal string diagrams? They felt like a good fix to the problem of alpha conversion etc. https://arxiv.org/abs/1904.07534

Fabrizio Genovese (Jul 07 2020 at 12:31):

It's quite fiddly, but in the end we managed to make it work :grinning:

Fabrizio Genovese (Jul 07 2020 at 12:32):

So the idea is that you create a type called "open hypegraph from l to m". This type is a record, so a term of this type is made of a bunch of other terms. Among those, there is this "wiring" which is just a permutation from a set of nats to another

Fabrizio Genovese (Jul 07 2020 at 12:32):

These nats represent indexings of boundaries and more importantly internal nodes. So you can re-index the internal nodes in any way you want, if you change the permutation accordingly you get the same thing

Fabrizio Genovese (Jul 07 2020 at 12:33):

so in the end we had to postulate this properties for idris typechecker not to complain.

Fabrizio Genovese (Jul 07 2020 at 12:33):

Let me see if we opened up our code already

Alexis Toumi (Jul 07 2020 at 12:33):

So this encoding works for hypergraph categories? or symmetric monoidal in general?

Fabrizio Genovese (Jul 07 2020 at 12:34):

https://github.com/statebox/fsm-oracle/blob/master/src/Cartographer/GoodHypergraphCategory.idr

Fabrizio Genovese (Jul 07 2020 at 12:34):

So, goodhypergraphSMC is the free symmetric strict monoidal category on a signature

Fabrizio Genovese (Jul 07 2020 at 12:35):

this is based on goodHypegraph which is a restriction of the hypegraph data structure, which is the one I was talking about.

Fabrizio Genovese (Jul 07 2020 at 12:35):

This is the hypegraph

Fabrizio Genovese (Jul 07 2020 at 12:35):

https://github.com/statebox/fsm-oracle/blob/master/src/Cartographer/Hypergraph.idr

Fabrizio Genovese (Jul 07 2020 at 12:35):

The postulate is on line 69.

Alexis Toumi (Jul 07 2020 at 12:35):

I think I remember this "good" business from the last time you explained this stuff. It's checking that each wire is connected to a single port on both ends?

Fabrizio Genovese (Jul 07 2020 at 12:36):

Yes, the idea is this: cartographer graphs can also form feedback loops, and we don't want them

Fabrizio Genovese (Jul 07 2020 at 12:37):

So we notice that:
A singleton hypegraph is free of loops
Permutations (hypegraphs with no internal nodes) are free of loops
Any composition and tensoring of those two building blocks is free of loops

Alexis Toumi (Jul 07 2020 at 12:37):

Do you know how much of this invariant encoding would work for non-symmetric cases?

Fabrizio Genovese (Jul 07 2020 at 12:37):

Like, you don't want symmetries around?

Fabrizio Genovese (Jul 07 2020 at 12:37):

This MAY make things easier, since the whole permutation business is a nightmare

Fabrizio Genovese (Jul 07 2020 at 12:38):

Maybe you could just rule the permutations bit out

Alexis Toumi (Jul 07 2020 at 12:38):

I'm wondering if the problem gets any easier if you solve it in two stages, first non-symmetric monoidal then symmetry and permutation nightmares?

Fabrizio Genovese (Jul 07 2020 at 12:38):

Nope, it doesn't

Fabrizio Genovese (Jul 07 2020 at 12:38):

because the problem IS the permutation nightmare xD

Fabrizio Genovese (Jul 07 2020 at 12:38):

So, for instance, our code is:

data GoodHypergraph : {s : Type} -> {ai, ao : s -> List o} -> (g : Hypergraph s ai ao k l) -> Type where
    Singleton : (edge : s) -> GoodHypergraph (singleton edge)
    Permutation : (p : Perm k l) -> GoodHypergraph (permutation p)
    HComp : (a : GoodHypergraph g)
         -> (b : GoodHypergraph h)
         -> GoodHypergraph (compose g h)
    VComp : (a : GoodHypergraph g)
         -> (b : GoodHypergraph h)
         -> GoodHypergraph (add g h)

Fabrizio Genovese (Jul 07 2020 at 12:39):

If you don't want to allow permutations you just rule them out in the record substituting them wit Identities

Fabrizio Genovese (Jul 07 2020 at 12:39):

So you want an identity datatype which is way easier than a permutation

Alexis Toumi (Jul 07 2020 at 12:40):

Don't you end up with factorial explosions when you try to handle permutations explicitly? Or did you manage to make the code lazy enough that it never actually run through all of them?

Fabrizio Genovese (Jul 07 2020 at 12:41):

So in this type signature s is the type of nodes (basic blocks), ai and ao are arity functions telling you inputs and outputs of wires, etc

Fabrizio Genovese (Jul 07 2020 at 12:41):

Alexis Toumi said:

Don't you end up with factorial explosions when you try to handle permutations explicitly? Or did you manage to make the code lazy enough that it never actually run through all of them?

You don't, because you don't deal with them explicitly

Alexis Toumi (Jul 07 2020 at 12:41):

Cool!

Alexis Toumi (Jul 07 2020 at 12:41):

I'm still curious whether/how nominal sets of wires would help for this nightmare

Fabrizio Genovese (Jul 07 2020 at 12:42):

If I write append to list :: a -> [a] -> [a] I'm not considering all lists over type a at once

Fabrizio Genovese (Jul 07 2020 at 12:42):

Nominal sets just hide permutations under the rug using a group action

Fabrizio Genovese (Jul 07 2020 at 12:42):

but guess what, we have to implement the group action anyway xD

Fabrizio Genovese (Jul 07 2020 at 12:42):

So at this point it was easier to use idris permutation library xD

Fabrizio Genovese (Jul 07 2020 at 12:43):

What would really help is HoTT

Fabrizio Genovese (Jul 07 2020 at 12:43):

Cos we could just use truncated types and define SMCs without constructing all this explicitly

Fabrizio Genovese (Jul 07 2020 at 12:45):

Which we did btw, actually @Fredrik Nordvall Forsberg did it for us: https://github.com/statebox/idris-ct/pull/32/files

Aleks Kissinger (Jul 07 2020 at 14:43):

Fabrizio Genovese said:

Aleks Kissinger said:

So, in your data structure, are any two descriptions of the same string diagram literally equal? Or are they equal upto some equivalence (e.g. alpha-conversion)?

Literally equal would be the dream. Actually the cartographer data structure goes very close to this modulo some slight reindexing

Yeah, this is basically what quanto does as well. I see Cartographer has a "HyperEdgeId" type, which is basically an int, which serves to give the hyperedge a unique (but meaningless) name, then you are always working modulo renaming. I don't know if there's really any way around that. There may even be some kind of "no free lunch" principle when it comes to data structures representing string diagrams

Aleks Kissinger (Jul 07 2020 at 14:49):

i've experimented some with representing string diagrams as Penrose abstract tensor systems (formalised using nominal algebra). theoretically, this looks quite nice. in practice, i lost weeks proving little lemmas about finite supports and equivarience in nominal isabelle, and never quite got it to understand the "obvious" way you can do equational reasoning with the abstract tensor notation.

Fabrizio Genovese (Jul 07 2020 at 15:05):

I think there is no way until we have a type theory that supports quotients well, like HoTT.