Quantales from Petri Nets

Azimuth 2019-10-05

A referee pointed out this paper to me:

• Uffe Engberg and Glynn Winskel, Petri nets as models of linear logic, Colloquium on Trees in Algebra and Programming, Springer, Berlin, 1990.

It contains a nice observation: we can get a commutative quantale from any Petri net.

To do this, we can compose three functors.

First, any Petri net gives a commutative monoidal category—that is, a commutative monoid object in $\mathsf{Cat}$ . Indeed, my student Jade has analyzed this in detail and shown the resulting functor from the category of Petri nets to the category of commutative monoidal categories is a left adjoint:

• Jade Master, Generalized Petri nets, Section 4.

Second, any category gives a poset where we say $x \le y$ if there is a morphism from $x$ to $y.$ Moreover, the resulting functor $\mathsf{Cat} \to \mathsf{Poset}$ preserves products. As a result, every commutative monoidal category gives a commutative monoidal poset: that is, a commutative monoid object in the category of Posets.

Composing these two functors, every Petri net gives a commutative monoidal poset. Elements are of this poset are markings of the Petri net, the partial order is “reachability”, and the commutative monoid structure is addition markings.

Third, any poset $P$ gives another poset $\widehat{P}$ whose elements are upsets of $P$ : that is, subsets $S \subseteq P$ such that

$x \in S, x \le y \; \implies \; y \in S$

The partial order on upsets is inclusion. This new poset $\widehat{P}$ is ‘better’ than $P$ because it’s cocomplete. That is, any union of upsets is again a upset.

Composing this third functor with the previous two, every Petri net gives a commutative monoid object in the category of cocomplete posets. But a commmutative monoid object in the category of cocomplete posets turns out to be exactly what people call a commutative quantale. (This fact may not be entirely obvious, depending on what definition of commutative quantale you use. But this bare minimum definition implies other things.)

What is this commutative quantale like? Its elements are upsets of markings of our Petri net: sets of markings such that if $x$ is in the set and $y$ is reachable from $x$ then $y$ is also in the set!

This is quite a reasonable thing to think about. But what does it have to do with linear logic?

In linear logic, propositions form a category where the morphisms are proofs and we have two kinds of ‘and’: $\&$ , which is a cartesian product on this category, and $\otimes$ , which is a symmetric monoidal structure. There’s more to linear logic to this (there are other connectives), and maybe also less (since we may want our category to be a mere poset), but never mind. I want to focus on the weird business of having two kinds of ‘and’.

Since $\&$ is cartesian we have $P \Rightarrow P \& P$ as usual in logic.

But since $\otimes$ is not cartesian we usually don’t have $P \Rightarrow P \otimes P.$ This other kind of ‘and’ is about resources: from one copy of a thing $P$ you can’t get two copies.

Here’s the way to think about it: if $P$ is “I have a sandwich”, $P \& P$ is like “I have a sandwich and I have a sandwich”, while $P \otimes P$ is like “I have two sandwiches”.

Now, it’s a fact that every cocomplete poset is also complete. That is, if every subset has an least upper bound, then every subset has a greatest lower bound. This is a fun exercise.

So, a quantale must have cartesian products as well as its original monoidal structure, and these give us the $\&$ and the $\otimes$ of linear logic, respectively.

But it’s nice to think about all this in the Petri net examples! A marking can be seen as a ‘resource’. For example, if our Petri net has a place in it called $\textrm{sandwich},$ there is a marking $2 \textrm{sandwich},$ which means you have two sandwiches. Up-sets of markings are sets of markings such that if $x$ is in the set and $y$ is reachable from $x$ then $y$ is also in the set! So, they are collections of resources, such that if a resource is in your collection, so is any resource obtainable from it.

The tensor product $\otimes$ comes from addition of markings, extended in the obvious way to up-sets of markings. So, a sandwich (and everything you can get from it) tensored with a sandwich (and everything you can get from it) is 2 sandwiches (and everything you can get from them).

On the other hand, the cartesian product $\&$ is the logical ‘and’: if you have a sandwich (and everything we can get from it) and you have a sandwich (and everything you can get from it) that simply means you have a sandwich (and everything you can get from it).

So that’s the basic idea!

At this point, I should admit that I get completely confused about two arbitrary conventions. Given two markings of a Petri net $x$ and $y$ , if $y$ is reachable from $x$ should we say $x \le y$ or $y \le x?$ There are reasonable arguments on both sides. Also: given a poset, to should we take its collection of downsets or its collection of upsets?

That amounts to 4 possible conventions. Which one is best? I want the cartesian product $\&$ to match the familiar logical ‘and’.

Luckily none of this matters much in the grand scheme of things….