Petri nets and programming languages · theory: applied category theory

I had no idea, but that makes sense given Scala's focus on FP for the purpose of achieving parallel computing.

Henry Story (May 26 2020 at 13:43):

I had no idea either. I keep seeing petri-nets pop up here and there but not realizing their relation to programming I had no Idea what they were: so I never looked there. Now I have a reason. :grinning:
This is actually the way I am guiding my research into (applied) category theory. I try to find out which categories relate to tools or problems in computing (and in philosophy) I have come across and when I find a few interesting relations I can then sketchily estimate the value of looking into them and the time it would take to learn it superficially and then in more detail if I find that it fits. With time of course I find more and more connections.

This makes me think that for the applied-CT what would be useful would be to build a map of such relations, so that people could find out where CT could help them.

sarahzrf (May 26 2020 at 21:09):

a petri net is like a quiver where the source and target of each edge is a formal sum of vertices

sarahzrf (May 26 2020 at 21:10):

so they're nice for freely generating "commutative monoidal categories" in the same way that quivers are nice for freely generating categories

sarahzrf (May 26 2020 at 21:11):

or, e.g., a "prenet" is like a quiver where the source and target of each edge is a word of vertices

sarahzrf (May 26 2020 at 21:11):

so these are nice for freely generating ordinary non-symmetric monoidal categories

sarahzrf (May 26 2020 at 21:13):

actually, for any lawvere theory Q you can pull this off—you can define some kind of "net" which is like a quiver but with edges that go between elements of the free model of Q on the set of vertices, and this is good for freely generating categories that have Q-like structure

sarahzrf (May 26 2020 at 21:13):

Jade Master (May 26 2020 at 21:15):

Jade Master (May 26 2020 at 21:17):

Yeah my perspective on Petri nets is basically that they are graphs whose vertices are allowed to be fancier.

John Baez (May 26 2020 at 21:18):

Instead of calling your generalized Petri nets "Q-nets" maybe you should have called them "fancy graphs".

Henry Story (May 27 2020 at 16:54):

I asked Odersky if Petri-nets was still something he thought as contributing to Scala3. And he wrote:

Still the functional nets page is an intriguing historical document. But it may be that there is some library in Scala that is motivated by it... I'll need to research further.

Henry Story (Jul 19 2020 at 11:06):

There was an excellent talk Whole Grain Petri Nets by @Joachim Kock last week at the Applied Category Theory online conference. Looking at it I remembered @GUI 's link from a few months ago (above) to Martin Odersky's (father of Scala) early work on Functional Nets. So today I started reading the 2000 paper Functional Nets.

I could not clearly follow the second half of @Joachim Kock's talk even though I know a bit of HoTT, but I guess that will be easier when I read the paper. I wonder if Joachim's work has implications for Odersky's work on functional nets from 2000, and if he could have gone further with that idea had he known about it then.
Did I say the talk was really good? It is worth watching just for the presentation style.

PS. In mathematics sometimes it takes 3 months for something to go click! Sometimes 20, sometimes 2000. One has to be patient in this field :-)

Henry Story (Jul 19 2020 at 11:26):

Henry Story (Jul 19 2020 at 11:27):

The paragraph just after mentions Colored Petri nets (I guess this is why @Joachim Kock was using colors in his slides.)

Henry Story (Jul 19 2020 at 13:33):

Fabrizio Genovese (Jul 19 2020 at 13:36):

Yes, functional nets are way more powerful than Petri nets. Still, this is not always an advantage, especially if you care about model checking.

Fabrizio Genovese (Jul 19 2020 at 13:37):

In my experience at Statebox, it has turned out that a whole lot of CompSci can be done in a Turing incomplete setting. Petri nets are a great tool because they allow you to orchestrate tasks while retaining nice model checking features

Henry Story (Jul 19 2020 at 13:41):

I am at the point where I am happy to find a link between petri nets and a programming language (even better one that I use a lot!). That helps make sense of both. (definitely a link to add to the engineering nlab mentioned at the conference). :-)

Fabrizio Genovese (Jul 19 2020 at 13:43):

Henry Story (Jul 19 2020 at 13:44):

That must be related to the W3C Principle of Least Power finding.
It may be there are mathematical principles behind that finding and your experience at Statebox. That could be of interest to the W3C Technical Architecture Group.

Henry Story (Jul 19 2020 at 14:03):

What is interesting is that one the Web we started with a declarative systems that worked really well, where the principle of least power holds and is important, and then slowly JavaScript - a turing complete language - entered the picture and the original wisdom is being forgotten. So it would be useful to have some criteria as to when one should go one way rather than the other. (perhaps something for a WebCats channel I was thinking of setting up here when I joined)

Paul Pukite (Jul 20 2020 at 21:43):

Since the thread topic is Petri nets and programming languages, should mention that Ada has built-in semantics for the PN place-transition notation in the form of the task rendezvous notation. This is an early paper which shows some of the inspiration for the syntax and making the complete connection, primarily based on the idea of Communicating Sequential Processes by C.A.R. Hoare. https://pdfs.semanticscholar.org/520a/1f7a3ffb5bc7ae7a04955ec79d3051c505fa.pdf BTW, I have a large Ada library on github called the PetriNet Ada Component Environment that I have used over the years to simulate real-time multi-threaded robotic applications.

Paul Pukite (Jul 20 2020 at 21:54):

And this paper by Shatz in IEEE Computer -- Shatz. (1984). Communication Mechanisms for Programming Distributed Systems. Computer, 17(6), 21–28. doi:10.1109/mc.1984.1659159

Henry Story (Jul 21 2020 at 14:49):

Half way through his paper on Functional Nets Martin Odersky brings in the Join Calculus. I had heard of it vaguely, but never understood what it was meant to do. Odersky even wrote a library for it, which I think every advanced Scala programmer has looked at, but wondering how it was meant to be used.

But now with the help of the Whole Grain Petri Nets talk, and the other talks at the Applied Category Theory Conference I felt that I was understanding what was going on. So I looked around if anything had been done in scala on this, and I found at talk 4 years ago Concurrent Join Calculus in Scala by Sergei Winitzki author of The Science of Functional Programming that came out last year. This was another very clear explanation. (A bit slow perhaps). Together with the Whole Grain talk I think that could form a very good introduction to the subject for newbies.
He does ask the question why these have not been used that much, and gives a list of many implementations. Could it be that Petri Nets really shine for modeling things such as Pandemics? @James Fairbanks's talk compositional Scientific Computing suggests so.

Petri-Nets can be used to model Epidemics. This talk by @fairbanksjp shows how by extending #Julia (a scientific programming language) with categories of Petri Nets, one could quickly put complex multi-dimensional models for #Covid19 together. @ejpatters https://www.youtube.com/watch?v=Q5BzzkNDpPE&list=PLCOXjXDLt3pYot9VNdLlZqGajHyZUywdI&index=27&t=0s

- The 🐟‍‍ BabelFish (@bblfish)

James Fairbanks (Jul 21 2020 at 14:53):

I think that one of the reasons that people haven't used Petri Nets for real programming is that they lack abstraction, until recently we haven't had the tools for boxing up a Petri Net as a subroutine in a bigger Net. I think this is the biggest advance of ACT the ability to take lots of mathematical things that look flat (ie. Petri Nets, Graphs, Networks, Circuits) and give them hierarchy. That is driving a lot of the work on AlgebraicJulia right now.

Henry Story (Jul 21 2020 at 18:13):

In this talk from April Structured Cospans and Double Categories where @John Baez talks about how to compose Petri Nets as mentioned by James Fairbanks above, a question came up as to their relation to Operads. John says there is bound to be a relation there, though he had not worked it out yet.
I mention this because I recently used Akka Streams to write a simple Web Crawler and they had images that reminded me of things I had seen in Category Theory about gluing processes together, and I was told those looked like Operads. Here is a diagram
composite.png and another image.png where the pieces are glued together and the main code for the crawler starting from a source of some uris is

    def crawlerSource(uris: AkkaUri*): Source[GraphImports, NotUsed] =
        Source
            .fromGraph(GraphDSL.create() { implicit builder =>
                import GraphDSL.Implicits._
                val merge = builder.add(
                    Merge[AkkaUri](2).addAttributes(Attributes.inputBuffer(1, 8192))
                    )
                val bcast = builder.add(Broadcast[GraphImports](2, true).async)
                val filterCntr = builder.add(new FilterDuplicateURIsCounter(uris.size))

                val in = Source(uris)

                in ~> merge ~> uri2graphFlow ~> owlImportURLs ~> filterCntr ~> bcast.in
                      merge                <~ getUris                       <~ bcast.out(1)

                SourceShape(bcast.out(0))
            }
}

The input is sent to a merge component that merges the flow from getUris and from in. merge sends it on to uri2graphFlow which fetches each URI asynchronously on the web. owlImportURLs finds the owl:imports relations in the graph and spits out pairs of Try[ (Graph,URLs)]. (Try because fetching may have failed). The filterCounter counts urls send out and coming in so that it knows to stop the process and filters those already seen. A broadcast component sends the flow in two directions: (0) to the output and (1) to a filter that retains just the urls of the pair.
I wonder if this is an instance of one of these concepts.

Paul Pukite (Jul 22 2020 at 02:23):

" I think this is the biggest advance of ACT the ability to take lots of mathematical things that look flat (ie. Petri Nets, Graphs, Networks, Circuits) and give them hierarchy. "

If I am not misinterpreting the remark, the entire logical circuit design industry hinges on being able to create massive hierarchical component structures using what are essentially programming languages such as VHDL. e.g.:

Jules Hedges (Jul 22 2020 at 07:51):

So I think this is a crucial point in general. Being able to black box bits of complex network, as long as they're composed in an obvious way like joining wires together, is an extremely obvious thing to do and it would be pretty much unbelievable to claim nobody did it before. So what do we have that's new? One thing we have is a decently behaved algebraic theory of composing black boxes, so we can hope that there's something interesting to say that you need those more advanced tools for vs the obvious naive thing. But that doesn't happen automatically...

Jules Hedges (Jul 22 2020 at 07:52):

The other thing we have going for us is that with ACT methods we can also treat semantics compositionally on the same footing as syntax/networks/diagrams/circuits etc, I think it's much less likely that someone would naively come up with something equivalent to semantic span categories for example.

Henry Story (Jul 22 2020 at 08:25):

Jules Hedges (Jul 22 2020 at 08:29):

Not that I can think of. I mean, roughly, things that look like generalised relations

Jules Hedges (Jul 22 2020 at 08:29):

An approximate rule of thumb (this isn't precise and probably shouldn't be load-bearing) is that syntax is cospan-ish and semantics is span-ish

Henry Story (Jul 22 2020 at 08:30):

Henry Story (Jul 22 2020 at 08:39):

Jokes aside. I was reading a lot about coalgebras a year or two ago. When I see a Petri Net I would have first seen them as coalgebras, since they have state and move from one state to the other. Is that also a good way to look at them? Is there something lost in translation? (Looking at the index of Bart Jacbos "Introduction to Coalgebra" there is a reference to petri nets on the first page, but only there)

Jules Hedges (Jul 22 2020 at 08:47):

For sure that should be a thing. Maybe one of the petri nets people knows a standard reference for it

Fabrizio Genovese (Jul 22 2020 at 10:14):

I am always wary of hierarchical Petri nets. People are very eager to describe all the possible ways we can compose Petri nets together, but there is something we have to always keep in mind: Petri nets are useful as long as their reachability semantics doesn't go out of hand. When this happens, they are literally worth nothing in practice, since they lose all their "predictive" power. A lot of hiearchical definitions for Petri nets are very problematic from this point of view. This is a nice paper on the topic: https://www.researchgate.net/publication/262001792_A_Survey_of_Decidability_Results_for_Elementary_Object_Systems

Fabrizio Genovese (Jul 22 2020 at 10:15):

In general, this is one of my main concerns with the theory of composing systems: In many real life applications it is easy to obtain notions of compositions that are practically useless. This is why we need a strict collaboration with people that use the things we compose on a daily basis.

James Fairbanks (Jul 22 2020 at 12:11):

I think circuits work for building computers because they are compositional. If Intel had to think about circuits at the level of individual transistors, they would never be able to build processors.

Petri nets have their flat structure of states and transitions and you need a tool like ACT to tell you how to put a useful hierarchy on them. For example if you want reaction network semantics, you can give them a hypergraph category structure for glueing along species. Then you get an Operad of wiring diagrams that you can use to design complex chemical systems. If you don’t put a hierarchy on your reaction networks it gets very hard to manage even relatively small systems.

Jules Hedges (Jul 22 2020 at 12:13):

I suspect that for a modern CPU there are significant failures of compositionality, coming from electromagnetic interaction effects between neighbouring components

Fabrizio Genovese (Jul 22 2020 at 12:41):

Fabrizio Genovese (Jul 22 2020 at 12:42):

Actually the CPU example is really a good one, because the current CPU design status is awful, exectly because people blackbox stuff in a compositional algebra style without thinking about their semantics

Fabrizio Genovese (Jul 22 2020 at 12:43):

Did you ever hear of RowHammer? It's an attack on Intel CPUs which depends on design flaws so embedded and radicated in intel's CPU architecture that there's very little to do about them.

Fabrizio Genovese (Jul 22 2020 at 12:44):

Literally the family of RowHammer attacks grows by the day and no one has a decisive answer to fix the problem once and for all.

Fabrizio Genovese (Jul 22 2020 at 12:45):

Long story short: Blackboxing things to compose them is not something new that ACT discovered. This is literally how engineering works since the beginning of time. The novelty is - or should be- doing so in a way that is compositional with respect to the implications that composition has on semantics and model checking.

James Fairbanks (Jul 22 2020 at 12:53):

Oh I guess I don’t need to learn category theory because it apparently useless.

Henry Story (Jul 22 2020 at 12:53):

Thanks @Fabrizio Genovese , I was wondering why there was talk of semantics in the various online lectures I saw recently on Petri-Nets, and so I missed that dimension (not a big problem, as I am just discovering them). I can already see how it could be useful in circuit modeling, without understanding how.
Is there an example of how the compositionally in semantics and model checking could improve pandemic simulation tools, as it is a topical subject?

Fabrizio Genovese (Jul 22 2020 at 13:04):

This is a silly answer. It is not useless, on the contrary. The advantage of category theory is exactly that you can consider syntax AND semantics at the same time using functors, and come up with notions of composition that are best suited for your syntax. But focusing only on the "wiring things together" part of the problem is indeed akin to approaching it as it has been already done in the past, and not very insightful in my opinion.

Fabrizio Genovese (Jul 22 2020 at 13:05):

Also, for the very same reason, we should focus on functors between syntax and semantics that are strict or strong. Lax monoidal functors, in this respect, just tell you that "the semantics of the composite is more than the sum of its parts", which can be a nice categorical result, but not very usable in practice...

Morgan Rogers (he/him) (Jul 22 2020 at 13:47):

Surely that depends on how constructively the laxness is described? If we know exactly how much "the semantics of the composite is more than the sum of its parts", we should be able shift our perspective and think of the augmented composite semantics as an alternative composition. Like how composition in a Kleisli category for a monad isn't just composition of arrows, but carries along some extra information.
(I recently saw the use of monads in computer science justified as enabling Kleisli composition which carries along extra information, which is where I'm getting this idea from; I don't know how theoretically sound it is.)

Fabrizio Genovese (Jul 22 2020 at 13:48):

So you aren't really adding much, since everything can be rebuilt from the generators

Fabrizio Genovese (Jul 22 2020 at 13:49):

So I guess I see what you say, but lax monoidality is most often treated as a black box in the literature

Fabrizio Genovese (Jul 22 2020 at 13:49):

I think that when you have a clear understanding of what happens, you should be able to turn a lax monoidal correspondence into something better in a way or another

Morgan Rogers (he/him) (Jul 22 2020 at 14:01):

I have a sneaky suspicion the necessary conditions for that to happen would turn out to be something like the existence of a strength, but yes, that's what I was trying to get at! Even when it's not completely possible, I wonder if there's some mileage in approximating a lax monoidal functor with one of these "nice" lax monoidal things which can be presented in a practical way.

Fabrizio Genovese (Jul 22 2020 at 14:09):

I think that's a nice idea. Having different ways to "frame" lax functors would be something that goes in the same direction of a previous discussion we had here about categories handling failure in compositionality

Fabrizio Genovese (Jul 22 2020 at 14:10):

That is, you have an algebraic framework for composition and a semantics that doesn't really compose over it because your functors are lax. But maybe you can try to refine the properties of the framework and semantics to get increasingly tamer notion of laxity. Hopefully, at some point you may get a fully compositional correspondence, where your functor is strict.

Fabrizio Genovese (Jul 22 2020 at 14:11):

Btw, this kind of reasoning doesn't apply just to tensoring, but also to composition. So the natural setting to formulate all this are bicategories I believe

Morgan Rogers (he/him) (Jul 22 2020 at 14:30):

Maybe a toy example to consider would be a free monoidal category on generating objects

X_1,\dotsc,X_n

and lax monoidal functors to

(\mathbb{N}, \leq, +)

sending

X_{i_1} \otimes \cdots \otimes X_{i_n}

F(X_1) + \cdots + F(X_n) + n - 1

(assuming this would be well-defined, I haven't checked).

Morgan Rogers (he/him) (Jul 22 2020 at 14:32):

Such a functor is lax monoidal relative to the stated monoidal structure on

\mathbb{N}

, but if we replace it with a tweaked monoidal structure,

m \otimes n = m+n+1

, it's monoidal.

Morgan Rogers (he/him) (Jul 22 2020 at 14:34):

There are probably some details that I'm missing but I think this conveys what we were discussing.

Jules Hedges (Jul 22 2020 at 18:43):

Paul Pukite (Jul 22 2020 at 23:31):

This is a bit of applied composition that we did years ago. The application domain was real-time software design of robotic systems that typically had lots of Petri net synchronization. The idea is to lift out the real-time "pthread" scheduler and replace it with a black-box discrete event scheduler that could compress a timeline so that a process that may take hours to complete would run nearly instantaneously in a simulated environment. I came up with this idea at the time because I thought there should be some way to make a general-purpose real-time programming language into a VHDL-like simulator. YMMV

Since that time, I have run across a few Haskell front-ends for generating VHDL code

Matteo Capucci (he/him) (Jul 27 2020 at 09:52):

Or 2-categories, for what matters. Monoidal categories are 2-categories with one object. I think laxity can be given some topological interpretation. Then failure to be a strict 2-functor is going to be detected by some cohomological tools.
The above can be retouched to cast the problem in a more traditional setting, thereby enabling more traditional interpretations of cohomology, e.g. by taking simplicial nerves.

Matteo Capucci (he/him) (Jul 27 2020 at 09:53):

I don't know enough cohomology nor higher category theory nor homotopy theory to actually know how to do that, though. I hope I can bridge the gap in the following year.

Henry Story (May 02 2022 at 12:12):

I came across an Open Source library developed by ING (a Dutch Bank) based on Petri-Nets to orchestrate their processes. Links here and in the thread links to the work on Petri-nets and CT
https://twitter.com/bblfish/status/1521084507541196800

"Orchestrate ING with Petri Nets" a 2017 talk by @adilakhter explaining the reason for developing the Baker open source library built on petri-nets at @ING_news (the bank). (The slides are a bit fuzzy in the video: are they online somewhere?) https://www.youtube.com/watch?v=wICfskNsa2E

- The 🐟‍‍ BabelFish (@bblfish)

Stream: theory: applied category theory

Topic: Petri nets and programming languages

James Fairbanks (May 26 2020 at 13:33):

Henry Story (May 26 2020 at 13:43):

sarahzrf (May 26 2020 at 21:09):

sarahzrf (May 26 2020 at 21:10):

sarahzrf (May 26 2020 at 21:11):

sarahzrf (May 26 2020 at 21:11):

sarahzrf (May 26 2020 at 21:13):

sarahzrf (May 26 2020 at 21:13):

Jade Master (May 26 2020 at 21:15):

Jade Master (May 26 2020 at 21:17):

John Baez (May 26 2020 at 21:18):

Henry Story (May 27 2020 at 16:54):

Henry Story (Jul 19 2020 at 11:06):

Henry Story (Jul 19 2020 at 11:26):

Henry Story (Jul 19 2020 at 11:27):

Henry Story (Jul 19 2020 at 13:33):

Fabrizio Genovese (Jul 19 2020 at 13:36):

Fabrizio Genovese (Jul 19 2020 at 13:37):

Henry Story (Jul 19 2020 at 13:41):

Fabrizio Genovese (Jul 19 2020 at 13:43):

Fabrizio Genovese (Jul 19 2020 at 13:43):

Henry Story (Jul 19 2020 at 13:44):

Henry Story (Jul 19 2020 at 14:03):

Paul Pukite (Jul 20 2020 at 21:43):

Paul Pukite (Jul 20 2020 at 21:54):

Henry Story (Jul 21 2020 at 14:49):

James Fairbanks (Jul 21 2020 at 14:53):

Henry Story (Jul 21 2020 at 18:13):

Paul Pukite (Jul 22 2020 at 02:23):

Jules Hedges (Jul 22 2020 at 07:51):

Jules Hedges (Jul 22 2020 at 07:52):

Henry Story (Jul 22 2020 at 08:25):

Jules Hedges (Jul 22 2020 at 08:29):

Jules Hedges (Jul 22 2020 at 08:29):

Henry Story (Jul 22 2020 at 08:30):

Henry Story (Jul 22 2020 at 08:39):

Jules Hedges (Jul 22 2020 at 08:47):

Fabrizio Genovese (Jul 22 2020 at 10:14):

Fabrizio Genovese (Jul 22 2020 at 10:15):

James Fairbanks (Jul 22 2020 at 12:11):

Jules Hedges (Jul 22 2020 at 12:13):

Fabrizio Genovese (Jul 22 2020 at 12:41):

Fabrizio Genovese (Jul 22 2020 at 12:42):

Fabrizio Genovese (Jul 22 2020 at 12:43):

Fabrizio Genovese (Jul 22 2020 at 12:44):

Fabrizio Genovese (Jul 22 2020 at 12:45):

James Fairbanks (Jul 22 2020 at 12:53):

Henry Story (Jul 22 2020 at 12:53):

Fabrizio Genovese (Jul 22 2020 at 13:04):

Fabrizio Genovese (Jul 22 2020 at 13:05):

Morgan Rogers (he/him) (Jul 22 2020 at 13:47):

Fabrizio Genovese (Jul 22 2020 at 13:48):

Fabrizio Genovese (Jul 22 2020 at 13:48):

Fabrizio Genovese (Jul 22 2020 at 13:49):

Fabrizio Genovese (Jul 22 2020 at 13:49):

Morgan Rogers (he/him) (Jul 22 2020 at 14:01):

Fabrizio Genovese (Jul 22 2020 at 14:09):

Fabrizio Genovese (Jul 22 2020 at 14:10):

Fabrizio Genovese (Jul 22 2020 at 14:11):

Morgan Rogers (he/him) (Jul 22 2020 at 14:30):

Morgan Rogers (he/him) (Jul 22 2020 at 14:32):

Morgan Rogers (he/him) (Jul 22 2020 at 14:34):

Jules Hedges (Jul 22 2020 at 18:43):

Paul Pukite (Jul 22 2020 at 23:31):

Matteo Capucci (he/him) (Jul 27 2020 at 09:52):

Matteo Capucci (he/him) (Jul 27 2020 at 09:53):

Henry Story (May 02 2022 at 12:12):