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: learning: questions

Topic: Rigorous string diagrams

Cole Comfort (Jul 10 2020 at 17:56):

Martti Karvonen said:

Jules Hedges said:

Wow.... I can imagine maybe having this opinion 10 years earlier, but by 1986 this was just flat out wrong

I'm sure there's still plenty of computer scientists who are skeptical of CT in TCS.

Yes, I remember the fellow who graded my undergraduate thesis wanted to fail me because "string diagrams aren't rigorous."

Jules Hedges (Jul 10 2020 at 19:28):

This view seems to be quite common. I think it's understandable, it's just also wrong, they need to be corrected by being introduced to the Joyal-Street paper

Martti Karvonen (Jul 16 2020 at 01:43):

Jules Hedges said:

This view seems to be quite common. I think it's understandable, it's just also wrong, they need to be corrected by being introduced to the Joyal-Street paper

To be fair, people use quite a lot of graphical languages for various kinds of cats, many of which weren't considered by Joyal-Street, and afaik people haven't done similar proofs for all of these elsewhere either.

Amar Hadzihasanovic (Jul 16 2020 at 09:05):

I think I've said it before, but I really don't think Joyal-Street is what "makes string diagrams rigorous". JS is a kind of local-to-global result saying that any such-and-such isotopy is sound for such-and-such monoidal categories, which means that it can be factorised into individual steps which are applications of the axioms of these monoidal categories.
But nobody gives diagrammatic proofs which are big complicated transformations all done at once! That would be unintelligible. Usually they are done in small steps where you can see with little work the individual axioms being applied. For the soundness of those there is no need for JS at all.

Amar Hadzihasanovic (Jul 16 2020 at 09:07):

I'm sure JS had a "social" impact in changing the perception of the rigour of diagrammatic proofs.

Amar Hadzihasanovic (Jul 16 2020 at 09:09):

But at the same time I think it's a bad idea to convince people that string diagrams are rigorous by saying "Look, there's this complicated paper involving a lot of topology which proves it all!" when actually it's much simpler than that.

Amar Hadzihasanovic (Jul 16 2020 at 09:12):

It's like convincing people that high school-level algebra of polynomials is rigorous by pointing them to Gröbner bases or something...

Amar Hadzihasanovic (Jul 16 2020 at 09:16):

And also, as Martti says, it opens the doors to responses like "Ah but there's no JS-style proof for balanced fusilli categories! That means you are not allowed to use diagrams with them!"

Jules Hedges (Jul 16 2020 at 10:30):

In general the result you use is "this class of diagrams (modulo bla bla bla) form the free wotsit on these generators". That makes it analogous to the corresponding result for 1d syntax, that strings on an alphabet form the free monoid

Jules Hedges (Jul 16 2020 at 10:31):

In general results like that are obvious but a nightmare to prove, but they can be proven if you care enough

Arthur Parzygnat (Jul 16 2020 at 10:53):

I'm sorry, what are the precise statements/qualms? From what I understood (colloquially---I have not read the paper in detail), JS show that given a decomposition of two morphisms in a hom-set of some symmetric monoidal category, these two morphisms are equal if and only if their corresponding graphs associated to those decompositions are isotopic. Or did they not actually prove this? Or is there some issue in some of these definitions?

Amar Hadzihasanovic (Jul 16 2020 at 10:56):

I disagree that Joyal-Street is analogous to “strings on an alphabet form the free monoid”. In the "free monoid" case you are passing from something quotiented by an equivalence relation to something free. In JS you are passing from something quotiented by an equivalence relation to something quotiented by a huge space of transformations. The “hard side” is the opposite.

Amar Hadzihasanovic (Jul 16 2020 at 10:58):

Hi Arthur, there's absolutely no issues about what Joyal-Street proved, nor with the fact that it's a great paper :)
The disagreement is about whether string diagrams need a Joyal-Street-type theorem to be “rigorous”. I do not think so.

Amar Hadzihasanovic (Jul 16 2020 at 11:00):

Jules: I think a better parallel would be between Joyal-Street and the statement that “Every permutation on a finite set can be factorised into a composition of permutations of two elements”.

Amar Hadzihasanovic (Jul 16 2020 at 11:00):

So, for instance, the equation ab = ba suffices to get the intended meaning of “commutative monoid”.

Amar Hadzihasanovic (Jul 16 2020 at 11:02):

Now my point is that even without this theorem, it is still perfectly sound to do a proof on “commutative monoids as presented by the equation ab = ba” using steps like abc = bac = bca = cba

Amar Hadzihasanovic (Jul 16 2020 at 11:04):

“Using Joyal-Street in a diagrammatic proof” is analogous to “showing that two expressions are equal in a commutative monoid by giving an actual bijection of all their terms”

Amar Hadzihasanovic (Jul 16 2020 at 11:05):

Which nobody would ever do...

James Wood (Jul 16 2020 at 11:11):

Isn't it taken as given that rearranging symbols on a page in principle does give rise to a bijection? Similarly to how string diagram manipulations in principle give rise to an isotopy? So in both cases, the theorem is necessary if you want to be fully rigorous, but not sufficient for formal proof.

Martti Karvonen (Jul 16 2020 at 14:19):

Amar Hadzihasanovic said:

I think I've said it before, but I really don't think Joyal-Street is what "makes string diagrams rigorous". JS is a kind of local-to-global result saying that any such-and-such isotopy is sound for such-and-such monoidal categories, which means that it can be factorised into individual steps which are applications of the axioms of these monoidal categories.
But nobody gives diagrammatic proofs which are big complicated transformations all done at once! That would be unintelligible. Usually they are done in small steps where you can see with little work the individual axioms being applied. For the soundness of those there is no need for JS at all.

Just to check I'm following: roughly, you're saying that soundness of diagrammatic proofs of the kind people actually write down rests on our ability to compile them into "honest proofs" if need be. Is that the claim?

Reid Barton (Jul 16 2020 at 14:29):

Well, it relies on being able to do at least one of the following two things:

1. Write down an "honest proof" -- by which I assume you mean a direct application of the axioms;
2. Write down an actual isotopy (say, by a formula), and then check a long list of conditions (e.g., that it really is an isotopy, and carries one of the diagrams you're claiming equal onto the other one, and preserves directedness of the "wires" at all intermediate times, etc.), and then apply the Joyal-Street theorem.

Reid Barton (Jul 16 2020 at 14:30):

If you were going to actually do one of these (say, for the purpose of machine formalization) it's hard for me to imagine that the second option would ever be easier than the first.

Martti Karvonen (Jul 16 2020 at 14:35):

I'm thinking about the cases that Joyal-Street didn't consider ("balanced fusilli categories" or whatever).

Reid Barton (Jul 16 2020 at 14:39):

I am arguing that even in the basic case of monoidal categories, string diagram reasoning is "rigorous" but not due to the Joyal-Street theorem, but rather because practitioners know how to read a sequence of string diagrams as a blueprint for an "honest proof".

Reid Barton (Jul 16 2020 at 14:52):

Here is another perspective. The Joyal-Street theorem is a theorem about real numbers and continuous functions. As such, it seems plausible that it uses some fact about continuous functions (like the intermediate value theorem) which is true classically but not in all constructive settings. Suppose for the sake of argument that it actually does use such a fact. Would you conclude that proofs by string diagram are valid classically but not constructively?

James Wood (Jul 16 2020 at 15:02):

string diagram reasoning is "rigorous" but not due to the Joyal-Street theorem, but rather because practitioners know how to read a sequence of string diagrams as a blueprint for an "honest proof".

I agree with this, but also claim the following: if we were to convince an outsider of the rigour of string diagrams, we would point them to Joyal-Street. It's reasonable to expect a general mathematician to reproduce an isotopy from pictures, in a similar process to how they will reproduce a proof from a typical written proof. It's less reasonable to get them to learn how to reproduce monoidal category equations from pictures from first principles.

Martti Karvonen (Jul 16 2020 at 15:09):

Reid Barton said:

I am arguing that even in the basic case of monoidal categories, string diagram reasoning is "rigorous" but not due to the Joyal-Street theorem, but rather because practitioners know how to read a sequence of string diagrams as a blueprint for an "honest proof".

Yes I agree, I just wanted to check that this was indeed what was being claimed.

Amar Hadzihasanovic (Jul 16 2020 at 15:40):

Yes, Reid said exactly what I meant, better than I could.

Amar Hadzihasanovic (Jul 16 2020 at 15:55):

By the way, there's a different issue which is the possibility of interpreting a diagram (prior to any quotient) univocally in some model. That's called a "pasting theorem" and it is indeed necessary to make diagrammatic reasoning rigorous! In 2D for monoidal categories, however, it is simple enough once you have Mac Lane's coherence theorem.

Jules Hedges (Jul 16 2020 at 17:01):

Ok, I see where the confusion comes from. I do not like to think about diagrammatic proof as a thing from which you can recover an honest proof. I like to think about diagrammatic proof as literally an honest proof by itself (technically there is always one implicit step, which is that there is an isotopy - that part is left as an exercise for the reader's primary visual cortex

Jules Hedges (Jul 16 2020 at 17:02):

For this you need to know that your intended semantics is an invariant for isotopy, which is what the coherence theorem says

James Wood (Jul 16 2020 at 17:34):

(technically there is always one implicit step, which is that there is an isotopy - that part is left as an exercise for the reader's primary visual cortex

This is basically what everyone else is talking about, right? Definitely, an isotopy fed into the Joyal-Street proof itself constitutes an honest proof, but this pushes the question back from honest proof to honest isotopy.

Jules Hedges (Jul 16 2020 at 17:44):

Right, but I'm claiming that somebody still needs to do the proof of J-S to know that this procedure always works, and that proof is not trivial

Jules Hedges (Jul 16 2020 at 17:45):

On the other hand I know that Amar knows a lot more than me about these kind of issues, so I'm kind of wondering what I've missed

Martti Karvonen (Jul 16 2020 at 18:43):

I do not like to think about diagrammatic proof as a thing from which you can recover an honest proof. I like to think about diagrammatic proof as literally an honest proof by itself

I'm not sure why the first stance should be disparaged. In a sense, most of math papers aren't about writing honest proofs anyway - rather, they're about giving the (expert) reader a recipe to construct one, should they wish to do so ("an easy induction shows that..."). Moreover, if you also insist that

I'm claiming that somebody still needs to do the proof of J-S to know that this procedure always works, and that proof is not trivial

then all string diagrams not covered by J-S (or someone else) are not rigorous, such as the string diagrams used to reason about a (lax) monoidal functor afaik. While proving similar theorems for more graphical languages is indeed desirable, Amar is arguing that using diagrammatic languages not covered by J-S-style proofs still count as rigorous (enough), provided one can (in principle) read off equations/(pasting) diagrams etc from the proof steps.

Jules Hedges (Jul 16 2020 at 19:04):

Ah, I think I see now

Jules Hedges (Jul 16 2020 at 19:04):

Hm, this is a really subtle issue

Jules Hedges (Jul 16 2020 at 19:07):

Martti Karvonen said:

then all string diagrams not covered by J-S (or someone else) are not rigorous, such as the string diagrams used to reason about a (lax) monoidal functor afaik

And I would indeed claim that they are not entirely rigorous (but personally I'm happy to use such languages anyway, because the coherence theorem is always obvious enough to feel like a safe thing to rely on as a conjecture)

Jules Hedges (Jul 16 2020 at 19:08):

I never considered the string diagram as a representation of an "underlying" proof before. Maybe you're right... need to think about that a bit

Martti Karvonen (Jul 16 2020 at 19:36):

As long as one isn't writing machine-checkable proofs, the difference between an "honest proof" and a recipe for one seems to be largely a matter of taste/familiarity/convention. So if/when everyone involved is used to string diagrams, they arguably are honest proofs in the same sense that ordinary (non-machine checkable) mathematical proofs are. One could also ask what's the "underlying proof" of the proof you get once you've replaced the string diagrams with say equations - there's still probably all kinds of stuff left implicit.

Morgan Rogers (he/him) (Jul 16 2020 at 19:38):

I am mildly amused by this discussion, since I believe everyone involved can agree that string diagrams are a valid/sufficiently rigorous method of proof (be it in themselves or as diagrammatic representations of some other formalism), while on the other hand any of the absent people who have made the argument that they aren't rigorous are more likely to have done so out of ignorance than from any evidence. It might be surprising to the uninitiated that string diagrams can be rigorous, because they are so different in form to the symbolic manipulation that they are used to. Yet, even in cases where they are being used as a calculus for some formal system which they haven't been proven to be a completely sound model of (by which I mean, a situation in which there could be some operation on a string diagram which is possible but doesn't represent a valid transformation on the formal system side), the 'potential for a step-by-step translation to "honest proof"' comes from an implicit proof of soundness of particular operations on the string diagrams, which therefore validate the string diagram calculations directly in situ.

John Baez (Jul 16 2020 at 20:45):

Jules Hedges said:

Ok, I see where the confusion comes from. I do not like to think about diagrammatic proof as a thing from which you can recover an honest proof. I like to think about diagrammatic proof as literally an honest proof by itself (technically there is always one implicit step, which is that there is an isotopy - that part is left as an exercise for the reader's primary visual cortex

Yes, I think this is an interesting fault line. Are diagrams just a thing from which you can recover an "honest proof", or can we call diagrammatic proofs "honest proofs"?

One could ask the same question for the usual proofs mathematicians write in papers. Are they just things from which you can recover an "honest proof" based on syntactically manipulating axioms the way a proof assistant would, or are they "honest proofs"?

I have no strong opinion about these questions. I tend to treat mathematics as a human activity, with a proof being a method of convincing other people that something is true. So, to me a written argument, or a series of pictures, or a verbal argument counts as an "honest proof" if the person it's addressed to understands it.... which in part means being able to fill in more detail if it's demanded.

This is a somewhat old-fashioned attitude now that a lot of people are dreaming of the day when people become somewhat obsolete and computerized mathematics is what counts as "honest" proof. But I don't care - if and when that day ever comes, I'll be doing something else: perhaps composing music, perhaps pushing up daisies.

Peter Arndt (Jul 16 2020 at 20:47):

This was very helpful for me to read. I never understood what string diagrams are meant to represent, and now I know a few view points - and in particular that there isn't a single view point. I should read Joyal-Street.

Jules Hedges (Jul 16 2020 at 21:03):

The practical question is: Is it conceivable (however unlikely) that a diagrammatic "proof" (of some class with no currently proven coherence theorem) could lead to a false conclusion? I thought that the answer was yes

Amar Hadzihasanovic (Jul 16 2020 at 21:36):

So, I'll start with some slight pedantry: Joyal-Street is not a coherence theorem.
A coherence theorem is a statement that “certain types are contractible” to use HoTT-jargon. Or “certain sets are singletons” in more classical cases. For example, Mac Lane's coherence for monoidal categories is the statement that “all hom-sets are singletons” in the free monoidal category on a set of objects, where the “theory of monoidal categories” is presented in the usual way by pentagon+triangle equations.
Joyal-Street is a more traditional “soundness and completeness” theorem (the axioms of (S)MCs are sound and complete for a certain isotopy relation between certain diagrams).

Amar Hadzihasanovic (Jul 16 2020 at 21:41):

As it is the two are independent. Without Mac Lane's coherence J-S would still be a valid theorem about strict monoidal categories. Coherence extends it to general monoidal categories, because it provides a pasting theorem for general monoidal categories, in the sense that I mentioned earlier.

Amar Hadzihasanovic (Jul 16 2020 at 21:41):

Now to answer your question:
I think that the lack of a coherence theorem can very easily lead to wrong diagrammatic proofs, where the error would lie before any manipulations are actually applied, at the level of “lack of a pasting theorem”.

Amar Hadzihasanovic (Jul 16 2020 at 21:43):

Basically we could draw a diagram in which two different structural morphisms of the same type in the non-coherent model are represented by the same diagram, falsely assuming coherence.

Jules Hedges (Jul 16 2020 at 21:43):

Amar Hadzihasanovic said:

So, I'll start with some slight pedantry: Joyal-Street is not a coherence theorem.

So this is something I've wondered about. I just checked for sanity that it's not only me that says this. Selinger's survey calls these results "coherence theorems" consistently throughout. My understanding has always been that there are 2 more-or-less unrelated classes of results that get called "coherence theorems", but I always wondered if they were secretly related

Amar Hadzihasanovic (Jul 16 2020 at 21:44):

And that would already be a false diagrammatic proof of the equality of those two morphisms. :)

Amar Hadzihasanovic (Jul 16 2020 at 21:46):

Jules Hedges said:

So this is something I've wondered about. I just checked for sanity that it's not only me that says this. Selinger's survey calls these results "coherence theorems" consistently throughout.

Yes! I am telling this here not as an “obvious fact”, but as something which it took me a very long time to understand, precisely because very different results are often conflated, including in Selinger's survey.

Jules Hedges (Jul 16 2020 at 21:50):

So refinement of the question: If there is a class of categories for which there is a known "everything is equivalent to a strict thing" theorem but not a known "the free thing is diagrams modulo isotopy" theorem, is it conceivable that a diagrammatic proof could go wrong?

Amar Hadzihasanovic (Jul 16 2020 at 21:52):

So my hunch is that, bar the coherence issues, there are a couple of possible types of errors. One is “simply” doing unsound things on single steps but that's not really specific to diagrammatic reasoning.

Amar Hadzihasanovic (Jul 16 2020 at 21:52):

Like, it's the same kind of error as “doing a cancellation in a non-cancellative monoid” because using cancellation is so ingrained in our equational reasoning...

Amar Hadzihasanovic (Jul 16 2020 at 21:53):

But that's also independent of whether we have a J-S type theorem.

Amar Hadzihasanovic (Jul 16 2020 at 21:55):

The only way I can imagine an error “due to lack of a J-S type theorem” would be to have a step which somehow goes out of step-by-step diagram manipulation.

Jules Hedges (Jul 16 2020 at 21:57):

Like, there is an isotopy but it necessarily has to pass through an invalid diagram?

Amar Hadzihasanovic (Jul 16 2020 at 21:57):

For example, say you have two diagrams of some kind, and there is a theorem in topology which says that any two diagrams with the same Hedges number are related by a Hedges transformation.

Amar Hadzihasanovic (Jul 16 2020 at 21:58):

You calculate that the two diagrams have the same Hedges number and conclude that there is a Hedges transformation. Then you falsely assume that the axioms of your model are complete for Hedges transformations.

Amar Hadzihasanovic (Jul 16 2020 at 21:59):

And conclude that the two diagrams are equal in the model.

Jason Erbele (Jul 16 2020 at 21:59):

Basically you'd be assuming a completeness result where only soundness is true?

Amar Hadzihasanovic (Jul 16 2020 at 22:00):

Yeah, I can see that happening...

Jules Hedges (Jul 16 2020 at 22:01):

So soundness can fail, but maybe those are just silly examples. For example you could try to draw string diagrams in a premonoidal category, and it would go horribly wrong. Then a diagram doesn't even uniquely define a morphism

Amar Hadzihasanovic (Jul 16 2020 at 22:02):

Agreed, that's what I called “lack of a pasting theorem”, you don't even know how to systematically soundly interpret the diagrams you're drawing.

Amar Hadzihasanovic (Jul 16 2020 at 22:06):

Another example is having a formalisation of 2D string diagrams where “scalars strictly commute” and trying to interpret that as 2-cells of a tricategory...

Jason Erbele (Jul 16 2020 at 22:10):

So given a pasting theorem, but lacking a J-S type theorem, and assuming the step-by-step manipulations are carried out correctly (as that's an error type that can appear anywhere), it sounds to me like the only error you could make involves falsely assuming/concluding the diagrammatic calculus is complete: "These two diagrams represent the same morphism, therefore there is a valid diagrammatic manipulation to get from one diagram to the other." Is that correct?

Amar Hadzihasanovic (Jul 16 2020 at 22:12):

Yes, thank you for the summary!
That's just what comes to my mind, btw -- maybe there's other cases that I haven't though about.

Jules Hedges (Jul 16 2020 at 22:13):

I'm struggling to get my head around the idea of having soundness but not completeness for a diagrammatic language.... I never really thought about it in logical terms but as "diagrams form the free thing", which I think conflates both together

Jules Hedges (Jul 16 2020 at 22:15):

Oh wait, I see. "Diagrams form the free thing" is just soundness. Since I nearly always work with non-complete languages I wasn't even thinking about it...

Amar Hadzihasanovic (Jul 16 2020 at 22:15):

(Maybe, rather than “represent the same morphism” I would say “are equal modulo some relation” -- the error would be exactly that they are not actually interpreted as the same morphism, because the axioms for the class of models that we are considering are not complete for that relation.)

Jules Hedges (Jul 16 2020 at 22:18):

Jason Erbele said:

"These two diagrams represent the same morphism, therefore there is a valid diagrammatic manipulation to get from one diagram to the other." Is that correct?

I don't see why anyone would ever write that though. Manipulating diagrams is much easier than checking morphisms for equality, so you'd generally be reasoning the other way - that's just what I call a "diagrammatic proof"

Martti Karvonen (Jul 16 2020 at 22:25):

Jules Hedges said:

Oh wait, I see. "Diagrams form the free thing" is just soundness. Since I nearly always work with non-complete languages I wasn't even thinking about it...

Isn't it both soundness and completeness? If an equation that was true for _all_ relevant things was not derivable from the equations, then it wouldn't be true in the syntactic structure you build out of the diagrams despite being true in the free thing.

Jason Erbele (Jul 16 2020 at 22:48):

Jules Hedges said:

Jason Erbele said:

"These two diagrams represent the same morphism, therefore there is a valid diagrammatic manipulation to get from one diagram to the other." Is that correct?

I don't see why anyone would ever write that though. Manipulating diagrams is much easier than checking morphisms for equality, so you'd generally be reasoning the other way - that's just what I call a "diagrammatic proof"

Perhaps the contrapositive would be an easier error to make: "There is no valid diagrammatic manipulation that can get you from one diagram to the other, therefore the two diagrams represent different morphisms." This kind of statement would only be valid in a complete language (even if it's true for the particular diagrams in an incomplete language – e.g. two diagrams with different arities).

John Baez (Jul 16 2020 at 23:35):

There's a certain limited but extremely important use of calculi of all sorts (diagram languages, logics, etc.), which is to show that things are equal, and for this soundness is enough. From this point of view, completeness is mainly to reassure ourselves that "we're not missing any tricks".

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

Yes, that's exactly how I see completeness: Completeness for string diagrams for me means "I can prove stuff diagrammatically. If I cannot, then I cannot equationally."

Jules Hedges (Jul 17 2020 at 10:42):

Ok, this makes total sense. Soundness allows you to do diagrammatic proofs of equality. Completeness allows you to do diagrammatic proofs of non-equality, either by eyeballing or by finding some geometric invariant that can distinguish your 2 diagrams

Fabrizio Genovese (Jul 17 2020 at 10:54):

Yes, this is particularly evindent when you think about soundess as $A \to B$, and about completeness as $B \to A$. Hence completeness is also $\neg A \to \neg B$.

Bob Haugen (Aug 15 2020 at 20:29):

Is there a difference between string diagrams and wiring diagrams? I see both being used in "Seven Sketches in Compositionality" https://arxiv.org/pdf/1803.05316.pdf but "wiring diagram" 116 times and "string diagram" 4 times.
Are they different words for the same type of diagram? Or do they have different meanings?
If different words for the same type of diagram, which is generally preferred by applied category theorists?

Evan Patterson (Aug 15 2020 at 23:24):

String diagrams and wiring diagrams are closely related in that both represent composites of morphisms in a monoidal category. The main difference is that string diagrams, in the sense of Joyal and Street, are geometric objects inhabiting two, three, or four dimensional space, whereas wiring diagrams are combinatorial objects not embedded in space. So, as a rough analogy, wiring diagrams are to string diagrams as graphs are to geometric graphs. The geometric perspective on string diagrams gets center stage in Selinger's survey of graphical languages, which talks a lot about isotopy of diagrams.

Evan Patterson (Aug 15 2020 at 23:27):

In my computational work, I exclusively use wiring diagrams, for the same reason that most people compute with graphs rather than geometric graphs.

Jules Hedges (Aug 16 2020 at 09:47):

I have never heard that distinction before

Jules Hedges (Aug 16 2020 at 09:49):

My answer would have been that the term "wiring diagram" is used for 2 different things: in the context of Spivak's wiring diagrams operad, and separately as a synonym for string diagrams

Bob Haugen (Aug 16 2020 at 11:03):

@Evan Patterson @Jules Hedges thanks for the responses. What would you call the lemon meringue pie diagram in "Seven Sketches", wiring or string?

Reason for asking: we decided to use that type of diagram as our standard way to document resource flows in economic networks, as you can see here: https://github.com/valueflows/valueflows/issues/507 (which includes that diagram, if you are not familiar with it, but I expect you are...)

We were inspired by that and other similar diagrams, and thought they were called string diagrams. But our diagrams are usually not embedded in space, they are more abstract diagrams of the directions, sources, and destinations of flows of resources by resource type. But we also cite applied category theory as the source of the diagramming format, and would like to call them by the correct name.

Jules Hedges (Aug 16 2020 at 12:23):

I don't know the right terminology was this (and until this morning I wasn't aware that there was any candidate terminology). Personally I use "string diagram" to refer to both the geometric and combinatorial version, same as eg. I use "simplex" to refer to both the geometric and combinatorial version. Curious to see how many people disagree with me...

Bob Haugen (Aug 16 2020 at 13:30):

Bob Haugen said:

our diagrams are usually not embedded in space, they are more abstract diagrams of the directions, sources, and destinations of flows of resources by resource type.

So analogous to electrical wiring diagrams, that would be a schematic rather than architectural diagram.

Fabrizio Genovese (Aug 16 2020 at 14:40):

"Wiring Diagrams" is also used in the work of Spivak, Valilakopoulou et al to denote diagrams which compose following lens-like rules. These are quite useful but I think they are way less general objects that string diagrams are.

Fabrizio Genovese (Aug 16 2020 at 14:40):

I think one thing to _really_ keep in mind is that "string diagrams = graphical calculus for some flavor of free category". Freeness is a very nice property: A free object of some sort can be thought of as the most general object of its kind, and as such it can always be mapped to other object of the same kind quite effortlessly.

Fabrizio Genovese (Aug 16 2020 at 14:43):

This means that when you use string diagrams, you get a very easy way to build functors mapping your morphisms to other similar cats. I am not an expert of the operadic formalism, but I don't know if this still holds in that setting. Personally, freeness is exactly what makes string diagrams useful for my research. String diagrams are also the preferred graphical formalism, by a great measure, both in categorical quantum mechanics and in categorical linguistics.

Bob Haugen (Aug 16 2020 at 17:19):

@Fabrizio Genovese thanks. Given those criteria, would you say that the lemon meringue pie diagram is a string diagram?

(I don't understand lens-like rules or free categories so can't tell. Or you or somebody else could point me to a reference that would explain those concepts.)

Bob Haugen (Aug 16 2020 at 17:25):

Ok, from https://julesh.com/2018/08/16/lenses-for-philosophers/ it looks like this defines the lens rules: http://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/www/FrankOlesThesis.pdf

Reading.........way over my head...sorry.

This is easier, I might be able to get it: https://ncatlab.org/nlab/show/lens+%28in+computer+science%29

Evan Patterson (Aug 16 2020 at 17:47):

Jules Hedges said:

I have never heard that distinction before

I know David Spivak makes this distinction, and I find it a useful one. I don't know how common it is. I guess less so than I thought!

Evan Patterson (Aug 16 2020 at 18:11):

Bob Haugen said:

Evan Patterson Jules Hedges thanks for the responses. What would you call the lemon meringue pie diagram in "Seven Sketches", wiring or string?

Even if you accept this distinction, you could call it either and people would understand what you mean. Although there are significant differences between the combinatorial and geometric approaches (e.g. wiring diagrams have not been worked out for braided monoidal categories, AFAIK, only symmetric ones), for the purpose of communicating to a human a composite of morphisms in an SMC, it doesn't matter how you think about the diagram.

OTOH, in your computational setting, you probably want the combinatorial notion. I'd prefer to call that a "wiring diagram," but as the other replies indicate the term "string diagram" is also used as a catchall for diagrams like this.

Bob Haugen (Aug 16 2020 at 18:17):

@Evan Patterson "wiring diagram" has the additional advantage that a lot of people already have a vague notion of what it means whereas "string diagram" is new to most people.

(On the other hand, we are not really doing electrical wiring diagrams for the most part, but we have done electrical system diagrams using the same style so I think it fits.)

Thanks a lot for the conversation. I'll switch to "wiring diagram" and see how it flies.

Bob Haugen (Aug 17 2020 at 18:37):

I'm writing a blog post about string and wiring diagrams. Here's the current text, not yet published. It will include several example diagrams. It's the first in a series of posts about different styles of diagrams for economic networks.

I'm posting it here to show y'all where I went with this conversation. Haven't settled on "wiring diagram" yet, waiting for feedback from the projects mentioned.

I would of course be grateful for any tips on errors or suggestions for improvement, but I'm not expecting anybody to do a lot of work.

Economic network pictures: string or wiring diagrams

This is what we have mostly used so far in two related projects, https://valueflo.ws/ and https://github.com/holo-rea

The diagrams show strings or wires or arrows between nodes, which can be individual or group Agents or Processes or Exchanges or any mixture thereof, at any level of abstraction or aggregation that suits the purpose of the diagram.

For example, you could use individual Agents, or group Agents, or types of Agents, or Agents performing some function like farmers. You could use small or large-grained Processes.

The arrows are directed, from one node to another node, and Economic Resources ride on them. You could depict the Resources as labels on the arrows or separate named shapes.

The Resources are usually abstract rather than tangible: Resource Specifications or classifications or taxonomy items at any level of specificity. For example, an arrow could show Fruit, or Apples, or Granny Smith Apples, or Organic Apples from Eve's Orchard (which is a real place).

The Resources on the arrows could be quantified, and if so, you could vary the width of the arrow according to the quantity of the Resources on it, creating something like a Sankey diagram.

The shapes don't matter, only that the reader be able to distinguish nodes from arrows and resources. The style as we use it is very flexible, but it's good to be consistent within a family of diagrams or a family of projects.

The diagram style comes from the Applied Category Theory community, where they use them with mathematical rigor and consider them the logical equivalent of code or proofs. We will not try to use them so rigorously...yet. None of us understands enough Category Theory to do that, and we have not yet attracted any experienced Category Theorists (Catsters) to help us. But becoming more mathematically rigorous with our diagrams would be a good research project for somebody, and would probably enable some new and interesting capabilities.

Two capabilities emerge easily:

1. If a node has a resource arrow as an input but the arrow has no source, another node could be connected which can provide that resource as an output. Same with node with a resource arrow as an output but no destination, another node could be connected that wants that resource as an input. Likewise with resource arrows with quantities: if the source or destination quantity is less than the resource arrow quantity, other nodes could be connected to take up the slack.

2. Our diagrams are already rigorous enough to be able to be generated programmatically from data. Here are a couple of not-very-good proofs of concept that could be improved:

• http://valueflows.pythonanywhere.com/vocab/egg2worm-flow/
• http://locecon.org/clusters/network/11/
  More rigor might allow generating code and data from diagram.

The name of the diagram style varies from one Catster publication to another. They mostly say String Diagram, but sometimes Wiring Diagram. Some of them consider those names to be synonomyms, some them assign different meanings to each name. I asked them which name we should use and the rough consensus seemed to be, if we are just using the diagrms to communicate with humans, it doesn't matter. If we become more rigorous and use the diagrams as code, it might matter.

Here is an overview and a bunch of references about string diagrams from a category theory viewpoint: https://ncatlab.org/nlab/show/string+diagram

Fabrizio Genovese (Aug 17 2020 at 19:27):

Bob Haugen said:

Fabrizio Genovese thanks. Given those criteria, would you say that the lemon meringue pie diagram is a string diagram?

(I don't understand lens-like rules or free categories so can't tell. Or you or somebody else could point me to a reference that would explain those concepts.)

I would say that the lemon meringue pie is a string diagram, yes.

Fabrizio Genovese (Aug 17 2020 at 19:28):

Bob Haugen said:

Evan Patterson "wiring diagram" has the additional advantage that a lot of people already have a vague notion of what it means whereas "string diagram" is new to most people.

(On the other hand, we are not really doing electrical wiring diagrams for the most part, but we have done electrical system diagrams using the same style so I think it fits.)

Thanks a lot for the conversation. I'll switch to "wiring diagram" and see how it flies.

This also depends on who you are talking to. For sure, string diagrams are much older and well studied than wiring diagrams in category theory, the latter being a relatively new thing. So I would guess that the average category theorist is more familiar with string diagrams than with wiring diagrams... :smile:

Bob Haugen (Aug 17 2020 at 20:35):

@Fabrizio Genovese thank you very much! As you can see from my draft blog post, i backpedaled a bit from switching to wiring diagram.