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