Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: theory: applied category theory

Topic: Whole-grain Petri nets


view this post on Zulip Joachim Kock (May 12 2020 at 01:37):

My Petri-net paper is out!

http://arxiv.org/abs/2005.05108

I hope it will be of interest to some people in this chat, and I am very eager to get feedback, especially regarding the proper place of all this in the theory of Petri nets. I have been interested in Petri nets for many years, but it's a huge field and most of it I cannot grasp, so I feel a bit awkward writing about it as if I were an expert.

Here is the title and abstract:

Elements of Petri nets and processes

We present a formalism for Petri nets based on polynomial-style finite-set configurations and etale maps. The formalism supports both a geometric semantics in the style of Goltz and Reisig (processes are etale maps from graphs) and an algebraic semantics in terms of free coloured props: the Segal space of P-processes is shown to be the free coloured prop-in-groupoids on P. There is also an unfolding semantics \`a la Winskel, which bypasses the classical symmetry problems. Since everything is encoded with explicit sets, Petri nets and their processes have elements. In particular, individual-token semantics is native, and the benefits of pre-nets in this respect can be obtained without the need of numberings. (Collective-token semantics emerges from rather drastic quotient constructions \`a la Best--Devillers, involving taking $\pi_0$ of the groupoids of states.)

view this post on Zulip Joe Moeller (May 12 2020 at 01:44):

Wow, this looks great. Looking forward to reading it!

view this post on Zulip Joachim Kock (May 12 2020 at 01:44):

Here is the main point of the paper, which is just a definition: I define Petri nets to be diagrams of finite sets SITOSS \leftarrow I \to T \leftarrow O \to S where TT is the set of transitions, SS is the set of places, and II and OO are the sets of incoming and outgoing arcs of transitions. In particular, for a transition tTt\in T, the fibres ItI_t and OtO_t are explicit sets, and they are not necessarily subsets of SS. It is only a slight modification of the usual definition. I like to call them whole-grain Petri nets. In fact the key point is to replace the usual notion of multiset (in terms of multiplicity functions) with the representable analogue where a multiset on SS is an element in the finite slice B/S\mathbb{B}_{/S}. In this sense, the definition can be seen as modifying the classical definition by replacing the free-commutative-monoid monad with the free-symmetric-monoidal-category monad --- but the definition is still just a configuration of finite sets! It can also be seen as a version of pre-nets, but without numberings. Once I have told you this, and since you are category theorists, I am afraid there are no more surprises, and maybe you will think it is all trivial.

(You might also say that changing the definition is cheating. But if you follow the development of the theory, there is always an escape route you can take if you don't like it: at any point you can take π0\pi_0 and get back to classical theory. My own opinion is that you should delay this as much as possible, because groupoids are so much cooler than sets.)

view this post on Zulip Joe Moeller (May 12 2020 at 01:55):

I like this idea. It definitely seems more natural than the way we've been doing it, ie with i,o ⁣:TN[S]i,o \colon T \to \mathbb N[S], which I always found awkward.

view this post on Zulip Joachim Kock (May 12 2020 at 01:55):

From this definition the theory develops quite naturally. There is a natural notion of etale map: they are maps between diagrams where the middle squares are pullbacks. There is a lot of recycling of a formalism for directed graphs I developed some years ago in connection with properads [Graphs, hypergraphs, and properads (2016)]. 'Graph' now means directed acyclic graph admitting open-ended edges.

A process of a Petri net P is just an etale map from a graph. There is a natural symmetric monoidal Segal space of processes, and it is shown to be the free prop-in-groupoids on P. Maybe that's the main theorem. (One can also extract a 1-categorical version of this.)

A digraphical species is a presheaf on the category of elementary graphs. The elementary graphs are the connected graphs without inner edges, so the only possibilities are: the unit graph (one edge, no nodes), and the (m,n)-corollas. A digraphical species is also called a coloured bi-collection. They are the kind of structure underlying props and properads -- and the kind of stuff you generate free props and properads from. The next key point is that there is a restricted-Yoneda embedding from whole-grain Petri nets to digraphical species. The image is shown to consist of the flat digraphical species -- that just means those whose symmetric-group actions are free. The free prop-in-groupoids has an explicit description in terms of graphs, easily seen to agree with the Segal space of processes.

All this is precisely analogous to the way polynomial endofunctors embed into ordinary coloured species (coloured collections). That was my motivation for doing all this.

One can also say that whole-grain Petri nets sit in between ordinary Petri nets and pre-nets in the same way as polynomial monads sit in between symmetric operads and non-symmetric operads.

view this post on Zulip Joe Moeller (May 12 2020 at 02:02):

In this sense, the definition can be seen as modifying the classical definition by replacing the free-commutative-monoid monad with the free-symmetric-monoidal-category monad --- but the definition is still just a configuration of finite sets!

I (and I guess a few other people) had the idea to do something nearly exactly like this not too long ago. I think this presentation is much cleaner than what I would have come up with though

view this post on Zulip John Baez (May 12 2020 at 02:04):

Joe Moeller said:

I like this idea. It definitely seems more natural than the way we've been doing it, ie with i,o ⁣:TN[S]i,o \colon T \to \mathbb N[S], which I always found awkward.

I wouldn't say that one is more natural or more awkward; they're just different. The ones are presentations of commutative monoidal categories. I suspect the ones Joachim is talking about are presentation of symmetric monoidal categories.

Mike Shulman, Jade Master, Fabio Genovese and I are writing a paper about this latter kind. Mike's preferred description is different than what Joachim just described, but I bet they're just different ways to formalize the same concept. This is just a guess; I'll check it.

view this post on Zulip Joe Moeller (May 12 2020 at 02:05):

Yes definitely, but I think commutative monoidal categories are inherently awkward, so this is an extension of that opinion.

view this post on Zulip John Baez (May 12 2020 at 02:06):

I don't like words like "awkward" very much: they're too vague. Commutative monoidal categories show up when one is taking the "collective token philosophy", i.e. when doesn't care at all about switching two tokens in the same place. Symmetric monoidal categories show up when one is taking the individual token philosophy. They're both important.

view this post on Zulip John Baez (May 12 2020 at 02:07):

For example, in applications to chemical reaction theory it's good to take the collective token philosophy.

view this post on Zulip John Baez (May 12 2020 at 02:07):

Anyway, in the paper with all those coauthors, we're going to show how these two philosophies fit together.

view this post on Zulip John Baez (May 12 2020 at 02:08):

So, now we have to read Joachim's paper and see how to adjust our paper to take it into account. If he's done everything we were going to do, that means less work for me! But I'm afraid that's probably not true.

view this post on Zulip Joachim Kock (May 12 2020 at 02:08):

Joe Moeller said:

In this sense, the definition can be seen as modifying the classical definition by replacing the free-commutative-monoid monad with the free-symmetric-monoidal-category monad --- but the definition is still just a configuration of finite sets!

I (and I guess a few other people) had the idea to do something nearly exactly like this not too long ago. I think this presentation is much cleaner than what I would have come up with though

I think that Sassone thought of the symmetric-monoidal-category monad ten years ago, but he didn't follow up on it, as far as I know. Personally I am fond of the fact that one can avoid the monad, and just talk about configurations of finite sets.

When you say N[S]\mathbb{N}[S] I suppose it is the commutative-monoid monad, like in Meseguer-Montanari?

view this post on Zulip Joe Moeller (May 12 2020 at 02:09):

Does this definition actually make Petri nets into a presheaf category on the (two spans sharing feet) category?

view this post on Zulip John Baez (May 12 2020 at 02:10):

Joachim Kock said:

I think that Sassone thought of the symmetric-monoidal-category monad ten years ago, but he didn't follow up on it, as far as I know.

I don't think he really quite managed to work this out.

When you say N[S]\mathbb{N}[S] I suppose it is the commutative-monoid monad, like in Meseguer-Montanari?

Yes, that's the notation for the commutative monoid monad that I use in all my papers on Petri nets.

view this post on Zulip John Baez (May 12 2020 at 02:11):

More generally for any commutative monoid MM I use M[S]M[S] for the set of finite linear combinations of elements of a set SS with coefficients in MM. The most famous case is a group ring like C[G]\mathbb{C}[G] when our set GG is a group.

view this post on Zulip John Baez (May 12 2020 at 02:13):

So we have M[S]MSM[S] \cong M^S when SS is finite but not otherwise.

view this post on Zulip Joachim Kock (May 12 2020 at 02:15):

John Baez said:

Mike Shulman, Jade Master, Fabio Genovese and I are writing a paper about this latter kind. Mike's preferred description is different than what Joachim just described, but I bet they're just different ways to formalize the same concept. This is just a guess; I'll check it.

I look forward to hear about that!

I am very much aware that maybe I mostly like the whole-grain formalism because it fits into my way of thinking in terms of polynomial functors. Not everybody thinks like that! I hope to get in contact with real users of Petri nets, and hear what they think.

view this post on Zulip John Baez (May 12 2020 at 02:16):

Here is the main point of the paper, which is just a definition: I define Petri nets to be diagrams of finite sets SITOSS \leftarrow I \to T \leftarrow O \to S where TT is the set of transitions, SS is the set of places, and II and OO are the sets of incoming and outgoing arcs of transitions.

Interestingly this is the approach I took back when I wanted to have Petri nets be the objects of a topos - Joe may remember that. But then I decided I didn't like the morphisms in that topos.

view this post on Zulip Joe Moeller (May 12 2020 at 02:17):

I don't remember that.

view this post on Zulip Joe Moeller (May 12 2020 at 02:18):

I do remember there being a category of Petri nets with undesirable morphisms.

view this post on Zulip John Baez (May 12 2020 at 02:20):

I was really excited about this particular approach because you can think of these diagrams as objects in a presheaf topos.

view this post on Zulip John Baez (May 12 2020 at 02:20):

But then there are morphisms that squash down two elements of II or OO ("arcs") to one.

view this post on Zulip John Baez (May 12 2020 at 02:21):

So I'm curious what Joachim's morphisms between Petri nets are!

view this post on Zulip Joachim Kock (May 12 2020 at 02:22):

Joe Moeller said:

Does this definition actually make Petri nets into a presheaf category on the (two spans sharing feet) category?

Depends on the maps you allow. I am not an expert, but it is not so clear to me what general maps of SITOS diagrams (so as to have a presheaf category) would mean. I think the nice maps are the etale maps, and then it is no longer a presheaf category. At the end of my paper I also consider some more general maps called rational maps, consisting of certain spans: a little backwards correction map before the main part which is a forward etale map.

view this post on Zulip Joachim Kock (May 12 2020 at 02:28):

John Baez said:

I don't like words like "awkward" very much: they're too vague. Commutative monoidal categories show up when one is taking the "collective token philosophy", i.e. when doesn't care at all about switching two tokens in the same place. Symmetric monoidal categories show up when one is taking the individual token philosophy. They're both important.

I am struggling to understand the significance of these two 'philosophies'. Lacking a philosophical education in Petri nets, I just followed my instinct: even if I were not interested in sets (arcs or tokens) other than their number and kind, my instinct would still be to deal with them as actual sets. And then take π0\pi_0 of some groupoids at some point.

view this post on Zulip Joachim Kock (May 12 2020 at 02:32):

John Baez said:

So, now we have to read Joachim's paper and see how to adjust our paper to take it into account. If he's done everything we were going to do, that means less work for me! But I'm afraid that's probably not true.

I am sure it is not true, because I do very little. Judging from the composition of your team, I am probably only scratching the surface of what you are doing.

view this post on Zulip Joachim Kock (May 12 2020 at 02:57):

John Baez said:

So I'm curious what Joachim's morphisms between Petri nets are!

They are morphisms of SITOS diagrams where the middle squares are pullbacks. They are called etale maps.
Both the diagrams and the etale maps are from my properads paper https://arxiv.org/abs/1407.3744
The digraphical species are also from that paper.

view this post on Zulip John Baez (May 12 2020 at 03:15):

Different applications of Petri nets make use of the two different philosophies. For example, chemistry uses the collective token philosophy (Petri nets as presentations of free commutative monoidal categories), because for them switching two oxygen atoms counts as doing nothing at all, while the people at Statebox applying Petri nets to industrial process use the individual token philosophy (Petri nets as presentations of free strict symmetric monoidal categories), because for them switching two people counts as doing something.

view this post on Zulip John Baez (May 12 2020 at 03:19):

I'll have to think about what etale maps actually are in concrete low-brow terms, before I can mentally process what you did. But it sounds interesting!

view this post on Zulip Daniel Geisler (May 12 2020 at 09:00):

@John Baez, is the following true?

view this post on Zulip James Fairbanks (May 12 2020 at 13:04):

John Baez said:

Different applications of Petri nets make use of the two different philosophies. For example, chemistry uses the collective token philosophy (Petri nets as presentations of free commutative monoidal categories), because for them switching two oxygen atoms counts as doing nothing at all, while the people at Statebox applying Petri nets to industrial process use the individual token philosophy (Petri nets as presentations of free strict symmetric monoidal categories), because for them switching two people counts as doing something.

yeah I think of this collective token philosophy as a big part of what makes petri nets interesting as a model of mass action. The idea that the molecules of a given species are interchangeable and the concentrations are uniform over space are pretty important. Outside of chemistry this assumption is used in the SIR epidemics modeling. If you don't take the collective token approach then you can't approximate the dynamics with simple ODEs.

If you are asking about the reachability relation then the individual token philosophy makes sense as an extension of vanilla petri nets, but in the chemical setting, distinguishing between tokens really doesn't make any sense from the perspective of the underlying chemistry. If you want to distinguish between molecules of the same species, you need a spatial model that talks about concentration as a function of position. Or your definition of "species" is too coarse.

view this post on Zulip Fabrizio Genovese (May 12 2020 at 13:13):

Daniel Geisler said:

John Baez, is the following true?

What is a (un)labelled combintorial structure?

view this post on Zulip Mike Shulman (May 12 2020 at 13:13):

Joachim Kock said:

Joe Moeller said:
Depends on the maps you allow. I am not an expert, but it is not so clear to me what general maps of SITOS diagrams (so as to have a presheaf category) would mean. I think the nice maps are the etale maps, and then it is no longer a presheaf category.

Do you know for sure that WGPNs with etale maps are not a presheaf category (on any domain category), or just that they are not a presheaf category in this particular way? (I ask because the BGMS notion of net is a presheaf category, albeit in a slightly non-obvious way; so if yours are not then it would give an easy proof that the two are different.)

view this post on Zulip Fabrizio Genovese (May 12 2020 at 13:13):

James Fairbanks said:

John Baez said:

Different applications of Petri nets make use of the two different philosophies. For example, chemistry uses the collective token philosophy (Petri nets as presentations of free commutative monoidal categories), because for them switching two oxygen atoms counts as doing nothing at all, while the people at Statebox applying Petri nets to industrial process use the individual token philosophy (Petri nets as presentations of free strict symmetric monoidal categories), because for them switching two people counts as doing something.

yeah I think of this collective token philosophy as a big part of what makes petri nets interesting as a model of mass action. The idea that the molecules of a given species are interchangeable and the concentrations are uniform over space are pretty important. Outside of chemistry this assumption is used in the SIR epidemics modeling. If you don't take the collective token approach then you can't approximate the dynamics with simple ODEs.

If you are asking about the reachability relation then the individual token philosophy makes sense as an extension of vanilla petri nets, but in the chemical setting, distinguishing between tokens really doesn't make any sense from the perspective of the underlying chemistry. If you want to distinguish between molecules of the same species, you need a spatial model that talks about concentration as a function of position. Or your definition of "species" is too coarse.

Another way to understand this is that, if you were to assign types to places, your places would all have type unit in the collective token philosophy.

view this post on Zulip Fabrizio Genovese (May 12 2020 at 13:15):

This also highlights very well why the collective token philosphy does not work well in many compsci applications. There your places do not have type unit, and being tokens terms of that type you need to distinguish between tokens in an execution.

view this post on Zulip Joachim Kock (May 12 2020 at 13:39):

John Baez said:

I'll have to think about what etale maps actually are in concrete low-brow terms, before I can mentally process what you did. But it sounds interesting!

I should have said that: they are just the maps that preserve in/out arities on transitions.
Or maybe I should not have said it --- I also hope you will read the paper :-)

view this post on Zulip Daniel Geisler (May 12 2020 at 13:52):

Daniel Geisler said:
Free commutative monoidal categories - unlabeled combinatorial structures
Free strict symmetric monoidal categories - labeled combinatorial structures

@Fabrizio Genovese said:

What is a (un)labelled combinatorial structure?

I picked the terms up from Philippe Flajolet's work and suspect it is in Combinatorial Analytics. A common example is the unlabeled integer partitions and labeled set partitions/Bell numbers. The different labeled set partitions map into the integer partitions.
{1,2,3},{2,3,1},{3,1,2},{3,2,1},{1,3,2},{2,1,3}1+1+1\{1,2,3\}, \{2,3,1\},\{ 3,1,2\},\{3,2,1\},\{1,3,2\},\{2,1,3\} \to 1+1+1

view this post on Zulip Joachim Kock (May 12 2020 at 13:57):

Mike Shulman said:

Joachim Kock said:

Joe Moeller said:
Depends on the maps you allow. I am not an expert, but it is not so clear to me what general maps of SITOS diagrams (so as to have a presheaf category) would mean. I think the nice maps are the etale maps, and then it is no longer a presheaf category.

Do you know for sure that WGPNs with etale maps are not a presheaf category (on any domain category), or just that they are not a presheaf category in this particular way? (I ask because the BGMS notion of net is a presheaf category, albeit in a slightly non-obvious way; so if yours are not then it would give an easy proof that the two are different.)

It is not a topos because there is no terminal object. A terminal object would amount to a finite-map classifier in Set.

(It would be an \infty-topos if we copied over the definition to \infty-groupoids and demanded the two middle maps to belong to a bounded local class, just like polynomial functors over \infty-groupoids form an \infty-topos is just the middle maps are demanded to belong to a bounded local class (see [Gepner-Haugseng-Kock]).)

On the other hand, WGPetri is locally a topos, in the sense that every slice of WGPetri is a topos. (This follows since the etale maps are really an example of the Joyal-Moerdijk axiomatic notion of class of etale maps.) In particular, pre-nets (In the sense of Bruni-Meseguer-Montanari-Sassone) form a topos (at least if we allow infinite nets), because pre-nets are WG Petri nets with an etale map to the Petri net obtained by gluing together all the elementary graphs at a single place (i.e. one transition for each (m,n)). (Just like nonsymmetric sequences are polynomial endofunctors cartesian over the free-monoid monad.)

view this post on Zulip Fabrizio Genovese (May 12 2020 at 13:57):

Yes, I think you can see it this way

view this post on Zulip Fabrizio Genovese (May 12 2020 at 13:57):

In symmetric monoidal categories different permutations of an object are distinct, while in commutative monoidal categories they are not.

view this post on Zulip (=_=) (May 12 2020 at 15:00):

Joachim Kock said:

My Petri-net paper is out!

It's interesting that you have Morse functions in your formalism. I'm wondering if this musing by @Jules Hedges could be formulated under this. :thinking:

I sometime use the phrase "future alien [wizard] mathematics". Usually I mean it for hypothetical stuff involving *taking the topology of syntax seriously*. For example if you're using surface diagrams to denote computer programs, then it's using Morse theory to study programming

- julesh (@_julesh_)

view this post on Zulip sarahzrf (May 12 2020 at 15:01):

morse theory seems really cool

view this post on Zulip sarahzrf (May 12 2020 at 15:01):

but i dont think i know enough diff geo to learn it :upside_down:

view this post on Zulip (=_=) (May 12 2020 at 15:02):

You don't really need diff geo in this case.

view this post on Zulip Amar Hadzihasanovic (May 12 2020 at 15:02):

You should start from discrete Morse theory, that's combinatorics ;)

view this post on Zulip sarahzrf (May 12 2020 at 15:02):

what does discrete morse theory do

view this post on Zulip Amar Hadzihasanovic (May 12 2020 at 15:05):

It starts from a combinatorial CW complex (for example, the face poset of a regular CW complex, or a simplicial complex) and gives you criteria for deleting cells without changing the homotopy type.

view this post on Zulip sarahzrf (May 12 2020 at 15:05):

interesting

view this post on Zulip (=_=) (May 12 2020 at 15:10):

The thought bubble I had was that Petri nets are already used to model programs, so Jules' vision could emerge if you could do Morse theory there.

view this post on Zulip Joachim Kock (May 12 2020 at 15:11):

James Fairbanks said:

I think of this collective token philosophy as a big part of what makes petri nets interesting as a model of mass action. The idea that the molecules of a given species are interchangeable and the concentrations are uniform over space are pretty important. Outside of chemistry this assumption is used in the SIR epidemics modeling. If you don't take the collective token approach then you can't approximate the dynamics with simple ODEs.

Hi James, all this is very interesting. I have some questions, if you don't mind. In these models for chemical reactions or epidemics,

1) is it correct that you are talking about Petri nets with rates?

2) is it correct that you are interested in markings where there are millions of tokens?

3) do you ever talk about events or concurrency?

4) do you ever play the token game and look at firing sequences or unfolding?

5) what is your actual use of monoidal categories semantics?

That would be a great starting point for me to try to understand what tiny little corner of Petri net theory I am actually working in. Maybe I need to rewrite the introduction of my paper to better delimit its potential interest.

I hope to see you again in the break-out rooms soon!

view this post on Zulip Joachim Kock (May 12 2020 at 15:28):

Daniel Geisler said:

That sounds like a very good analogy to me. (But I might have to revise my opinion over the coming days...)

As a further analogy in this directions, the relation between ordinary generating functions and exponential generating functions.

And as an addition to the reference to [Flajolet-Sedgewick], let me add the theory of combinatorial species. That's built on the idea of labelled combinatorial structures -- the objects are really sets equipped with a structure, not just iso-classes of such things. But it is also a great tool to deal with unlabelled structures, through fix-point calculus and cycle index series.

Where combinatorial species are 'structures that sets can have', I see Petri nets as '(local) structures that graphs can have'. (These graphs are the processes.) Graphs decorated with Petri nets exist both in the collective- and the individual-token viewpoints, but in the collective-token viewpoint these graphs do not work as arrows in categories.

view this post on Zulip Mike Shulman (May 12 2020 at 15:30):

Joachim Kock said:

It is not a topos because there is no terminal object. A terminal object would amount to a finite-map classifier in Set.

Excellent, thanks! So our categories are definitely different.

view this post on Zulip Joachim Kock (May 12 2020 at 15:39):

Amar Hadzihasanovic said:

It starts from a combinatorial CW complex (for example, the face poset of a regular CW complex, or a simplicial complex) and gives you criteria for deleting cells without changing the homotopy type.

That's fine, but in this thread I should probably point out that the Morse functions in my paper are not the discrete Morse functions from the theory of simplicial complexes! I have an explicit warning in my paper. Maybe it is silly of me to call them Morse functions, it's just that I rely on intuition from cobordism categories.

view this post on Zulip John Baez (May 12 2020 at 15:42):

Fabrizio Genovese said:

This also highlights very well why the collective token philosophy does not work well in many compsci applications. There your places do not have type unit, and being tokens terms of that type you need to distinguish between tokens in an execution.

What's a "type unit"? I don't understand the last sentence here, in part because of that and in part because the chunk after "and" isn't grammatical (as far as I can tell). But I think I understand the basic idea in a vague way, and I'd like to understand it the way you do.

view this post on Zulip Nathanael Arkor (May 12 2020 at 15:44):

It should be read as "the type of each place is the unit (i.e. terminal/singleton) type".

view this post on Zulip John Baez (May 12 2020 at 15:44):

@Joachim Kock - here's a lazy request: could you describe your etale maps between your whole-grain Petri nets in a very lowbrow undergraduate-style way?

view this post on Zulip John Baez (May 12 2020 at 15:45):

Say I have two of them:

SITOSS \leftarrow I \to T \leftarrow O \to S

and

SITOSS' \leftarrow I' \to T' \leftarrow O' \to S'

view this post on Zulip John Baez (May 12 2020 at 15:46):

Is an etale map from the first to the second a function from SS to SS', a function from TT to TT', a function from OO to OO' and a function from II to II' obeying some property?

view this post on Zulip Joachim Kock (May 12 2020 at 15:47):

John Baez said:

Joachim Kock - here's a lazy request: could you describe your etale maps between Petri nets in a very lowbrow undergraduate-style way?

It's a map of diagrams from one SITOS diagram to another. So it maps transitions to transitions and places to places. It also maps arcs to arcs, and all incidences must be preserved. So far these are just the maps in the presheaf category Joe described. The etale condition says that a transition with m incoming arcs and n outgoing arc must map to another transition with this same interface.

view this post on Zulip John Baez (May 12 2020 at 15:50):

Yay! That's what I was hoping! This extra "etale" condition is what I hadn't considered when I discarded a similar idea.

view this post on Zulip sarahzrf (May 12 2020 at 15:50):

i guess regardless of whether this category forms a topos, we know it forms a sitos :thinking:

view this post on Zulip John Baez (May 12 2020 at 15:51):

Without that extra condition on the morphisms you get a very cute little presheaf topos of Petri nets, but it's not useful in applications.

view this post on Zulip John Baez (May 12 2020 at 15:51):

So, I said goodbye to it and moved on.

view this post on Zulip John Baez (May 12 2020 at 15:52):

Your category sounds a lot more reasonable.

view this post on Zulip Joachim Kock (May 12 2020 at 15:54):

Petri nets are a bit complicated to consider. Let's first consider graphs. Actually let's just consider trees. Then etale maps send nodes with n inputs to nodes with n inputs. From the viewpoint of operads you would not think of other maps. For trees, the pullback condition actually forces etale maps to be injections (because trees are connected and simply connected) -- see my tree paper https://arxiv.org/abs/0807.2874, which was the first restaurant in the chain. For graphs it is essential to allow etale maps that are not injective, because if you cut an edge which is not a bridge, then the corresponding cover duplicates that edge. For Petri nets it is even more essential to consider etale maps, because you would like to run around in the net for a long time. In all three cases, the correct notion is just the pullback condition! And after that, all arguments are with pullbacks :-)

view this post on Zulip Amar Hadzihasanovic (May 12 2020 at 16:02):

Joachim Kock said:

That's fine, but in this thread I should probably point out that the Morse functions in my paper are not the discrete Morse functions from the theory of simplicial complexes! I have an explicit warning in my paper. Maybe it is silly of me to call them Morse functions, it's just that I rely on intuition from cobordism categories.

Yes, sorry, I didn't want to be confusing :D I looked at the corresponding section of your paper only after replying. It seems fine to call it a Morse function, in any case.

view this post on Zulip Jade Master (May 12 2020 at 16:20):

Ah wow. I am very impressed by this paper :)

view this post on Zulip Joachim Kock (May 12 2020 at 16:28):

John Baez said:

Without that extra condition on the morphisms you get a very cute little presheaf topos of Petri nets, but it's not useful in applications.
So, I said goodbye to it and moved on.

The full presheaf category is curious. In the case of trees (where the shape is A <- M -> N -> A), I never found any use of the general presheaf maps. But just this Spring, David Myers and David Spivak discovered that the general presheaf maps are the natural transformations of Dirichlet functors! (And that Dirichlet functors are the contravariant polynomial functors.) I find it amazing!

(For the SITOS diagrams, I used the general maps in the case of graphs. They are not directly useful for props or properads, but they turned out to be useful for technical purposes, to describe an adjunction with closed graphs, and to deal with paths and convexity of graphs.)

view this post on Zulip Mike Shulman (May 12 2020 at 16:52):

What are Dirchlet functors and contravariant polynomial functors?

view this post on Zulip Joachim Kock (May 12 2020 at 17:41):

Mike Shulman said:

What are Dirchlet functors and contravariant polynomial functors?

Briefly, where a polynomial functor is a sum of representable functors, a Dirichlet functor is a sum of corepresentable functors.

See Myers-Spivak: Dirichlet Functors are Contravariant Polynomial Functors
http://arxiv.org/abs/2004.04183

view this post on Zulip John Baez (May 12 2020 at 17:55):

Oh, I see - they really are like categorified Dirichlet series, sorta kinda.

view this post on Zulip Joachim Kock (May 12 2020 at 20:19):

John Baez said:

Different applications of Petri nets make use of the two different philosophies. For example, chemistry uses the collective token philosophy (Petri nets as presentations of free commutative monoidal categories), because for them switching two oxygen atoms counts as doing nothing at all
[snip]

I think I am fine with the idea that in some situations the natural questions to ask concern the number of tokens instead of the set of tokens.

Another example found in some places is that of some school boys, collecting money for a present to their math(?) teacher. Each boy contributes 1 pound, but when buying the present not all the money is spent. Does it then make sense to ask whose pounds were spent?

But I am still struggling with the philosophy part. Is it never useful to consider the groupoid of states instead of only it isomorphism class, even if you are only interested in number?

I am not trying to impose the individual-token philosophy on anyone. I would just like to understand why my groupoid intuition does not work in this case. Instinctively, when I see a natural number, I think it should be a set, and when I see a natural-number linear combination I think it should be a span. I learned this from reading the Baez-Dolans.

If you set 10 hydrogens loose on 5 oxigens, are you never interested in how they pair up? I understand that the answer is 'no' from a macroscopic viewpoint. But is it never useful to think about some sum of histories, or at least care about whether the two hydrogen atoms from the same molecule remain together when they become a water molecule?

From what I read here, the answer is no: it is not relevant.

Maybe I am just being silly or naive, thinking that I can transfer intuition from concurrency to something as different as chemical reactions, where there are billions of tokens. Maybe it is never relevant to consider a single firing of a transition, or care about which events depend causally on which others. Could it be that the very idea of process -- in the Goltz-Reisig sense I consider in my paper -- is irrelevant in this context?

I hope it does not sound like I am stubborn. Only slow.

view this post on Zulip Nathaniel Virgo (May 12 2020 at 21:25):

I am not sure how this connects to the mathematical discussion, but sometimes people do care about which oxygen atoms go where. It comes up if you use isotopes to study biochemistry. Then you need to know whether the O2 that plants give off is the O from the CO2 they breathe or from the H2O they drink. (I think it's from the H2O, but don't quote me.) I think it's mostly the carbon atoms that are important to keep track of. The group that includes Jakob Andersen study this kind of thing with their computational models.

view this post on Zulip James Fairbanks (May 12 2020 at 21:26):

I think that if you care about which molecule matches up with the other, you are taking a single token philosophy. You still have processes in chemistry it’s just not distinguishable to say which molecules went where, if you could, then it wouldn’t be mass action. It would be a different model of chemical theory.

view this post on Zulip James Fairbanks (May 12 2020 at 21:27):

I think the atomic isotopes issue is best thought of as different species for the different isotopes

view this post on Zulip James Fairbanks (May 12 2020 at 21:29):

In biochemistry you have this spatial structure too so you can think of cells as machines for enforcing the violation of mass action assumptions. They have a lot of complex processes going on to ensure that things don’t become uniformly distributed.

view this post on Zulip Fabrizio Genovese (May 13 2020 at 22:38):

John Baez said:

Fabrizio Genovese said:

This also highlights very well why the collective token philosophy does not work well in many compsci applications. There your places do not have type unit, and being tokens terms of that type you need to distinguish between tokens in an execution.

What's a "type unit"? I don't understand the last sentence here, in part because of that and in part because the chunk after "and" isn't grammatical (as far as I can tell). But I think I understand the basic idea in a vague way, and I'd like to understand it the way you do.

What I mean is that places do not have type unit. unit is the type with just one term. So two terms of this type are always the same term and you can't really distinguish between them. I'd say my last sentence is grammatical tho. I parse it like this:
(and (being tokens terms of that type)) (you need to distinguish between tokens in an execution.) The only part I am not 100% sure about is "being tokens terms of that type", which I interpret as equivalent to "given that tokens are terms of that type". I've found some sentences that were of this form in some books though, so I assumed it's a thing in English.

view this post on Zulip Nathanael Arkor (May 13 2020 at 22:42):

I think if you transpose "being" and "tokens", it becomes clear.

There your places do not have type unit, and, tokens being terms of that type, you need to distinguish between tokens in an execution.

view this post on Zulip Fabrizio Genovese (May 13 2020 at 22:48):

Yes, that's probably the confusing part. Transposing "tokens" and "being" like that sounds way more natural in English, but feels very unnatural in my first language, so probably that's the source of confusion :slight_smile:

view this post on Zulip John Baez (May 13 2020 at 22:50):

Yes, "being tokens of that type" isn't grammatical in English unless it's part of something like "the aforementioned items being tokens of that type". That's what was throwing me.