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 a lot of examples of monoidal categories that can’t be made symmetric or even braided, even though the tensor product of objects is commutative! The proof boils down to this:



Here i represents the catalysts, and f and f' are two processes which we can carry out using these catalysts. We can do either one first, but we get different morphisms as a result.

The paper has lots of pictures like this—many 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.


Symposium on Compositional Structures 2

7 December, 2018

I’ve been asleep at the switch; this announcement is probably too late for anyone outside the UK. But still, it’s great to see how applied category theory is taking off! And this conference is part of a series, so if you miss this one you can still go to the next.

Second Symposium on Compositional Structures (SYCO2), 17-18 December 2018, University of Strathclyde, Glasgow.

Accepted presentations

http://events.cs.bham.ac.uk/syco/2/accepted.html

Registration

Please register asap so that catering can be arranged. Late registrants
might go hungry.

https://docs.google.com/forms/d/e/1FAIpQLSeePRCzbmg-wS3C2laQVfnE_hL8et7sxI9fyXFh5EpfIhkEmw/viewform?entry.1910951876=I+am+happy+to+be+listed+as+a+participant+on+the+webpage

Invited speakers

• Corina Cirstea, University of Southampton – Quantitative Coalgebras for
Optimal Synthesis

• Martha Lewis, University of Amsterdam – Compositionality in Semantic Spaces

Description

The Symposium on Compositional Structures (SYCO) is an interdisciplinary series of meetings aiming to support the growing community of researchers interested in the phenomenon of compositionality, from both applied and abstract perspectives, and in particular where category theory serves as a unifying common language. The first SYCO was held at the School of Computer Science, University of Birmingham, 20-21 September, 2018, attracting 70 participants.

We welcome submissions from researchers across computer science, mathematics, physics, philosophy, and beyond, with the aim of fostering friendly discussion, disseminating new ideas, and spreading knowledge between fields. Submission is encouraged for both mature research and work in progress, and by both established academics and junior researchers, including students.

Submission is easy, with no format requirements or page restrictions. The meeting does not have proceedings, so work can be submitted even if it has been submitted or published elsewhere.

While no list of topics could be exhaustive, SYCO welcomes submissions with a compositional focus related to any of the following areas, in particular from the perspective of category theory:

• logical methods in computer science, including classical and quantum programming, type theory, concurrency, natural language processing and machine learning;

• graphical calculi, including string diagrams, Petri nets and reaction networks;

• languages and frameworks, including process algebras, proof nets, type theory and game semantics;

• abstract algebra and pure category theory, including monoidal category
theory, higher category theory, operads, polygraphs, and relationships to homotopy theory;

• quantum algebra, including quantum computation and representation theory;

• tools and techniques, including rewriting, formal proofs and proof assistants, and game theory;

• industrial applications, including case studies and real-world problem
descriptions.

This new series aims to bring together the communities behind many previous successful events which have taken place over the last decade, including “Categories, Logic and Physics”, “Categories, Logic and Physics (Scotland)”, “Higher-Dimensional Rewriting and Applications”, “String Diagrams in Computation, Logic and Physics”, “Applied Category Theory”, “Simons Workshop on Compositionality”, and the “Peripatetic Seminar in Sheaves and Logic”.

SYCO will be a regular fixture in the academic calendar, running regularly throughout the year, and becoming over time a recognized venue for presentation and discussion of results in an informal and friendly atmosphere. To help create this community, and to avoid the need to make difficult choices between strong submissions, in the event that more good-quality submissions are received than can be accommodated in the timetable, the programme committee may choose to defer some submissions to a future meeting, rather than reject them. This would be done based largely on submission order, giving an incentive for early submission, but would also take into account other requirements, such as ensuring a broad scientific programme. Deferred submissions would be accepted for presentation at any future SYCO meeting without the need for peer review. This will allow us to ensure that speakers have enough time to present their ideas, without creating an unnecessarily competitive reviewing process. Meetings would be held sufficiently frequently to avoid a backlog of deferred papers.

PROGRAMME COMMITTEE

Ross Duncan, University of Strathclyde
Fabrizio Romano Genovese, Statebox and University of Oxford
Jules Hedges, University of Oxford
Chris Heunen, University of Edinburgh
Dominic Horsman, University of Grenoble
Aleks Kissinger, Radboud University Nijmegen
Eliana Lorch, University of Oxford
Guy McCusker, University of Bath
Samuel Mimram, École Polytechnique
Koko Muroya, RIMS, Kyoto University & University of Birmingham
Paulo Oliva, Queen Mary
Nina Otter, UCLA
Simona Paoli, University of Leicester
Robin Piedeleu, University of Oxford and UCL
Julian Rathke, University of Southampton
Bernhard Reus, Univeristy of Sussex
David Reutter, University of Oxford
Mehrnoosh Sadrzadeh, Queen Mary
Pawel Sobocinski, University of Southampton (chair)
Jamie Vicary, University of Birmingham and University of Oxford (co-chair)


ACT 2019 – First Announcement

2 October, 2018

 

animation by Marius Buliga

I’m helping organize ACT 2019, an applied category theory conference and school at Oxford, July 15-26, 2019.

If you’re a grad student or postdoc interested in this subject, you should apply for the ‘school’ before January 30th. Later people can submit papers for the conference:

Dear all,

As part of a new growing community in Applied Category Theory, now with a dedicated journal Compositionality, a traveling workshop series SYCO, a forthcoming Cambridge U. Press book series Reasoning with Categories, and several one-off events including at NIST, we launch an annual conference+school series named Applied Category Theory, the coming one being at Oxford, July 15-19 for the conference, and July 22-26 for the school. The dates are chosen such that CT 2019 (Edinburgh) and the ACT 2019 conference (Oxford) will be back-to-back, for those wishing to participate in both.

There already was a successful invitation-only pilot, ACT 2018, last year at the Lorentz Centre in Leiden, also in the format of school+workshop.

For the conference, for those who are familiar with the successful QPL conference series, we will follow a very similar format for the ACT conference. This means that we will accept both new papers which then will be published in a proceedings volume (most likely a Compositionality special Proceedings issue), as well as shorter abstracts of papers published elsewhere. There will be a thorough selection process, as typical in computer science conferences. The idea is that all the best work in applied category theory will be presented at the conference, and that acceptance is something that means something, just like in CS conferences. This is particularly important for young people as it will help them with their careers.

Expect a call for submissions soon, and start preparing your papers now!

The school in ACT 2018 was unique in that small groups of students worked closely with an experienced researcher (these were John Baez, Aleks Kissinger, Martha Lewis and Pawel Sobociński), and each group ended up producing a paper. We will continue with this format or a closely related one, with Jules Hedges and Daniel Cicala as organisers this year. As there were 80 applications last year for 16 slots, we may want to try to find a way to involve more students.

We are fortunate to have a number of private sector companies closely associated in some way or another, who will also participate, with Cambridge Quantum Computing Inc. and StateBox having already made major financial/logistic contributions.

On behalf of the ACT Steering Committee,

John Baez, Bob Coecke, David Spivak, Christina Vasilakopoulou


Complex Adaptive System Design (Part 8)

22 August, 2018

John Foley, Joe Moeller and I have made some nice progress on compositional tasking for the Complex Adaptive System Composition and Design Environment project.

‘Compositional tasking’ means assigning tasks to networks agents in such a way that you can connect or even overlay such tasked networks and get larger ones. This lets you build up complex plans from smaller pieces.

In my last post in this series, I sketched an approach using ‘commitment networks’. A commitment network is a graph where nodes represent agents and edges represent commitments, like “A should move toward B either for 3 hours or until they meet, whichever comes first”. By overlaying such graphs we can build up commitment networks that describe complex plans of action. The rules for overlaying incorporate ‘automatic deconflicting’. In other words: don’t need to worry about agents being given conflicting duties as you stack up plans… because you’ve decided ahead of time what they should do in these situations.

I still like that approach, but we’ve been asked to develop some ideas more closely connected to traditional methods of tasking, like PERT charts, so now we’ve done that.

‘PERT’ stands for ‘program evaluation and review technique’. PERT charts were developed by the US Navy in 1957, but now they’re used all over industry to help plan and schedule large projects.

Here’s simple example:


The nodes in this graph are different states, like “you have built the car but not yet put on the tires”. The edges are different tasks, like “put the tires on the car”. Each state is labelled with an arbitrary name: 10, 20, 30, 40 and 50. The tasks also have names: A, B, C, D, E, and F. More importantly, each task is labelled by the amount of time that task requires!

Your goal is to start at state 10 and move all the way to state 50. Since you’re bossing lots of people around, you can make them do tasks simultaneously. However, you can only reach a state after you have done all the tasks leading up to that state. For example, you can’t reach state 50 unless you have already done all of tasks C, E, and F. Some typical questions are:

• What’s the minimum amount of time it takes to get from state 10 to state 50?

• Which tasks could take longer, without changing the answer to the previous question? How much longer could each task take, without changing the answer? This amount of time is called the slack for that task.

There are known algorithms for solving such problems. These help big organizations plan complex projects. So, connecting compositional tasking to PERT charts seems like a good idea.

At first this seemed confusing because in our previous work the nodes represented agents, while in PERT charts the nodes represent states. Of course graphs can be used for many things, even in the same setup. But the trick was getting everything to fit together nicely.

Now I think we’re close.

John Foley has been working out some nice example problems where a collection of agents need to move along the edges of a graph from specified start locations to specified end locations, taking routes that minimize their total fuel usage. However, there are some constraints. Some edges can only be traversed by specified teams of agents: they can’t go alone. Also, no one agent is allowed to run out of fuel.

This is a nice problem because while it’s pretty simple and specific, it’s representative of a large class of problems where a collection of agents are trying to carry out tasks together. ‘Moving along the edge of a graph’ can stand for a task of any sort. The constraint that some edges can only be traversed by specified teams is then a way of saying that certain tasks can only be accomplished by teams.

Furthermore, there are nice software packages for optimization subject to constraints. For example, John likes one called Choco. So, we plan to use one of these as part of the project.

What makes this all compositional is that John has expressed this problem using our ‘network model’ formalism, which I began sketching in Part 6. This allows us to assemble tasks for larger collections of agents from tasks for smaller collections.

Here, however, an idea due to my student Joe Moeller turned out to be crucial.

In our first examples of network models, explained earlier in this series, we allowed a monoid of networks for any set of agents of different kinds. A monoid has a binary operation called ‘multiplication’, and the idea here was this could describe the operation of ‘overlaying’ networks: for example, laying one set of communication channels, or committments, on top of another.

However, Joe knew full well that a monoid is a category with one object, so he pushed for a generalization that allowed not just a monoid but a category of networks for any set of agents of different kinds. I didn’t know what this was good for, but I figured: what the heck, let’s do it. It was a mathematically natural move, and it didn’t make anything harder—in fact it clarified some of our constructions, which is why Joe wanted to do it.

Now that generalization is proving to be crucial! We can take our category of networks to have states as objects and tasks (ways of moving between states) as morphisms! So, instead of ‘overlaying networks’, the basic operation is now composing tasks.

So, we now have a framework where if you specify a collection of agents of different kinds, we can give you the category whose morphisms are tasks those agents can engage in.

An example is John’s setup where the agents are moving around on a graph.

But this framework also handles PERT charts! While the folks who invented PERT charts didn’t think of them this way, one can think of them as describing categories of a certain specific sort, with states as objects and tasks as morphisms.

So, we now have a compositional framework for PERT charts.

I would like to dive deeper into the details, but this is probably enough for one post. I will say, though, that we use some math I’ve just developed with my grad student Jade Master, explained here:

Open Petri nets (part 3), Azimuth, 19 August 2018.

The key is the relation between Petri nets and PERT charts. I’ll have more to say about that soon, I hope!


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.


Open Petri Nets (Part 3)

19 August, 2018

I’ve been talking about my new paper with Jade Master:

• John Baez and Jade Master, Open Petri nets.

In Part 1 we saw the double category of open Petri nets; in Part 2 we saw the reachability semantics for open Petri nets as a double functor. Now I’d like to wrap up by showing you the engine beneath the hood of our results.

I fell in love with Petri nets when I realized that they were really just presentations of free symmetric monoidal categories. If you like category theory, this turns Petri nets from something mysterious into something attractive.

In any category you can compose morphisms f\colon X \to Y and g\colon Y \to Z and get a morphism gf \colon X \to Z. In a monoidal category you can also tensor morphisms f \colon X \to X' and g \colon Y \to Y' and get a morphism f \otimes g \colon X \otimes X' \to Y \otimes Y'. This of course relies on your ability to tensor objects. In a symmetric monoidal category you also have X \otimes Y \cong Y \otimes X. And of course, there is more to it than this. But this is enough to get started.

A Petri net has ‘places’ and also ‘transitions’ going between multisets of places:

From this data we can try to generate a symmetric monoidal category whose objects are built from the places and whose morphisms are built from the transitions. So, for example, the above Petri net would give a symmetric monoidal category with an object

2 susceptible + infected

and a morphism from this to the object

susceptible + 2 infected

(built using the transition infection), and a morphism
from this to the object

susceptible + infected + resistant

(built using the transition recovery) and so on. Here we are using + to denote the tensor product in our symmetric monoidal category, as usual in chemistry.

When we do this sort of construction, the resulting symmetric monoidal category is ‘free’. That is, we are not imposing any really interesting equations: the objects are freely generated by the places in our Petri net by tensoring, and the morphisms are freely generated by the transitions by tensoring and composition.

That’s the basic idea. The problem is making this idea precise!

Many people have tried in many different ways. I like this approach the best:

• José Meseguer and Ugo Montanari, Petri nets are monoids, Information and Computation 88 (1990), 105–155.

but I think it can be simplified a bit, so let me describe what Jade and I did in our paper.

The problem is that there are different notions of symmetric monoidal category, and also different notions of morphism between Petri nets. We take the maximally strict approach, and work with ‘commutative’ monoidal categories. These are just commutative monoid objects in \mathrm{Cat}, so their associator:

\alpha_{A,B,C} \colon (A + B) + C \stackrel{\sim}{\longrightarrow} A + (B + C)

their left and right unitor:

\lambda_A \colon 0 + A \stackrel{\sim}{\longrightarrow} A

\rho_A \colon A + 0 \stackrel{\sim}{\longrightarrow} A

and even—disturbingly—their braiding:

\sigma_{A,B} \colon A + B \stackrel{\sim}{\longrightarrow} B + A

are all identity morphisms.

The last would ordinarily be seen as ‘going too far’, since while every symmetric monoidal category is equivalent to one with trivial associator and unitors, this ceases to be true if we also require the braiding to be trivial. However, it seems that Petri nets most naturally serve to present symmetric monoidal categories of this very strict sort. There just isn’t enough information in a Petri net to make it worthwhile giving them a nontrivial braiding

\sigma_{A,B} \colon A + B \stackrel{\sim}{\longrightarrow} B+A

It took me a while to accept this, but now it seem obvious. If you want a nontrivial braiding, you should be using something a bit fancier than a Petri net.

Thus, we construct adjoint functors between a category of Petri nets, which we call \textrm{Petri}, and a category of ‘commutative monoidal categories’, which we call \textrm{CMC}.

An object of \textrm{Petri} is a Petri net: that is, a set S of places, a set T of transitions, and source and target functions

s, t \colon T \to \mathbb{N}[S]

where \mathbb{N}[S] is the underlying set of the free commutative monoid on S.

More concretely, \mathbb{N}[S] is the set of formal finite linear combinations of elements of S with natural number coefficients. The set S naturally includes in \mathbb{N}[S], and for any function

f \colon S \to S'

there is a unique monoid homomorphism

\mathbb{N}[f] \colon \mathbb{N}[S] \to \mathbb{N}[S']

extending f.

A Petri net morphism from a Petri net

s, t \colon T \to \mathbb{N}[S]

to a Petri net

s', t' \colon T' \to \mathbb{N}[S']

is a pair of functions

f \colon T \to T'

g \colon S \to S'

making the two obvious diagrams commute:

There is a category \textrm{Petri} with Petri nets as objects and Petri net morphisms as morphisms.

On the other hand, a commutative monoidal category is a commutative monoid object in \mathrm{Cat}. Explicitly, it’s a strict monoidal category (C,+,0) such that for all objects A and B we have

A + B = B + A

and for all morphisms f and g

f + g = g + f

Note that a commutative monoidal category is the same as a strict symmetric monoidal category where the symmetry isomorphisms

\sigma_{A,B} \colon A + B \stackrel{\sim}{\longrightarrow} B+A

are all identity morphisms. Every strict monoidal functor between commutative monoidal categories is automatically a strict symmetric monoidal functor. So, we let \mathrm{CMC} be the category whose objects are commutative monoidal categories and whose morphisms are strict monoidal functors.

There’s a functor

U \colon \mathrm{CMC} \to \mathrm{Petri}

sending any commutative monoidal category C to its underlying Petri net. This Petri net has the set of objects \mathrm{Ob}(C) as its set of places and the set of morphisms \mathrm{Mor}(C) as its set of transitions, and

s, t \colon \mathrm{Mor}(C) \to \mathrm{Ob}(C) \hookrightarrow \mathbb{N}[\mathrm{Ob}(C)]

as its source and target maps.

Proposition. The functor U \colon \mathrm{CMC} \to \mathrm{Petri} has a left adjoint

F \colon \mathrm{Petri} \to \mathrm{CMC}

This is Proposition 10 in our paper, and we give an explicit construction of this left adjoint.

So that’s our conception of the free commutative monoidal category on a Petri net. It’s pretty simple. How could anyone have done anything else?

Montanari and Meseguer do almost the same thing, but our category of Petri nets is a subcategory of theirs: our morphisms of Petri nets send places to places, while they allow more general maps that send a place to a formal linear combination of places. On the other hand, they consider a full subcategory of our \mathrm{CMC} containing only commutative monoidal categories whose objects form a free commutative monoid.

Other papers do a variety of more complicated things. I don’t have the energy to explain them all, but you can see some here:

• Pierpaolo Degano, José Meseguer and Ugo Montanari, Axiomatizing net computations and processes, in Logic in Computer Science 1989, IEEE, New Jersey, 1989, pp. 175–185.

• Vladimiro Sassone, Strong concatenable processes: an approach to the category of Petri net computations, BRICS Report Series, Dept. of Computer Science, U. Aarhus, 1994.

• Vladimiro Sassone, On the category of Petri net computations, in Colloquium on Trees in Algebra and Programming, Springer, Berlin, 1995.

• Vladimiro Sassone, An axiomatization of the algebra of Petri net concatenable processes, in Theoretical Computer Science 170 (1996), 277–296.

• Vladimiro Sassone and Pavel Sobociński, A congruence for Petri nets, Electronic Notes in Theoretical Computer Science 127 (2005), 107–120.

Getting the free commutative monoidal category on a Petri net right is key to developing the reachability semantics for open Petri nets in a nice way. But to see that, you’ll have to read our paper!


Part 1: the double category of open Petri nets.

Part 2: the reachability semantics for open Petri nets.

Part 3: the free symmetric monoidal category on a Petri net.


Open Petri Nets (Part 2)

18 August, 2018

I’d like to continue talking about this paper:

• John Baez and Jade Master, Open Petri nets.

Last time I explained, in a sketchy way, the double category of open Petri nets. This time I’d like to describe a ‘semantics’ for open Petri nets.

In his famous thesis Functorial Semantics of Algebraic Theories, Lawvere introduced the idea that semantics, as a map from expressions to their meanings, should be a functor between categories. This has been generalized in many directions, and the same idea works for double categories. So, we describe our semantics for open Petri nets as a map

\blacksquare \colon \mathbb{O}\mathbf{pen}(\mathrm{Petri}) \to \mathbb{R}\mathbf{el}

from our double category of open Petri nets to a double category of relations. This map sends any open Petri net to its ‘reachability relation’.

In Petri net theory, a marking of a set X is a finite multisubset of X. We can think of this as a way of placing finitely ‘tokens’—little black dots—on the elements of X. A Petri net lets us start with some marking of its places and then repeatedly change the marking by moving tokens around, using the transitions. This is how Petri nets describe processes!

For example, here’s a Petri net from chemistry:

Here’s a marking of its places:

But using the transitions, we can repeatedly change the marking. We started with one atom of carbon, one molecule of oxygen, one molecule of sodium hydroxide and one molecule of hydrochloric acid. But they can turn into one molecule of carbon dioxide, one molecule of sodium hydroxide and one molecule of hydrochloric acid:

These can then turn into one molecule of sodium bicarbonate and one molecule of hydrochloric acid:

Then these can turn into one molecule of carbon dioxide, one molecule of water and one molecule of sodium chloride:

People say one marking is reachable from another if you can get it using a finite sequence of transitions in this manner. (Our paper explains this well-known notion more formally.) In this example every marking has 0 or 1 tokens in each place. But that’s not typical: in general we could have any natural number of tokens in each place, so long as the total number of tokens is finite.

Our paper adapts the concept of reachability to open Petri nets. Let \mathbb{N}[X] denote the set of markings of the set X. Given an open Petri net P \colon X \nrightarrow Y there is a reachability relation

\blacksquare P \subseteq \mathbb{N}[X] \times \mathbb{N}[Y]

This relation holds when we can take a given marking of X, feed those tokens into the Petri net P, move them around using transitions in P, and have them pop out and give a certain marking of Y, leaving no tokens behind.

For example, consider this open Petri net P \colon X \nrightarrow Y:

Here is a marking of X:

We can feed these tokens into P and move them around using transitions in P:

They can then pop out into Y, leaving none behind:

This gives a marking of Y that is ‘reachable’ from the original marking of X.

The main result of our paper is that the map sending an open Petri net P to its reachability relation \blacksquare P extends to a ‘lax double functor’

\blacksquare \colon \mathbb{O}\mathbf{pen}(\mathrm{Petri}) \to \mathbb{R}\mathbf{el}

where \mathbb{O}\mathbf{pen}(\mathrm{Petri}) is a double category having open Petri nets as horizontal 1-cells and \mathbb{R}\mathbf{el} is a double category having relations as horizontal 1-cells.

I can give you a bit more detail on those double categories, and also give you a clue about what ‘lax’ means, without it becoming too stressful.

Last time I said the double category \mathbb{O}\mathbf{pen}(\mathrm{Petri}) has:

• sets X, Y, Z, \dots as objects,

• functions f \colon X \to Y as vertical 1-morphisms,

• open Petri nets P \colon X \nrightarrow Y as horizontal 1-cells—they look like this:



• morphisms between open Petri nets as 2-morphisms—an example would be the visually obvious map from this open Petri net:

to this one:

What about \mathbb{R}\mathbf{el}? This double category has

• sets X, Y, Z, \dots as objects,

• functions f \colon X \to Y as vertical 1-morphisms,

• relations R \subseteq X \times Y as horizontal 1-cells from X to Y, and

• maps between relations as 2-morphisms. Here a map between relations is a square

that obeys

(f \times g) R \subseteq S

So, the idea of the reachability semantics is that it maps:

• any set X to the set \mathbb{N}[X] consisting of all markings of that set.

• any function f \colon X \to Y to the obvious function

\mathbb{N}(f) \colon \mathbb{N}[X] \to \mathbb{N}[Y]

(Yes, \mathbb{N} is a really a functor.)

• any open Petri net P \colon X \nrightarrow Y to its reachability relation

\blacksquare P \colon \mathbb{N}[X] \to \mathbb{N}[Y]

• any morphism between Petri nets to the obvious map between their reachability relations.

Especially if you draw some examples, all this seems quite reasonable and nice. But it’s important to note that \blacksquare is a lax double functor. This means that it does not send a composite open Petri net PQ to the composite of the reachability relations for P and Q. So, we do not have

\blacksquare Q \; \blacksquare P = \blacksquare (QP)

Instead, we just have

\blacksquare Q \; \blacksquare P \subseteq \blacksquare (QP)

It’s easy to see why. Take P \colon X \nrightarrow Y to be this open Petri net:

and take Q \colon Y \nrightarrow Z to be this one:

Then their composite QP \colon X \nrightarrow Y is this:

It’s easy to see that \blacksquare (QP) is a proper subset of \blacksquare Q \; \blacksquare P. In QP a token can move all the way from point 1 to point 5. But it does not do so by first moving through P and then moving through Q! It has to take a more complicated zig-zag path where it first leaves P and enters Q, then comes back into P, and then goes to Q.

In our paper, Jade and I conjecture that we get

\blacksquare Q \; \blacksquare P = \blacksquare (QP)

if we restrict the reachability semantics to a certain specific sub-double category of \mathbb{O}\mathbf{pen}(\mathrm{Petri}) consisting of ‘one-way’ open Petri nets.

Finally, besides showing that

\blacksquare \colon \mathbb{O}\mathbf{pen}(\mathrm{Petri}) \to \mathbb{R}\mathbf{el}

is a lax double functor, we also show that it’s symmetric monoidal. This means that the reachability semantics works as you’d expect when you run two open Petri nets ‘in parallel’.

In a way, the most important thing about our paper is that it illustrates some methods to study semantics for symmetric monoidal double categories. Kenny Courser and I will describe these methods more generally in our paper “Structured cospans.” They can be applied to timed Petri nets, colored Petri nets, and various other kinds of Petri nets. One can also develop a reachability semantics for open Petri nets that are glued together along transitions as well as places.

I hear that the company Statebox wants these and other generalizations. We aim to please—so we’d like to give it a try.

Next time I’ll wrap up this little series of posts by explaining how Petri nets give symmetric monoidal categories.


Part 1: the double category of open Petri nets.

Part 2: the reachability semantics for open Petri nets.

Part 3: the free symmetric monoidal category on a Petri net.