Applied Category Theory 2021 — Call for Papers

16 April, 2021


The deadline for submitting papers is coming up soon: May 10th.

Fourth Annual International Conference on Applied Category Theory (ACT 2021), July 12–16, 2021, online and at the Computer Laboratory of the University of Cambridge.

Plans to run ACT 2021 as one of the first physical conferences post-lockdown are progressing well. Consider going to Cambridge! Financial support is available for students and junior researchers.

Applied category theory is a topic of interest for a growing community of researchers, interested in studying many different kinds of systems using category-theoretic tools. These systems are found across computer science, mathematics, and physics, as well as in social science, linguistics, cognition, and neuroscience. The background and experience of our members is as varied as the systems being studied. The goal of the Applied Category Theory conference series is to bring researchers together, disseminate the latest results, and facilitate further development of the field.

We accept submissions of both original research papers, and work accepted/submitted/ published elsewhere. Accepted original research papers will be invited for publication in a proceedings volume. The keynote addresses will be drawn from the best accepted papers. The conference will include an industry showcase event.

We hope to run the conference as a hybrid event, with physical attendees present in Cambridge, and other participants taking part online. However, due to the state of the pandemic, the possibility of in-person attendance is not yet confirmed. Please do not book your travel or hotel accommodation yet.

Financial support

We are able to offer financial support to PhD students and junior researchers. Full guidance is on the webpage.

Important dates (all in 2021)

• Submission Deadline: Monday 10 May
• Author Notification: Monday 7 June
• Financial Support Application Deadline: Monday 7 June
• Financial Support Notification: Tuesday 8 June
• Priority Physical Registration Opens: Wednesday 9 June
• Ordinary Physical Registration Opens: Monday 13 June
• Reserved Accommodation Booking Deadline: Monday 13 June
• Adjoint School: Monday 5 to Friday 9 July
• Main Conference: Monday 12 to Friday 16 July

Submissions

The following two types of submissions are accepted:

Proceedings Track. Original contributions of high-quality work consisting of an extended abstract, up to 12 pages, that provides evidence of results of genuine interest, and with enough detail to allow the program committee to assess the merits of the work. Submission of work-in-progress is encouraged, but it must be more substantial than a research proposal.

Non-Proceedings Track. Descriptions of high-quality work submitted or published elsewhere will also be considered, provided the work is recent and relevant to the conference. The work may be of any length, but the program committee members may only look at the first 3 pages of the submission, so you should ensure that these pages contain sufficient evidence of the quality and rigour of your work.

Papers in the two tracks will be reviewed against the same standards of quality. Since ACT is an interdisciplinary conference, we use two tracks to accommodate the publishing conventions of different disciplines. For example, those from a Computer Science background may prefer the Proceedings Track, while those from a Mathematics, Physics or other background may prefer the Non-Proceedings Track. However, authors from any background are free to choose the track that they prefer, and submissions may be moved from the Proceedings Track to the Non-Proceedings Track at any time at the request of the authors.

Contributions must be submitted in PDF format. Submissions to the Proceedings Track must be prepared with LaTeX, using the EPTCS style files available at http://style.eptcs.org.

The submission link will soon be available on the ACT2021 web page: https://www.cl.cam.ac.uk/events/act2021

Program Committee

Chair:

• Kohei Kishida, University of Illinois, Urbana-Champaign

Members:

• Richard Blute, University of Ottawa
• Spencer Breiner, NIST
• Daniel Cicala, University of New Haven
• Robin Cockett, University of Calgary
• Bob Coecke, Cambridge Quantum Computing
• Geoffrey Cruttwell, Mount Allison University
• Valeria de Paiva, Samsung Research America and University of Birmingham
• Brendan Fong, Massachusetts Institute of Technology
• Jonas Frey, Carnegie Mellon University
• Tobias Fritz, Perimeter Institute for Theoretical Physics
• Fabrizio Romano Genovese, Statebox
• Helle Hvid Hansen, University of Groningen
• Jules Hedges, University of Strathclyde
• Chris Heunen, University of Edinburgh
• Alex Hoffnung, Bridgewater
• Martti Karvonen, University of Ottawa
• Kohei Kishida, University of Illinois, Urbana -Champaign (chair)
• Martha Lewis, University of Bristol
• Bert Lindenhovius, Johannes Kepler University Linz
• Ben MacAdam, University of Calgary
• Dan Marsden, University of Oxford
• Jade Master, University of California, Riverside
• Joe Moeller, NIST
• Koko Muroya, Kyoto University
• Simona Paoli, University of Leicester
• Daniela Petrisan, Université de Paris, IRIF
• Mehrnoosh Sadrzadeh, University College London
• Peter Selinger, Dalhousie University
• Michael Shulman, University of San Diego
• David Spivak, MIT and Topos Institute
• Joshua Tan, University of Oxford
• Dmitry Vagner
• Jamie Vicary, University of Cambridge
• John van de Wetering, Radboud University Nijmegen
• Vladimir Zamdzhiev, Inria, LORIA, Université de Lorraine
• Maaike Zwart


Mathematics in the 21st Century

16 March, 2021

I’m giving a talk in the Topos Institute Colloquium on Thursday March 25, 2021 at 18:00 UTC. That’s 11:00 am Pacific Time.

I’ll say a bit about the developments we might expect if mathematicians could live happily in an ivory tower and never come down for the rest of the century. But my real focus will be on how math will interact with the world outside mathematics.

Mathematics in the 21st Century

Abstract. The climate crisis is part of a bigger transformation in which humanity realizes that the Earth is a finite system and that no physical quantity can grow exponentially forever. This transformation may affect mathematics—and be affected by it—just as dramatically as the agricultural and industrial revolutions. After a review of the problems, we discuss how mathematicians can help make this transformation a bit easier, and some ways in which mathematics may change.

You can see my slides here, and click on links in dark brown for more information. You can watch the talk on YouTube here, either live or recorded later:

You can also watch the talk live on Zoom. Only Zoom lets you ask questions. The password for Zoom can be found on the Topos Institute Colloquium website.


Emerging Researchers in Category Theory

11 March, 2021

 

Eugenia Cheng is an expert on giving clear, fun math talks.

Now you can take a free class from her on how to give clear, fun math talks!

You need to be a grad student in category theory—and priority will be given to those who aren’t at fancy schools, etc.

Her course is called the Emerging Researchers in Category Theory Virtual Seminar, or Em-Cats for short. You can apply for it here:

https://topos.site/em-cats/

The first round of applications is due April 30th. It looks pretty cool, and knowing Eugenia, you’ll get a lot of help on giving talks.

Aims

The aims are, broadly:

• Help the next generation of category theorists become wonderful speakers.
• Make use of the virtual possibilities, and give opportunities to graduate students in places where there is not a category theory group or local seminar they can usefully speak in.
• Give an opportunity to graduate students to have a global audience, especially giving more visibility to students from less famous/large groups.
• Make a general opportunity for community among category theorists who are more isolated than those with local groups.
• Make a series of truly intelligible talks, which we hope students and researchers around the world will enjoy and appreciate.

Talk Preparation and Guidelines

Eugenia Cheng has experience with training graduate students in giving talks, from when she ran a similar seminar for graduate students at the University of Sheffield. Everyone did indeed give an excellent talk.

We ask that all Em-Cats speakers are willing to work with Eugenia and follow her advice. The guidelines document outlines what she believes constitutes a good talk. We acknowledge that this is to some extent a matter of opinion, but these are the guidelines for this particular seminar. Eugenia is confident that with her assistance everyone who wishes to do so will be able to give an excellent, accessible talk, and that this will benefit both the speaker and the community.


Magic Numbers

9 March, 2021

Working in the Manhattan Project, Maria Goeppert Mayer discovered in 1948 that nuclei with certain numbers of protons and/or neutrons are more stable than others. In 1963 she won the Nobel prize for explaining this discovery with her ‘nuclear shell model’.

Nuclei with 2, 8, 20, 28, 50, or 82 protons are especially stable, and also nuclei with 2, 8, 20, 28, 50, 82 or 126 neutrons. Eugene Wigner called these magic numbers, and it’s a fun challenge to explain them.

For starters one can imagine a bunch of identical fermions in a harmonic oscillator potential. In one-dimensional space we have evenly spaced energy levels, each of which holds one state if we ignore spin. I’ll write this as

1, 1, 1, 1, ….

But if we have spin-1/2 fermions, each of these energy levels can hold two spin states, so the numbers double:

2, 2, 2, 2, ….

In two-dimensional space, ignoring spin, the pattern changes to

1, 1+1, 1+1+1, 1+1+1+1, ….

or in other words

1, 2, 3, 4, ….

That is: there’s one state of the lowest possible energy, 2 states of the next energy, and so on. Including spin the numbers double:

2, 4, 6, 8, ….

In three-dimensional space the pattern changes to this if we ignore spin:

1, 1+2, 1+2+3, 1+2+3+4, ….

or

1, 3, 6, 10, ….

So, we’re getting triangular numbers! Here’s a nice picture of these states, drawn by J. G. Moxness:


Including spin the numbers double:

2, 6, 12, 20, ….

So, there are 2 states of the lowest energy, 2+6 = 8 states of the first two energies, 2+6+12 = 20 states of the first three energies, and so on. We’ve got the first 3 magic numbers right! But then things break down: next we get 2+6+12+20 = 40, while the next magic number is just 28.

Wikipedia has a nice explanation of what goes wrong and how to fix it to get the next few magic numbers right:

Nuclear shell model.

We need to take two more effects into account. First, ‘spin-orbit interactions’ decrease the energy of a state when some spins point in the opposite direction from the orbital angular momentum. Second, the harmonic oscillator potential gets flattened out at large distances, so states of high angular momentum have less energy than you’d expect. I won’t attempt to explain the details, since Wikipedia does a pretty good job and I’m going to want breakfast soon. Here’s a picture that cryptically summarizes the analysis:

The notation is old-fashioned, from spectroscopy—you may know it if you’ve studied atomic physics, or chemistry. If you don’t know it, don’t worry about it! The main point is that the energy levels in the simple story I just told change a bit. They don’t change much until we hit the fourth magic number; then 8 of the next 20 energy levels get lowered so much that this magic number is 2+6+12+8 = 28 instead of 2+6+12+20 = 40. Things go on from there.

But here’s something cute: our simplified calculation of the magic numbers actually matches the count of states in each energy level for a four-dimensional harmonic oscillator! In four dimensions, if we ignore spin, the number of states in each energy level goes like this:

1, 1+3, 1+3+6, 1+3+6+10, …

These are the tetrahedral numbers:

Doubling them to take spin into account, we get the first three magic numbers right! Then, alas, we get 40 instead of 28.

But we can understand some interesting features of the world using just the first three magic numbers: 2, 8, and 20.

For example, helium-4 has 2 protons and 2 neutrons, so it’s ‘doubly magic’ and very stable. It’s the second most common substance in the universe! And in radioactive decays, often a helium nucleus gets shot out. Before people knew what it was, people called it an ‘alpha particle’… and the name stuck.

Oxygen-16, with 8 protons and 8 neutrons, is also doubly magic. So is calcium-40, with 20 protons and 20 neutrons. This is the heaviest stable element with the same number of protons and neutrons! After that, the repulsive electric charge of the protons needs to be counteracted by a greater number of neutrons.

A wilder example is helium-10, with 2 protons and 8 neutrons. It’s doubly magic, but not stable. It just barely clings to existence, helped by all that magic.

Here’s one thing I didn’t explain yet, which is actually pretty easy. Why is it true that—ignoring the spin—the number of states of the harmonic oscillator in the nth energy level follows this pattern in one-dimensional space:

1, 1, 1, 1, ….

and this pattern in two-dimensional space:

1, 1+1 = 2, 1+1+1 = 3, 1+1+1+1 = 4, …

and this pattern in three-dimensional space:

1, 1+2 = 3, 1+2+3 = 6, 1+2+3+4 = 10, ….

and this pattern in four-dimensional space:

1, 1+3 = 4, 1+3+6 = 10, 1+3+6+10 = 20, ….

and so on?

To see this we need to know two things. First, the allowed energies for a harmonic oscillator in one-dimensional space are equally spaced. So, if we say the lowest energy allowed is 0, by convention, and choose units where the next allowed energy is 1, then the allowed energies are the natural numbers:

0, 1, 2, 3, 4, ….

Second, a harmonic oscillator in n-dimensional space is just like n independent harmonic oscillators in one-dimensional space. In particular, its energy is just the sum of their energies.

So, the number of states of energy E for an n-dimensional oscillator is just the number of ways of writing E as a sum of a list of n natural numbers! The order of the list matters here: writing 3 as 1+2 counts as different than writing it as 2+1.

This leads to the patterns we’ve seen. For example, consider a harmonic oscillator in two-dimensional space. It has 1 state of energy 0, namely

0+0

It has 2 states of energy 1, namely

1+0 and 0+1

It has 3 states of energy 2, namely

2+0 and 1+1 and 0+2

and so on.

Next, consider a harmonic oscillator in three-dimensional space. This has 1 state of energy 0, namely

0+0+0

It has 3 states of energy 1, namely

1+0+0 and 0+1+0 and 0+0+1

It has 6 states of energy 2, namely

2+0+0 and 1+1+0 and 1+0+1 and 0+2+0 and 0+1+1 and 0+0+2

and so on. You can check that we’re getting triangular numbers: 1, 3, 6, etc. The easiest way is to note that to get a state of energy E, the first of the three independent oscillators can have any natural number j from 0 to E as its energy, and then there are E – j ways to choose the energies of the other two oscillators so that they sum to E – j. This gives a total of

E + (E-1) + (E-2) + \cdots + 1

states, and this is a triangular number.

The pattern continues in a recursive way: in four-dimensional space the same sort of argument gives us tetrahedral numbers because these are sums of triangular numbers, and so on. We’re getting the diagonals of Pascal’s triangle, otherwise known as binomial coefficients.



We often think of the binomial coefficient

\displaystyle{\binom{n}{k} }

as the number of ways of choosing a k-element subset of an n-element set. But here we are seeing it’s the number of ways of choosing an ordered (k+1)-tuple of natural numbers that sum to n. You may enjoy finding a quick proof that these two things are equal!


Native Type Theory

24 February, 2021

guest post by Christian Williams

Native Type Theory is a new paper by myself and Mike Stay. We propose a unifying method of reasoning for programming languages: model a language as a theory, form the category of presheaves, and use the internal language of the topos.

\mathtt{language} \xrightarrow{\;\Lambda\;} \mathtt{category} \xrightarrow{\;\mathscr{P}\;} \mathtt{topos} \xrightarrow{\;\Phi\;} \mathtt{type\; system}

Though these steps are known, the original aspect is simply the composite and its application to software. If implemented properly, we believe that native types can be very useful to the virtual world. Here, I want to share some of what we’ve learned so far.

The Free Lunch

The biggest lesson of this paper was to have faith in what John Baez calls the dao of mathematics. For two years, Mike and I and Greg Meredith looked for ways to generate logics for programming languages; we tried many approaches, but ultimately the solution was the simplest.

Two facts of category theory provide an abundance of structure, for free:

  1. Every category embeds into its presheaf topos.
  2. Every topos has a rich internal language.

The embedding preserves limits and exponents, hence we can apply this to “higher-order theories”.

For now we explore the language of a topos. There are multiple views, and often its full power is not used. Toposes support geometric logic, predicate logic, and moreover dependent type theory. We emphasize the latter: dependent types are expressive and pervasive, yet underutilized in mathematics.

The Language of a Topos

My thinking has been shaped by the idea that even foundations are categorical. Virtually any language can be modelled as a structured category: the most comprehensive reference I’ve found is Categorical Logic and Type Theory by Bart Jacobs.

Probably the most studied categorical structure of logic is the topos. Toposes of sheaves, functors which coherently assign data to a space, were first applied to algebraic geometry. A continuous map f\colon X\to Y induces an inverse image f\colon  Sh(Y)\to Sh(X) which is a left adjoint that preserves finite limits. This gives geometric morphisms of toposes, and geometric logic (\wedge and \exists) as the language of classifying toposes.

Though geometric logic is an important level of generality, the language of toposes is more powerful. In La Jolla, California 1965, the budding category theory community recognized Grothendieck’s categories of sheaves as being fundamentally logical structures, which generalize set theory. An elementary topos is a cartesian closed category with finite limits and a subobject classifier, an object which represents the correspondence of predicates and subobjects.

The language of an elementary topos T is encapsulated in a pair of structures.

• The predicate fibration \Omega\text{T}\to \text{T} reasons about predicates, like subsets.

• The codomain fibration \Delta\text{T}\to \text{T} reasons about dependent types, like indexed sets.

Predicate Logic

Throughout mathematics, we use the internal predicate logic of Set. It is the canonical example of a topos: a predicate such as \varphi(x)= (x+3\geq 5) is a function \varphi:X\to 2=\{t,f\}, which corresponds to its comprehension, the subobject of true terms \{x\in X \;|\; \varphi(x)=t\}\subseteq X.

Predicates on any set X form a Boolean algebra P(X)=[X,2], ordered by implication. Every function f:X\to Y gives an inverse image P(f):P(Y)\to P(X). This defines a functor P:\text{Set}^{\text{op}} \to \text{Bool} which is a first-order hyperdoctrine: each P(f) has adjoints \exists_f\dashv P(f)\dashv \forall_f representing quantification, which satisfy the Beck–Chevalley condition.

Altogether, this structure formalizes classical higher-order predicate logic. Most formulae, such as

\forall x,y:\mathbb{Q}.\; \exists z:\mathbb{Q}.\; x< z \wedge z< y

\forall f:Y^X.\; \forall y:Y.\; \exists x:X.\; f(x)=y \Rightarrow
\exists g:X^Y.\; \forall y:Y.\; f(g(y))=y

can be modelled in this logical structure of \text{Set}.

This idea is fairly well-known; people often talk about the “Mitchell-Benabou language” of a topos. However, this language is predicate logic over a simple type theory, meaning that the only type formation rules are products and functions. Many constructions in mathematics do not fit into this language, because types often depend on terms:

\text{Nat}(n) := \{m:\mathbb{N} \;|\; m\leq n\}

\mathbb{Z}_p := \mathbb{Z}/\langle x\sim y \equiv \exists z:\mathbb{Z}.\; (x-y)=z\cdot p\rangle

This is provided by extending predicate logic with dependent types, described in the next section.

So, we have briefly discussed how the structure of Set allows for the the explicit construction of predicates used in everyday mathematics. The significance is that these can be constructed in any topos: we thereby generalize the historical conception of logic.

For example, in a presheaf topos [C^{\text{op}},\text{Set}], the law of excluded middle does not hold, and for good reason. Negation of a sieve is necessarily more subtle than negation of subsets, because we must exclude the possibility that a morphism is not in but “precomposes in” to a sieve. This will be explored more in the applications post.

Dependent Type Theory

Dependency is pervasive throughout mathematics. What is a monoid? It’s a set M, and then operations m,e on M, and then conditions on m,e. Most objects are constructed in layers, each of which depends on the ones before. Type theory is often regarded as “fancy” and only necessary in complex situations, similar to misperceptions of category theory; yet dependent types are everywhere.

The basic idea is to represent dependency using preimage. A type which depends on terms of another type, x:A\vdash B(x):\text{Type}, can be understood as an indexed set \{B(x)\}_{x:A}, and this in turn is represented as a function \coprod x:A.\; B(x)\to A. Hence the “world of types which depend on A” is the slice category \text{Set}/A.

The poset of “A-predicates” sits inside the category of “A-types”: a comprehension is an injection \{x\in A \;|\; \varphi(x)\}\to A. This is a degenerate kind of dependent type, where preimages are truth values rather than sets. So we are expanding into a larger environment, which shares all of the same structure. The slice category \text{Set}/A is a categorification of P(A): its morphisms are commuting triangles, understood as A-indexed functions.

Every function f\colon A\to B gives a functor f^\ast: \text{Set}/B\to \text{Set}/A by pullback; this generalizes preimage, and can be expressed as substitution: given p:S\to B, we can form the A-type

x:A\vdash f^\ast(S)(x) = S(f(x)):\text{Type}.

This functor has adjoints \Sigma_f\dashv f^\ast\dashv \Pi_f, called dependent sum and dependent product: these are the powerful tools for constructing dependent types. They generalize not only quantification, but also product and hom: the triple adjunction induces an adjoint co/monad on \text{Set}/B

\Sigma_f\circ f^\ast = -\times f \dashv [f,-] = \Pi_f\circ f^\ast.

These dependent generalizations of product and function types are extremely useful.

Indexed sum generalizes product type by allowing the type of the second coordinate to depend on the term in the first coordinate. For example: \Sigma n:\mathbb{N}.\text{List}(n) consists of dependent pairs \langle n, l:\text{List}(n)\rangle.

Indexed product generalizes function type by allowing the type of the codomain to depend on the term in the domain. For example: \Pi S:\text{Set}.\text{List}(S) consists of dependent functions \lambda S:\text{Set}.\varphi(S):\text{List}(S).

See how natural they are? We use them all the time, often without realizing. Simply by using preimage for indexing, we generalize product and function types to “branching” versions, allowing us to build up complex objects such as

\text{Monoid}:= \Sigma M:\text{Set}.\Sigma m:M^2\to M.\Sigma e:1\to M...
...\Pi (a,b,c):M^3. m(m(a,b),c)=m(a,m(b,c)).
\Pi a:M. m(e,a)=a=m(a,e).

This rich language is available in any topos. I think we’ve hardly begun to see its utility in mathematics, computation, and everyday life.

All Together

A topos has two systems, predicate logic and dependent type theory. Each is modelled by a fibration, a functor into the topos for which the preimage of A are the A-predicates / A-types. A morphism in the domain is a judgement of the form “in the context of variables of these (dependent) types, this term is of this (dependent) type”.

a:A,b:B(a),\dots, z:Z(y)\vdash t:T

The two fibrations are connected by comprehension which converts a predicate to a type, and image factorization which converts a type to a predicate. These give that the predicate fibration is a reflective subcategory of the type fibration.

Altogether, this forms the full higher-order dependent type theory of a topos (Jacobs Ch.11). As far as I know, this is what deserves to be called “the” language of a topos, in its full glory. This type theory is used in proof assistants such as Coq and Agda; eventually, this expressive logic + dependent types will be utilized in many programming languages.

Conclusion

Native Type Theory gives provides a shared framework of reasoning for a broad class of languages. We believe that this could have a significant impact on software and system design, if integrated into existing systems.

In the next post, we’ll explore why this language is so useful for the topos of presheaves on theories. Please let me know any thoughts or questions about this post and especially the paper. Thank you.


Applied Category Theory 2021

17 February, 2021


The big annual applied category theory conference is coming! It’s the fourth one: the first three were at Leiden, Oxford and (virtually) MIT. This one will be online and also, with luck, in person—but don’t make your travel arrangements just yet:

Fourth Annual International Conference on Applied Category Theory (ACT 2021), 12–16 July 2021, online and at the Computer Laboratory of the University of Cambridge.

It will take place shortly after the Applied Category Theory Adjoint School, which will—with luck—culminate in a meeting 5–9 July at the same location.

You can now submit a paper! As in a computer science conference, that’s how you get to give a talk. For more details, read on.

Overview

Applied category theory is a topic of interest for a growing community of researchers, interested in studying many different kinds of systems using category-theoretic tools. These systems are found across computer science, mathematics, and physics, as well as in social science, linguistics, cognition, and neuroscience. The background and experience of our members is as varied as the systems being studied. The goal of the Applied Category Theory conference series is to bring researchers
together, disseminate the latest results, and facilitate further development of the field.

We accept submissions of both original research papers, and work accepted/submitted/ published elsewhere. Accepted original research papers will be invited for publication in a proceedings volume. The keynote addresses will be drawn from the best accepted papers. The conference will include an industry showcase event.

We hope to run the conference as a hybrid event, with physical attendees present in Cambridge, and other participants taking part online. However, due to the state of the pandemic, the possibility of in-person attendance is not yet confirmed. Please do not book your travel or hotel accommodation yet.

Important dates (all in 2021)

• Submission of contributed papers: Monday 10 May

• Acceptance/rejection notification: Monday 7 June

• Adjoint school: Monday 5 July to Friday 9 July

• Main conference: Monday 12 July to Friday 16 July

Submissions

The following two types of submissions are accepted:

• Proceedings Track. Original contributions of high-quality work consisting of an extended abstract, up to 12 pages, that provides evidence of results of genuine interest, and with enough detail to allow the program committee to assess the merits of the work. Submission of work-in-progress is encouraged, but it must be more substantial than a research proposal.

• Non-Proceedings Track. Descriptions of high-quality work submitted or published elsewhere will also be considered, provided the work is recent and relevant to the conference. The work may be of any length, but the program committee members may only look at the first 3 pages of the submission, so you should ensure that these pages contain sufficient evidence of the quality and rigour of your work.

Papers in the two tracks will be reviewed against the same standards of quality. Since ACT is an interdisciplinary conference, we use two tracks to accommodate the publishing conventions of different disciplines. For example, those from a Computer Science background may prefer the Proceedings Track, while those from a Mathematics, Physics or other background may prefer the Non-Proceedings Track. However, authors from any background are free to choose the track that they prefer, and submissions may be moved from the Proceedings Track to the Non-Proceedings Track at any time at the request of the authors.

Contributions must be submitted in PDF format. Submissions to the Proceedings Track must be prepared with LaTeX, using the EPTCS style files available at

http://style.eptcs.org

The submission link will soon be available on the ACT2021 web page:

https://www.cl.cam.ac.uk/events/act2021

Program committee

Chair: Kohei Kishida, University of Illinois, Urbana-Champaign

The full program committee will be announced soon.

Local organizers

• Lukas Heidemann, University of Oxford
• Nick Hu, University of Oxford
• Ioannis Markakis, University of Cambridge
• Alex Rice, University of Cambridge
• Calin Tataru, University of Cambridge
• Jamie Vicary, University of Cambridge

Steering committee

• John Baez, University of California Riverside and Centre for Quantum Technologies
• Bob Coecke, Cambridge Quantum Computing
• Dorette Pronk, Dalhousie University
• David Spivak, Topos Institute


Structured vs Decorated Cospans

30 January, 2021

Some of us just finished a paper clarifying the connection between two approaches to describing open systems—that is, systems that can interact with their environment, and can be composed to form larger open systems:

• John Baez, Kenny Courser and Christina Vasilakopolou, Structured versus decorated cospans.

And, next week I’m giving a talk about it at YAMCaTS! This is not a conference for felines who like sweet potatoes: it’s the Yorkshire and Midlands Category Seminar, organized by Simona Paoli, Nicola Gambino and Steve Vickers.

In my talk, I’ll start by sketching some ideas behind Halter and Patterson’s software for quickly assembling larger models of COVID-19 from smaller models. Then, I’ll dig deeper into the underlying math, where we use ‘structured’ or ‘decorated’ cospans to model open systems.

This quickly gets into some serious category theory—and since YAMCaTS is a category theory seminar, I won’t shy away from that. Here are my slides:

• John Baez, Structured vs decorated cospans, YAMCaTS, Friday 5 February 2021, 17:00 UTC. Zoom link here, meeting ID 810 4239 7132; to get in use 68302x where x is a one-digit perfect number.

Abstract. One goal of applied category theory is to understand open systems: that is, systems that can interact with the external world. We compare two approaches to describing open systems as cospans equipped with extra data: structured and decorated cospans. Each approach provides a symmetric monoidal double category, and we prove that under certain conditions these symmetric monoidal double categories are isomorphic. We illustrate these ideas with applications to dynamical systems and epidemiological modeling. This is joint work with Kenny Courser and Christina Vasilakopoulou.

I don’t know if my talk will be recorded, but it will be on Zoom so recording it would be easy, and I’ll try to get the organizers to do that.

For videos and slides of two related talks go here:

Structured cospans and double categories.

Structured cospans and Petri nets.

For more, read these:

• Evan Patterson and Micah Halter, Compositional epidemiological modeling using structured cospans.

• John Baez and Kenny Courser, Structured cospans.

• Kenny Courser, Open Systems: a Double Categorical Perspective. (Blog articles here.)

• Michael Shulman, Framed bicategories and monoidal fibrations.

• Joe Moeller and Christina Vasilakopolou, Monoidal Grothendieck construction.

To read more about the network theory project, go here:

Network theory.


Open Systems: A Double Categorical Perspective (Part 3)

23 January, 2021

Back to Kenny Courser’s thesis:

• Kenny Courser, Open Systems: A Double Categorical Perspective, Ph.D. thesis, U. C. Riverside, 2020.

Last time I explained the problems with decorated cospans as a framework for dealing with open systems. I vaguely hinted that Kenny’s thesis presents two solutions to these problems: so-called ‘structured cospans’, and a new improved approach to decorated cospans. Now let me explain these!

You may wonder why I’m returning to this now, after three months of silence. The reason is that Kenny, Christina Vasilakopolou, and I just finished a paper that continues this story:

• John Baez, Kenny Courser and Christina Vasilakopoulou, Structured versus decorated cospans.

We showed that under certain conditions, structured and decorated cospans are equivalent. So, I’m excited about this stuff again.

Last time I explained Fong’s theorem about decorated cospans:

Fong’s Theorem. Suppose \mathsf{A} is a category with finite colimits, and make \mathsf{A} into a symmetric monoidal category with its coproduct as the tensor product. Suppose F\colon (\mathsf{A},+) \to (\mathsf{Set},\times) is a symmetric lax monoidal functor. Define an F-decorated cospan to be a cospan

in \mathsf{A} together with an element x\in F(N) called a decoration. Then there is a symmetric monoidal category with

• objects of \mathsf{A} as objects,
• isomorphism classes of F-decorated cospans as morphisms.

The theorem is true, but it doesn’t apply to all the examples we wanted it to. The problem is that it’s ‘not categorified enough’. It’s fine if we want to decorate the apex N of our cospan with some extra structure: we do this by choosing an element of some set F(N). But in practice, we often want to decorate N with some extra stuff, which means choosing an object of a category F(N). So we should really use not a functor

F\colon (\mathsf{A},+) \to (\mathsf{Set},\times)

but something like a functor

F\colon (\mathsf{A},+) \to (\mathbf{Cat},\times)

What do I mean by ‘something like a functor?’ Well, \mathbf{Cat} is not just a category but a 2-category: it has categories as objects, functors as morphisms, but also natural transformations as 2-morphisms. The natural notion of ‘something like a functor’ from a category to a 2-category is called a pseudofunctor. And just as we can define symmetric lax monoidal functor, we can define a symmetric lax monoidal pseudofunctor.

All these nuances really matter when we’re studying open graphs, as we were last time!

Here we want the feet of our structured cospan to be finite sets and the apex to be a finite graph. So, we have \mathsf{A} = \mathsf{FinSet} and for any N \in \mathsf{FinSet} we want F(N) to be the set, or category, of finite graphs having N as their set of nodes.

I explained last time all the disasters that ensue when you try to let F(N) be the set of finite graphs having N as its set of nodes. You can try, but you will pay dearly for it! You can struggle and fight, like Hercules trying to chop all the heads off the Hydra, but you still can’t get a symmetric lax monoidal functor

F\colon (\mathsf{A},+) \to (\mathsf{Set},\times)

that sends any finite set N to the set of graphs having N as their set of nodes.

But there is a perfectly nice category F(N) of all finite graphs having N as their set of nodes. And you can get a symmetric lax monoidal pseudofunctor

F\colon (\mathsf{A},+) \to (\mathbf{Cat},\times)

that sends any any finite set to the category of finite graphs having it as nodes. So you should stop fighting and go with the flow.

Kenny, Christina and I proved an enhanced version of Fong’s theorem that works starting from this more general kind of F. And instead of just giving you a symmetric monoidal category, this theorem gives you a symmetric monoidal double category.

In fact, that is something you should have wanted already, even with Fong’s original hypotheses! The clue is that Fong’s theorem uses isomorphism classes of decorated cospans, which suggests we’d get something better if we used decorated cospans themselves. Kenny tackled this a while ago, getting a version of Fong’s theorem that produces a symmetric monoidal double category, and another version that produces a symmetric monoidal bicategory:

• Kenny Courser, A bicategory of decorated cospans, Theory and Applications of Categories 32 (2017), 995–1027.

Over the years we’ve realized that the double category is better, because it contains more information and is easier to work with. So, in our new improved approach to decorated cospans, we go straight for the jugular and get a double category. And here’s how it works:

Theorem. Suppose \mathsf{A} is a category with finite colimits, and make \mathsf{A} into a symmetric monoidal category with its coproduct as the tensor product. Suppose F\colon (\mathsf{A},+) \to (\mathbf{Cat},\times) is a symmetric lax monoidal pseudofunctor. Then there is a symmetric monoidal double category F\mathbb{C}\mathbf{sp} in which

• an object is an object of \mathsf{A}
• a vertical morphism is a morphism in \mathsf{A}
• a horizontal morphism is an F-decorated cospan, meaning a cospan in \mathsf{A} together with a decoration:


• a 2-morphism is a map of decorated cospans, meaning a commutative diagram in \mathsf{A}:

together with a morphism \tau \colon F(h)(x) \to x', the map of decorations.

We call F\mathbb{C}\mathbf{sp} a decorated cospan double category. And as our paper explains, this idea lets us fix all the broken attempted applications of Fong’s original decorated cospan categories!

All this is just what any category theorist worth their salt would try, in order to fix the original problems with decorated cospans. It turns out that proving the theorem above is not so easy, mainly because the definition of ‘symmetric monoidal double category’ is rather complex. But if you accept the theorem—including the details of how you get the symmetric monoidal structure on the double category, which I have spared you here—then it doesn’t really matter much that the proof takes work.

Next time I’ll tell you about the other way to fix the original decorated cospan formalism: structured cospans. When these work, they are often easier to use.


Part 1: an overview of Courser’s thesis and related papers.

Part 2: problems with the original decorated cospans.

Part 3: the new improved decorated cospans.


Categories of Nets (Part 2)

20 January, 2021

guest post by Michael Shulman

Now that John gave an overview of the Petri nets paper that he and I have just written with Jade and Fabrizio, I want to dive a bit more into what we accomplish. The genesis of this paper was a paper written by Fabrizio and several other folks entitled Computational Petri Nets: Adjunctions Considered Harmful, which of course sounds to a category theorist like a challenge. Our paper, and particularly the notion of Σ-net and the adjunction in the middle column relating Σ-nets to symmetric strict monoidal categories, is an answer to that challenge.

Suppose you wanted to “freely” generate a symmetric monoidal category from some combinatorial data. What could that data be? In other words (for a category theorist at least), what sort of category \mathsf{C} appears in an adjunction \mathsf{C} \rightleftarrows \mathsf{SMC}? (By the way, all monoidal categories in this post will be strict, so I’m going to drop that adjective for conciseness.)

Perhaps the simplest choice is the same data that naturally generates a plain category, namely a directed graph. However, this is pretty limited in terms of what symmetric monoidal categories it can generate, since the generating morphisms will always only have single generating objects as their domain and codomain.

Another natural choice is the same data that naturally generates a multicategory, which might be called a “multigraph”: a set of objects together with, for every tuple of objects x_1,\dots,x_n and single object y, a set of arrows from (x_1,\dots,x_n) to y. In the generated symmetric monoidal category, such an arrow gives rise to a morphism x_1\otimes\cdots\otimes x_n \to y; thus we can now have multiple generating objects in the domains of generating morphisms, but not the codomains.

Of course, this suggests an even better solution: a set of objects, together with a set of arrows for every pair of tuples (x_1,\dots,x_m) and (y_1,\dots,y_n). I’d be tempted to call this a “polygraph”, since it also naturally generates a polycategory. But other folks got there first and called it a “tensor scheme” and also a “pre-net”. In the latter case, the objects are called “places” and the morphisms “transitions”. But whatever we call it, it allows us to generate free symmetric monoidal categories in which the domains and codomains of generating morphisms can both be arbitrary tensor products of generating objects. For those who like fancy higher-categorical machinery, it’s the notion of computad obtained from the monad for symmetric monoidal categories.

However, pre-nets are not without flaws. One of the most glaring, for people who actually want to compute with freely generated symmetric monoidal categories, is that there aren’t enough morphisms between them. For instance, suppose one pre-net N has three places x,y,z and a transition f:(x,x,y) \to z, while a second pre-net N' has three places x',y',z' and a transition f':(x',y',x') \to z'. Once we generate a symmetric monoidal category, then f can be composed with a symmetry x\otimes y \otimes x \cong x\otimes x\otimes y and similarly for f'; so the symmetric monoidal categories generated by N and N' are isomorphic. But there isn’t even a single map of pre-nets from N to N' or vice versa, because a map of pre-nets has to preserve the ordering on the inputs and outputs. This is weird and annoying for combinatorial data that’s supposed to present a symmetric monoidal category.

Another way of making essentially the same point is that just as the adjunction between SMCs and directed graphs factors through categories, and the adjunction between SMCs and multigraphs factors through multicategories, the adjunction between SMCs and pre-nets factors through non-symmetric monoidal categories. In other words, a pre-net is really better viewed as data for generating a non-symmetric monoidal category, which we can then freely add symmetries to.

By contrast, in the objects that we call “Petri nets”, the domain and codomain of each generating morphism are elements of the free commutative monoid on the set of places—as opposed to elements of the free monoid, which is what they are for a pre-net. Thus, the domain of f and f' above would be x+x+y and x+y+x respectively, which in a commutative monoid are equal (both are 2x+y). So the corresponding Petri nets of N and N' are indeed isomorphic. However, once we squash everything down in this way, we lose the ability to functorially generate a symmetric monoidal category; all we can generate is a commutative monoidal category where all the symmetries are identities.

At this point we’ve described the upper row and the left- and right-hand columns in John’s diagram:

What’s missing is a kind of net in the middle that corresponds to symmetric monoidal categories. To motivate the definition of Σ-net, consider how to solve the problem above of the “missing morphisms”. We want to send f:(x,x,y) \to z to a “permuted version” of f':(x',y',x') \to z'. For this to be implemented by an actual set-map, we need this “permuted version” to be present in the data of N' somehow. This suggests that the transitions should come with a permutation action like that of, say, a symmetric multicategory. Then inside N' we can actually act on f' by the transposition \tau = (2,3) \in S_3, yielding a new morphism \tau(f') : (x',x',y')\to z' which we can take to be the image of f. Of course, we can also act on f' by other permutations, and likewise on f; but since these permutation actions are part of the structure they must be preserved by the morphism, so sending f to \tau(f') uniquely determines where we have to send all these permutation images.

Now you can go back and look again at John’s definition of Σ-net: a set S, a groupoid T, and a discrete opfibration T \to P S \times P S ^{op}, where P denotes the free-symmetric-strict-monoidal-category functor \mathsf{Set} \to \mathsf{Cat}. Such a discrete opfibration is the same as a functor N \colon P S \times P S ^{op} \to \mathsf{Set}, and the objects of P S are the finite sequences of elements of S while its morphisms are permutations; thus this is precisely a pre-net (the action of the functor N on objects) with permutation actions as described above. I won’t get into the details of constructing the adjunction relating Σ-nets to symmetric monoidal categories; you can read the paper, or maybe I’ll blog about it later.

However, in solving the “missing morphisms” problem, we’ve introduced a new possibility. Suppose we act on f \colon (x,x,y) \to z by the transposition \sigma = (1,2) \in S_3 that switches the first two entries. We get another transition (x,x,y)\to z with the same domain and codomain as f; so it might equal f, or it might not! In other words, transitions in a Σ-net can have isotropy. If \sigma(f)=f, then when we generate a free symmetric monoidal category from our Σ-net, the corresponding morphism f:x\otimes x \otimes y \to z will have the property that when we compose it with the symmetry morphism x\otimes x\otimes y \cong x\otimes x\otimes y we get back f again. No symmetric monoidal category generated by a pre-net has this property; it’s more like the behavior of the commutative monoidal category generated by a Petri net, except that in the latter case the symmetry x\otimes x\otimes y \cong x\otimes x\otimes y itself is the identity, rather than just acting by the identity on f.

This suggests that Σ-nets can either “behave like pre-nets” or “behave like Petri nets”. This is made precise by the bottom row of adjunctions in the diagram. On one hand, we can map a pre-net to a Σ-net by freely generating the action of all permutations. This has a right adjoint that just forgets the permutation action (which actually has a further right adjoint, although that’s a bit weird). On the other hand, we can map a Petri net to a Σ-net by making all the permutations act as trivially as possible; this has a left adjoint that identifies each transition with all its permutation images. And these adjunctions commute with the three “free monoidal category” adjunctions in reasonable ways (see the paper for details).

The right adjoint mapping Petri nets into Σ-nets is fully faithful, so we really can say that Σ-nets “include” Petri nets. The left adjoint mapping pre-nets to Σ-nets is not fully faithful—it can’t possibly be, since the whole point of introducing Σ-nets was that pre-nets don’t have enough morphisms! But the full image of this functor is equivalent to a fourth kind of net: Kock’s whole-grain Petri nets. Kock’s approach to solving the problem of pre-nets is somewhat different, more analogous to the notion of “fat” symmetric monoidal category: he takes the domain and codomain of each transition to be a family of places indexed by a finite set. But his category turns out to be equivalent to the category of Σ-nets that are freely generated by some pre-net. (Kock actually proved this himself, as well as sketching the adjunction between Σ-nets and symmetric monoidal categories. He called Σ-nets “digraphical species”.)

So Σ-nets “include” both Petri nets and pre-nets, in an appropriate sense. The pre-nets (or, more precisely, whole-grain nets) are the Σ-nets with free permutation actions (trivial isotropy), while the Petri nets are the Σ-nets with trivial permutation actions (maximal isotropy). In Petri-net-ese, these correspond to the “individual token philosophy” and the “collective token philosophy”, respectively. (This makes it tempting to refer to the functors from Σ-nets to pre-nets and Petri nets as individuation and collectivization respectively.) But Σ-nets also allow us to mix and match the two philosophies, having some transitions with trivial isotropy, others with maximal isotropy, and still others with intermediate isotropy.

I like to think of Σ-nets as a Petri net analogue of orbifolds. Commutative-monoid-based Petri nets are like “coarse moduli spaces”, where we’ve quotiented by all symmetries but destroyed all the isotropy information; while whole-grain Petri nets are like manifolds, where we have no singularities but can only quotient by free actions. Pre-nets can then be thought of a “presentation” of a manifold, such as by a particular way of gluing coordinate patches together: useful in concrete examples, but not the “invariant” object we really want to study mathematically.


Part 1: three kinds of nets, and the kinds of monoidal categories they generate.

Part 2: what kind of net is best for generating symmetric monoidal categories?


Categories of Nets (Part 1)

17 January, 2021

I’ve been thinking about Petri nets a lot. Around 2010, I got excited about using them to describe chemical reactions, population dynamics and more, using ideas taken from quantum physics. Then I started working with my student Blake Pollard on ‘open’ Petri nets, which you can glue together to form larger Petri nets. Blake and I focused on their applications to chemistry, but later my student Jade Master and I applied them to computer science and brought in some new math. I was delighted when Evan Patterson and Micah Halter used all this math, along with ideas of Joachim Kock, to develop software for rapidly assembling models of COVID-19.

Now I’m happy to announce that Jade and I have teamed up with Fabrizio Genovese and Mike Shulman to straighten out a lot of mysteries concerning Petri nets and their variants:

• John Baez, Fabrizio Genovese, Jade Master and Mike Shulman, Categories of nets.

This paper is full of interesting ideas, but I’ll just tell you the basic framework.

A Petri net is a seemingly simple thing:

It consists of places (drawn as circles) and transitions (drawn as boxes), with directed edges called arcs from places to transitions and from transitions to places.

The idea is that when you use a Petri net, you put dots called tokens in the places, and then move them around using the transitions:

A Petri net is actually a way of describing a monoidal category. A way of putting a bunch of tokens in the places gives an object of this category, and a way of moving them around repeatedly (as above) gives a morphism.

The idea sounds straightforward enough. But it conceals some subtleties, which researchers have been struggling with for at least 30 years.

There are various ways to make the definition of Petri net precise. For example: is there a finite set of arcs from a given place to a given transition (and the other way around), or merely a natural number of arcs? If there is a finite set, is this set equipped with an ordering or not? Furthermore, what is a morphism between Petri nets?

Different answers are good for different purposes. In the so-called ‘individual token philosophy’, we allow a finite set of tokens in each place. In the ‘collective token philosophy’, we merely allow a natural number of tokens in each place. It’s like the difference between having 4 individual workers named John, Fabrizio, Jade and Mike where you can tell who did what, and having 4 anonymous workers: nameless drones.

Our goal was to sort this out all and make it crystal clear. We focus on 3 kinds of net, each of which naturally generates its own kind of monoidal category:

pre-nets, which generate free strict monoidal categories.

Σ-nets, which generate free symmetric strict monoidal categories.

Petri nets, which generate free commutative monoidal categories.

These three kinds of monoidal category differ in how ‘commutative’ they are:

• In a strict monoidal category we typically have x \otimes y \ne y \otimes x.

• In a strict symmetric monoidal category we have for each pair of objects a chosen isomorphism x \otimes y \cong y \otimes x.

• A commutative monoidal category is a symmetric strict monoidal category where the symmetry isomorphisms are all identities, so x \otimes y = y \otimes x.

So, we have a spectrum running from hardcore individualism, where two different things of the same type are never interchangeable… to hardcore collectivism, where two different things of the same type are so interchangeable that switching them counts as doing nothing at all! In the theory of Petri nets and their variants, the two extremes have been studied better than the middle.

You can summarize the story with this diagram:

There are three different categories of nets at bottom, and three diffferent categories of monoidal categories on top — all related by adjoint functors! Here the left adjoints point up the page — since different kinds of nets freely generate different kinds of monoidal categories — and also to the right, in the direction of increasing ‘commutativity’.

If you’re a category theorist you’ll recognize at least two of the three categories on top:

\mathsf{StrMC}, with strict monoidal categories as objects and strict monoidal functors as morphisms.

\mathsf{SSMC}, with symmetric strict monoidal categories as objects and strict symmetric monoidal functors as their morphisms.

\mathsf{CMC}, with commutative monoidal categories as objects and strict symmetric monoidal functors as morphisms. A commutative monoidal category is a symmetric strict monoidal category where the symmetry is the identity.

The categories of nets are probably less familiar. But they are simple enough. Here I’ll just describe their objects. The morphisms are fairly obvious, but read our paper for details.

\mathsf{PreNet}, with pre-nets as objects. A pre-net consists of a set S of places, a set T of transitions, and a function T \to S^\ast\times S^\ast, where S^\ast is the set of lists of elements of S.

\Sigma\mathsf{-net}, with Σ-nets as objects. A Σ-net consists of a set S, a groupoid T, and a discrete opfibration T \to P S \times P S^{\mathrm{op}}, where P S is the free symmetric strict monoidal category generated by a set of objects S and no generating morphisms.

\mathsf{Petri}, with Petri nets as objects. A Petri net, as we use the term, consists of a set S, a set T, and a function T \to \mathbb{N}[S] \times \mathbb{N}[S], where \mathbb{N}[S] is the set of multisets of elements of S.

What does this mean in practice?

• In a pre-net, each transition has an ordered list of places as ‘inputs’ and an ordered list of places as ‘outputs’. We cannot permute the inputs or outputs of a transition.

• In a Σ-net, each transition has an ordered list of places as inputs and an ordered list of places as outputs. However, permuting the entries of these lists gives a new transition with a new list of inputs and a new list of outputs!

• In a Petri net, each transition has a multiset of places as inputs and a multiset of places as outputs. A multiset is like an ‘unordered list’: entries can appear repeatedly, but the order makes no difference at all.

So, pre-nets are rigidly individualist. Petri nets are rigidly collectivist. And Σ-nets are flexible, including both extremes as special cases!

On the one hand, we can use the left adjoint functor

\mathsf{PreNet} \to \Sigma\mathsf{-net}

to freely generate Σ-nets from pre-nets. If we do this, we get Σ-nets such that permutations of inputs and outputs act freely on transitions. Joachim Kock has recently studied Σ-nets of this sort. He calls them whole-grain Petri nets, and he treats them as forming a category in their own right, but it’s also the full image of the above functor.

On the other hand, we can use the right adjoint functor

\mathsf{Petri} \to \Sigma\mathsf{-net}

to turn Petri nets into Σ-nets. If we do this, we get Σ-nets such that permutations of inputs and outputs act trivially on transitions: the permutations have no effect at all.

I’m not going to explain how we got any of the adjunctions in this diagram:

That’s where the interesting category theory comes in. Nor will I tell you about the various alternative mathematical viewpoints on Σ-nets… nor how we draw them. I also won’t explain our work on open nets and open categories of all the various kinds. I’m hoping Mike Shulman will say some more about what we’ve done. That’s why this blog article is optimistically titled “Part 1”.

But I hope you see the main point. There are three different kinds of things like Petri nets, each of which serves to freely generate a different kind of monoidal category. They’re all interesting, and a lot of confusion can be avoided if we don’t mix them up!


Part 1: three kinds of nets, and the kinds of monoidal categories they generate.

Part 2: what kind of net is best for generating symmetric monoidal categories?