Quantales from Petri Nets

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 \otimes, 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 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 one 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”.

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 x \le y as “x implies y”. 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 \otimes. 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 \otimes 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 \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 downsets of P: that is, subsets S \subseteq P such that

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

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

\downarrow x = \{y \in P : \; y \le x \}

and clearly

x \le y \; \iff \;  \downarrow x \subseteq \downarrow y

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 x is in the set and x is reachable from y then y 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 x is in the set and x is reachable from y then y 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 \otimes 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.

7 Responses to Quantales from Petri Nets

  1. Samuel Vidal says:

    Mind-blowing John! Thanks for sharing!

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

  3. John Baez says:

    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”.)

  4. arch1 says:

    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”

    • John Baez says:

      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!

  5. John Baez says:

    Over on Twitter Jules Hedges said:

    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 P is a Bool-enriched category and a downset is a Bool-functor F: P^{\mathrm{op}} \to \mathrm{Bool}, just as a presheaf on a category is a functor F: C^{\mathrm{op}} \to \mathrm{Set}.

    To see this, notice that given a poset P, a Bool-functor F: P^{\mathrm{op}} \to \mathrm{Bool} is a map from P to truth values such that if F(p) = true and q ≤ p then F(q) = true. So, the subset of P where P equals true is a downset… and conversely, any downset gives a Bool-functor F: P^{\mathrm{op}} \to \mathrm{Bool}.

    So, when we form the poset of all downsets in P, it’s the Bool-enriched version of forming the category of all presheaves on a category C. Both are examples of a general ‘cocompletion’ process.

    The category of presheaves on a category C is the free cocomplete category on C. The poset of downsets of P (ordered by inclusion) is the free cocomplete poset on P.

    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 \to 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!

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.

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.