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: learning: questions

Topic: smc to petri nets

Matteo Capucci (he/him) (Apr 23 2021 at 11:27):

What's the right (or left?) part of the adjunction between SMCs and Petri nets? I mean $U$ functor going $SMC \to PN$.
I readily find the construction of $F : PN \to SMC$ but I couldn't quickly find a reference to the other part

Fabrizio Genovese (Apr 23 2021 at 12:31):

Because it's not an easy question

Fabrizio Genovese (Apr 23 2021 at 12:32):

There are multiple possible answers, one of them is:
Use the net to generate a commutative monoidal category, which is a particular case of SMC

Fabrizio Genovese (Apr 23 2021 at 12:33):

The other is: Use a Petri net to generate a pre-net, and use this pre-net to generate the SMC

Fabrizio Genovese (Apr 23 2021 at 12:33):

If you check here: https://arxiv.org/abs/2101.04238 just look at the diagram, all the paths from Petri to SMC answer your questions

Fabrizio Genovese (Apr 23 2021 at 12:33):

all the adjunctions are spelled out in great detail in the paper

Jade Master (Apr 23 2021 at 14:24):

Yes. My opinion is that the strict commutativity of Petri nets means that they most naturally present commutative monoidal categories. If you're fine with using that adjunction then still the right adjoint is kind of hairy. It sends a CMC $s,t : Mor \to Ob$ to the Petri net with transitions $E=\{(\tau,x,y) \in Mor \times \mathbb{N}(Ob) \times \mathbb{N}(Ob) \, | \, s(\tau), t(\tau) \text{reduce to x and y}\}$.

Matteo Capucci (he/him) (Apr 23 2021 at 16:13):

Thanks Fab, that's where I went to look immediately but I don't see where the adjunctions are spelled out

John Baez (Apr 23 2021 at 16:20):

Matteo Capucci (he/him) said:

What's the right (or left?) part of the adjunction between SMCs and Petri nets? I mean $U$ functor going $SMC \to PN$.
I readily find the construction of $F : SMC \to PN$ but I couldn't quickly find a reference to the other part

You mean $F: PN \to SMC$, of course.

One useful realization is that Petri nets as traditionally defined naturally generate commutative monoidal categories, which are a very special class of symmetric strict monoidal categories where the symmetry is the identity.

So, @Jade Master and I worked out an adjunction between a rather obvious category $\mathsf{Petri}$ and the category $\mathsf{CMC}$ of commutative monoidal categories and strict symmetric monoidal functors. We guessed the correct left adjoint $F: \mathsf{Petri} \to \mathsf{CMC}$ easily but we got stuck on the right adjoint $U: \mathsf{CMC} \to \mathsf{Petri}$ - the part you're wondering - until @Mike Shulman helped us. Jade explained it all here:

• Jade Master, Petri nets based on Lawvere theories - Section 4, Generating free commutative monoidal categories from Petri nets.

The title of the section emphasizes the left adjoint, but I promise that your question about the right adjoint is answered. In fact, in one passage she mentions the reason we got stuck:

The reader at this point may guess a simpler formula for the right adjoint... Unfortunately this construction is doomed to fail.

John Baez (Apr 23 2021 at 16:22):

Indeed, this experience made me realize that besides a right adjoint, sometimes a functor will have a wrong adjoint.

John Baez (Apr 23 2021 at 16:26):

Later we teamed up with @Mike Shulman and @Fabrizio Genovese and worked out a more elaborate story involving adjunctions between 3 kinds of nets and 3 kinds of monoidal categories:

• strict monoidal categories, $\mathsf{StrMC}$
• symmetric strict monoidal categories, $\mathsf{SSMC}$
• commutative monoidal categories, $\mathsf{CMC}$.

@Fabrizio Genovese mentioned it already:

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

John Baez (Apr 23 2021 at 16:31):

Fabrizio gave a link to the arXiv version, but this minute I just made a newer, better version available on my website and linked to that.

John Baez (Apr 23 2021 at 16:34):

Here are the adjunctions we describe.

Matteo Capucci (he/him) (Apr 23 2021 at 16:34):

John Baez said:

Matteo Capucci (he/him) said:

What's the right (or left?) part of the adjunction between SMCs and Petri nets? I mean $U$ functor going $SMC \to PN$.
I readily find the construction of $F : SMC \to PN$ but I couldn't quickly find a reference to the other part

You mean $F: PN \to SMC$, of course.

Ha, yes, haha

Matteo Capucci (he/him) (Apr 23 2021 at 16:46):

Ok I'm digging the literature

Matteo Capucci (he/him) (Apr 23 2021 at 16:47):

@John Baez in the LICS version I still only see the construction of the left adjoints. Did I miss the other?

Matteo Capucci (he/him) (Apr 23 2021 at 16:51):

Proposition 2.4 of 'Functorial semantics of Petri nets' says that there is an 'obvious forgetful functor' from $FSSMC$ to $PreNet$.
So I guess what @Jade Master suggested above 'works' for ITP Petri nets (prenets?) too?

Matteo Capucci (he/him) (Apr 23 2021 at 16:52):

Jade Master said:

Yes. My opinion is that the strict commutativity of Petri nets means that they most naturally present commutative monoidal categories. If you're fine with using that adjunction then still the right adjoint is kind of hairy. It sends a CMC $s,t : Mor \to Ob$ to the Petri net with transitions $E=\{(\tau,x,y) \in Mor \times \mathbb{N}(Ob) \times \mathbb{N}(Ob) \, | \, s(\tau), t(\tau) \text{reduce to x and y}\}$.

If I understand correctly, this treats objects of $C$ (a SMC) as places and morphisms as transitions

Matteo Capucci (he/him) (Apr 23 2021 at 16:52):

Right, it is obvious indeed...

Matteo Capucci (he/him) (Apr 23 2021 at 16:54):

This might be the answer to this tweet of mine then:
https://twitter.com/mattecapu/status/1364139727964811264?s=20

Can I read every string diagram in an SMC as a Petri net whose places are wires and transitions are boxes? Summoning the Petri gang @JadeMasterMath @fabgenovese

- hom(—, matteo) (@mattecapu)

Matteo Capucci (he/him) (Apr 23 2021 at 16:55):

The idea would be to regard a string diagram as a presentation itself of an SMC, then run this SMC through the adjunction SMC-PN and voilà

John Baez (Apr 23 2021 at 17:00):

Matteo Capucci (he/him) said:

John Baez in the LICS version I still only see the construction of the left adjoints. Did I miss the other?

You need to read Jade's paper to see the right adjoint from $\mathsf{SSMC}$ to $\mathsf{Petri}$ worked out in detail. That's why I pointed you to Section 4 of that paper:

• Jade Master, Petri nets based on Lawvere theories - Section 4, Generating free commutative monoidal categories from Petri nets.

She also does the right adjoint from $\mathsf{StrMC}$ to $\mathsf{PreNet}$ in that paper - but it's a corollary of a more general result.

John Baez (Apr 23 2021 at 17:01):

Our LiCS paper, "Categories of nets", just cites Jade's work for those results.

Jade Master (Apr 23 2021 at 20:10):

Thanks for the great description John. Regarding your question @Matteo Capucci (he/him) the answer is yes, at least informally you can write every string diagram as a Petri net (but you'd probably be better off with a pre-net if you want to keep the ordering on the strings). If you want something more formal, I'd first ask how you are defining string diagrams.

Matteo Capucci (he/him) (Apr 23 2021 at 20:12):

i'm happy with this atm... but... I think the best way to define a string diagram for this problem is as an hypergraph?

Jade Master (Apr 23 2021 at 20:15):

A hypergraph is already very close to a Petri net so you don't need to do anything with the adjunction to get from hypergraphs to Petri nets.

Jade Master (Apr 23 2021 at 20:17):

I was expecting you to say "a morphism of a smc". If that's your definition of string diagram then the adjunction will help.

Fabrizio Genovese (Apr 23 2021 at 20:18):

Matteo Capucci (he/him) said:

The idea would be to regard a string diagram as a presentation itself of an SMC, then run this SMC through the adjunction SMC-PN and voilà

I agree with Jade,you want a pre-net

Fabrizio Genovese (Apr 23 2021 at 20:19):

You take an SMC. At that point, you can build a Pre-net from the smc: All objects of the SMC become places, all morphisms become transitions

Fabrizio Genovese (Apr 23 2021 at 20:19):

So you have this HUGE pre-net

Fabrizio Genovese (Apr 23 2021 at 20:19):

When you do the free SMC on it, you are essentially promoting each object/morphism of the original SMC to a generator

Fabrizio Genovese (Apr 23 2021 at 20:19):

So what you get is something like "execution trees" i guess

Fabrizio Genovese (Apr 23 2021 at 20:20):

That is, you have string diagrams that de facto combine string diagrams

Matteo Capucci (he/him) (Apr 23 2021 at 20:20):

bingo, but why trees? i was thinking of execution traces

Fabrizio Genovese (Apr 23 2021 at 20:20):

Because for me they are the same thing, I'm a mathematician not a programmer lol

Fabrizio Genovese (Apr 23 2021 at 20:21):

as you can already guess, there is a natural algebra operation that evaluates this traces, or whatever you wanna call them

Matteo Capucci (he/him) (Apr 23 2021 at 20:21):

Jade Master said:

I was expecting you to say "a morphism of a smc". If that's your definition of string diagram then the adjunction will help.

yeah but would this help to transform it into a petri net (or pre net as you and fabrizio pointed out)?

Fabrizio Genovese (Apr 23 2021 at 20:21):

This is related by the fact that composing the adjunctions gives you a monad or a comonad, I always have to think a good thirty seconds to figure out in which case I am

Matteo Capucci (he/him) (Apr 23 2021 at 20:22):

yeah, it'd be the action of the one of those lol

Fabrizio Genovese (Apr 23 2021 at 20:22):

Yes

Matteo Capucci (he/him) (Apr 23 2021 at 20:23):

even though something less might suffice. I mean, I really care about turning one morphism into a prenet into a SMC, not a whole SMC

Matteo Capucci (he/him) (Apr 23 2021 at 20:26):

so maybe the progression is more like: take an SMC, map it into a category of 'diagrammatic realizations' of its morphisms (hence its hom-sets are sets of hypergraphs), then map this category into a category of open pre-nets, then finally apply $U:PreNet \to SMC$ hom-wise to this category to get a category enriched in SMC (i.e. use the base-change along $U$)

Matteo Capucci (he/him) (Apr 23 2021 at 20:27):

the category you get has the same objects and morphisms are replaced by 'execution traces'

Fabrizio Genovese (Apr 23 2021 at 20:31):

Mhhhh, I guess you may have problems with objects

Fabrizio Genovese (Apr 23 2021 at 20:33):

pre-nets always generate a SMC with a free monoid of objects

Fabrizio Genovese (Apr 23 2021 at 20:33):

you see that if your SMC has a non-free monoid of objects (so you have equations like $A \otimes B = C$ floating around) than this approach won't work

Fabrizio Genovese (Apr 23 2021 at 20:33):

the only way of making it work is to promote _any_ object to a place in the pre-net

Matteo Capucci (he/him) (Apr 23 2021 at 20:36):

Fabrizio Genovese said:

pre-nets always generate a SMC with a free monoid of objects

yes this is needed to get executions from markings with many tokens, i.e. representing 'sending many values along a wire of the given string diagrams'

Matteo Capucci (he/him) (Apr 23 2021 at 20:36):

the rest I don't understand what you mean in the context of the construction I sketched :thinking:

Fabrizio Genovese (Apr 23 2021 at 20:37):

Matteo Capucci (he/him) said:

so maybe the progression is more like: take an SMC, map it into a category of 'diagrammatic realizations' of its morphisms (hence its hom-sets are sets of hypergraphs), then map this category into a category of open pre-nets, then finally apply $U:PreNet \to SMC$ hom-wise to this category to get a category enriched in SMC (i.e. use the base-change along $U$)

Oh, you are applying this hom-wise

Fabrizio Genovese (Apr 23 2021 at 20:37):

mhhh

Fabrizio Genovese (Apr 23 2021 at 20:38):

I don't sure if everything stays coherent working hom-wise

Fabrizio Genovese (Apr 23 2021 at 20:38):

Does it explode?

Matteo Capucci (he/him) (Apr 23 2021 at 20:38):

probably :laughter_tears: i just made it up so there's a high chance of nonsense

Fabrizio Genovese (Apr 23 2021 at 20:39):

Those are usually the things that work best

Fabrizio Genovese (Apr 23 2021 at 20:39):

modulo some fiddling

Fabrizio Genovese (Apr 23 2021 at 20:39):

But I don't really understand why you want to leave your object fixed

Fabrizio Genovese (Apr 23 2021 at 20:39):

It feels strange to change the morphisms but not the objects

Matteo Capucci (he/him) (Apr 23 2021 at 20:41):

i'll think about it... in my head it makes sense but i really don't know if it's the thing I want

Fabrizio Genovese (Apr 23 2021 at 20:41):

It feels quite unnatural from a net perspective, but maybe your application requires it

Matteo Capucci (he/him) (Apr 23 2021 at 20:42):

in simple terms, i'd like to turn a diagram of a morphism $X \to Y$ into a stream transformer $X^\omega \to Y^\omega$

Fabrizio Genovese (Apr 23 2021 at 20:42):

The standard way to get something aking to what you want (that can be found in the literature) is by looking at adjunctions between categories of nets and categories of _free_ SMCs

Fabrizio Genovese (Apr 23 2021 at 20:43):

What is a stream transformer? It's like you take infinite sequences of X and infinite sequences of Y and turn one into the other applying $f: X \to Y$ to the head of the stream (co?)recursively?

Matteo Capucci (he/him) (Apr 23 2021 at 20:44):

you take a stream of $X$ and turn it into a stream of $Y$

Fabrizio Genovese (Apr 23 2021 at 20:45):

Yeah, I'm thinking about streams as infinite sequences of things from $X$ or $Y$

Fabrizio Genovese (Apr 23 2021 at 20:45):

Not really infinite sequences, I'm being handwavy

Matteo Capucci (he/him) (Apr 23 2021 at 20:45):

yes infinite sequences works

Matteo Capucci (he/him) (Apr 23 2021 at 20:45):

though I guess prenets really give you $X^* \to Y^*$

Fabrizio Genovese (Apr 23 2021 at 20:46):

I'm not sure

Matteo Capucci (he/him) (Apr 23 2021 at 20:46):

Fabrizio Genovese said:

What is a stream transformer? It's like you take infinite sequences of X and infinite sequences of Y and turn one into the other applying $f: X \to Y$ to the head of the stream (co?)recursively?

anyway, it could happen you have loops so this is non-trivial

Fabrizio Genovese (Apr 23 2021 at 20:47):

So suppose you have the morphism $X \xrightarrow{f} Y \xrightarrow{g} Z$

Fabrizio Genovese (Apr 23 2021 at 20:47):

Now you say: I consider this as a hypergraph, and I turn this hypergraph into a pre-net

Matteo Capucci (he/him) (Apr 23 2021 at 20:47):

Fabrizio Genovese said:

I'm not sure

you can only represent finitely many tokens in any given place right? bc you use the free monoid on the places

Fabrizio Genovese (Apr 23 2021 at 20:47):

This pre-net will have places $X, Y , Z$

Fabrizio Genovese (Apr 23 2021 at 20:48):

and transitions $f, g$

Fabrizio Genovese (Apr 23 2021 at 20:48):

So in the resulting SMC you can also consider just the morphism $g: Y \to Z$, say

Fabrizio Genovese (Apr 23 2021 at 20:48):

which doesn't match your domain

Fabrizio Genovese (Apr 23 2021 at 20:48):

And yes, monoids are finite

Matteo Capucci (he/him) (Apr 23 2021 at 20:48):

oooh...

Matteo Capucci (he/him) (Apr 23 2021 at 20:49):

i didn't realize you could mark in perverse ways like that

Fabrizio Genovese (Apr 23 2021 at 20:49):

You can mark on _any_ place, as you like

Fabrizio Genovese (Apr 23 2021 at 20:49):

Instead, in the approach me and Jade were sketching, you are _not_ allowed to decompose morphisms that way

Fabrizio Genovese (Apr 23 2021 at 20:49):

each string diagram gets promoted to an atomic transition

Fabrizio Genovese (Apr 23 2021 at 20:49):

So I will only be able to apply $f;g$ as an atomic event

Morgan Rogers (he/him) (Apr 23 2021 at 20:50):

Jade and I are still (on and off) working out whether these adjunctions are monadic. Maybe I'll work on that some more next week since you guys are discussing it...

Matteo Capucci (he/him) (Apr 23 2021 at 20:52):

Fabrizio Genovese said:

Instead, in the approach me and Jade were sketching, you are _not_ allowed to decompose morphisms that way

i guess then this is what i want

Fabrizio Genovese (Apr 23 2021 at 20:52):

But then you will appreciate the necessity of ballooning up objects as well! :grinning:

Matteo Capucci (he/him) (Apr 23 2021 at 20:52):

Morgan Rogers (he/him) said:

Jade and I are still (on and off) working out whether these adjunctions are monadic. Maybe I'll work on that some more next week since you guys are discussing it...

so this might be an opportunity to ask... what does monadicity buy you?

Morgan Rogers (he/him) (Apr 23 2021 at 20:55):

Ha, not a great deal, besides some formal nonsense about how the category of SMCs is structured over the category of nets (everything is a coequalizer of free things) which isn't much of an improvement over the existing results about these categories

Morgan Rogers (he/him) (Apr 23 2021 at 20:56):

It will confirm that SMC homs are the "right" morphisms in the Kleisli category, which people have been assuming anyway.

Morgan Rogers (he/him) (Apr 23 2021 at 20:58):

More likely it will come in handy later when someone has a monad on the category of nets and they want to argue that it lifts to the category of SMCs: knowing that the latter is a category of algebras will provide an efficient abstract path to making that deduction. (Also we're doing it for Q-nets, so maybe there is a variant of nets where that will be more important).

Morgan Rogers (he/him) (Apr 23 2021 at 21:00):

To be honest, failure of monadicity would be a lot more work but a lot more interesting. I'll let you know which way the cookie crumbles when we get there :joy:

John Baez (Apr 23 2021 at 22:44):

Morgan Rogers (he/him) said:

Jade and I are still (on and off) working out whether these adjunctions are monadic. Maybe I'll work on that some more next week since you guys are discussing it...

Yay!

John Baez (Apr 23 2021 at 22:46):

Jade is at that stage where work on the thesis becomes a somewhat panicky rush to meet the deadline... so it may be mainly you doing this for a while.

John Baez (Apr 23 2021 at 22:48):

I don't know exactly what monadicity buys you, but it seems like a really natural question, so once it's answered I bet people will start figuring out things to do with it. @Evan Patterson and @James Fairbanks and I have a bunch of things we can do with the Kleisli category, for example. A bunch of these may work even if the adjunction between Petri nets and commutative monoidal categories is not monadic - as we discussed earlier here, there's still a Kleisli-like category.