4 ms·

I kind of agree with you (especially on "math-lite category theory" being upvoted by people who read it and feel smart for understanding it), but I think the po

I kind of agree with you (especially on "math-lite category theory" being upvoted by people who read it and feel smart for understanding it), but I think the point has slightly been missed. The blog is a sort of side project, a popular treatment of the linear algebra stuff coming out of the "real research", which is applying the string diagrams to find graphical, compositional axiomatisations of concurrent systems. The programme has had some success with signal flow graphs (even making it onto the blog: https://graphicallinearalgebra.net/2016/09/07/31-fibonacci-and-sustainable-rabbit-farming/ https://graphicallinearalgebra.net/2016/09/07/31-fibonacci-a... ) and they were starting to look into Petri nets as my study was wrapping up. (source: I was a postgrad supervised by Pawel)

spekcular 6y ago
What "success" has this research program had with signal flow graphs? What problems has it helped solved? My impression is that it ends up being largely some kind of linguistic translation project, or abstraction for the sake of abstraction, but I'm happy to be corrected on this point.
- jshholland 6y ago
  We have a way to write traditional SFGs as string diagrams and an isomorphism to behaviours which respects the kind of graphical reasoning used in the blog. So you can show that two SFGs are behaviourally equivalent, or, using some more recent work, that all the behaviours of one are also behaviours of another, i.e. inclusion of sets of behaviours. String diagrams are also more general than SFGs, but can still be mapped to behaviours, so you could have an "unimplementable" string diagram to serve as a specification, and use the axiomatisation of inclusion to show that a particular SFG is a valid implementation of that spec. As for whether anyone outside the research programme is actually doing that, I don't know. But in principle it's a useful formal methods type theory.

spekcular 6y ago

What "success" has this research program had with signal flow graphs? What problems has it helped solved? My impression is that it ends up being largely some kind of linguistic translation project, or abstraction for the sake of abstraction, but I'm happy to be corrected on this point.

jshholland 6y ago
We have a way to write traditional SFGs as string diagrams and an isomorphism to behaviours which respects the kind of graphical reasoning used in the blog. So you can show that two SFGs are behaviourally equivalent, or, using some more recent work, that all the behaviours of one are also behaviours of another, i.e. inclusion of sets of behaviours. String diagrams are also more general than SFGs, but can still be mapped to behaviours, so you could have an "unimplementable" string diagram to serve as a specification, and use the axiomatisation of inclusion to show that a particular SFG is a valid implementation of that spec. As for whether anyone outside the research programme is actually doing that, I don't know. But in principle it's a useful formal methods type theory.