A referee pointed out this paper to me:

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

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

I’ll explain how in a minute. But first, what does 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 , which is a symmetric monoidal structure. There’s much more to linear logic than this (since 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 as usual in logic.

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

Here’s one way to think about it: if is “I have a sandwich”, is like “I have a sandwich and I have a sandwich”, while is like “I have two sandwiches”.

A commutative quantale captures these two forms of ‘and’, and more. A commutative quantale is a commutative monoid object in the category of cocomplete posets: that is, posets where every subset has a least upper bound. But it’s a fact that any cocomplete poset is also complete: every subset has a greatest lower bound!

If we think of the elements of our commutative quantale as propositions, we interpret as “ implies ”. The least upper bound of any subset of proposition is their ‘or’. Their greatest lower bound is their ‘and’. But we also have the commutative monoid operation, which we call This operation distributes over least upper bounds.

So, a commutative quantale has both the logical (not just for pairs of propositions, but arbitrary sets of them) and the operation that describes combining resources.

To get from a Petri net to a commutative quantale, we can compose three functors.

First, any Petri net gives a commutative monoidal category—that is, a commutative monoid object in . 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 if there is a morphism from to Moreover, the resulting functor 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 gives another poset whose elements are **downsets** of : that is, subsets such that

The partial order on downsets is inclusion. This new poset is ‘better’ than because it’s cocomplete. That is, any union of downsets is again a downset. Moreover, contains as a sub-poset. The reason is that each gives a downset

and clearly

Composing this third functor with the previous two, every Petri net gives a commutative monoid object in the category of cocomplete posets. But this is just a commutative quantale!

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

It’s good to contemplate this a bit more. A marking can be seen as a ‘resource’. For example, if our Petri net has a place in it called `sandwich`

there is a marking 2`sandwich`

, which means you have two sandwiches. Downsets of markings are sets of markings such that if is in the set and is reachable from then is also in the set! An example of a downset would be “a sandwich, or anything that can give you a sandwich”. Another is “two sandwiches, or anything that can give you two sandwiches”.

The tensor product comes from addition of markings, extended in the obvious way to downsets of markings. For example, “a sandwich, or anything that can give you a sandwich” tensored with “a sandwich, or anything that can give you a sandwich” equals “two sandwiches, or anything that can give you two sandwiches”.

On the other hand, the cartesian product is the logical ‘and’:

if you have “a sandwich, or anything that can give you a sandwich” and you have “a sandwich, or anything that can give you a sandwich”, then you just have “a sandwich, or anything that can give you a sandwich”.

So that’s the basic idea.

Mind-blowing John! Thanks for sharing!

Glad you liked it. It came as a little revelation to me.

How do you show that a cocomplete poset is also complete?

I bet someone here can do the exercise Jade mentions.

Why is every greatest lower bound an example of a least upper bound? That’s the key.

(Hint: think about the word “greatest” in the phrase “greatest lower bound”.)

John, thank you for using sandwiches in today’s examples. They are so nonthreatening that I was seduced into reading further than I otherwise would have:-)

possible typo: “then x is also in the set” -> “then y is also in the set”

I started out writing a version where I front-loaded all the abstract math and only illustrated it with sandwiches at the end. Then I realized that the sandwiches should come first, as an appetizer. Mathematicians tend to write in a top-down way, but it’s often easier to understand bottom-up.

If I hadn’t made that edit, you probably wouldn’t have caught that typo! Thanks—I’ll fix it now!

Over on Twitter Jules Hedges said:

I replied:

Wow! Elena Di Lavore and Xiaoyan Li explained 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:

• Elena Di Lavore and Xiaoyan Li, Linear logic flavoured composition of Petri nets,

The n-Category Café, 27 July 2020.It’s worth comparing this paper:

• Uffe Engberg and Glynn Winskel, Petri nets as models of linear logic, in

Colloquium on Trees in Algebra and Programming, Springer, Berlin, 1990, pp. 147–161.Engberg and Winskel get a model of linear logic—or to be precise, a ‘commutative quantale’—by taking the category you get from a

singlePetri net as in item 1) and massaging it a bit.