[Prev][Next][Index][Thread]
A little linear logic observation about Petri Nets
Date: Tue, 11 Dec 90 13:57:43 GMT
A little linear logic observation about Petri Nets
Carolyn Brown (from Edinburgh) was here (Imperial College, London) last week
talking about her categories of Petri nets based on Valeria de Paiva's
"dialectica categories" (Carolyn presented her work at LiCS this year).
Afterwards, Carolyn and I tried but failed to make sense of an idea of mine
that Petri nets were "internal categories" in some context in which Valeria's
construction provided the "sets". However we did come up with a cute little
formula for sequences of actions which has a linear logic interpretation.
For those who are confused by the many different understandings of linear
logic in Petri Nets, let me just point out that what follows depends only on
the "trivial" observation that markings are additive, whereas Valeria &
Carolyn's work involves amuch more suble tensor.
I have in mind Petri nets which
* at first require at most one token from each place for an event,
* in the second case require an arbitrary natural number of them,
* and in the general case the input (and similarly the output) is an
element of a complete ordered monoid, or even a monoidal category.
First I'll phrase my argument in the "natural numbers" case. I want to
find the pre- and postconditions of the sequence $e;f$ in terms of those
of the events $e$ and $f$.
For each place $b\in B$, clearly we need at least $pre(e,b)$, else we
couldn't perform $e$. Then we need no more if $post(e,b)\geq pre(f,b)$,
but otherwise $pre(f,b)-post(e,b)$ in addition. Likewise the output is
at least $post(f,b)$, but there may be a left-over $post(e,b)-pre(f,b)$
in addition if this is nonnegative.
Writing $Se=<pre(e,b):b\in B>$ for the vector of inputs and likewise $Te$
for outputs, and using $+$ for componentwise addition and $-$ for
componentwise truncated subtraction (in which negative results are treated
as zero), we have
$$ S(e;f) = Se + (Sf - Te) $$
$$ T(e;f) = (Te - Sf) + Tf $$
(note carefully that the order of subtraction is reversed).
The generalisation and the linear logic observation depend on:
$(N,\geq,+,0)$ is a symmetric monoidal closed category
(note that the order is reversed: $n\to m$ iff $n\geq m$, contrary to the usual
convention). Bill Lawvere remarked this in his famous paper "Metric Spaces,
Generalized Logic and Closed Categories". The "internal hom" is exactly
truncated subtraction (with the arguments the other way round).
\def\llto{\mathbin{-\mkern-3mu\circ}}% TeX "-o" for linear implication
The formula for the input or precondition then becomes
$$ S(e;f) = Se \otimes (Te \llto Sf) $$
which we can immediately re-interpret using linear logic as
the input of $e;f$ is the input of $e$, together with
a way of turning the output of $e$ into the input of $f$
The output formula is
$$ T(e;f) = (Sf \llto Te) \otimes Se $$
which means
the output of $e;f$ is a way of using the requirements of $f$
to obtain output from $e$, together with the output of $e$.
which really uses the "contrapositive" meaning of the linear implication.
In fact, this interpretation works best if $\otimes$ is non-commutative and
the two different internal homs are used in the respective cases.
Paul Taylor