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: deprecated: concurrency

Topic: Nets Within Nets From Grothendieck

Jade Master (Jan 29 2021 at 02:55):

Following the discussion about concurrency with a local and a global layer, I wanted to share my favorite model of concurrency which captures this hierarchical structure. They are called object systems and I wrote a blog post describing them with the language of category theory:

• Nets within nets from the Grothendieck construction
  Please let me know if you have any comments, questions, or feedback.

Fabrizio Genovese (Jan 29 2021 at 10:03):

This is very nice. I'm putting out a paper about hierarchical nets in a few days. We do a similar thing (functors -> Grothendieck) but you described nets where tokens are themselves nets. In my model instead firing a transition corresponds to fire a sequence of transitions in another net.

Fabrizio Genovese (Jan 29 2021 at 10:04):

In any case, it's super cool that all these things are somehow similar. This doesn't do anything but reinforce my assumption that extensions of Petri nets are lax functors from a free category to Span.

Fabrizio Genovese (Jan 29 2021 at 10:05):

(The Grothendieck construction on your functor Net -> CMC -> Cat gives the same result of the total category construction applied to a functor Net -> Span :smile: )

Fabrizio Genovese (Jan 29 2021 at 10:06):

We should really coordinate and classify these functors at some point. I'm 100% convinced I can represent even nets with inhibitor arcs in this formalism.

Chad Nester (Jan 29 2021 at 14:24):

This is such a fun idea :D

Chad Nester (Jan 29 2021 at 14:32):

It’s only two-level right? Does anything go wrong if we make it N-level?

Fabrizio Genovese (Jan 29 2021 at 16:41):

I don't know Jade's case. in my case you can do it multi-level but it's a bit disappointing. Basically if your net $N$ has $n$ transitions, you need to define $n$ hierarchical nets $F_i : N_i \to Span$ (I'm intentionally confusing nets with the categories they generate). Then you can define a functor $F: N \to Span$ Where you put the morphism of $\int F_i$ in the tips of the spans corresponding to generating morphisms

Fabrizio Genovese (Jan 29 2021 at 16:42):

The reason why I don't like this too much is because you are forced to internalize to recurse the hierarchical construction, somehow losing type hygiene in the process.

Jade Master (Jan 29 2021 at 16:55):

@Fabrizio Genovese do you know about displayed categories?

Fabrizio Genovese (Jan 29 2021 at 16:55):

This is precisely what we have been using in the paper stream we are putting out, yes

Jade Master (Jan 29 2021 at 16:57):

Oh right, I just wasn't sure if you because I don't remember you using that terminology. But anyway Lax functors C -> Span end up being equivalent to arbitrary functors D -> C, you don't need any sort of fibration property

Fabrizio Genovese (Jan 29 2021 at 16:58):

Yes, that is correct

Fabrizio Genovese (Jan 29 2021 at 16:58):

This is the main mechanism we use

Fabrizio Genovese (Jan 29 2021 at 16:58):

Not all extensions of Petri nets are fibrations in the end

Jade Master (Jan 29 2021 at 16:59):

So yeah it seems like this your idea in the end, that basically an extension of a Petri net P is a functor D -> FP

Fabrizio Genovese (Jan 29 2021 at 16:59):

This is why classifying lax functors C -> Span is important

Fabrizio Genovese (Jan 29 2021 at 17:00):

Jade Master said:

So yeah it seems like this your idea in the end, that basically an extension of a Petri net P is a functor D -> FP

In the most general definition, yes. Clearly many of them are totally useless and ugly

Fabrizio Genovese (Jan 29 2021 at 17:00):

So the question becomes: What classes of functors FP -> Span give you meaningful extensions?

Fabrizio Genovese (Jan 29 2021 at 17:00):

By flipping things around and seeing things this way we were able to represent bounded nets, for instance

Jade Master (Jan 29 2021 at 17:01):

Hm cool

Fabrizio Genovese (Jan 29 2021 at 17:01):

And the guarded nets as functors FP -> Span is just a super restricted case of this, when your semantics is local

Fabrizio Genovese (Jan 29 2021 at 17:02):

the point of the functor being lax is exactly that you can endow tokens with global properties of the net, such as the "bound status" of the net places

Jade Master (Jan 29 2021 at 17:02):

Yeah the laxator gives the guards in colored Petri nets?

Jade Master (Jan 29 2021 at 17:03):

Uh wait not exactly

Fabrizio Genovese (Jan 29 2021 at 17:03):

The laxator is a sort of entanglement, it allows tokens to share the global properties that each token knows individually into a global thing

Jade Master (Jan 29 2021 at 17:03):

Right yeah

Fabrizio Genovese (Jan 29 2021 at 17:03):

Jade Master said:

Yeah the laxator gives the guards in colored Petri nets?

So guarded nets are fully local, your functors are strict monoidal

Fabrizio Genovese (Jan 29 2021 at 17:03):

In this interpretation this means that guards precisely act on information pertaining the single tokens being processed and nothing else

Fabrizio Genovese (Jan 29 2021 at 17:04):

A hierarchical nets in the sense of "transitions firing correspond to executions in a subnet" is just a guarded net, where in the tips of the span you are putting executions of the children net as witnesses

Fabrizio Genovese (Jan 29 2021 at 17:04):

So you are saying "to fire you have to prove to me that this happened in the child net first"

Jade Master (Jan 29 2021 at 17:08):

@Chad Nester thanks! Yeah I think you can keep going deeper, once you have the category of ObSys of object systems as constructed in my post, then you can consider functors FP -> ObSys to give a Petri net, whose tokens are object systems

Jade Master (Jan 29 2021 at 17:10):

That's a cool idea, I wonder if nets within nets within nets has any practical interpretation :thinking:

Jade Master (Jan 29 2021 at 17:11):

@Fabrizio Genovese sounds cool I'm excited to read your paper on it.

Jade Master (Jan 29 2021 at 17:18):

Anyway @Joe Moeller the monoidal structure on marked Petri nets that I mention here is an instance of the fibrewise monoidal Grothendieck construction I'm pretty sure.

Joe Moeller (Jan 29 2021 at 17:21):

That seems reasonable to me.

John Baez (Jan 29 2021 at 18:42):

Jade Master said:

That's a cool idea, I wonder if nets within nets within nets has any practical interpretation :thinking:

It probably does. I can write a Petri net program that does things with tokens, and you can design those tokens to be Petri nets of your choosing, which do their own things with tokens, and Fabrizio can design those tokens to be Petri nets in their own right. And this can keep going: since people build software on top of other software, this doesn't seem so weird.

Have one of you worked out a "flattening" functor that turns a net-of-nets into a net? This might be useful. Then there should a theorem saying that if you have a net-of-net-of-nets, the two ways of flattening it down to a net (in two steps) are equal, or at least isomorphic.

Joe Moeller (Jan 29 2021 at 18:57):

Usually when you look up operads of graphs (something I was doing a lot when I first started my thesis work), you get operads where the composition involves blowing up a node into a graph, and then attaching edges coming from the edges which were attached to the now blown up node. This seems pretty similar to what's happening here I think.

Jade Master (Jan 29 2021 at 19:14):

Yes @John Baez that makes sense to me, I think programs which manipulate programs which manipulate programs happens a lot in computer science. Regarding the flattening functor @Joe Moeller and I started to work out something like this in our un-released paper on colored Petri nets. For a colored Petri net, you can use the Grothendieck construction to turn it into an ordinary Petri net with the same behavior. I'm guessing you can do the same thing for object systems.

Jade Master (Jan 29 2021 at 19:15):

Also @Fabrizio Genovese's papers have this as well...I'm pretty sure he calls it the unfolding? Or maybe just the Grothendieck construction.

Jade Master (Jan 29 2021 at 19:19):

I'm not sure how the flattening should actually work for object systems but I bet something like that exists and it's a great suggestion.

Jade Master (Jan 29 2021 at 19:21):

@Joe Moeller yes it does feel kind of operadic, I see what you mean.

dan pittman (Jan 29 2021 at 19:27):

What do I need to know to understand Grothendieck constructions? Is there a type theoretic analogue? That'd help me.

Kenji Maillard (Jan 29 2021 at 19:38):

dan pittman said:

What do I need to know to understand Grothendieck constructions? Is there a type theoretic analogue? That'd help me.

From (dependent) type theory, Grothendieck constructions are quite easy to get: they are glorified dependent sums. Of course the tricky part is to actually get them right so that whathever structure you have on your base and on the fibers "glue together" to form the adequate structure on the whole dependent sum.

John Baez (Jan 29 2021 at 20:09):

What do I need to know to understand Grothendieck constructions?

Maybe this:

If you have a category functor $F: C \to \mathsf{Cat}$, you get a category $\int F$ where:

• an object is a pair $(c,x)$ consisting of object $c \in C$ together with an object $x \in F(c)$,

• a morphism from $(c,x)$ to $(c',x')$ is a morphism $f: c \to c'$ in $C$ together with a morphism $g: F(f)(x) \to x'$ in the category $F(c')$.

This is the Grothendieck construction. Work out a few examples and you'll get the point: it "glues together" or "integrates" all the categories $F(x)$ in one big category. That's why it's called $\int F$.

John Baez (Jan 29 2021 at 20:14):

For an easy example take $C$ to be the category with two objects 1 and 2, and one morphism from the first to the second. Draw pictures of some simple categories $F(1)$ and $F(2)$, and draw them sitting inside the category $\int F$, which has extra morphisms going from the objects of $F(1)$ to some of the objects of $F(2)$.

Fabrizio Genovese (Jan 29 2021 at 21:09):

John Baez said:

Jade Master said:

That's a cool idea, I wonder if nets within nets within nets has any practical interpretation :thinking:

It probably does. I can write a Petri net program that does things with tokens, and you can design those tokens to be Petri nets of your choosing, which do their own things with tokens, and Fabrizio can design those tokens to be Petri nets in their own right. And this can keep going: since people build software on top of other software, this doesn't seem so weird.

Have one of you worked out a "flattening" functor that turns a net-of-nets into a net? This might be useful. Then there should a theorem saying that if you have a net-of-net-of-nets, the two ways of flattening it down to a net (in two steps) are equal, or at least isomorphic.

Not sure this is possible. I think the language of nets within nets may be strictly more expressive than the language of Petri nets. If this is the case, then I don't think the internalized version of that functor is necessarily a free monoidal category

Fabrizio Genovese (Jan 29 2021 at 21:10):

So, for instance, if you consider nets with inhibitor arcs then it's true that their categorical semantics cannot be a monoidal category, because the functoriality of the tensor product gives you something wrong. This has to do with the fact that nets with inhibitor arcs are turing complete, while Petri nets are not.

Fabrizio Genovese (Jan 29 2021 at 21:11):

This is why the approach of defining extensions as functors is useful. By internalizing (using Grothendieck, total category etc) you get a categorical semantics in a canonical way, that may be completely different from the thing you imagined you'd get

Fabrizio Genovese (Jan 29 2021 at 21:15):

Fabrizio Genovese said:

So, for instance, if you consider nets with inhibitor arcs then it's true that their categorical semantics cannot be a monoidal category, because the functoriality of the tensor product gives you something wrong

To see this, imagine a net where there are:

• 2 places, $A$ and $B$.
• 2 transitions: $u: A \to B$, and $t: B \to B$. $t$ also has an inhibitor arc from $A$. Then:

$A \otimes B \xrightarrow{u \otimes id_B} B \otimes B \xrightarrow{id_B \otimes t} B \otimes B = A \otimes B \xrightarrow{id_A \otimes t} A \otimes B \xrightarrow{u \otimes id_B} B \otimes B$
But the right-hand-side is not a valid execution of the net.

Fabrizio Genovese (Jan 29 2021 at 21:16):

I have zero clue about how to define a categorical semantics of this, but I have a very good idea of how to define this as a lax functor from a free monoidal category to Span. Then I can get the categorical semantics for free by taking the total category.

dan pittman (Feb 01 2021 at 05:23):

Fwiw, a net of nets of nets would be endlessly (pun intended) useful in CS, and not just for cases where programs manipulate programs, but in cases like you shared in your post, where each actor has its own set of places to transition through, and so on and so on. I can't think of a better way to describe a distributed system.

dan pittman (Feb 01 2021 at 14:19):

Thinking about this again this morning, is flattening a requirement of the Petri net formalism? I ask because when thinking about applying these ideas as I mentioned above, I'm not sure it'd be necessary. Or to put it another way, I wouldn't have thought of doing such a thing.

Jade Master (Feb 01 2021 at 16:40):

@dan pittman I wouldn't say that it's necessary, but it's nice to be able to flatten your nets because if you can turn your object system into an ordinary Petri net with the same behavior, then there are lots of already developed techniques, theorems, and software you can use on the flattened net to tell you about the original one.

dan pittman (Feb 04 2021 at 01:24):

I've spent some time with this now, and I have a few questions. There are some hazy terms below that I realize aren't ideal terminology. I tried to put those things in “quotes”.

1. I think I understand the category $F P$: The objects are specific markings of Petri net $P$, and its morphisms are transitions between those markings. Does this imply that $F: \textbf{Petri} \rightarrow \mathbf{Cat}$, then?
2. If that's the case why do we need to pass through $\textbf{CMC}$ to get to $\textbf{Cat}$?
3. Is this the right intuition? $E$ is “lifting” the local net at place p to be at the same “level” as the global net P? I think I understand conceptually that the morphisms in $\textbf{MkPetri}$ entail the firing the initial marking, but how is the relation of the lifted local net at p to P retained?

Maybe 3 isn't a coherent question. Another possible intuition could perhaps be analogous to graph rewriting? Where place p is rewritten with its local net?

John Baez (Feb 04 2021 at 02:47):

Questions 1 and 2 look like a question about my paper with Jade Master. So even though @dan pittman probably isn't talking about that paper, I'll answer them as if he were talking about it.

1) There is a functor sending any Petri net $P$ to a category where the objects are markings and the morphisms are certain equivalence classes of sequences of transitions. (If you compose two transitions you don't get a transition, so we need to correct your statement this way.)

This category is very nice: it's a commutative monoidal category.

2) We pass through $\mathsf{CMC}$ because we want to understand what's going on. $F$ sends any Petri net $P$, not just to any old category, but to a very special one: the free commutative monoidal category on $P$. Thus, $F: \mathsf{Petri} \to \mathsf{CMC}$ is a left adjoint. This fact is very powerful. In particular, it guides us to getting the correct equivalence relation mentioned above. It also does a lot more.

There is also a forgetful functor $U: \mathsf{CMC} \to \mathsf{Cat}$ where we take a commutative monoidal category and think of it as a mere category. It sounds like you'd prefer to think about the composite $U F: \mathsf{Petri} \to \mathsf{Cat}$. This is indeed a functor, but it doesn't have any great properties: it's not anything nice like a left adjoint. The best way to understand $UF$ is to say that it's $U F$ and separately describe $U$ (which is a right adjoint) and $F$ (which is a left adjoint).

dan pittman (Feb 04 2021 at 03:01):

Heck yes. That makes so much sense, although I'd need to spend some quality time with the paper you linked to intuit the “equivalence classes of sequences”. I have an inkling of what that means in general, but would need to spend some time with the details.

John Baez (Feb 04 2021 at 03:15):

Great. The bulleted items on the top of page 7 says most of what you need to know, but at the end we slack off and say "mod out by the equivalence relations that must hold to get a commutative monoidal category" - or something like that.

If you want to see those equivalence relations spelled out, see the bulleted items on top of page 12 of Jade's paper Generalized Petri nets.

John Baez (Feb 04 2021 at 03:15):

I suppose we should have included them in our other paper too.

Fabrizio Genovese (Feb 04 2021 at 15:29):

Jade Master said:

dan pittman I wouldn't say that it's necessary, but it's nice to be able to flatten your nets because if you can turn your object system into an ordinary Petri net with the same behavior, then there are lots of already developed techniques, theorems, and software you can use on the flattened net to tell you about the original one.

It has to be noted that not all functors, when flattened, give you a petri net (that is, some kind of free monoidal categories). The functors that don't flatten nicely are the most interesting ones imho, providing extensions of nets that are non trivial (i.e. do not fit into a monoidal formalism), as for instance nets with inhibitor arcs, that cannot be done monoidally since functoriality of tensor cannot hold.

Jade Master (Feb 04 2021 at 16:07):

@Fabrizio Genovese you mean functors of type $FP \to \mathsf{Span}$? That's interesting about inhibitor arcs...why does it break monoidalness?

Jade Master (Feb 04 2021 at 16:08):

And thanks John, you explained it better than I could.

Fabrizio Genovese (Feb 04 2021 at 16:08):

Fabrizio Genovese said:

Fabrizio Genovese said:

So, for instance, if you consider nets with inhibitor arcs then it's true that their categorical semantics cannot be a monoidal category, because the functoriality of the tensor product gives you something wrong

To see this, imagine a net where there are:

• 2 places, $A$ and $B$.
• 2 transitions: $u: A \to B$, and $t: B \to B$. $t$ also has an inhibitor arc from $A$. Then:

$A \otimes B \xrightarrow{u \otimes id_B} B \otimes B \xrightarrow{id_B \otimes t} B \otimes B = A \otimes B \xrightarrow{id_A \otimes t} A \otimes B \xrightarrow{u \otimes id_B} B \otimes B$
But the right-hand-side is not a valid execution of the net.

See here

Fabrizio Genovese (Feb 04 2021 at 16:10):

This is obvious when you think about it. A net with inhibitor arcs has transitions that can check for "absence of objects", so you have to keep track of which objects appear first than others. In general, this also breaks concurrency in some ways, which again becomes obvious when you draw examples

Fabrizio Genovese (Feb 04 2021 at 16:11):

Jade Master said:

Fabrizio Genovese you mean functors of type $FP \to \mathsf{Span}$? That's interesting about inhibitor arcs...why does it break monoidalness?

For me a functor FP -> C or even CP -> C for any C can be considered in some way an "extension" of a Petri net. Clearly some functors are more interesting than others. Grothendieck provides a way to internalize the extended semantics. Sometimes we already know what to expect, some other times we do not. Those are the most interesting cases

Jade Master (Feb 04 2021 at 16:12):

Yeah that makes sense about inhibitor arcs. I've never known how to describe them categorically. Did you figure it out?

Fabrizio Genovese (Feb 04 2021 at 16:12):

I have a pretty good idea of how to represent a functorial semantics for nets with inhibitor arcs

Fabrizio Genovese (Feb 04 2021 at 16:13):

No clue what properties the grothendieck construction ends up having. For sure it's not monoidal nor free

Fabrizio Genovese (Feb 04 2021 at 16:13):

Jade Master said:

Yeah that makes sense about inhibitor arcs. I've never known how to describe them categorically. Did you figure it out?

If you tweak the definition of mana-net, you get what you want

Jade Master (Feb 04 2021 at 16:13):

Oh I guess you can represent the inhibitor arcs using guards?

Fabrizio Genovese (Feb 04 2021 at 16:13):

• Take a net
• Delete all the places with an inhibitor arc from them to a transition
• Add these places back in the non-local span semantics

Jade Master (Feb 04 2021 at 16:14):

Or yeah, using Mana nets.

Fabrizio Genovese (Feb 04 2021 at 16:14):

Jade Master said:

Oh I guess you can represent the inhibitor arcs using guards?

Yes, exactly

Fabrizio Genovese (Feb 04 2021 at 16:14):

But it's a "weird" kind of guards, like "dependently typed guards"

Fabrizio Genovese (Feb 04 2021 at 16:15):

In standard guarded nets a transition just checks for conditions on the tokens being processed. Here these conditions must be global (tokens have to testify for absence of tokens in other places)

Fabrizio Genovese (Feb 04 2021 at 16:15):

I guess there's some cleaner way to do all this, for sure, but at least it's a start XD