Today I’m going to this workshop:
• Higher-Dimensional Rewriting and Applications, 28-29 June 2015, Warsaw, Poland.
Many of the talks will be interesting to people who are trying to use category theory as a tool for modelling networks!
For example, though they can’t actually attend, Lucius Meredith and my student Mike Stay hope to use Google Hangouts to present their work on Higher category models of the π-calculus. The π-calculus is a way of modelling networks where messages get sent here and there, e.g. the internet. Check out Mike’s blog post about this:
• Mike Stay, A 2-categorical approach to the pi calculus, The n-Category Café, 26 May 2015.
Krzysztof Bar, Aleks Kissinger and Jamie Vicary will be speaking about Globular, a proof assistant for computations in n-categories:
This talk is a progress report on Globular, an online proof assistant for semistrict higher-dimensional rewriting. We aim to produce a tool which can visualize higher-dimensional categorical diagrams, assist in their construction with a point-and-click interface, perform type checking to prevent incorrect composites, and automatically handle the interchanger data at each dimension. Hosted on the web, it will have a low barrier to use, and allow hyperlinking of formalized proofs directly from research papers. We outline the theoretical basis for the tool, and describe the challenges we have overcome in its design.
Eric Finster will be talking about another computer system for dealing with n-categories, based on the ‘opetopic’ formalism that James Dolan and I invented. And Jason Morton is working on a computer system for computation in compact closed categories! I’ve seen it, and it’s cool, but he can’t attend the workshop, so David Spivak will be speaking on his work with Jason on the theoretical foundations of this software:
We consider the linked problems of (1) finding a normal form for morphism expressions in a closed compact category and (2) the word problem, that is deciding if two morphism expressions are equal up to the axioms of a closed compact category. These are important ingredients for a practical monoidal category computer algebra system. Previous approaches to these problems include rewriting and graph-based methods. Our approach is to re-interpret a morphism expression in terms of an operad, and thereby obtain a single composition which is strictly associative and applied according to the abstract syntax tree. This yields the same final operad morphism regardless of the tree representation of the expression or order of execution, and solves the normal form problem up to automorphism.
Recently Eugenia Cheng has been popularizing category theory, touring to promote her book Cakes, Custard and Category Theory. But she’ll be giving two talks in Warsaw, I believe on distributive laws for Lawvere theories.
As for me, I’ll be promoting my dream of using category theory to understand networks in electrical engineering. I’ll be giving a talk on control theory and a talk on electrical circuits: two sides of the same coin, actually.
• John Baez, Jason Erbele and Nick Woods, Categories in control.
If you’ve seen a previous talk of mine with the same title, don’t despair—this one has new stuff! In particular, it talks about a new paper by Nick Woods and Simon Wadsley.
Abstract. Control theory is the branch of engineering that studies dynamical systems with inputs and outputs, and seeks to stabilize these using feedback. Control theory uses “signal-flow diagrams” to describe processes where real-valued functions of time are added, multiplied by scalars, differentiated and integrated, duplicated and deleted. In fact, these are string diagrams for the symmetric monoidal category of finite-dimensional vector spaces, but where the monoidal structure is direct sum rather than the usual tensor product. Jason Erbele has given a presentation for this symmetric monoidal category, which amounts to saying that it is the PROP for bicommutative bimonoids with some extra structure.
A broader class of signal-flow diagrams also includes “caps” and “cups” to model feedback. This amounts to working with a larger symmetric monoidal category where objects are still finite-dimensional vector spaces but the morphisms are linear relations. Erbele also found a presentation for this larger symmetric monoidal category. It is the PROP for a remarkable thing: roughly speaking, an object with two special commutative dagger-Frobenius structures, such that the multiplication and unit of either one and the comultiplication and counit of the other fit together to form a bimonoid.
• John Baez and Brendan Fong, Circuits, categories and rewrite rules.
Abstract. We describe a category where a morphism is an electrical circuit made of resistors, inductors and capacitors, with marked input and output terminals. In this category we compose morphisms by attaching the outputs of one circuit to the inputs of another. There is a functor called the ‘black box functor’ that takes a circuit, forgets its internal structure, and remembers only its external behavior. Two circuits have the same external behavior if and only if they impose same relation between currents and potentials at their terminals. This is a linear relation, so the black box functor goes from the category of circuits to the category of finite-dimensional vector spaces and linear relations. Constructing this functor makes use of Brendan Fong’s theory of ‘decorated cospans’—and the question of whether two ‘planar’ circuits map to the same relation has an interesting answer in terms of rewrite rules.
The answer to the last question, in the form of a single picture, is this:
(Click to enlarge.) How can you change an electrical circuit made out of resistors without changing what it does? 5 ways are shown here:
- You can remove a loop of wire with a resistor on it. It doesn’t do anything.
- You can remove a wire with a resistor on it if one end is unattached. Again, it doesn’t do anything.
- You can take two resistors in series—one after the other—and replace them with a single resistor. But this new resistor must have a resistance that’s the sum of the old two.
- You can take two resistors in parallel and replace them with a single resistor. But this resistor must have a conductivity that’s the sum of the old two. (Conductivity is the reciprocal of resistance.)
- Finally, the really cool part: the Y-Δ transform. You can replace a Y made of 3 resistors by a triangle of resistors But their resistances must be related by the equations shown here.
For circuits drawn on the plane, these are all the rules you need! This was proved here:
• Yves Colin de Verdière, Isidoro Gitler and Dirk Vertigan, Réseaux électriques planaires II.
It’s just the beginning of a cool story, which I haven’t completely blended with the categorical approach to circuits. Doing so clearly calls for 2-categories: those double arrows are 2-morphisms! For more, see:
• Joshua Alman, Carl Lian and Brandon Tran, Circular planar electrical networks I: The electrical poset EPn.
Azimuth 
These rules for planar resistor circuits are beautiful. But I don’t see why they have to be interpreted as 2-morphisms in a 2-category, rather than simply as generators of morphism equality in a 1-category.
I’m not claiming that these rules have to be interpreted as 2-morphisms, just that it’s a fun thing to do.
If we impose them as equations, we get an interesting category where morphisms are ‘behaviors’ of planar electrical circuits: two circuits can look different yet behave the same way. More mathematically speaking, if we impose them as equations we get a category that’s the ‘full image’ of the black box functor
■:
which sends circuits to their behaviors.
If we don’t impose them at all, we get the category PlaneCirc.
But if we work 2-categorically and impose them as 2-morphisms we can ‘have our cake and eat it too’, getting a single structure that knows both about circuits and their behaviors.
This is my standard mantra about higher categorical structures: they let you talk about how things are ‘the same in a way, yet not identical’. I’ve been slacking off on higher category theory lately, trying to understand network theory with categories, but the higher categorical approach will eventually be good to try.
And we can do it using your program Globular! I’m eager to see it on a web browser.
Eugenia Cheng’s book is sold in North America under a different name: “How to Bake Pi: An Edible Exploration of the Mathematics of Mathematics.” I thought part I of the book was great. Part II seems to be missing a punchline, but it is hard to say how one would have done it better.
It was fun talking to Eugenia; she’s now in Ireland doing interviews for her book. She gave a really good talk about distributive laws for Lawvere theories, and if I have enough energy I’ll blog about it on the n-Café. It was full of crunchy facts, as irresistibly tasty as peanuts.