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: event: ACT20

Topic: Linear logic and Petri nets

John Baez (Jul 27 2020 at 19:46):

The first of the blog posts from the ACT2020 Adjoint School:

• Elena Di Lavore and Xiaoyan Li, Linear logic flavoured composition of Petri nets, The n-Category Cafe.

John Baez (Jul 27 2020 at 19:47):

And here's my summary - a series of tweets, which starts here (click to read more):

https://twitter.com/johncarlosbaez/status/1287787675634634761

Wow! Di Lavore and Li explain how to make a category of Petri nets that's a model of linear logic! I consider myself a sort of expert on Petri nets, but I didn't know this stuff: https://golem.ph.utexas.edu/category/2020/07/linear_logic_flavoured_composi.html Great pictures, too. Let me summarize a tiny bit. (1/n) https://twitter.com/johncarlosbaez/status/1287787675634634761/photo/1

- John Carlos Baez (@johncarlosbaez)

John Baez (Jul 27 2020 at 19:47):

My main question is whether this can be generalized from "elementary nets" to arbitrary Petri nets.

Valeria de Paiva (Jul 28 2020 at 17:40):

well, yes, it has been generalized to arbitrary Petri nets. the mathematical basis is the paper that Wilmer Leal and Eigil Rischel were working over, "Categorical multirelations, linear logic and Petri nets" TR from Cambridge http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-225.pdf. Thanks for the great summary and twitter thread!!

JS PL (he/him) (Jul 28 2020 at 18:33):

I have two questions:
1) Are there exponential modalities $!$ and $?$
2) Is it ever the case that we obtain biproducts? (possibly if the base category has biproducts?)

Valeria de Paiva (Jul 29 2020 at 04:09):

JS Pacaud Lemay said:

I have two questions:
1) Are there exponential modalities $!$ and $?$
2) Is it ever the case that we obtain biproducts? (possibly if the base category has biproducts?)

1) Yes, there are exponentials $!$ and $?$. (this was always the goal).
2) not naturally the case, but if the base category has biproducts, you probably can have them in dialectica too.
the product of $(U,X, \alpha)$ and $(V,Y, \beta)$ is $(U\times V, X+Y, choose)$. so if $U\times X\cong U+X$ you should end up with a byproduct.
(for our Petri nets the base category is Sets, so no biproducts.)

John Baez (Jul 29 2020 at 17:18):

Thanks, @Valeria de Paiva. The blog article didn't say that the work on elementary Petri nets was a "degeneralization" of your earlier work on Petri nets.

Valeria de Paiva (Jul 29 2020 at 17:32):

John Baez said:

Thanks, Valeria de Paiva. The blog article didn't say that the work on elementary Petri nets was a "degeneralization" of your earlier work on Petri nets.

hey, but it isn't a "degeneralization", really! the original work by Brown and Gurr was for elementary Petri nets. When I joined them I said I thought I knew how to make it work for "general Petri nets" and wrote the "math version" of the paper. Then we wrote the applied version jointly, submitted, had it accepted with modifications and then never had the time to do the modifications. because people were moving house, countries, etc. So I thought this was a good idea for the ACT Summer School, to pick up this old work and see how it stacked against newer work (The comparison is not so easy though). so the group was divided into two and Elena and Xiaoyan had the first part, Wilmer and Eigil the second. For the school we all chatted together and they convinced me of how we should proceed. Hopefully it will all work, but of course, the new research is all new, and hence, like all research, it might work. or not. Hopefully it will!

Valeria de Paiva (Aug 01 2020 at 00:42):

it's probably only me, but I've tried 4 times to reply to a comment in the n-cafe and four times the gadget destroyed my message and didn't post it (I've tried both chrome and firefox).
So hoping @Mike Shulman will see it here:

hi Mike,

Does an element of a multiset simply have a number of times that it occurs
yes, I think so.

As far I am concerned there are no non-monos $A\to E\times B$. The original constructions insist on monos, always. this is why I say the categories are equivalent over Sets.

Elena wants to generalize it to non-monos $A\to E\times B$, and this is cool. I mentioned to her that this was a suggestion of the late Aurelio Carboni, who was also very fond of spans. I was and still am reluctant, as I think the asymmetry given by the 'lax' condition on morphisms is what makes the dialectica constructive. But we're investigating!

Mike Shulman (Aug 01 2020 at 00:47):

The laxness seems unrelated to the mono-ness to me. If it's not a mono then the inclusion between subobjects would be replaced just by a map in the slice category. I would expect that since the categorified Chu construction like Chu(Cat,Set) is interesting, so would a categorified Dialectica construction be.

Valeria de Paiva (Aug 01 2020 at 01:03):

[Quoting…]
I beg to differ, the Dialectica construction is already a category, you don't need to categorify it!
but more seriously, sure, you may be right that maps in the slice category can be enough for a construction with the same characteristics. I don't know and this is why we're investigating--but I am skeptical.

Valeria de Paiva (Aug 01 2020 at 01:30):

Mike Shulman said:

The laxness seems unrelated to the mono-ness to me. If it's not a mono then the inclusion between subobjects would be replaced just by a map in the slice category. I would expect that since the categorified Chu construction like Chu(Cat,Set) is interesting, so would a categorified Dialectica construction be.

let me expand on why I am skeptical here. Sets have an initial and a terminal object that do not coincide. if I'm reading the nLab page https://ncatlab.org/nlab/show/span correctly Span(Sets) is such that "Span(Sets) is evidently equivalent to its opposite category, it follows that to the extent that limits exists they are also colimits and vice versa." so it seems to me that the initial and terminal objects here will coincide and this will make hmm, maybe this is wrong, but I assumed this would give me an isomorphism between $A$ and $A^\bot$, which is fine for classical linear logic, but not for FILL.

Mike Shulman (Aug 02 2020 at 01:32):

Where did the spans come from? I didn't hear anything about spans. I suppose a non-mono $A\to E\times B$ can be considered a span, but in that case you're comparing it to a mono $A\to E\times B$ which is a relation, and the category Rel(Sets) is equivalent to its opposite just like Span(Sets) is.