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