• 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.
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:
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 2sandwich, 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.
Related
This entry was posted on Sunday, October 6th, 2019 at 1:21 am and is filed under mathematics, networks. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.
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!
Is there a reason we can’t do a similar “downset” construction directly on the monoidal category? (I think it would give a distributive monoidal category or something similar.) Quantales have a cool name, but in general it’s better to use categories than posets whenever possible.
I replied:
Downsets are to posets as presheaves are to categories!
A poset is a Bool-enriched category and a downset is a Bool-functor just as a presheaf on a category is a functor
To see this, notice that given a poset a Bool-functor is a map from to truth values such that if true and q ≤ p then true. So, the subset of where equals true is a downset… and conversely, any downset gives a Bool-functor
So, when we form the poset of all downsets in , it’s the Bool-enriched version of forming the category of all presheaves on a category . Both are examples of a general ‘cocompletion’ process.
The category of presheaves on a category is the free cocomplete category on . The poset of downsets of (ordered by inclusion) is the free cocomplete poset on
A cocomplete poset is one that has all colimits. But this just says every subset has a least upper bound, also known as its join. A cocomplete poset is also called a suplattice.
There’s a category SupLat of suplattices, where morphisms are order-preserving maps that preserve least upper bounds (= colimits = joins):
Taking the poset of all downsets is the left adjoint of the forgetful functor SupLat Poset.
There’s a tensor product of suplattices, and a quantale is just a monoid object in (SupLat, ⊗).
There’s a tensor product of cocomplete categories, and a pseudomonoid in (complete categories, ⊗) is what I call a 2-rig. A 2-rig is a monoidal category with colimits, where tensoring with any object (on either the left or right) preserves colimits.
So yeah, we don’t have to descend to the world of posets. Any Petri net gives a commutative monoidal category, and the category of presheaves on that is a commutative 2-rig!
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:
• 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 single Petri net as in item 1) and massaging it a bit.
You can use Markdown or HTML in your comments. You can also use LaTeX, like this: $latex E = m c^2 $. The word 'latex' comes right after the first dollar sign, with a space after it. Cancel reply
You need the word 'latex' right after the first dollar sign, and it needs a space after it. Double dollar signs don't work, and other limitations apply, some described here. You can't preview comments here, but I'm happy to fix errors.
Azimuth 
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 single Petri net as in item 1) and massaging it a bit.