ACT2020 Program

27 June, 2020


Applied Category Theory 2020 is coming up soon! After the Tutorial Day on Sunday July 6th, there will be talks from Monday July 7th to Friday July 10th. Here is the program—click on it to download a more readable version:

All talks will be live on Zoom. Recorded versions should appear on YouTube later.

Here are the talks! They come in three kinds: keynotes, regular presentations and short industry presentations. Within each I’ve listed them in alphabetical order by speaker: I believe the first author is the speaker.

This is gonna be fun.

Keynote presentations (35 minutes)

• Henry Adams, Johnathan Bush and Joshua Mirth, Operations on metric thickenings.

• Nicolas Blanco and Noam Zeilberger: Bifibrations of polycategories and classical linear logic.

• Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore and Mario Román: Profunctor optics, a categorical update.

• Tobias Fritz, Tomáš Gonda, Paolo Perrone and Eigil Rischel: Distribution functors, second-order stochastic dominance and the Blackwell–Sherman–Stein Theorem in categorical probability.

• Micah Halter, Evan Patterson, Andrew Baas and James Fairbanks: Compositional scientific computing with Catlab and SemanticModels.

• Joachim Kock: Whole-grain Petri nets and processes.

• Andre Kornell, Bert Lindenhovius and Michael Mislove: Quantum CPOs.

• Martha Lewis: Towards logical negation in compositional distributional semantics.

• Jade Master and John Baez: Open Petri nets.

• Lachlan McPheat, Mehrnoosh Sadrzadeh, Hadi Wazni and Gijs Wijnholds, Categorical vector space semantics for Lambek calculus with a relevant modality.

• David Jaz Myers: Double categories of open dynamical systems.

• Toby St Clere Smithe, Cyber Kittens, or first steps towards categorical cybernetics.

Regular presentations (20 minutes)

• Robert Atkey, Bruno Gavranović, Neil Ghani, Clemens Kupke, Jeremy Ledent and Fredrik Nordvall Forsberg: Compositional game theory, compositionally.

• John Baez and Kenny Courser: Coarse-graining open Markov processes.

• Georgios Bakirtzis, Christina Vasilakopoulou and Cody Fleming, Compositional cyber-physical systems modeling.

• Marco Benini, Marco Perin, Alexander Alexander Schenkel and Lukas Woike: Categorification of algebraic quantum field theories.

• Daniel Cicala: Rewriting structured cospans.

• Bryce Clarke: A diagrammatic approach to symmetric lenses.

• Bob Coecke, Giovanni de Felice, Konstantinos Meichanetzidis, Alexis Toumi, Stefano Gogioso and Nicolo Chiappori: Quantum natural language processing.

• Geoffrey Cruttwell, Jonathan Gallagher and Dorette Pronk: Categorical semantics of a simple differential programming language.

• Swaraj Dash and Sam Staton: A monad for probabilistic point processes.

• Giovanni de Felice, Elena Di Lavore, Mario Román and Alexis Toumi: Functorial language games for question answering.

• Giovanni de Felice, Alexis Toumi and Bob Coecke: DisCoPy: monoidal categories in Python.

• Brendan Fong, David Jaz Myers and David I. Spivak: Behavioral mereology: a modal logic for passing constraints.

• Rocco Gangle, Gianluca Caterina and Fernando Tohme, A generic figures reconstruction of Peirce’s existential graphs (alpha).

• Jules Hedges and Philipp Zahn: Open games in practice.

• Jules Hedges: Non-compositionality in categorical systems theory.

• Michael Johnson and Robert Rosebrugh, The more legs the merrier: A new composition for symmetric (multi-)lenses.

• Joe Moeller, John Baez and John Foley: Petri nets with catalysts.

• John Nolan and Spencer Breiner, Symmetric monoidal categories with attributes.

• Joseph Razavi and Andrea Schalk: Gandy machines made easy via category theory.

• Callum Reader: Measures and enriched categories.

• Mario Román: Open diagrams via coend calculus.

• Luigi Santocanale, Dualizing sup-preserving endomaps of a complete lattice.

• Dan Shiebler: Categorical stochastic processes and likelihood.

• Richard Statman, Products in a category with only one object.

• David I. Spivak: Poly: An abundant categorical setting for mode-dependent dynamics.

• Christine Tasson and Martin Hyland, The linear-non-linear substitution 2-monad.

• Tarmo Uustalu, Niccolò Veltri and Noam Zeilberger: Proof theory of partially normal skew monoidal categories.

• Dmitry Vagner, David I. Spivak and Evan Patterson: Wiring diagrams as normal forms for computing in symmetric monoidal categories.

• Matthew Wilson, James Hefford, Guillaume Boisseau and Vincent Wang: The safari of update structures: visiting the lens and quantum enclosures.

• Paul Wilson and Fabio Zanasi: Reverse derivative ascent: a categorical approach to learning Boolean circuits.

• Vladimir Zamdzhiev: Computational adequacy for substructural lambda calculi.

• Gioele Zardini, David I. Spivak, Andrea Censi and Emilio Frazzoli: A compositional sheaf-theoretic framework for event-based systems.

Industry presentations (8 minutes)

• Arquimedes Canedo (Siemens Corporate Technology).

• Brendan Fong (Topos Institute).

• Jelle Herold (Statebox): Industrial strength CT.

• Steve Huntsman (BAE): Inhabiting the value proposition for category theory.

• Ilyas Khan (Cambridge Quantum Computing).

• Alan Ransil (Protocol Labs): Compositional data structures for the decentralized web.

• Alberto Speranzon (Honeywell).

• Ryan Wisnesky (Conexus): Categorical informatics at scale.

ACT2020 Tutorial Day

17 June, 2020

If you’re wanting to learn some applied category theory, register for the tutorials that are taking place on July 5, 2020 as part of ACT2020!

Applied category theory offers a rigorous mathematical language and toolset for relating different concepts from across math, science, and technology. For example, category theory finds common patterns between geometry (shapes), algebra (equations), numbers, logic, probability, etc. Applied category theory (ACT) looks for how those very same patterns extend outward to data, programs, processes, physics, linguistics, and so on—things we see in the real world. The field is currently growing, as new applications and common patterns are being found all the time. When you understand these ideas, more of your intuitions about the world can be made rigorous and thus be communicated at a larger scale. This in turn gives our community a chance to solve larger and more complex scientific, technological, and maybe even societal problems.

This year’s international applied category theory conference ACT2020 is having a tutorial day, meant to introduce newcomers to applied category theory. Tutorial day will take place on July 5 and will include a few main topics that will be taught semi-traditionally (via presentation, exercises, and discussion) over Zoom, as well as mentors who will be available throughout the day to work with smaller groups and/or individuals. We invite you to sign up here if you’re interested, so we can keep you posted. Hope to see you there!

The four courses will be roughly as follows:

• David Spivak: categorical databases for introducing sets, functions, categories, and functors.

• Fabrizio Genovese: string diagrams as a graphical language for category theory.

• Emily Riehl: the Yoneda lemma in the context of matrices.

• Paolo Perrone: monads and comonads.

A Complete Axiomatisation of Partial Differentiation

18 May, 2020

In the eighth talk of the ACT@UCR seminar, Gordon Plotkin told us about partial differentiation, viewed as a logical theory.

He gave his talk on Wednesday May 20th. Afterwards we discussed it on the Category Theory Community Server, here:

You can view or join the conversation there if you sign in.

You can see his slides here, or download a video of his talk here, or watch his video here:

• Gordon Plotkin, A complete axiomatisation of partial differentiation.

Abstract. We formalise the well-known rules of partial differentiation in a version of equational logic with function variables and binding constructs. We prove the resulting theory is complete with respect to polynomial interpretations. The proof makes use of Severi’s theorem that all multivariate Hermite problems are solvable. We also hope to present a number of related results, such as decidability and Hilbert–Post completeness.


The Category Theory Behind UMAP

10 February, 2020

An interesting situation has arisen. Some people working on applied category theory have been seeking a ‘killer app’: that is, an application of category theory to practical tasks that would be so compelling it would force the world to admit categories are useful. Meanwhile, the UMAP algorithm, based to some extent on category theory, has become very important in genomics:

• Leland McInnes, John Healy and James Melville, UMAP: uniform manifold approximation and projection for dimension reduction.

But while practitioners have embraced the algorithm, they’re still puzzled by its category-theoretic underpinnings, which are discussed in Section 2 of the paper. (You can read the remaining sections, which describe the algorithm quite concretely, without understanding Section 2.)

I first heard of this situation on Twitter when James Nichols wrote:

Wow! My first sighting of applied category theory: the UMAP algorithm. I’m a category novice, but the resulting adjacency-graph algorithm is v simple, so surely the theory boils down to reasonably simple arguments in topology/Riemannian geometry?

Do any of you prolific ACT tweeters know much about UMAP? I understand the gist of the linked paper, but not say why we need category theory to define this “fuzzy topology” concept, as opposed to some other analytic defn.

Junhyong Kim added:

What was gained by CT for UMAP? (honest question, not trying to be snarky)

Leland McInnes, one of the inventors of UMAP, responded:

It is my math background, how I think about the problem, and how the algorithm was derived. It wasn’t something that was added, but rather something that was always there—for me at least. In that sense what was gained was the algorithm.

I don’t really understand UMAP; for a good introduction to it see the original paper above and also this:

• Nikolay Oskolkov, How Exactly UMAP Works—and Why Exactly It Is Better Than tSNE, 3 October 2019.

tSNE is an older algorithm for taking clouds of data points in high dimensions and mapping them down to fewer dimensions so we can understand what’s going on. From the viewpoint of those working on genomics, the main good thing about UMAP is that it solves a bunch of problems that plagued tSNE. Oskolkov explains what these problems are and how UMAP deals with them. But he also alludes to the funny disconnect between these practicalities and the underlying theory:

My first impression when I heard about UMAP was that this was a completely novel and interesting dimension reduction technique which is based on solid mathematical principles and hence very different from tSNE which is a pure Machine Learning semi-empirical algorithm. My colleagues from Biology told me that the original UMAP paper was “too mathematical”, and looking at the Section 2 of the paper I was very happy to see strict and accurate mathematics finally coming to Life and Data Science. However, reading the UMAP docs and watching Leland McInnes talk at SciPy 2018, I got puzzled and felt like UMAP was another neighbor graph technique which is so similar to tSNE that I was struggling to understand how exactly UMAP is different from tSNE.

He then goes on and attempts to explain exactly why UMAP does so much better than tSNE. None of his explanation mentions category theory.

Since I don’t really understand UMAP or why it does better than tSNE, I can’t add anything to this discussion. In particular, I can’t say how much the category theory really helps. All I can do is explain a bit of the category theory. I’ll do that now, very briefly, just as a way to get a conversation going. I will try to avoid category-theoretic jargon as much as possible—not because I don’t like it or consider it unimportant, but because that jargon is precisely what’s stopping certain people from understanding Section 2.

I think it all starts with this paper by Spivak, which McInnes, Healy and Melville cite but for some reason don’t provide a link to:

• David Spivak, Metric realization of fuzzy simplicial sets.

Spivak showed how to turn a ‘fuzzy simplicial set’ into an ‘uber-metric space’ and vice versa. What are these things?

An ‘uber-metric space’ is very simple. It’s a slight generalization of a metric space that relaxes the usual definition in just two ways: it lets distances be infinite, and it lets distinct points have distance zero from each other. This sort of generalization can be very useful. I could talk about it a lot, but I won’t.

A fuzzy simplicial set is a generalization of a simplicial set.

A simplicial set starts out as a set of vertices (or 0-simplices), a set of edges (or 1-simplices), a set of triangles (or 2-simplices), a set of tetrahedra (or 3-simplices), and so on: in short, a set of n-simplices for each n. But there’s more to it. Most importantly, each n-simplex has a bunch of faces, which are lower-dimensional simplices.

I won’t give the whole definition. To a first approximation you can visualize a simplicial set as being like this:

But of course it doesn’t have to stop at dimension 3—and more subtly, you can have things like two different triangles that have exactly the same edges.

In a ‘fuzzy’ simplicial set, instead of a set of n-simplices for each n, we have a fuzzy set of them. But what’s a fuzzy set?

Fuzzy set theory is good for studying collections where membership is somewhat vaguely defined. Like a set, a fuzzy set has elements, but each element has a ‘degree of membership’ that is a number 0 < x ≤ 1. (If its degree of membership were zero, it wouldn't be an element!)

A map f: X → Y between fuzzy sets is an ordinary function, but obeying this condition: it can only send an element x ∈ X to an element f(x) ∈ Y whose degree of membership is greater than or equal to that of x. In other words, we don't want functions that send things to things with a lower degree of membership.

Why? Well, if I'm quite sure something is a dog, and every dog has a nose, then I'm must be at least equally sure that this dog has a nose! (If you disagree with this, then you can make up some other concept of fuzzy set. There are a number of such concepts, and I'm just describing one.)

So, a fuzzy simplicial set will have a set of n-simplices for each n, with each n-simplex having a degree of membership… but the degree of membership of its faces can't be less than its own degree of membership.

This is not the precise definition of fuzzy simplicial set, because I'm leaving out some distracting nuances. But you can get the precise definition by taking a nuts-and-bolts definition of simplicial set, like Definition 3.2 here:

• Greg Friedman, An elementary illustrated introduction to simplicial sets.

and replacing all the sets by fuzzy sets, and all the maps by maps between fuzzy sets.

If you like visualizing things, you can visualize a fuzzy simplicial set as an ordinary simplicial set, as in the picture above, but where an n-simplex is shaded darker if its degree of membership is higher. An n-simplex can’t be shaded darker than any of its faces.

How can you turn a fuzzy simplicial set into an uber-metric space? And how can you turn an uber-metric space into a fuzzy simplicial set?

Spivak focuses on the first question, because the answer is simpler, and it determines the answer to the second using some category theory. (Psst: adjoint functors!)

The answer to the first question goes like this. Say you have a fuzzy simplicial set. For each n-simplex whose degree of membership equals a, you turn it into a copy of this uber-metric space:

\{ (t_0, t_1, \dots, t_n) : t_0 + \cdots + t_n = - \log a , \; t_0, \ldots, t_n \geq 0 \} \subseteq \mathbb{R}^{n+1}

This is really just an ordinary metric space: an n-simplex that’s a subspace of Euclidean (n+1)-dimensional space with its usual Euclidean distance function. Then you glue together all these uber-metric spaces, one for each simplex in your fuzzy simplical set, to get a big fat uber-metric space.

This process is called ‘realization’. The key here is that if an n-simplex has a high degree of membership, it gets ‘realized’ as a metric space shaped like a small n-simplex. I believe the basic intuition is that an n-simplex with a high degree of membership describes an (n+1)-tuple of things—its vertices—that are close to each other.

In theory, I should try to describe the reverse process that turns an uber-metric space into a fuzzy simplicial set. If I did, I believe we would see that whenever an (n+1)-tuple of things—that is, points of our uber-metric space—are close, they give an n-simplex with a high degree of membership.

If so, then both uber-metric spaces and fuzzy simplicial sets are just ways of talking about which collections of data points are close, and we can translate back and forth between these descriptions.

But I’d need to think about this a bit more to do a good job of going further, and reading the UMAP paper a bit more I’m beginning to suspect that’s not the main thing that practitioners need to understand. I’m beginning to think the most useful thing is to get a feeling for fuzzy simplicial sets! I hope I’ve helped a bit in that direction. They are very simple things. They are also closely connected to an idea from topological data analysis:

• Nina Otter, Magnitude meets persistence. Homology theories for filtered simplicial sets.

I should admit that McInnes, Healy and Melville tweak Spivak’s formalism a bit. They call Spivak’s uber-metric spaces ‘extended-pseudo-metric spaces’, but they focus on a special kind, which they call ‘finite’. Unfortunately, I can’t find where they define this term. They also only consider a special sort of fuzzy simplicial set, which they call ‘bounded’, but I can’t find the definition of this term either! Without knowing these definitions, I can’t comment on how these tweaks change things.

Applied Category Theory Meeting at UCR (Part 2)

30 September, 2019


Joe Moeller and I have finalized the schedule of our meeting on applied category theory:

Applied Category Theory, special session of the Fall Western Sectional Meeting of the AMS, U. C. Riverside, Riverside, California, 9–10 November 2019.

It’s going to be really cool, with talks on everything from brakes to bicategories, from quantum physics to social networks, and more—with the power of category theory as the unifying theme!

You can get information on registration, hotels and such here. If you’re coming, you might also want to attend Eugenia Cheng‘s talk on the afternoon of Friday November 8th.   I’ll announce the precise title and time of her talk, and also the location of all the following talks, as soon as I know!

In what follows, the person actually giving the talk has an asterisk by their name. You can click on talk titles to see abstracts of the talks.

Saturday November 9, 2019, 8:00 a.m.-10:50 a.m.

Saturday November 9, 2019, 3:00 p.m.-5:50 p.m.

Sunday November 10, 2019, 8:00 a.m.-10:50 a.m.

Sunday November 10, 2019, 2:00 p.m.-4:50 p.m.

Applied Category Theory 2019 Program

3 July, 2019

Bob Coecke, David Spivak, Christina Vasilakopoulou and I are running a conference on applied category theory:

Applied Category Theory 2019, 15–19 July, 2019, Lecture Theatre B of the Department of Computer Science, 10 Keble Road, Oxford.

You can now see the program here, or below. Hope to see you soon!

Enriched Lawvere Theories

16 May, 2019

My grad student Christian Williams and I finished this paper just in time for him to talk about it at SYCO:

• John Baez and Christian Williams, Enriched Lawvere theories for operational semantics.

Abstract. Enriched Lawvere theories are a generalization of Lawvere theories that allow us to describe the operational semantics of formal systems. For example, a graph-enriched Lawvere theory describes structures that have a graph of operations of each arity, where the vertices are operations and the edges are rewrites between operations. Enriched theories can be used to equip systems with operational semantics, and maps between enriching categories can serve to translate between different forms of operational and denotational semantics. The Grothendieck construction lets us study all models of all enriched theories in all contexts in a single category. We illustrate these ideas with the SKI-combinator calculus, a variable-free version of the lambda calculus, and with Milner’s calculus of communicating processes.

When Mike Stay came to U.C. Riverside to work with me about ten years ago, he knew about computation and I knew about category theory, and we started trying to talk to each other. I’d heard that categories and computer science were deeply connected: for example, people like to say that the lambda-calculus is all about cartesian closed categories. But we soon realized something funny was going on here.

Computer science is deeply concerned with processes of computation, and category theory uses morphisms to describe processes… but when cartesian closed categories are applied to the lambda calculus, their morphisms do not describe processes of computation. In fact, the process of computation is effectively ignored!

We decided that to fix this we could use 2-categories where

• objects are types. For example, there could be a type of integers, INT. There could be a type of pairs of integers, INT × INT. There could also be a boring type 1, which represents something there’s just one of.

• morphisms are terms. For example, a morphism f: 1 → INT picks out a specific natural number, like 2 or 3. There could also be a morphism +: INT × INT → INT, called ‘addition’. Combining these, we can get expressions like 2+3.

• 2-morphism are rewrites. For example, there could be a rewrite going from 2+3 to 5.

Later Mike realized that instead of 2-categories, it can be good to use graph-enriched categories: that is, things like categories where instead of a set of morphisms from one object to another, we have a graph.

In other words: instead of hom-sets, a graph-enriched category has ‘hom-graphs’. The objects of a graph-enriched category can represent types, the vertices of the hom-graphs can represent terms, and the edges of the hom-graphs can represent rewrites.

Mike teamed up with Greg Meredith to write a paper on this:

• Mike Stay and Greg Meredith, Representing operational semantics
with enriched Lawvere theories

Christian decided to write a paper building on this, and I’ve been helping him out because it’s satisfying to see an old dream finally realized—in a much more detailed, beautiful way than I ever imagined!

The key was to sharpen the issue by considering enriched Lawvere theories. Lawvere theories are an excellent formalism for describing algebraic structures obeying equational laws, but they do not specify how to compute in such a structure, for example taking a complex expression and simplifying it using rewrite rules. Enriched Lawvere theories let us study the process of rewriting.

Maybe I should back up a bit. A Lawvere theory is a category with finite products T generated by a single object t, for ‘type’. Morphisms t^n \to t represent n-ary operations, and commutative diagrams specify equations these operations obey. There is a theory for groups, a theory for rings, and so on. We can specify algebraic structures of a given kind in some ‘context’—that is, in some category C with finite products—by a product-preserving functor \mu: T \to C. For example, if T is the theory of groups and C is the category of sets then such a functor describes a group, but if C is the category of topological space then such a functor describes a topological group.

All this is a simple and elegant form of what computer scientists call denotational semantics: roughly, the study of types and terms, and what they signify. However, Lawvere theories know nothing of operational semantics: that is, how we actually compute. The objects of our Lawvere are types and the morphisms are terms. But there are no rewrites going between terms, only equations!

This is where enriched Lawvere theories come in. Suppose we fix a cartesian closed category V, such as the category of sets, or the category of graphs, or the category of posets, or even the category of categories. Then V-enriched category is a thing like a category, but instead of having a set of morphisms from any object to any other object, it has an object of V. That is, instead of hom-sets it can have hom-graphs, or hom-posets, or hom-categories. If it has hom-categories, then it’s a 2-category—so this setup includes my original dream, but much more!

Our paper explains how to generalize Lawvere theories to this enriched setting, and how to use these enriched Lawvere theories in operational semantics. We rely heavily on previous work, especially by Rory Lucyshyn-Wright, who in turn built on work by John Power and others. But we’re hoping that our paper, which is a bit less high-powered, will be easier for people who are familiar with category theory but not yet enriched categories. The novelty lies less in the math than its applications. Give it a try!

Here is a small piece of a hom-graph in the graph-enriched theory of the SKI combinator calculus, a variable-free version of the lambda calculus invented by Moses Schönfinkel and Haskell Curry back in the 1920s:


Symposium on Compositional Structures 4: Program

11 May, 2019

Here’s the program for this conference:

Symposium on Compositional Structures 4, 22–23 May, 2019, Chapman University, California. Organized by Alexander Kurz.

A lot of my students and collaborators are speaking here! The meeting will take place in Beckman Hall 101.

Wednesday May 22, 2019

• 10:30–11:30 — Registration.

• 11:30–12:30 — John Baez, “Props in Network Theory“.

• 12:30–1:00 — Jade Master, “Generalized Petri Nets”.

• 1:00–2:00 — Lunch.

• 2:00–2:30 — Christian Williams, “Enriched Lawvere Theories for Operational Semantics”.

• 2:30–3:00 — Kenny Courser, “Structured Cospans”.

• 3:00–3:30 — Daniel Cicala, “Rewriting Structured Cospans”.

• 3:30–4:00 — Break.

• 4:00–4:30 — Samuel Balco and Alexander Kurz, “Nominal String Diagrams”.

• 4:30–5:00 — Jeffrey Morton, “2-Group Actions and Double Categories”.

• 5:00–5:30 — Michael Shulman, “All (∞,1)-Toposes Have Strict Univalent Universes”.

• 5:30–6:30 — Reception.

Thursday May 23, 2019

• 9:30–10:30 — Nina Otter, “A Unified Framework for Equivalences in Social Networks”.

• 10:30–11:00 — Kohei Kishida, Soroush Rafiee Rad, Joshua Sack and Shengyang Zhong, “Categorical Equivalence between Orthocomplemented Quantales and Complete Orthomodular Lattices”.

• 11:00–11:30 — Break.

• 11:30–12:00 — Cole Comfort, “Circuit Relations for Real Stabilizers: Towards TOF+H”.

• 12:00–12:30 — Owen Biesel, “Duality for Algebras of the Connected Planar Wiring Diagrams Operad”.

• 12:30–1:00 — Joe Moeller and Christina Vasilakopoulou, “Monoidal Grothendieck Construction”.

• 1:00–2:00 — Lunch.

• 2:00–3:00 — Tobias Fritz, “Categorical Probability: Results and Challenges”.

• 3:00–3:30 — Harsh Beohar and Sebastian Küpper, “Bisimulation Maps in Presheaf Categories”.

• 3:30–4:00 — Break.

• 4:00–4:30 — Benjamin MacAdam, Jonathan Gallagher and Rory Lucyshyn-Wright, “Scalars in Tangent Categories”.

• 4:30–5:00 — Jonathan Gallagher, Benjamin MacAdam and Geoff Cruttwell, “Towards Formalizing and Extending Differential Programming via Tangent Categories”.

• 5:00–5:30 — David Sprunger and Shin-Ya Katsumata, “Differential Categories, Recurrent Neural Networks, and Machine Learning”.

The Pi Calculus: Towards Global Computing

4 April, 2019


Check out the video of Christian Williams’’s talk in the Applied Category Theory Seminar here at U. C. Riverside. It was nicely edited by Paola Fernandez and uploaded by Joe Moeller.

Abstract. Historically, code represents a sequence of instructions for a single machine. Each computer is its own world, and only interacts with others by sending and receiving data through external ports. As society becomes more interconnected, this paradigm becomes more inadequate – these virtually isolated nodes tend to form networks of great bottleneck and opacity. Communication is a fundamental and integral part of computing, and needs to be incorporated in the theory of computation.

To describe systems of interacting agents with dynamic interconnection, in 1980 Robin Milner invented the pi calculus: a formal language in which a term represents an open, evolving system of processes (or agents) which communicate over names (or channels). Because a computer is itself such a system, the pi calculus can be seen as a generalization of traditional computing languages; there is an embedding of lambda into pi – but there is an important change in focus: programming is less like controlling a machine and more like designing an ecosystem of autonomous organisms.

We review the basics of the pi calculus, and explore a variety of examples which demonstrate this new approach to programming. We will discuss some of the history of these ideas, called “process algebra”, and see exciting modern applications in blockchain and biology.

“… as we seriously address the problem of modelling mobile communicating systems we get a sense of completing a model which was previously incomplete; for we can now begin to describe what goes on outside a computer in the same terms as what goes on inside – i.e. in terms of interaction. Turning this observation inside-out, we may say that we inhabit a global computer, an informatic world which demands to be understood just as fundamentally as physicists understand the material world.” — Robin Milner

The talks slides are here.

Reading material:

• Robin Milner, The polyadic pi calculus: a tutorial.

• Robin Milner, Communicating and Mobile Systems.

• Joachim Parrow, An introduction to the pi calculus.

Complex Adaptive System Design (Part 9)

24 March, 2019

Here’s our latest paper for the Complex Adaptive System Composition and Design Environment project:

• John Baez, John Foley and Joe Moeller, Network models from Petri nets with catalysts.

Check it out! And please report typos, mistakes, or anything you have trouble understanding! I’m happy to answer questions here.

The idea

Petri nets are a widely studied formalism for describing collections of entities of different types, and how they turn into other entities. I’ve written a lot about them here. Network models are a formalism for designing and tasking networks of agents, which our team invented for this project. Here we combine these ideas! This is worthwhile because while both formalisms involve networks, they serve a different function, and are in some sense complementary.

A Petri net can be drawn as a bipartite directed graph with vertices of two kinds: places, drawn as circles, and transitions drawn as squares:

When we run a Petri net, we start by placing a finite number of dots called tokens in each place:

This is called a marking. Then we repeatedly change the marking using the transitions. For example, the above marking can change to this:

and then this:

Thus, the places represent different types of entity, and the transitions are ways that one collection of entities of specified types can turn into another such collection.

Network models serve a different function than Petri nets: they are a general tool for working with networks of many kinds. Mathematically a network model is a lax symmetric monoidal functor G \colon \mathsf{S}(C) \to \mathsf{Cat}, where \mathsf{S}(C) is the free strict symmetric monoidal category on a set C. Elements of C represent different kinds of ‘agents’. Unlike in a Petri net, we do not usually consider processes where these agents turn into other agents. Instead, we wish to study everything that can be done with a fixed collection of agents. Any object x \in \mathsf{S}(C) is of the form c_1 \otimes \cdots \otimes c_n for some c_i \in C; thus, it describes a collection of agents of various kinds. The functor G maps this object to a category G(x) that describes everything that can be done with this collection of agents.

In many examples considered so far, G(x) is a category whose morphisms are graphs of some sort whose nodes are agents of types c_1, \dots, c_n. Composing these morphisms corresponds to ‘overlaying’ graphs. Network models of this sort let us design networks where the nodes are agents and the edges are communication channels or shared commitments. In our first paper the operation of overlaying graphs was always commutative:

• John Baez, John Foley, Joe Moeller and Blake Pollard, Network models.

Subsequently Joe introduced a more general noncommutative overlay operation:

• Joe Moeller, Noncommutative network models.

This lets us design networks where each agent has a limit on how many communication channels or commitments it can handle; the noncommutativity lets us take a ‘first come, first served’ approach to resolving conflicting commitments.

Here we take a different tack: we instead take G(x) to be a category whose morphisms are processes that the given collection of agents, x, can carry out. Composition of morphisms corresponds to carrying out first one process and then another.

This idea meshes well with Petri net theory, because any Petri net P determines a symmetric monoidal category FP whose morphisms are processes that can be carried out using this Petri net. More precisely, the objects in FP are markings of P, and the morphisms are sequences of ways to change these markings using transitions, e.g.:

Given a Petri net, then, how do we construct a network model G \colon \mathsf{S}(C) \to \mathsf{Cat}, and in particular, what is the set C? In a network model the elements of C represent different kinds of agents. In the simplest scenario, these agents persist in time. Thus, it is natural to take C to be some set of ‘catalysts’. In chemistry, a reaction may require a catalyst to proceed, but it neither increases nor decrease the amount of this catalyst present. In everyday life, a door serves as a catalyst: it lets you walk though a wall, and it doesn’t get used up in the process!

For a Petri net, ‘catalysts’ are species that are neither increased nor decreased in number by any transition. For example, in the following Petri net, species a is a catalyst:

but neither b nor c is a catalyst. The transition \tau_1 requires one token of type a as input to proceed, but it also outputs one token of this type, so the total number of such tokens is unchanged. Similarly, the transition \tau_2 requires no tokens of type a as input to proceed, and it also outputs no tokens of this type, so the total number of such tokens is unchanged.

In Theorem 11 of our paper, we prove that given any Petri net P, and any subset C of the catalysts of P, there is a network model

G \colon \mathsf{S}(C) \to \mathsf{Cat}

An object x \in \mathsf{S}(C) says how many tokens of each catalyst are present; G(x) is then the subcategory of FP where the objects are markings that have this specified amount of each catalyst, and morphisms are processes going between these.

From the functor G \colon \mathsf{S}(C) \to \mathsf{Cat} we can construct a category \int G by ‘gluing together’ all the categories G(x) using the Grothendieck construction. Because G is symmetric monoidal we can use an enhanced version of this construction to make \int G into a symmetric monoidal category. We already did this in our first paper on network models, but by now the math has been better worked out here:

• Joe Moeller and Christina Vasilakopoulou, Monoidal Grothendieck construction.

The tensor product in \int G describes doing processes ‘in parallel’. The category \int G is similar to FP, but it is better suited to applications where agents each have their own ‘individuality’, because FP is actually a commutative monoidal category, where permuting agents has no effect at all, while \int G is not so degenerate. In Theorem 12 of our paper we make this precise by more concretely describing \int G as a symmetric monoidal category, and clarifying its relation to FP.

There are no morphisms between an object of G(x) and an object of G(x') when x \not\cong x', since no transitions can change the amount of catalysts present. The category FP is thus a ‘disjoint union’, or more technically a coproduct, of subcategories FP_i where i, an element of free commutative monoid on C, specifies the amount of each catalyst present.

The tensor product on FP has the property that tensoring an object in FP_i with one in FP_j gives an object in FP_{i+j}, and similarly for morphisms. However, in Theorem 14 we show that each subcategory FP_i also has its own tensor product, which describes doing one process after another while reusing catalysts.

This tensor product is a very cool thing. On the one hand it’s quite obvious: for example, if two people want to walk through a door, they can both do it, one at a time, because the door doesn’t get used up when someone walks through it. On the other hand, it’s mathematically interesting: it turns out to give, not a monoidal category, but something called a ‘premonoidal’ category. This concept, which we explain in our paper, was invented by John Power and Edmund Robinson for use in theoretical computer science.

The paper has lots of pictures involving jeeps and boats, which serve as catalysts to carry people first from a base to the shore and then from the shore to an island. I think these make it clear that the underlying ideas are quite commonsensical. But they need to be formalized to program them into a computer—and it’s nice that doing this brings in some classic themes in category theory!

Some posts in this series:

Part 1. CASCADE: the Complex Adaptive System Composition and Design Environment.

Part 2. Metron’s software for system design.

Part 3. Operads: the basic idea.

Part 4. Network operads: an easy example.

Part 5. Algebras of network operads: some easy examples.

Part 6. Network models.

Part 7. Step-by-step compositional design and tasking using commitment networks.

Part 8. Compositional tasking using category-valued network models.

Part 9 – Network models from Petri nets with catalysts.