Tropical Algebra and Railway Optimization

24 May, 2018

Simon Willerton pointed out a wonderful workshop, which unfortunately neither he nor I can attend… nor Jamie Vicary, who is at Birmingham:

Tropical Mathematics & Optimisation for Railways, University of Birmingham, School of Engineering, Monday 18 June 2018.

If you can go, please do—and report back!

Tropical algebra involves the numbers (-\infty, \infty] made into a rig with minimization as the addition and addition as the multiplication. It’s called a rig because it’s a “ring without negatives”.

Tropical algebra is important in algebraic geometry, because if you take some polynomial equations and rewrite them replacing + with min and × with +, you get equations that describe shapes with flat pieces replacing curved surfaces, like this:


These simplified shapes are easier to deal with, but they shed light on the original curved ones! Click the picture for more on the subject from Johannes Rau.

Tropical algebra is also important for quantization, since classical mechanics chooses the path with minimum action while quantum mechanics sums over paths. But it’s also important for creating efficient railway time-tables, where you’re trying to minimize the total time it takes to get from one place to another. Finally these worlds are meeting!

Here’s the abstract, which shows that the reference to railway optimization is not just a joke:

Abstract. The main purpose of this workshop is to bring together specialists in tropical mathematics and mathematical optimisation applied in railway engineering and to foster further collaboration between them. It is inspired by some applications of tropical mathematics to the analysis of railway timetables. The most elementary of them is based on a controlled tropically linear dynamic system, which allows for a stability analysis of a regular timetable and can model the delay propagation. Tropical (max-plus) switching systems are one of the extensions of this elementary model. Tropical mathematics also provides appropriate mathematical language and tools for various other applications which willbe presented at the workshop.

The talks on mathematical optimisation in railway engineering will be given by Professor Clive Roberts and other prominent specialists working at the Birmingham Centre for Railway Research and Education (BCRRE). They will inform the workshop participants about the problems that are of actual interest for railways, and suggest efficient and practical methods of their solution.

For a glimpse of some of the category theory lurking in this subject, see:

• Simon Willerton, Project scheduling and copresheaves, The n-Category Café.


Applied Category Theory 2018 – Videos

30 April, 2018

Some of the talks at Applied Category Theory 2018 were videotaped by the Statebox team. You can watch them on YouTube:

• David Spivak, A higher-order temporal logic for dynamical systems. Book available here and slides here.

• Fabio Zanasi and Bart Jacobs, Categories in Bayesian networks. Paper available here. (Some sound missing; when you hit silence skip forwards to about 15:00.)

• Bob Coecke and Aleks Kissinger, Causality. Paper available here.

• Samson Abramsky, Games and constraint satisfaction, Part 1 and Part 2. Paper available here.

• Dan Ghica, Diagrammatic semantics for digital circuits. Paper available here.

• Kathryn Hess, Towards a categorical approach to neuroscience.

• Tom Leinster, Biodiversity and the theory of magnitude. Papers available here and here.

• John Baez, Props in network theory. Slides available here, paper here and blog article here.


Props in Network Theory

27 April, 2018

Long before the invention of Feynman diagrams, engineers were using similar diagrams to reason about electrical circuits and more general networks containing mechanical, hydraulic, thermodynamic and chemical components. We can formalize this reasoning using ‘props’: a certain kind of categories whose objects are natural numbers, with the tensor product of objects given by addition. In this approach, each kind of network corresponds to a prop, and each network of this kind is a morphism in that prop. A network with m inputs and n outputs is a morphism from m to n. Putting networks together in series is composition, and setting them side by side is tensoring.

In this paper, we study the props for various kinds of electrical circuits:

• John Baez, Brandon Coya and Franciscus Rebro, Props in network theory.

We start with circuits made solely of ideal perfectly conductive wires. Then we consider circuits with passive linear components like resistors, capacitors and inductors. Finally we turn on the power and consider circuits that also have voltage and current sources.

And here’s the cool part: each kind of circuit corresponds to a prop that pure mathematicians would eventually invent on their own! So, what’s good for engineers is often mathematically natural too.

We describe the ‘behavior’ of these various kinds of circuits using morphisms between props. In particular, we give a new proof of the black-boxing theorem proved earlier with Brendan Fong. Unlike the original proof, this new one easily generalizes to circuits with nonlinear components! We also use a morphism of props to clarify the relation between circuit diagrams and the signal-flow diagrams in control theory.

Here’s a quick sketch of the main ideas.

Props in network theory

In his 1963 thesis, Lawvere introduced functorial semantics: the use of categories with specified extra structure as ‘theories’ whose ‘models’ are structure-preserving functors into other such categories:

• F. W. Lawvere, Functorial semantics of algebraic theories, Ph.D. thesis, Department of Mathematics, Columbia University, 1963. Also in Reprints in Theory and Applications of Categories 5 (2003), 1–121.

In particular, a Lawvere theory is a category with finite cartesian products and a distinguished object X such that every object is a power X^n. These can serve as theories of mathematical structures that are sets X equipped with n-ary operations

f \colon X^n \to X

obeying equational laws. However, structures of a more linear-algebraic nature are often vector spaces equipped with operations of the form

f \colon X^{\otimes m} \to X^{\otimes n}

To extend functorial semantics to these, Mac Lane introduced props—or as he called them, ‘PROPs’. The acronym stands for ‘products and permutations’:

• Saunders Mac Lane, Categorical algebra, Bulletin of the American Mathematical Society 71 (1965), 40–106.

A prop is a symmetric monoidal category equipped with a distinguished object X such that every object is a tensor power X^{\otimes n}. Working with tensor products rather than cartesian products puts operations having multiple outputs on an equal footing with operations having multiple inputs.

Already in 1949 Feynman had introduced his famous diagrams, which he used to describe theories of elementary particles. For a theory with just one type of particle, Feynman’s method amounts to specifying a prop where an operation f \colon X^{\otimes m} \to X^{\otimes n} describes a process with m particles coming in and n going out. Although Feynman diagrams quickly caught on in physics, only in the 1980s did it become clear that they were a method of depicting morphisms in symmetric monoidal categories. A key step was the work of Joyal and Street, which rigorously justified reasoning in any symmetric monoidal category using ‘string diagrams’—a generalization of Feynman diagrams:

• André Joyal and Ross Street, The geometry of tensor calculus I, Advances in Mathematics 88 (1991), 55–112.

By now, many mathematical physicists are aware of props and the general idea of functorial semantics. In constrast, props seem to be virtually unknown in engineering!

But engineers have been using diagrammatic methods ever since the rise of electrical circuits. And in the 1940s, Olson explained how to apply circuit diagrams to networks of mechanical, hydraulic, thermodynamic and chemical components:

• Harry F. Olson, Dynamical Analogies, Van Nostrand, New York, 1943.

By 1961, Paynter had made the analogies between these various systems mathematically precise using ‘bond graphs’:

• Henry M. Paynter, Analysis and Design of Engineering Systems, MIT Press, Cambridge, Massachusetts, 1961.

Here he shows a picture of a hydroelectric power plant, and the bond graph that abstractly describes it:

By 1963, Forrester was using circuit diagrams in economics:

• Jay Wright Forrester, Industrial Dynamics, MIT Press, Cambridge, Massachusetts, 1961.

In 1984, Odum published a beautiful and influential book on their use in biology and ecology:

• Howard T. Odum, Ecological and General Systems: An Introduction to Systems Ecology, Wiley, New York, 1984.

Energy Systems Symbols

We can use props to study circuit diagrams of all these kinds! The underlying mathematics is similar in each case, so we focus on just one example: electrical circuits. For other examples, take a look at this:

• John Baez, Network theory (part 29), Azimuth, 23 April 2013.

In our new paper, we illustrate the usefulness of props by giving a new, shorter proof of the ‘black-boxing theorem’ proved here:

• John Baez and Brendan Fong, A compositional framework for passive linear networks. (Blog article here.)

A ‘black box’ is a system with inputs and outputs whose internal mechanisms are unknown or ignored. A simple example is the lock on a doorknob: one can insert a key and try to turn it; it either opens the door or not, and it fulfills this function without us needing to know its inner workings. We can treat a system as a black box through a process called ‘black-boxing’, which forgets its inner workings and records only the relation it imposes between its inputs and outputs. Systems with inputs and outputs can be seen as morphisms in a category, where composition uses the outputs of the one system as the inputs of another. We thus expect black-boxing to be a functor out of a category of this sort. A ‘black-boxing theorem’ makes this intuition precise.

In an electrical circuit, associated to each wire there is a pair of variables called the potential \phi and current I. When we black-box such a circuit, we record only the relation it imposes between the variables on its input and output wires. Since these variables come in pairs, this is a relation between even-dimensional vector spaces. But these vector spaces turn out to be equipped with extra structure: they are symplectic vector spaces, meaning they are equipped with a nondegenerate antisymmetric bilinear form. Black-boxing gives a relation that respects this extra structure: it is a ‘Lagrangian’ relation.

Why does symplectic geometry show up when we black-box an electrical circuit? The first proof of the black-boxing theorem answered this question. A circuit made of linear resistors acts to minimize the total power dissipated in the form of heat. More generally, any circuit made of linear resistors, inductors and capacitors obeys a generalization of this ‘principle of minimum power’. Whenever a system obeys a minimum principle, it establishes a Lagrangian relation between input and output variables. This fact was first noticed in classical mechanics, where systems obey the ‘principle of least action’. Indeed, symplectic geometry has its origins in classical mechanics. But it applies more generally: for any sort of system governed by a minimum principle, black-boxing should give a functor to some category where the morphisms are Lagrangian relations.

The first step toward such a theorem for electrical circuits is to treat circuits as morphisms in a suitable category. We start with circuits made only of ideal perfectly conductive wires. These are morphisms in a prop we call \mathrm{Circ}, defined in Section 3 of our paper. In Section 8 we construct a black-boxing functor

\blacksquare \colon \mathrm{Circ} \to \mathrm{LagRel}_k

sending each such circuit to the relation it defines between its input and output potentials and currents. Here \mathrm{LagRel}_k is a prop with symplectic vector spaces of the form k^{2n} as objects and linear Lagrangian relations as morphisms, and \blacksquare is a morphism of props. We work in a purely algebraic fashion, so k here can be any field.

In Section 9 we extend black-boxing to a larger class of circuits that include linear resistors, inductors and capacitors. This gives a new proof of the black-boxing theorem that Brendan and I proved: namely, there is a morphism of props

\blacksquare \colon \mathrm{Circ}_k \to \mathrm{LagRel}_k

sending each such linear circuit to the Lagrangian relation it defines between its input and output potentials and currents. The ease with which we can extend the black-boxing functor is due to the fact that all our categories with circuits as morphisms are props. We can describe these props using generators and relations, so that constructing a black-boxing functor simply requires that we choose where it sends each generator, and check that the all the relations hold. In Section 10 we explain how electric circuits are related to signal-flow diagrams, used in control theory. Finally, in Section 11, we illustrate how props can be used to study nonlinear circuits.

Outline of the results

The paper is pretty long, so here’s a more detailed outline of the results.

In Section 1 we explain a general notion of `L-circuit’ that was first introduced under a different name here:

• R. Rosebrugh, N. Sabadini and R. F. C. Walters, Generic commutative separable algebras and cospans of graphs, Theory and Applications of Categories 15 (2005), 164–177.

An L-circuit is a cospan of finite sets where the apex is the set of nodes of a graph whose edges are labelled by elements of some set L. In applications to electrical engineering, the elements of L describe different ‘circuit elements’ such as resistors, inductors and capacitors. We discuss a symmetric monoidal category \mathrm{Circ}_L whose objects are finite sets and whose morphisms are (isomorphism classes of) L-circuits.

In Section 2 we study \mathrm{Circ}_L when L is a 1-element set. We call this category simply \mathrm{Circ}. In applications to engineering, a morphism in \mathrm{Circ} describes circuit made solely of ideal conductive wires. We show how such a circuit can be simplified in two successive stages, described by symmetric monoidal functors:

\mathrm{Circ} \stackrel{G}{\longrightarrow} \mathrm{FinCospan} \stackrel{H}{\longrightarrow} \mathrm{FinCorel}

Here \mathrm{FinCospan} is the category of cospans of finite sets, while \mathrm{FinCorel} is the category of ‘corelations’ between finite sets. Corelations, categorically dual to relations, are already known to play an important role in network theory:

• Brendan Fong, Decorated corelations.

Just as a relation can be seen as a jointly monic span, a corelation can be seen as a jointly epic cospan. The functor G crushes any graph down to its set of components, while H reduces any cospan to a jointly epic one.

In Section 4 we turn to props. Propositions 11 and 12, proved in Appendix A.1 with the help of Steve Lack, characterize which symmetric monoidal categories are equivalent to props and which symmetric monoidal functors are isomorphic to morphisms of props. We use these to find props equivalent to \mathrm{Circ}_L, \mathrm{Circ}, \mathrm{FinCospan} and \mathrm{FinCorel}. This lets us reinterpret the arrows here as morphisms of props:

\mathrm{Circ} \stackrel{G}{\longrightarrow} \mathrm{FinCospan} \stackrel{H}{\longrightarrow} \mathrm{FinCorel}

In Section 5 we discuss presentations of props. Proposition 19, proved in Appendix A.2 using a result of Todd Trimble, shows that the category of props is monadic over the category of signatures, \mathrm{Set}^{\mathbb{N} \times \mathbb{N}}. This lets us work with props using generators and relations. We conclude by recalling a presentation of \mathrm{FinCospan} due to Lack and a presentation of \mathrm{FinCorel} due to Coya and Fong:

• Steve Lack, Composing PROPs, Theory and Applications of Categories 13 (2004), 147–163.

• Brandon Coya and Brendan Fong, Corelations are the prop for extraspecial commutative Frobenius monoids, Theory and Applications of Categories 32 (2017), 380–395. (Blog article here.)

In Section 6 we introduce the prop \mathrm{FinRel}_k. This prop is equivalent to the symmetric monoidal category with finite-dimensional vector spaces over the field k as objects and linear relations as morphisms, with direct sum as its tensor product. A presentation of this prop was given in these papers:

• Filippo Bonchi, Pawel Sobociénski and Fabio Zanasi, Interacting Hopf algebras, Journal of Pure and Applied Algebra 221 (2017), 144–184.

• John Baez and Jason Erbele, Categories in control, Theory and Application of Categories 30 (2015), 836–881. (Blog article here.)

In Section 7 we state the main result in the paper by Rosebrugh, Sabadini and Walters. This gives a presentation of \mathrm{Circ}_L. Equivalently, it says that \mathrm{Circ}_L is the coproduct, in the category of props, of \mathrm{FinCospan} and the free prop on a set of unary operations, one for each element of L. This result makes it easy to construct morphisms from \mathrm{Circ}_L to other props.

In Section 8 we introduce the prop \mathrm{LagRel}_k where morphisms are Lagrangian linear relations between symplectic vector spaces, and we construct the black-boxing functor \blacksquare \colon \mathrm{Circ} \to \mathrm{LagRel}_k. Mathematically, this functor is the composite

\mathrm{Circ} \stackrel{G}{\longrightarrow} \mathrm{FinCospan} \stackrel{H}{\longrightarrow} \mathrm{FinCorel} \stackrel{K}{\longrightarrow} \mathrm{LagRel}_k

where K is a symmetric monoidal functor defined by its action on the generators of \mathrm{FinCorel}. In applications to electrical engineering, the black-boxing functor maps any circuit of ideal conductive wires to its ‘behavior’: that is, to the relation that it imposes on the potentials and currents at its inputs and outputs.

In Section 9 we extend the black-boxing functor to circuits that include resistors, inductors, capacitors and certain other linear circuit elements. The most elegant prop having such circuits as morphisms is \mathrm{Circ}_k, meaning \mathrm{Circ}_L with the label set L taken to be a field $k.$ We characterize the black-boxing functor

\blacksquare \colon \mathrm{Circ}_k \to \mathrm{LagRel}_k

in Theorem 41.

In Section 10 we expand the scope of inquiry to include ‘signal-flow diagrams’, which are important in control theory. We explain how signal-flow diagrams serve as a syntax for linear relations. Concretely, this means that signal-flow diagrams are morphisms in a free prop \mathrm{SigFlow}_k with the same generators as \mathrm{FinRel}_k, but no relations. There is thus a morphism of props

\square \colon \mathrm{SigFlow}_k \to \mathrm{FinRel}_k

mapping any signal-flow diagrams to the linear relation that it denotes. It is natural to wonder how this is related to the black-boxing functor

\blacksquare \colon \mathrm{Circ}_k \to \mathrm{LagRel}_k

The answer involves the free prop \widetilde{\mathrm{Circ}}_k which arises when we take the simplest presentation of \mathrm{Circ}_k and omit the relations. This comes with a map

P \colon \widetilde{\mathrm{Circ}}_k \to \mathrm{Circ}_k

which reinstates those relations, and in Theorem 44 we show there is a map of props T \colon \widetilde{\mathrm{Circ}}_k \to \mathrm{SigFlow}_k making this diagram commute:

Putting everything together, we get this grand commuting diagram relating circuit diagrams, linear circuits, signal flow diagrams, cospans, corelations, Lagrangian relations, and linear relations:

Finally, in Section 11 we illustrate how props can also be used to study nonlinear circuits. Namely, we show how to include voltage and current sources. Black-boxing these gives Lagrangian affine relations between symplectic vector spaces! Eventually we’ll get around to studying more general nonlinear circuits… but not today.


Applied Category Theory at NIST (Part 1)

17 February, 2018

I think it’s really cool how applied category theory is catching on. My former student Blake Pollard is working at the National Institute of Standards and Technology on applications of category theory to electrical engineering. He’s working with Spencer Breiner… and now Breiner is helping run a workshop on this stuff:

• Applied Category Theory: Bridging Theory & Practice, March 15–16, 2018, NIST, Gaithersburg, Maryland, USA. Organized by Spencer Breiner and Eswaran Subrahmanian.

It’s by invitation only, but I can’t resist mentioning its existence. Here’s the idea:

What: The Information Technology Laboratory at NIST is pleased to announce a workshop on Applied Category Theory to be held at NIST’s Gaithersburg, Maryland campus on March 15 & 16, 2018. The meeting will focus on practical avenues for introducing methods from category theory into real-world applications, with an emphasis on examples rather than theorems.

Who: The workshop aims to bring together two distinct groups. First, category theorists interested in pursuing applications outside of the usual mathematical fields. Second, domain experts and research managers from industry, government, science and engineering who have in mind potential domain applications for categorical methods.

Intended Outcomes: A proposed landscape of potential CT applications and the infrastructure needed to realize them, together with a 5-10 year roadmap for developing the field of applied category theory. This should include perspectives from industry, academia and government as well as major milestones, potential funding sources, avenues for technology transfer and necessary improvements in tool support and methodology. Exploratory collaborations between category theorists and domain experts. We will ask that each group come prepared to meet the other side. Mathematicians should be prepared with concrete examples that demonstrate practical applications of CT in an intuitive way. Domain experts should bring to the table specific problems to which they can devote time and/or funding as well as some reasons about why they think CT might be relevant to this application.

Invited Speakers:
John Baez (University of California at Riverside) and John Foley (Metron Scientific Solutions).
Bob Coecke (University of Oxford).
Dusko Pavlovic (University of Hawaii).

Some other likely participants include Chris Boner (Metron), Arquimedes Canedo (Siemens at Princeton), Stephane Dugowson (Supméca), William Edmonson (North Carolina A&T), Brendan Fong (MIT), Mark Fuge (University of Maryland), Jack Gray (Penumbra), Helle Hansen (Delft), Jelle Herold (Statebox), Marisa Hughes (Johns Hopkins), Steve Huntsman (BAE Systems), Patrick Johnson (Dassault Systèmes), Al Jones (NIST), Cliff Joslyn (Pacific Northwest National Laboratory), Richard Malek (NSF), Tom Mifflin (Metron), Ira Monarch (Carnegie Mellon), John Paschkewitz (DARPA), Evan Patterson (Stanford), Blake Pollard (NIST), Emilie Purvine (Pacific Northwest National Laboratory), Mark Raugas (Pacific Northwest National Laboratory), Bill Regli (University of Maryland), Michael Robinson (American U.) Alberto Speranzon (Honeywell Aerospace), David Spivak (MIT), Eswaran Subrahmanian (Carnegie Mellon), Jamie Vicary (Birmingham and Oxford), and Ryan Wisnesky (Categorical Informatics).

A bunch of us will stay on into the weekend and talk some more. I hope we make a lot of progress—and I plan to let you know how it goes!

I’ll be giving a joint talk with John Foley about our work using operads to design networks. This work is part of the Complex Adaptive System Composition and Design Environment project being done by Metron Scientific Solutions and managed by John Paschkewitz at DARPA.


Postdoc in Applied Category Theory

8 September, 2017

guest post by Spencer Breiner

One Year Postdoc Position at Carnegie Mellon/NIST

We are seeking an early-career researcher with a background in category theory, functional programming and/or electrical engineering for a one-year post-doctoral position supported by an Early-concept Grant (EAGER) from the NSF’s Systems Science program. The position will be managed through Carnegie Mellon University (PI: Eswaran Subrahmanian), but the position itself will be located at the US National Institute for Standards and Technology (NIST), located in Gaithersburg, Maryland outside of Washington, DC.

The project aims to develop a compositional semantics for electrical networks which is suitable for system prediction, analysis and control. This work will extend existing methods for linear circuits (featured on this blog!) to include (i) probabilistic estimates of future consumption and (ii) top-down incentives for load management. We will model a multi-layered system of such “distributed energy resources” including loads and generators (e.g., solar array vs. power plant), different types of resource aggregation (e.g., apartment to apartment building), and across several time scales. We hope to demonstrate that such a system can balance local load and generation in order to minimize expected instability at higher levels of the electrical grid.

This post is available full-time (40 hours/5 days per week) for 12 months, and can begin as early as October 1st.

For more information on this position, please contact Dr. Eswaran Subrahmanian (sub@cmu.edu) or Dr. Spencer Breiner (spencer.breiner@nist.gov).