BRICS RS-94-3 U. H. Engberg & G. Winskel: Linear Logic on Petri Nets

BRICS

Basic Research in Computer Science

Linear Logic on Petri Nets

Uffe H. Engberg Glynn Winskel

BRICS Report Series RS-94-3 ISSN 0909-0878 February 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

Linear Logic on Petri Nets

Uffe H. Engberg  Glynn Winskel

BRICS^{∗}

Computer Science Department^{†} Aarhus University Ny Munkegade DK-8000 Aarhus C, Denmark

Abstract. This article shows how individual Petri nets form models of Girard’s intuitionistic linear logic. It explores questions of expressiveness and completeness of linear logic with respect to this interpretation. An aim is to use Petri nets to give an understanding of linear logic and give some appraisal of the value of linear logic as a specification logic for Petri nets. This article might serve as a tutorial, providing one in-road into Girard’s linear logic via Petri nets. With this in mind we have added several exercises and their solutions. We have made no attempt to be exhaustive in our treatment, dedicating our treatment to one semantics of intuitionistic linear logic.

Completeness is shown for several versions of Girard’s linear logic with respect to Petri nets as the class of models. The strongest logic considered is intuitionistic linear logic, with ⊗, ⊸, &, ⊕ and the exponential ! (“of course”), and forms of quantification. This logic is shown sound and complete with respect to atomic nets (these include nets in which every transition leads to a nonempty multiset of places). The logic is remarkably expressive, enabling descriptions of the kinds of properties one might wish to show of nets; in particular, negative properties, asserting the impossibility of an assertion, can also be expressed. A start is made on decidability issues.

Keywords. Linear logic, Petri nets.

Contents

1 Introduction 2

2 Intuitionistic Linear Logic 5

3 Proof Rules 5

4 Quantale Interpretation 8

5 Petri Nets 10 6 Quantales from Petri-Nets 12

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation.

†e-mail address: {engberg,gwinskel}@daimi.aau.dk, fax: +45 89 42 32 55

7 Petri-Net Interpretation 13

8 Expressing Properties of Nets 16

9 The “Of Course” Operator 19

10 Linear Negation 20

11 Recursion 23

12 Equivalences on Nets 24

13 Elementary Completeness Results 26

14 Quantification and Atomic Nets 33

15 Decidability Issues 47

16 Conclusion 50

A Answers to exercises 51

1 Introduction

Girard’s linear logic arose in part from Girard’s insights into particular categorical models for intuitionistic logic. In giving a domain-theoretic semantics to his System F (the polymorphic λ-calculus) [Gir86], Girard re-invented the stable domain theory of Berry based on the category dI-domains and stable functions [Ber78], though for rather special domains, the coherence spaces. It turns out that Girard’s construction for modelling polymorphic types can be carried through, with some modifications, in the more standard domain theory based on the category of Scott domains and continuous functions (see [CGW89]). But Girard’s use of the category of coherence spaces and stable functions led to a significant discovery, that of classical linear logic. Girard recognised that the category of coherence spaces with stable functions contained a reflective subcategory in which morphisms were “linear”; the adjunction explained how the larger category could be derived from the linear one, and through the propositions-as-types reading of logic it gave an explanation of intuitionistic logic in terms of a more primitive and new classical linear logic. Again, it turns out a similar observation could have been made were Girard to have used Scott’s domain theory, though the linear logic would then have had less structure (that of intuitionistic rather than classical linear logic). This is a thumbnail sketch of the discovery of linear logic, and indicates why it is viewed as “a logic to explain logic”.

Right from the start [Gir87], the categorical model of coherence spaces played a prominent role in the presentation of linear logic, and since other categorical models, arguably of a more informative character, have appeared; notable are those based on game semantics, initiated by Blass’s work (see [Bla92, AJ92]). Not everyone is happy with a categorical model as the explanation of a new logic, and in his pioneering paper [Gir87], Girard also gave a “phase–space” semantics for linear logic. There have since been investigations of several other kinds of structures as models of linear logic, quantales (e.g.[AV88]), generalised Kripke structures [AD93], and Petri nets—the main topic here.

Girard’s linear logic has sparked off a great deal of interest in how it might be useful in the theory of parallelism, not least because of Girard’s initial claims for it [Gir87]. Linear logic has been described as a “resource conscious” logic by Martí-Oliet and Meseguer [MOM89]; in its proofs occurrences of propositions cannot be used more than once or disappear unless they are explicitly created or used up by the rules of inference. People were not long in spotting a relationship with Petri nets where there are similar ideas. Places in a Petri net hold to certain nonnegative multiplicities forming a multiset of places, traditionally called a marking; as transitions occur, multiplicities of places are consumed and produced in accord with a dynamic behaviour of nets, formalised in the so-called “token game”. Independently, Gunter and Gehlot [GG89a], Asperti [Asp87] and Brown [Bro89] showed that places are like atomic propositions in linear logic and transitions like proof rules. In [GG89a] and [Asp87], the fine grain of linear logic proofs for the ⊗-fragment of linear logic is related to the token game in Petri nets. Essentially it is shown how a proof of A ⊢ B in linear logic, where A and B are built from place names just with ⊗, corresponds to a play of the token game taking the marking corresponding to A to that corresponding to B.

The work of Martí-Oliet and Meseguer [MOM89] extends that of [GG89a] and [Asp87]. It is known that certain kinds of “linear” categories are models for linear logic. The work [MOM89] essentially proceeds by letting Petri nets freely generate a linear category and then interpreting linear logic in that setting. One problem with their approach is its consequence that if a net satisfies an proposition of linear logic then so does any augmentation of the net, obtained by adding transitions arbitrarily. This considerably weakens the case for regarding linear logic as a specification logic with respect to their notion of satisfaction.^{1} Nor at this exploratory stage, when we are trying to understand what use linear logic might be on Petri nets, is it so clear, that a linear category with lots of proof terms as morphisms has any advantage over a more accessible partial order semantics, of the kind presented here.

1No one would take seriously a program logic with the property that if a program satisfied an assertion then so did the program with GOTO statements inserted arbitrarily.

Alongside the work on Petri nets and linear logic, came the realisation that models of linear logic had arisen before in the form of quantales. Indeed Girard’s phase semantics in [Gir87] for linear logic uses free quantales. Abramsky and Vickers [AV88] approached quantales from a computer science viewpoint, the hope being that it would lead to a “linear process logic”. Yetter [Yet] and Rosenthal [Ros89] looked at quantales and linear logic more from the perspective of pure mathematics—how to represent them and their relationship with other bits of mathematics.

We point out a straightforward way in which a Petri net induces a quantale and so becomes a model for intuitionistic linear logic. The model is for all of intuitionistic linear logic. A prime feature is its accessibility; this is important with the new logic, where working out what you can and cannot say is tricky. That it generalises the work of [GG89a] and [Asp87] is clear. The paper provides evidence that intuitionistic linear logic, with the right notion of satisfaction, can be a reasonably expressive specification logic for parallel processes. It also throws some light on the use of classical linear logic; via a construction, observed by Abramsky and Vickers [AV88], generalising that of Girard’s for phase semantics, a quantale can easily be turned into a model for classical linear logic, although unfortunately when taken to nets, the resulting semantics of classical linear logic is often trivial.

Our strongest completeness result is for the full logic described in [GL87, Laf88], viz. it includes

⊗, ⊸, ⊕, &, and !

though at a cost, to the purity of the linear logic, of adding quantification over markings and axioms special to the net semantics. For this strongest completeness result, a slight restriction is also made to the Petri nets considered as models; they should be atomic (see definition 36), but fortunately this restriction is one generally met, and even often enforced, in working with Petri nets. The step of considering only atomic nets as models has two important pay-offs: one is that the exponential !A becomes definable as A & 1, where 1 is the unit of ⊗; the other is that we can say internally, within the logic, that an assertion is not satisfied—the possibility of asserting such negative properties boosts the logic’s expressive power considerably. We can achieve completeness for more modest fragments of the logic without extra axioms and with respect to the entire class of nets as models (see section 13).

The work here (filling out that of [EW90, EW93]) contrasts with other approaches to linear logic on Petri nets in that they either apply only to much smaller fragments of the logic such as the ⊗-fragment (cf. [GG89b]), or use the transitions of a Petri net to freely generate a linear-logic theory (cf. [MOM91]), in which case the logic becomes rather inexpressive, and in particular cannot capture negative properties, or they don’t address completeness at all.

2 Intuitionistic Linear Logic

In the Gentzen sequent calculus for intuitionistic logic a sequent, A_{1}, …, A_{n} ⊢ A, is written to mean that the formula A is deducible from the assumption formulae A_{1}, …, A_{n} (we shall use Γ as an abbreviation for a (possibly empty) sequence of assumption formulae). The calculus has the two structural rules

\frac{Γ ⊢ B}{Γ, A ⊢ B} (thinning) \frac{Γ, A, A ⊢ B}{Γ, A ⊢ B} (contraction)  (1)

for adding an assumption and removal of a duplicate. In the presence of these rules the following two right introduction rules for conjunction

\frac{Γ ⊢ A Δ ⊢ B}{Γ, Δ ⊢ A ∧ B} \frac{Γ ⊢ A Γ ⊢ B}{Γ ⊢ A ∧ B}  (2)

become interderivable in the sense that the first rule can be derived from the second by thinning, and the second from the first by contraction.

Now, as remarked in [AV88], if a proof is to be seen as representing the process of proving, then these structural rules become far from self-evident. Indeed, in intuitionistic linear logic these rules are dropped and the rules of (2) are no longer interderivable. Without them, propositions cannot be introduced arbitrarily into a list of assumptions and nor can a duplication in the assumptions be removed. It is in this sense that linear logic is a “resource conscious” logic. As a consequence of dropping (1) the two rules, (2), become two separate right introduction rules for two fundamentally different forms of conjunction; they are written as ⊗ and & respectively. These new connectives are part of Girard’s intuitionistic linear logic, which we shall now present.

3 Proof Rules

The connectives of intuitionistic linear logic are:

⊗ tensor, with unit 1, called one,
& conjunction, with unit T, called true,
⊕ disjunction, with unit F, called false.

We take as the definition of intuitionistic linear logic the proof rules presented in [GL87, Laf88]:

Structural rules

\overline{A ⊢ A} (identity) \frac{Γ ⊢ A Δ, A ⊢ B}{Γ, Δ ⊢ B} (cut) \frac{Γ, A, B, Δ ⊢ C}{Γ, B, A, Δ ⊢ C} (exchange)

Logical rules

\frac{Γ ⊢ A Δ ⊢ B}{Γ, Δ ⊢ A ⊗ B} (⊢⊗) \frac{Γ, A, B ⊢ C}{Γ, A ⊗ B ⊢ C} (⊗⊢) \frac{Γ ⊢ A}{Γ, 1 ⊢ A}  \overline{⊢ 1}
\frac{Γ ⊢ A Γ ⊢ B}{Γ ⊢ A & B} (⊢&) \frac{Γ, A ⊢ C}{Γ, A & B ⊢ C} (l&⊢) \frac{Γ, B ⊢ C}{Γ, A & B ⊢ C} (r&⊢)  \overline{Γ ⊢ T}
\frac{Γ ⊢ A}{Γ ⊢ A ⊕ B} (⊢⊕l) \frac{Γ ⊢ B}{Γ ⊢ A ⊕ B} (⊢⊕r) \frac{Γ, A ⊢ C Γ, B ⊢ C}{Γ, A ⊕ B ⊢ C} (⊕⊢) \overline{Γ, F ⊢ A}
\frac{Γ, A ⊢ B}{Γ ⊢ A ⊸ B} (⊢⊸) \frac{Γ ⊢ A Δ, B ⊢ C}{Γ, Δ, A ⊸ B ⊢ C} (⊸⊢)

As an example of a proof, we can derive the rule \frac{Γ ⊢ A ⊸ B}{Γ, A ⊢ B} from (⊸⊢) by

\frac{Γ ⊢ A ⊸ B \frac{_{\overline{A ⊢ A} \overline{B ⊢ B}}}{A, A ⊸ B ⊢ B}}{Γ, A ⊢ B} .

The absence of the rules for thinning and contraction is compensated, to some extent, by the addition of the logical operator “of course”. In [GL87, Laf88] this operator is presented with the following proof rules (stronger than those in [Gir87]):

“Of course” rules

\overline{!A ⊢ A} \overline{!A ⊢ 1} \overline{!A ⊢ !A ⊗!A}  (3)

\frac{B ⊢ A B ⊢ 1 B ⊢ B ⊗ B}{B ⊢ !A}  (4)

Given a proposition A, the assertion of !A has the possibility of being instantiated by the proposition A, the unit 1 or !A⊗!A, and thus of arbitrarily many assertions of !A.

How this operator compensates for the absence of the two structural rules can be seen from the (weaker) derived rules Girard originally presented in [Gir87]

\frac{Γ, A ⊢ B}{Γ,!A ⊢ B} \frac{Γ ⊢ B}{Γ,!A ⊢ B} \frac{Γ,!A,!A ⊢ B}{Γ,!A ⊢ B}  (5)

and

\frac{!Γ ⊢ B}{!Γ ⊢ !B}  (6)

where !Γ is a shorthand for !A_{1}, …,!A_{n} when Γ = A_{1}, …, A_{n}.

Once a logical constant, ⊥, denoting linear-absurdity is fixed on, linear negation (not to be mistaken for intuitionistic negation) is derivable:

A^{⊥} = A ⊸ ⊥ .

We end the section by showing that the original “of course” rules indeed are derivable.

(5) is derived from (3) as follows

\frac{_{\overline{!A ⊢ A} Γ, A ⊢ B}}{Γ,!A ⊢ A} \frac{\overline{!A ⊢ 1} \frac{Γ ⊢ B}{Γ, 1 ⊢ B}}{Γ,!A ⊢ B} \frac{!A ⊢ !A ⊗!A \frac{Γ,!A,!A ⊢ B}{Γ,!A ⊗!A ⊢ B}}{Γ,!A ⊢ B}

leaving out use of the exchange rule. (6) is however not so directly derivable from (4). At first we derive

\frac{!A ⊢ B}{!A ⊢ !B}  and  \frac{A ⊢ B}{!A ⊢ !B}  (7)

from (4) by

\frac{_{!A ⊢ B \overline{!A ⊢ 1} \overline{!A ⊢ !A ⊗!A}}}{!A ⊢ !B}  and  \frac{\frac{_{\overline{!A ⊢ A} A ⊢ B}}{!A ⊢ B}}{!A ⊢ !B} .

We are then in a position to derive

!(A & B) ⊣⊢ !A ⊗!B

where A ⊣⊢ B means A ⊢ B and B ⊢ A are provable. Using (4) the first proof is

\frac{\frac{\frac{_{\overline{!A ⊢ A} \overline{!B ⊢ 1}}}{!A ⊗!B ⊢ A ⊗ 1}}{!A ⊗!B ⊢ A} \frac{\frac{_{\overline{!A ⊢ 1} \overline{!B ⊢ B}}}{!A ⊗!B ⊢ 1 ⊗ B}}{!A ⊗!B ⊢ B}}{!A ⊗!B ⊢ A & B} \frac{\frac{_{\overline{!A ⊢ 1} \overline{!B ⊢ 1}}}{!A ⊗!B ⊢ 1 ⊗ 1}}{!A ⊗!B ⊢ 1} \frac{\frac{_{\overline{!A ⊢ !A ⊗!A}  \overline{!B ⊢ !B ⊗!B}}}{!A ⊗!B ⊢ (!A ⊗!A) ⊗ (!B ⊗!B)}}{!A ⊗!B ⊢ (!A ⊗!B) ⊗ (!A ⊗!B)}

and the other proof follows from the second rule of (7) by:

\frac{\overline{!(A & B) ⊢ !(A & B) ⊗!(A & B)} \frac{\frac{\frac{\frac{\overline{A ⊢ A}}{A & B ⊢ A}}{!(A & B) ⊢ !A} \frac{\frac{\overline{B ⊢ B}}{A & B ⊢ B}}{!(A & B) ⊢ !B}}{!(A & B),!(A & B) ⊢ !A ⊗!B}}{!(A & B) ⊗!(A & B) ⊢ !A ⊗!B}}{!(A & B) ⊢ !A ⊗!B} .

!A ⊗!B ⊢ !(A & B)

Next from the inductively derivable proof rules

\frac{Γ ⊢ B}{⨂ Γ ⊢ B}  \frac{⨂ Γ ⊢ B}{Γ ⊢ B}

we get

!(& Γ) ⊣⊢ ⨂!Γ

where for Γ = A_{1}, …, A_{n}, ⨂ Γ means A_{1} ⊗ … ⊗ A_{n} and similarly for & Γ. With this we then obtain (6) from the first rule of (7).

Exercise 1 Show the following:

(i) \frac{Γ ⊢ A & B}{Γ ⊢ A} and \frac{Γ, A ⊗ B ⊢ C}{Γ, A, B ⊢ C}

(ii) (A ⊕ B) ⊸ C ⊢ (A ⊸ C) & (B ⊸ C)

(iii) A ⊗ (B ⊕ C) ⊣⊢ (A ⊗ B) ⊕ (A ⊗ C) □

4 Quantale Interpretation

We have just seen the proof rules of intuitionistic linear logic. What are its models? As recognised by several people [AV88, Yet, Ros89, Sam], quantales^{2} provide an algebraic semantics for intuitionistic linear logic. Quantales are to intuitionistic linear logic as complete Heyting algebras are to intuitionistic logic. A quantale is a commutative monoid on a complete join semilattice. Spelled out:

Definition 2 A quantale Q is a complete join semilattice (i.e. a partial order with an operation forming joins of arbitrary sets) together with an associative, commutative, binary operation ⊗ and constant 1 such that

\begin{matrix}q ⊗ 1 = q \\ q ⊗ ⋁ P = ⋁\{q ⊗ p | p ∈ P \} \end{matrix} □

Entailment is interpreted as the order relation, ≤, on the underlying lattice of a quantale. The logical operation, ⊗, is interpreted by the corresponding binary operation in the quantale and the logical constant 1 is interpreted as 1 in the quantale. The disjunction, ⊕, of linear logic is understood as binary join and the conjunction, &, as binary meet. The logical constants T and F are interpreted as the top and bottom element respectively of the complete lattice. Linear implication is a derived operation

p ⊸ q =^{def} ⋁{r | r ⊗ p ≤ q}

2As originally defined, quantales need not be commutative and should satisfy the idempotency law q ⊗ q = q. We shall take quantales to be commutative and relax the idempotency law.

with respect to a quantale. The definition is analogous to that of implication on a complete Heyting algebra, but this time w.r.t. ⊗ in place of ∧. The definition of linear implication ensures the adjunction:

r ⊗ p ≤ q iff r ≤ p ⊸ q .

With respect to a quantale, and interpretations of the atomic propositions as elements of a quantale, we can inductively associate a proposition A in linear logic with its denotation as a quantale element [[A]]. An entailment

A_{1}, …, A_{n} ⊧ A

holds in the quantale iff

[[A_{1}]] ⊗ ⋯ ⊗ [[A_{n}]] ≤ [[A]] .

The special case where n = 0 is allowed, in which case the situation amounts to

⊧ A iff 1 ≤ [[A]] .

It is a routine matter to check that each rule is sound with respect to this interpretation. For example the right and left introduction rules for disjunction, ⊕, and conjunction, &, express that they are the join and meet with respect to entailment while the rules for linear implication express the adjunction which characterise it (with the help of the little proof given as an example in section 2). In this way it can be seen that, with respect to a quantale:

Theorem 3 If ⊢ A then ⊧ A.

We have so far ignored the treatment of !A. The rules of (3) for !A are interderivable with the following single rule:

\overline{!A ⊢ 1 & A & (!A ⊗!A)}

So, as an interpretation of !q, for an element q of a quantale, we require an element x such that

x ≤ 1 & q & (x ⊗ x) .  (8)

This will not in general characterise a unique value of the quantale; for instance taking x to be the bottom element of the lattice will always do. However from (4) it follows that any x satisfying (8) should be below !q, and hence !q should be the greatest postfixed point, and so fixed point, of

x ↦ 1 & q & (x ⊗ x)

in the complete lattice given together with the quantale. Such a solution ensures the soundness of the proof rules extended by those for !A.

Another operation is that of linear negation. Its semantics with respect to a quantale is determined by a choice for the denotation of ⊥. Then A^{⊥} is understood as A ⊸ ⊥. In this abstract set-up, for a general quantale we cannot hope to say much more. However, in a moment, when considering quantales got from a Petri net, a special element will be proposed as being useful. We can observe, following Abramsky and Vickers [AV88], that from a choice for ⊥ in a quantale, we can obtain a model of classical linear logic. The key feature of the classical version is that linear negation is an involution. With respect to an element ⊥ of a quantale Q, write q^{⊥} for q ⊸ ⊥. We cannot expect q = q^{⊥⊥} to hold for a general quantale. However, the image of the map (−)^{⊥⊥} : Q → Q is a subquantale of Q on which (−)^{⊥} is involutive, so forming a model of classical linear logic.

Exercise 4

1. Show that ⊗ is monotonic (recall p ≤ q ⇔ p ∨ q = q).

2. Prove the adjunction r ⊗ p ≤ q iff r ≤ p ⊸ q.

□

5 Petri Nets

Petri nets are a model of processes (or systems) in terms of types of resources, represented by places which can hold to arbitrary nonnegative multiplicity, and how those resources are consumed or produced by actions, represented by transitions. They are described using the notation of multisets.

A multiset over a set P is a function, M : P ⟶ IN. We shall henceforth only be concerned with finite multisets, i.e. {a ∈ P | M(a) ≠ 0} finite. With addition, +, of multisets defined by (M + M′)(a) = M(a) + M′(a) for all a ∈ P, multisets over P form a (free) commutative monoid with \underline{0} (∀a ∈ P. \underline{0}(a) = 0), the empty multiset, as unit. An element a of P can be turned into the singleton multiset with multiplicity 1 at a and 0 elsewhere. Observe that multisets are partially ordered by M ≤ M′ iff ∀a ∈ P. M(a) ≤ M′(a). For n ∈ IN and M a multiset, the scalar multiplication nM is defined by (nM)(a) = n · M(a).

We take a Petri net N to consist of (P, T,^{•}(−), (−)^{•}), where P, a set of places, and T, a set of transitions, are accompanied by maps ^{•}(−), (−)^{•} on transitions T which for each t ∈ T give a multiset of P, called the pre- and post (multi)set of t respectively. For the moment there are none of the usual restrictions on the net, such as absence of isolated elements, and in particular transitions with empty pre sets and/or post sets will be allowed. And we are actually considering nets with unconstrained capacity.

A Petri net possesses a notion of state, intuitively corresponding to a finite distribution of resources, formalized in the definition of a marking. A marking of N will simply be a finite multiset over P. We use M to denote the set of markings of the net, understood from the context. Sometimes nets are associated with an initial marking M_{0}. The behaviour of a net is expressed by saying how markings change as transitions occur (or fire). For markings, M, M′, and a transition t ∈ T, M [t⟩ M′ stands for t fires from M to M′; that is the firing relation [t⟩ is given by

M [t⟩ M′ iff ∃M′′ ∈ M. M = M′′ +^{•}t and t^{•} + M′′ = M′ .

So t is enabled at M if there is an M′ ∈ M such that M [t⟩ M′. We shall write M → M′ for the reachability relation, the reflexive and transitive closure of the firing relations.^{3}

\begin{aligned}M → M′ iff & ∃t_{1}, …, t_{n} ∈ T, M_{1}, …, M_{n} ∈ M, n ≥ 0. \\ & M [t_{1}⟩ M_{1} ⋯ [t_{n}⟩ M_{n} = M′ \end{aligned}

The markings, [M⟩, forwards reachable from M form the set {M′ ∈ M | M → M′}. We shall use ↓M to denote the set of markings which can reach M. We will generally call this set the downwards closure of M. It is defined by ↓M = {M′ ∈ M | M′ → M}. We shall also use this notation, extended pointwise, on sets of markings H, taking e.g. ↓H = {M′ | ∃M ∈ H. M′ → M}.

Petri nets can be presented by using the well-known graphical notation, which will be used throughout this paper. Places are represented by circles, transitions as squares, and arcs of appropriate multiplicities used to indicate the pre and post sets. The formal definitions can then be brought to life in the so called “token game” where markings are visualised as consisting of a distribution of tokens over places; the number of tokens residing on a place expresses the multiplicity to which it holds according to the marking. The tokens are consumed and produced as transitions occur. A basic reference for Petri nets is [Rei85].

Since we are dealing with place/transition nets without capacities we have the following proposition which is crucial for the net semantics of linear logic in the sequel.

Proposition 5 For any M, M′, M′′ ∈ M we have:

M → M′ implies M + M′′ → M′ + M′′ .

3Because we shall be chiefly concerned with the reachability relation between markings, we can get by with single steps in the firing relation, and ignore the variant in which transitions can fire concurrently.

6 Quantales from Petri-Nets

From a given net N, and associated markings and reachability relation M, → a quantale, Q, can be constructed. Its elements are to be the downwards closed subsets of markings; a subset H of M is downwards closed iff it satisfies

M′ → M and M ∈ H implies M′ ∈ H .

The set Q is ordered by inclusion, ⊆. With respect to inclusion, it is easy to see that union and intersection form the join and meet operations. The binary operation ⊗ has as unit element: 1 = ↓\underline{0}. For p, q ∈ Q the binary operation ⊗ is defined by:

p ⊗ q = ↓(p + q), where p + q = {M_{p} + M_{q} | M_{p} ∈ p, M_{q} ∈ q} .

Thus

p ⊗ q = {M | ∃M_{p} ∈ p, M_{q} ∈ q. M → M_{p} + M_{q}} .

The downwards closure, ↓, in the definition of ⊗ above is needed to make ⊗ well-defined as can be seen from this net:

[figure: a; b; c]

Clearly ↓\underline{b} + ↓\underline{c} = \{M\} ≠ \{\underline{a}, M\} = ↓\{M\}, where M = \underline{b} + \underline{c}.

That Q is indeed a commutative quantale follows from the commutativity of + and the fact that for p ∈ Q, and Q ⊆ Q:

\begin{aligned}p ⊗ ⋃ Q & = ↓(p + ⋃ Q) = ↓(⋃\{p + q | q ∈ Q\}) \\ & = ⋃\{↓(p + q) | q ∈ Q\} = ⋃\{p ⊗ q | q ∈ Q\} . \end{aligned}

Defining p ⊸ q = ⋃{r | r ⊗ p ⊆ q} we can simplify it to

p ⊸ q = {M | ∀M_{p} ∈ p. M + M_{p} ∈ q} .

This is because

M ∈ p ⊸ q
iff ∃r. M ∈ r, r ⊗ p ⊆ q
iff ↓M ⊗ p ⊆ q,  as ↓M ∈ Q and
M ∈ r ⇒ ↓M ⊆ r
iff ∀M′ ∈ ↓M, M_{p} ∈ p. M′ + M_{p} ∈ q, as q is downwards closed
iff ∀M_{p} ∈ p. M + M_{p} ∈ q

where the “if ” of the last equivalence follows from the downwards closure of q and M′ ∈ ↓M ⇒ M′ → M ⇒ M′ + M_{p} → M + M_{p} ⇒ M′ + M_{p} ∈ ↓(M + M_{p}).

7 Petri-Net Interpretation

In order to fix an interpretation of linear logic in a net we just need an interpretation of the atomic propositions as elements of the associated quantale. For simplicity we consider a linear logic language where the atomic propositions a name singleton multisets of places \underline{a}, not necessarily injectively. The net, together with the naming function, we call a net valuation. Formulae are given by:

A ::= T | F | 1  constants
| a  atomic propositions
| A ⊗ A | A ⊸ A multiplicative connectives
| A & A | A ⊕ A additive connectives

We make the choice of interpreting an atomic proposition as the downwards closure of the associated place, but we could just as well have used the downwards closure of some marking without altering our results. This choice is consistent with the following intuitive understanding: the denotation of an assertion is to be thought of as the set of requirements sufficient to establish it.

With respect to a net valuation N, linear logic formulae are interpreted as follows:

\begin{matrix}[[T]]_{N}  = & M \\ [[F]]_{N}  = & ∅ \\ [[1]]_{N}  = & \{M | M → \underline{0}\} \\ [[a]]_{N}  = & \{M | M → \underline{a}\} \\ [[A ⊗ B]]_{N} = & \{M | ∃M_{A} ∈ [[A]]_{N}, M_{B} ∈ [[B]]_{N}. M → M_{A} + M_{B}\} \\ [[A ⊸ B]]_{N} = & \{M | ∀M_{A} ∈ [[A]]_{N}. M + M_{A} ∈ [[B]]_{N}\} \\ [[A & B]]_{N} = & [[A]]_{N} ∩ [[B]]_{N} \\ [[A ⊕ B]]_{N} = & [[A]]_{N} ∪ [[B]]_{N} \end{matrix}

The semantics of [Bro89] is similar, but somehow dual to that here.

Because of the interpretation of 1 validity of an assertion A for the given net valuation, N, can be expressed by:

⊧_{N} A iff \underline{0} ∈ [[A]]_{N} .

Semantic entailment between assertions A and B amounts to:

A ⊧_{N} B iff [[A]]_{N} ⊆ [[B]]_{N} .

Because of the interpretation of linear implication, this is equivalent to

⊧_{N} A ⊸ B .

For Γ = A_{1}, …, A_{n} denote A_{1} ⊗⋯⊗A_{n} by ⨂ Γ. We write Γ ⊧_{N} B for ⨂ Γ ⊧_{N} B. General validity, ⊧ A, of an assertion A is defined by

⊧ A iff ⊧_{N} A, for every net valuation N

and with respect to entailment: Γ ⊧ B iff Γ ⊧_{N} B, for every net valuation N.

As a special case that quantale semantics is sound, we have the soundness result:

Theorem 6 If Γ ⊢ A then Γ ⊧ A.

So we see that with respect to a Petri net, an assertion A is denotes a set of markings [[A]]_{N}. As we have discussed, a marking of net can be viewed as a distribution of resources. When M ∈ [[A]]_{N} we can think of the marking M as a distribution of resources sufficient to establish A according to the net; in this sense the marking M is one of the (in general many) requirements sufficient to establish A. The meaning of an assertion A is specified by saying what requirements are sufficient to establish it—this is the content of the denotation [[A]]_{N}. Accordingly, a net satisfies an assertion A when \underline{0} ∈ [[A]]_{N}, expressing that A can be established with no resources.

This reading squares with the fact that assertions denote subsets of markings which are downwards closed with respect to the reachability relation of the net; if M ∈ [[A]]_{N}, so M is a requirement sufficient to establish A, and M′ → M so we can obtain M for M′, then so also is M′ a sufficient requirement of A. Casting an eye over the definition of the semantics of assertions we can read, for example, the definition of [[a]]_{N}, for an atom a, as expressing that a sufficient requirement of a is any marking from which the marking \underline{a} can be reached according to the net. Similarly, the sufficient requirements of A & B are precisely those which are sufficient requirements of both A and of B. An element of [[A ⊸ B]]_{N} can be seen as what is required, in addition to any requirement of A, in order to establish B. There are similar restatements of the semantics for the other connectives as well.

This understanding should be born in mind when considering the examples that follow, where we shall make use of the fact that ⊗, & and ⊕ are associative and assume the precedence:

⊸ < &, ⊕ < ⊗ .

Examples Consider the net:

N_{1} = [figure: d; a; b; e; c]

Here we have [[b]]_{N_{1}} = \{\underline{d}, \underline{a}, \underline{b}\}, …, [[c]]_{N_{1}} = \{\underline{a}, \underline{c}\} and [[b ⊗ c]]_{N_{1}} = \{\underline{d} + \underline{a}, \underline{d} + \underline{c}, \underline{a} + \underline{a}, \underline{a} + \underline{c}, \underline{b} + \underline{a}, \underline{b} + \underline{c}\}, so consequently

[[d ⊗ a]]_{N_{1}} ⊆ [[b ⊗ c]]_{N_{1}} or equivalently ⊧_{N_{1}} d ⊗ a ⊸ b ⊗ c
⊧_{N_{1}} a ⊗ a ⊸ b ⊗ c
⊧_{N_{1}} a ⊸ b ⊕ c, ⊧_{N_{1}} d ⊕ a ⊸ b, ⊧_{N_{1}} d ⊸ b ⊕ c
⊧_{N_{1}} b & c ⊸ e, ⊧_{N_{1}} a ⊸ b & c .

The most difficult connective to comprehend is probably linear implication so we give a few more examples here. For the nets

N_{2} = [figure: a; b; c; d]  and  N_{3} = [figure: a; b; c; d; e]

we have:

[[c ⊸ d]]_{N_{2}} = ∅ and ⊧_{N_{2}} (c ⊸ d) ⊸ F
[[b ⊸ d]]_{N_{2}} = \{\underline{a}\} and ⊧_{N_{2}} (b ⊸ d) ⊸ a
[[a ⊸ e]]_{N_{3}} = \{\underline{b} + \underline{d}\} .

A more peculiar example of linear implication is given by the following net N:

[figure: a; b]

In this net [[a ⊸ a]]_{N} = \{n\underline{b} | n ∈ IN\}. Exercise 7 Determine [[d]]_{N}, [[d ⊗ e]]_{N}, [[d & e]]_{N}, [[b ⊸ d]]_{N} and [[c ⊸ d]]_{N} for:

N = [figure: a; b; c; d; e]
□

Exercise 8

(i) Construct a net N which shows that the distributivity

(A ⊗ C) & (B ⊗ C) ⊧_{N} (A & B) ⊗ C

fails. (ii) Prove that (A & B) ⊗ C ⊧ (A ⊗ C) & (B ⊗ C). (iii) Does (A & C) ⊗ (B & C) ⊧ (A ⊗ B) & C hold? (iv) What about (A ⊗ B) & C ⊧ (A & C) ⊗ (B & C)?

□

Exercise 9 Which of the following statements are true, if any?

(i) A ⊕ (B ⊗ C) ⊧ (A ⊕ B) ⊗ (A ⊕ C)

(ii) (A ⊕ B) ⊗ (A ⊕ C) ⊧ A ⊕ (B ⊗ C) □

8 Expressing Properties of Nets

Notation: For a multiset, M, of assertions of our logic, we associate the formula M̂ which when M is nonempty is given by

_{M(A)≠0}^{⨂} A^{M(A)} where A^{n} = \overbrace{A ⊗ ⋯ ⊗ A}^{n}, for n > 0

and otherwise, when M = \underline{0}, is given by the formula 1. With respect to a net valuation, for a multiset M of atoms of the logic we can write \underline{M} for the marking satisfying

\underline{M}(p) = _{\underline{a}=p}^{∑} M(a)

16 for a place p.

We let the context distinguish M, and its understanding as M̂ and \underline{M}, except for a few crucial statements and proofs.

We can then express that one marking is reachable in a net N:

Proposition 10 For any multisets of atoms M and M′,

M → M′ in the net N iff ⊧_{N} M ⊸ M′ .

Proof Simply note that M → M′ in N iff ↓M ⊆ ↓M′ iff [[M]]_{N} ⊆ [[M′]]_{N} iff ⊧_{N} M ⊸ M′. □

Before reading the list of sample properties below observe:

[[M ⊗ T]]_{N} = ↓{M′ | M′ ≥ M} .

Sample Properties

Suppose a net N with initial marking M_{0}.

• From the initial marking it is possible to reach a marking where a is marked: ⊧_{N} M_{0} ⊸ a ⊗ T.

• From the initial marking it is possible to reach a marking where a place, a, of S ⊆^{fin} P is marked: ⊧_{N} M_{0} ⊸ (⨁_{a∈S} a) ⊗ T.

• Once a is marked it is possible to reach a marking where b is marked: ⊧_{N} a ⊗ T ⊸ b ⊗ T.

• Once a is marked either b or c can become marked (but we do not know which): ⊧_{N} a ⊗ T ⊸ (b ⊕ c) ⊗ T.

• Once a is marked both b and c can become marked (but not necessarily simultaneously): ⊧_{N} a ⊗ T ⊸ (b & c) ⊗ T.

Example 11 (Mutual exclusion) Consider the net N:

[figure: c_{1}; p_{1}; w_{1}; a; b; w_{2}; p_{2}; c_{2}]

where the marking of the place w_{1} indicates that the first process, p_{1}, is working outside its critical region, c_{1}, and similarly for the other process, p_{2}. The resource corresponding to b is used to ensure mutual exclusion of the critical regions and after a process has been in its critical region it returns a resource, a, which then is prepared (transformed into b) for the next turn. The initial marking, M_{0}, will be M_{0} = b_{0} ⊗w_{1} ⊗w_{2}. We can now express that e.g. p_{1} can enter its critical region (from the initial marking) by: ⊧_{N} M_{0}⊸c_{1}⊗T. However this does not ensure that no undesired tokens are present, so it is better to express it: ⊧_{N} M_{0} ⊸ c_{1} ⊗ w_{2}. If the system is in a “working state” then both processes have the possibility of entering their critical section: ⊧_{N} w_{1} ⊗ (a ⊕ b) ⊗ w_{2} ⊸ c_{1} ⊗ w_{2} & w_{1} ⊗ c_{2}. The property, that when p_{1} is in its critical section and p_{2} is working it is possible that p_{2} can later come into its critical section with p_{1} working, is expressed by: ⊧_{N} c_{1} ⊗ w_{2} ⊸ w_{1} ⊗ c_{2}. Similar other “positive” properties can be expressed. Shortly we shall see how to express the “negative” property that both processes cannot be in their critical regions at the same time.

Exercise 12 Let N be the net of example 11.

(i) Which of the following statements are true?

⊧_{N} (c_{1} ⊸ w_{1}) ⊸ F, ⊧_{N} (w_{1} ⊸ c_{1}) ⊸ F, ⊧_{N} (M_{0} ⊸ c_{1} ⊗ c_{2}) ⊸ F

(ii) A new proof system for the net N can be obtained by adding to the proof

rules an axiom ^{ ˆ•}t ⊢ t̂^{•} for each transition t in the net, e.g. \overline{w_{1} ⊗ b ⊢ c_{1}.}

Prove ⊢ w_{1} ⊗ (a ⊕ b) ⊗ w_{2} ⊸ c_{1} ⊗ w_{2} in this new proof system.

□

Exercise 13 Consider the following net N_{V} describing a vending machine for cheap hot drinks:

[figure: (Coffee); (Tea); 2; 2; 3; t; c; k; f; 3; 3; 2; (five pence); a; (a penny); (Chocolate)]

Express in linear logic the following statements and consider in what way the statements are made more precise.

(i) For 2 pence one can get a cup of coffee, tea or chocolate.

(ii) For 2 pence one can get a cup of coffee and a cup of tea.

(iii) For five pence one can get a cup of coffee and in addition a cup of tea as well as a penny back.

(iv) If one has a penny and a part from that sufficient mony to get both tea and coffee then one can also get chocolate.

(v) Think of more yourself.

□

9 The “Of Course” Operator

From the discussion in section 4 it immediately follows how to interpret an “of course” formula:

Definition 14 Given a net N with associated quantale Q and a formula A, the interpretation of “of course” A, is

[[!A]]_{N} = ⋃{q ∈ Q | q is a postfixed point of f_{A}}

where f_{A} : Q ⟶ Q is the function given by:

x ↦ [[1]]_{N} ∩ [[A]]_{N} ∩ (x ⊗ x)  (9)
□

In order to gain a better understanding of the “of course” operator we give the following characterisation of a postfixed point.

Proposition 15 q ∈ Q is a post fixed point of (9) iff there exists an H ⊆ M such that

(i) q = ↓H

(ii) H ⊆ [[A]]_{N}

(iii) ∀M ∈ H. M → \underline{0}

(iv) ∀M ∈ H∃M′, M′′ ∈ H. M → M′ + M′′ .

Proof if : ↓H = q a postfixed point of (9) means q ⊆ 1 ∩ [[A]]_{N} ∩ (q ⊗ q). From (iii) follows q = ↓H ⊆ ↓\underline{0} = 1 and from (ii) q = ↓H ⊆ ↓[[A]]_{N} = [[A]]_{N} as [[A]]_{N} is downwards closed. To see q ⊆ q ⊗ q assume M ∈ q. Then ∃M′′′ ∈ H. M → M′′′ and so by iv) ∃M′, M′′ ∈ H. M′′′ → M′ + M′′. Transitivity of → then gives M ∈ ↓(H + H) = H ⊗ H ⊆ ↓H ⊗ ↓H = q ⊗ q.

only if : Take H = q and we have ↓H = H. Properties (i) – (iii) follows readily as does (iv) by q ⊆ q ⊗ q and the downwards closure of H. □

In the light of this proposition, we can see a requirement of !A as any requirement of A which can both vanish and duplicate into any number of additional requirements of !A.

Example 16 For the net N:

[figure: b; a]

we get: [[b]]_{N} = \{\underline{b}\} ∪ \{n\underline{a} | n > 0\} which properly contains [[!b]]_{N} = \{n\underline{a} | n > 0\}.

10 Linear Negation

We have discovered that in a net N one useful interpretation of the extra logical constant ⊥, for linear-absurdity, is:

[[⊥]]_{N} = \{M | \underline{0} ↛ M in N\} .

That is ⊥ denotes exactly the set of markings which cannot be reached from the empty marking. For [[⊥]]_{N} to be well-defined, we need that it is downwards-closed: To see this, suppose M′ → M for M ∈ [[⊥]]_{N}. Assume M′ ∉ [[⊥]]_{N}. Then \underline{0} → M′, whence from M′ → M and transitivity of → we conclude \underline{0} → M—contradicting M ∈ [[⊥]]_{N}.

Since linear negation can be expressed in terms of ⊥ and ⊸ (by A^{⊥} = A ⊸ ⊥), we get:

[[A^{⊥}]]_{N} = \{M | ∀M_{A} ∈ [[A]]_{N}. \underline{0} ↛ M_{A} + M\} .

The interesting consequence of this particular choice for ⊥ is, that whatever property we could state before in terms of validity of a formula A can now be stated negatively as ⊧_{N} A^{⊥}. Formally:

Proposition 17

⊧_{N} A^{⊥} iff |̸=_{N} A  (10)

Proof Immediate from: |̸=_{N} A^{⊥} iff |̸=_{N} A⊸⊥ iff [[A]]_{N} ⊈ [[⊥]]_{N} iff [[A]]_{N} ⊈ {M | \underline{0} ↛ M in N\} iff ∃M_{A} ∈ [[A]]_{N}. \underline{0} → M_{A} iff \underline{0} ∈ [[A]]_{N} iff ⊧_{N} A, where the second last equivalence follows from the downwards closure of [[A]]_{N}. □

Clearly \{M | \underline{0} ↛ M in N\} is the largest element which can be used for the interpretation of ⊥ should (10) hold. Suppose on the contrary M ∈ [[⊥]]_{N} and M ∉ \{M | \underline{0} ↛ M in N\}. Then \underline{0} → M and so ⊧_{N} ⊥ but also ⊧_{N} ⊥^{⊥}.

If furthermore each place is named by some atomic proposition then (10) uniquely determines the interpretation of ⊥. To see this notice that each marking is then denotable and that

\underline{M} ∈ [[⊥]]_{N} iff M̂ ⊧_{N} ⊥
iff ⊧_{N} M̂ ⊸ ⊥
iff ⊧_{N} M̂^{⊥}
iff |̸=_{N} M̂ by (10)
iff \underline{0} ↛ \underline{M} in N

Combining proposition 17 with proposition 10 we can express that a marking M′ cannot be reached from another M:

Corollary 18 For markings M and M′:

M ↛ M′ iff ⊧_{N} (M ⊸ M′)^{⊥} .

Example 11 (continued) We can now express that the processes, p_{1} and p_{2} cannot get into their critical regions at the same time. We might try ⊧_{N} (M_{0} ⊸ c_{1} ⊗ c_{2})^{⊥}. This is not quite right however, since ⊧_{N} (M_{0} ⊸ c_{1} ⊗ c_{2})^{⊥} merely states that the two processes cannot be in their critical regions at the same time when no other tokens are present; the correct statement is ⊧_{N} (M_{0} ⊸ c_{1} ⊗ c_{2} ⊗ T)^{⊥}.

Sample Properties

Suppose a net N.

• There is a marking with a marked such that b will never be marked in any

reachable marking:

⊧_{N} (a ⊗ T ⊸ b ⊗ T)^{⊥} .

• For any marking obtained from M the load on the place a cannot exceed n ∈ IN, i.e. with M = M_{0} this means that a is n-safe:

⊧_{N} (M ⊸ a^{n+1} ⊗ T)^{⊥} .

Suppose on the contrary ∃M′.M → M′ and M′(\underline{a}) > n; that is M′ ≥ (n+1)\underline{a}. Then M′ belongs to [[a_{N}^{n+1} ⊗ T]] which is downwards closed and so M ∈ [[a^{n+1}⊗T]]_{N} wherefore ⊧_{N} M⊸a^{n+1}⊗T—contradicting ⊧_{N} (M⊸a^{n+1}⊗T)^{⊥}.

• That a transition t is M-dead in a net N, i.e. ∀M′ ∈ [M⟩. M′ [t⟩, is expressed

by: ⊧_{N} (M ⊸^{•}t ⊗ T)^{⊥} .

• If N only have finitely many places, we can express safeness, i.e. ∀M ∈[M_{0}⟩ ∀a ∈ P. M(a) ≤ 1 (N is 1-safe):

⊧_{N} (M_{0} ⊸ (_{a∈P}^{⨁} a ⊗ a) ⊗ T)^{⊥} .

Again suppose on the contrary ∃M′∃a. M_{0} → M′ and M′(a) > 1. Then M′ ∈ [[(⨁_{a∈P} a⊗a)⊗T]]_{N} and so ⊧_{N} M_{0}⊸(⨁_{a∈P} a⊗a)⊗T—a contradiction.

This definition of linear negation actually allows us to state any propositional combination of validity of linear formulae simply as the validity of a single formula. Abbreviating in a formula A^{⊥} ⊕ B by A ⇒ B we can read ⇒ as implication, ⊕ as disjunction etc. For example:

if b can be reached from a then so can c:

⊧_{N} a ⊸ b implies ⊧_{N} a ⊸ c

can be expressed by a single formula:

⊧_{N} (a ⊸ b) ⇒ (a ⊸ c)

Exercise 19 Formulate the following statement in linear logic.

If it is possible to reach b from a in the net then c can be reached as well. □

It follows from the remarks of section 4 that by denoting a proposition A by [[A]]_{N}^{⊥⊥} we obtain a Petri-net semantics of classical linear logic. In general it is hard to get an impression of [[A]]_{N}^{⊥⊥}, but by slightly narrowing the class of nets we consider to those whose transitions always have a nonempty preset, i.e. \underline{0} ≠ ^{•}t for all transitions t, we get:

[[A]]_{N}^{⊥⊥} = \begin{cases}[[T]]_{N} & if ⊧_{N} A \\ [[F]]_{N} & otherwise . \end{cases}  (11)

To see this notice first for each net we have [[⊥]]_{N} = \{M | M ≠ \underline{0}\} = M \ \{\underline{0}\} and so

q^{⊥} = \{M | ∀M_{q} ∈ q. M + M_{q} ≠ \underline{0}\}
= M \ \{M | ∃M_{q} ∈ q. M + M_{q} = \underline{0}\}
= \begin{cases}M \ \{\underline{0}\} & if \underline{0} ∈ q \\ M & otherwise . \end{cases}

22 from which (11) follows. It also follows that the image of the map (−)^{⊥⊥} forms a 2-element quantale where the logical operations act as the usual operations of propositional logic, and ⊗ acts like &. In this quantale all the atomic propositions would have the same interpretation as F and ⊥. Such a classical interpretation seems of limited interest.

11 Recursion

Though we now have the possibility to use linear negation to express properties of a net it is hard to express properties such as:

From the initial marking it is possible to reach a marking where just a is marked (to arbitrary multiplicity).

One way to increase the power of the logic language is to extend it with the possibility of writing recursive formulae using least (μ) and greatest (ν) fixpoint operators on assertions.

With their aid we can define propositions a^{+} and a^{∗}. Abbreviating μx. a ⊕ (a ⊗ x) by a^{+} and 1 ⊕ a^{+} by a^{∗} we have:

\begin{matrix}M ∈ [[a^{+}]] iff & ∃n > 0. M → n\underline{a} \\ M ∈ [[a^{∗}]] iff & ∃n ≥ 0. M → n\underline{a} \end{matrix}

Clearly the “of course” operator can be expressed as a maximum fixed point: !A = νx. A & 1 & x ⊗ x.

Sample Properties

Suppose a net N.

• From the initial marking it is possible to reach a marking where just a is marked: ⊧_{N} M_{0} ⊸ a^{+}.

• From the marking M it is possible in a finite net to reach a marking with a marked and b unmarked: ⊧_{N} M ⊸ a^{+} ⊗ (⨂_{c∈P \{a,b}} c^{∗}).

• The places of S ⊆^{fin} P can always be emptied of tokens: ⊧_{N} T ⊸ ⨂_{a∈P \S} a^{∗}.

Another possible extension is to add second order quantifiers with variables ranging over elements of the quantale, or quantifiers with variables over markings, for example; they can be understood as special kinds of meet and join operations. We introduce a restricted form of second-order quantification in section 14.

12 Equivalences on Nets

Linear logic induces an equivalence relation between nets having the same set of places. With respect to a set of places, we build up the propositions of a linear logic with the places as atoms. If A is such a proposition whose atoms are amongst the places of a net N we say N satisfies A, written ⊧_{N} A, iff A is valid with respect to the semantics of section 7. We say two nets N_{0}, N_{1} with the same places are equivalent if they make the same propositions valid, i.e. we define

N_{0} ∼ N_{1} iff (⊧_{N_{0}} A iff ⊧_{N_{1}} A, for all propositions A) .

A less refined equivalence can be got by taking two nets to be equivalent iff they give rise to the isomorphic quantales. The latter notion has the advantage of not depending on the nets having the same set of places. We shall concentrate on the former equivalence as it implies the latter and suffices to point out some of the idiosyncrasies of linear logic when interpreted on nets. The equivalence has a direct bearing on the suitability of linear logic as a specification language for Petri nets. If it is wished to distinguish between two nets which are equivalent, there is no hope of specifying one and not the other within pure linear logic.

Observe that because our semantics of linear logic is built on the relation →, any two nets, over a common set of places, which induce the same relation → are bound to be equivalent. This means that whenever M → M′, for a net N, we can adjoin a new transition t with the pre places M and post places M′, and still get a net equivalent to N. So, given any net N, we can add “identity” transitions at any multiset of places, “compositions” and “synchronizations” of transitions as new transitions and obtain a net equivalent to N.

Examples

Adding “identity” transitions:  [figure] ∼ [figure]

Adding “composition” transitions:  [figure] ∼ [figure]

Adding “synchronization” transitions:  [figure] ∼ [figure]

Also note that these two nets are equivalent:

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .]

where the direction of the loop has changed! (It’s easy to see both nets have the same → relation.) However, we can distinguish between different directions of looping if another place is present to act like a loop counter:

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .]

These nets are not equivalent.

Notice that whether or not the equivalence induced on nets is reasonable, if two nets are equivalent in our sense then so are they too with respect to the satisfaction relation of [MOM89]. This is because their construction of a linear category from a net factors through the construction of what they call a Petri-category. The Petri-category made from a net has objects the net’s markings and has a morphism f : M → M′ iff M → M′ in our sense. A difference with the approach of [MOM89] can be seen by considering a preorder induced by the logic rather than just equivalence. For nets with the same set of places, define

N_{0} ⪯ N_{1} iff (⊧_{N_{0}} A implies ⊧_{N_{1}} A, for all propositions A) .

The preorder induced by our definition of satisfaction will differ from theirs. In [MOM89], if a net N satisfies a formula A, in their sense, then any net obtained from N by adding an arbitrary number of new transitions will also satisfy A. This is not the case for our definition of satisfaction, as can be seen by adding transitions to the nets N_{1} and N_{2} in section 7: Take

N′_{1} = [figure: d; b; e; c; a]  and  N′_{2} = [figure: a; b; c; d]

For these nets we have |̸=_{N′_{1}} b & c ⊸ e and |̸=_{N′_{2}} (b ⊸ d) ⊸ a whereas ⊧_{N_{1}} b & c ⊸ e and ⊧_{N_{2}} (b ⊸ d) ⊸ a.

These remarks imply that proof system described in (ii) of exercise 12 does not describe a net up to ∼.

13 Elementary Completeness Results

In this section we shall be concerned with completeness results for different fragments of linear logic without exponentials.

We start by sketching the completeness proof for quantale semantics.

The idea in showing completeness is to build a quantale by taking the ideal completion of the Lindenbaum algebra. More precisely take Q to be ⊆-ordered set of subsets I of assertions of linear logic, without exponentials, such that

A ⊢ B ∈ I ⇒ A ∈ I, X ⊆^{fin} I ⇒ ⨁ X ∈ I (We understand ⨁ ∅ = F) .

The ⊗-operation on ideals is got by taking:

I ⨂ J =_{def} {C | ∃A ∈ I, B ∈ J. C ⊢ A ⊗ B} .

That this yields an ideal follows routinely: clearly I ⊗ J is closed with respect to entailment, i.e. B ⊢ C ∈ I ⊗ J implies B ∈ I ⊗ J; it is closed under ⨁ because it contains ⨁ ∅ = F and if C, C′ ∈ I ⊗ J then C ⊢ A ⊗ B and C′ ⊢ A′ ⊗ B′, for A, A′ ∈ I, B, B′ ∈ J, whence

\begin{matrix}C ⊕ C′ ⊢ & (A ⊗ B) ⊕ (A′ ⊗ B′) \\ ⊢ & (A ⊗ B) ⊕ (A′ ⊗ B) ⊕ (A ⊗ B′) ⊕ (A′ ⊗ B′) \\ ⊢ & (A ⊕ A′) ⊗ (B ⊕ B′), \end{matrix}

where (A ⊕ A′) ∈ I and (B ⊕ B′) ∈ J thus ensuring C ⊕ C′ ∈ I ⊗ J—thus it is closed under ⊕.

The quantale Q interprets assertions once we decide to interpret atoms a in the following way:

[[a]]_{Q} = {B | B ⊢ a} .

It is a relatively simple matter to show the following agreement between the semantics in the constructed quantale and the proof system:

Lemma 20 Letting A be an assertion of linear logic without exponentials,

[[A]]_{Q} = {B | B ⊢ A} .

Proof By structural induction. We consider two cases:

A ≡ A_{1} ⊕ A_{2}: The denotation [[A_{1} ⊕ A_{2}]]_{Q} = [[A_{1}]]_{Q} ∨ [[A_{2}]]_{Q}, the join in Q, which contains A_{1} ⊕ A_{2}, and hence must equal the principal ideal {B | B ⊢ A_{1} ⊕ A_{2}}.

A ≡ A_{1} ⊸ A_{2}: By definition,

[[A_{1} ⊸ A_{2}]]_{Q} = ⋁ {I | I ⨂ [[A_{1}]]_{Q} ⊆ [[A_{2}]]_{Q}}

a join in Q which contains A_{1} ⊸ A_{2} and hence includes the principal ideal {B | B ⊢ A_{1} ⊸ A_{2}}. It is in fact equal to this principal ideal. To see this, let B ∈ I where I ⨂ [[A_{1}]]_{Q} ⊆ [[A_{2}]]_{Q}. Then B ⊗A_{1} ∈ [[A_{2}]]_{Q}, so by structural induction B ⊗ A_{1} ⊢ A_{2}, whence B ⊢ A_{1} ⊸ A_{2}. □

Corollary 21 Let A be an assertion of linear logic without exponentials. Then

⊧_{Q} A iff ⊢ A .

As a corollary we from A ⊢ B iff ⊢ A ⊸ B obtain completeness with respect to quantales:

Theorem 22 For the fragment without exponentials we have:

Γ ⊧ A iff Γ ⊢ A .

In the remaining sections we shall only be concerned with completeness proofs for the net semantics.

Completeness for the ⊕-free Fragment

Restrict the syntax to the fragment:

A ::= T | 1 | a | A_{1} & A_{2} | A_{1} ⊗ A_{2} | A_{1} ⊸ A_{2}  (⊕-free)

where a ranges over atoms. For the ⊕-free fragment we construct a net N where the places are formulae and the transitions essentially correspond to the provable sequents. I.e.

• Places are assertions of (⊕-free) above. An atom will be interpreted as its singleton marking.

• Transitions are pairs (M, M′) of multisets of places for which M̂ ⊢ M̂′ with pre- and postset maps ^{•}(M, M′) = M and (M, M′)^{•} = M′.

For instance the net has the following transition

[figure: (A + A ⊸ B, B); B; A; A ⊸ B]

because A ⊗ (A ⊸ B) ⊢ B. Lemma 23 For markings M, M′ of the net N,

M → M′ in the net iff M̂ ⊢ M̂′ .

Proof “if”: It is clear by definition that if M̂ ⊢ M̂′ then M → M′ for any markings M, M′ ∈ M. “only if”: Follows by a simple inductive argument once we have established

M [t⟩ M′ implies M̂ ⊢ M̂′ .

However, if M [t⟩ M′ then, by definition, there is some M′′ ∈ M such that

M = M′′ +^{•}t and t^{•} + M′′ = M′ .

From ^{ ˆ•}t ⊢ t̂^{•} we derive M̂′′ ⊗ ^{ ˆ•}t ⊢ t̂^{•} ⊗ M̂′′. The result then follows from M̂ ⊣⊢ M̂′′ ⊗ ^{ ˆ•}t and M̂′ ⊣⊢ t̂^{•} ⊗ M̂′′. □

Lemma 24 For the ⊕-free fragment we have: [[A]]_{N} = {M | M̂ ⊢ A}.

Proof By induction on the structure of A using the previous lemma. A ≡ T: [[T]]_{N} = M = {M ∈ M | M ⊢ T} by axiom Γ ⊢ T (recall M consists of finite multisets). A ≡ 1: [[1]]_{N} = \{M ∈ M | M → \underline{0}\} = \{M ∈ M | M ⊢ ˆ \underline{0} = 1\} by lemma 23. A ≡ a: [[a]]_{N} = {M ∈ M | M → a} = {M ∈ M | M ⊢ a} by lemma 23. A ≡ A_{1}⊗A_{2}: M ∈ [[A_{1} ⊗ A_{2}]]_{N} ⇔ ∃M_{1} ∈ [[A_{1}]]_{N}, M_{2} ∈ [[A_{2}]]_{N}. M → M_{1} + M_{2} by definition, ⇔ ∃M_{1}, M_{2} ∈ M. M_{1} ⊢ A_{1}, M_{2} ⊢ A_{2} and M → M_{1} + M_{2} by induction, ⇔ ∃M_{1}, M_{2} ∈ M. M_{1} ⊢ A_{1}, M_{2} ⊢ A_{2} and M ⊢ M_{1} ⊗ M_{2} by lemma 23, ⇔ M ⊢ A_{1} ⊗ A_{2} by (⊢⊗), (⊗⊢) and (identity).

A ≡ A_{1} ⊸ A_{2}:

M ∈ [[A_{1} ⊸ A_{2}]]_{N} ⇔ ∀M_{1} ∈ [[A_{1}]]_{N}. M + M_{1} ∈ [[A_{2}]]_{N} by definition,
⇔ ∀M_{1} ∈ M. M_{1} ⊢ A_{1} ⇒ M ⊗ M_{1} ⊢ A_{2} by induction,
⇒ M ⊢ A_{1} ⊸ A_{2} by (⊢⊸) and (identity).

To see “⇐” suppose M ⊢ A_{1} ⊸ A_{2}. From (⊸⊢) we derive M, A_{1} ⊢ A_{2}. Using (cut) and M_{1} ⊢ A_{1} we then get M, M_{1} ⊢ A_{2}. A ≡ A_{1} & A_{2}: M ∈ [[A_{1} & A_{2}]]_{N} ⇔ M ∈ [[A_{1}]]_{N} and M ∈ [[A_{2}]]_{N} by definition, ⇔ M ⊢ A_{1} and M ⊢ A_{2} by induction, ⇒ M ⊢ A_{1} & A_{2} by (⊢&).

For the other direction “⇐” we by (identity) and (l&⊢) obtain A_{1} & A_{2} ⊢ A_{1} and so M ⊢ A_{1} from M ⊢ A_{1} & A_{2} and (cut). By symmetry M ⊢ A_{2}. □

Because ⊧_{N} A follows from ⊧ A, and the fragment contains implication we deduce:

Theorem 25 For the ⊕-free fragment we have:

Γ ⊧ A iff Γ ⊢ A .

As observed by Sergei Soloviev, the net need for a particular sequent only to be constructed with a finite number of places corresponding to subformulae of the sequent. However, it not clear that the net can be finite if the sequent contains & or ⊸.

Completeness for the −_{}-free Fragment

We can obtain completeness for the ⊸-free fragment of propositional intuitionistic logic. Its syntax:

A ::= T | F | 1 | a | A_{1} ⊕ A_{2} | A_{1} & A_{2} | A_{1} ⊗ A_{2}  (⊸-free)

where a ranges over atoms. With a similar construction to that in the previous section we can define a net N (this time with places in the ⊸-free fragment) to obtain a rather weak form of completeness for the ⊸-free fragment.

Lemma 26 For the ⊸-free fragment we have [[A]]_{N} ⊆ {M | M ⊢ A}.

Proof Induction on the structure of A. All the cases except A ≡ F and A ≡ A_{1}⊕ A_{2} are handled exactly as the ⊆-part of lemma 24 (notice the weaker hypothesis).

A ≡ F: Evident as [[F]]_{N} = ∅.

A ≡ A_{1} ⊕ A_{2}: M ∈ [[A_{1} ⊕ A_{2}]]_{N} ⇔ M ∈ [[A_{1}]]_{N} or M ∈ [[A_{2}]]_{N} by definition, ⇒ M ⊢ A_{1} or M ⊢ A_{2} by induction, ⇒ M ⊢ A_{1} ⊕ A_{2} by (⊢⊕l) or (⊢⊕r).

□

As a corollary we have:

Theorem 27 For the ⊸-free fragment we have:

⊧ A iff ⊢ A .

We have not used the distributive law yielded by the net semantics:

(A ⊕ B) & C ⊢ (A & C) ⊕ (B & C) (&-⊕-dist.)

With this as an additional proof rule we can obtain a stronger completeness result for the ⊸-free fragment of propositional intuitionistic logic.

To show completeness we construct a net with places (and markings) identified with assertions in the ⊕-free subfragment:

A ::= T | 1 | a | A_{1} & A_{2} | A_{1} ⊗ A_{2}  (⊸-⊕-free)

We will just call it the ⊕-free fragment in the rest of this section. Construct a net N where:

• Places are assertions in the ⊕-free fragment (atoms are to be interpreted as their singleton markings).

• Transitions are pairs (M, M′) of multisets of places for which M̂ ⊢ M̂′.

Lemma 28 For markings M, M′ of the net,

M → M′ in the net iff M, M′ ⊕-free and M ⊢ M′ in the logic.

Proof The proof is like that for lemma 23. □

Lemma 29 (Decomposition lemma). For any ⊸-free assertion A there is a finite set I indexing ⊸-⊕-free assertions M_{i}, such that

A ⊣⊢ _{i∈I}^{⨁} M_{i} .

Proof The proof proceeds by structural induction on the assertion A.

The base cases are routine; for example F ⊣⊢ ⨁ ∅ (= F by definition), i.e. falsity is interderivable with the empty disjunction. Of the remaining cases, that where A has the form A_{1}&A_{2} makes use, as is to be expected, of the additional distributivity rules for & and ⊕. Inductively, assume

A_{1} ⊣⊢ _{i∈I}^{⨁} M_{i}^{1} and A_{2} ⊣⊢ _{j∈J}^{⨁} M_{j}^{2} .

Then, from these assumptions and repeated use of &-⊕-distributivity

\begin{matrix}A_{1} & A_{2} ⊣⊢ & (⨁_{i} M_{i}^{1}) & (⨁_{j} M_{j}^{2}) \\ ⊣⊢ & ⨁_{i}(M_{i}^{1} & (⨁_{j} M_{j}^{2})) \\ ⊣⊢ & ⨁_{(i,j)∈I×J}(M_{i}^{1} & M_{j}^{2}) . \end{matrix}

The case where A has the form A_{1} ⊗ A_{2} is exactly analogous, making use instead of the standard ⊗-⊕-distributivity of linear logic. □

Lemma 30 Let Γ = B_{1}, …, B_{n}, possibly empty, be list of assumptions in the ⊕-free fragment above. Then,

Γ ⊬ F

and

if Γ ⊢ C ⊕ D then Γ ⊢ C or Γ ⊢ D .

Proof By cut-elimination any proof of a sequent can be replaced by a cut-free proof. The above lemma follows by induction or the size of cut-free proofs. □

Lemma 31 For any ⊸-free assertion A, [[A]]_{N} = {M | M is ⊕-free, M ⊢ A} .

Proof The proof proceeds by structural induction on the assertion A. A ≡ T : Clearly, [[T]]_{N} = M = {M | M ⊕-free} = {M ⊕-free | M ⊢ T}. A ≡ F : Now, using lemma 30, [[F]]_{N} = ∅ = {M | M ⊕-free, M ⊢ F}. A ≡ 1: [[1]]_{N} = \{M | M → \underline{0}\} = \{M | M ⊕-free, M ⊢ 1\} by lemma 28. A ≡ a: [[a]]_{N} = {M | M → a} = {M | M ⊕-free, M ⊢ a} by lemma 28. A ≡ A_{1} & A_{2} : We argue straightforwardly that

M ∈ [[A_{1} & A_{2}]]_{N} ⇔ M ∈ [[A_{1}]]_{N} and M ∈ [[A_{2}]]_{N} by definition,
⇔ M ⊕-free, M ⊢ A_{1} and M ⊢ A_{2} by induction,
⇔ M ⊕-free, M ⊢ A_{1} & A_{2} by the proof rules.

A ≡ A_{1} ⊕ A_{2}: Argue: M ∈ [[A_{1} ⊕ A_{2}]]_{N} ⇔ M ∈ [[A_{1}]]_{N} or M ∈ [[A_{2}]]_{N} by definition, ⇔ M ⊕-free and either M ⊢ A_{1} or M ⊢ A_{2} by induction, ⇔ M ⊕-free, M ⊢ A_{1} ⊕ A_{2} by lemma 30 and (⊢⊕).

A ≡ A_{1} ⊗ A_{2}: The proof in this case is a little more involved. Argue:

M ∈ [[A_{1} ⊗ A_{2}]]_{N} ⇔ ∃M_{1} ∈ [[A_{1}]]_{N}, M_{2} ∈ [[A_{2}]]_{N}. M → M_{1} + M_{2} by definition,
⇔ M ⊕-free, ∃M_{1}, M_{2} ⊕-free. M_{1} ⊢ A_{1}, M_{2} ⊢ A_{2} and M ⊢ M_{1} ⊗ M_{2} by induction and lemma 28,
⇒ M ⊕-free, M ⊢ A_{1} ⊗ A_{2} from the proof rules.

To show the converse implication, and so equivalence, assume M is ⊕-free and M ⊢ A_{1} ⊗ A_{2}. By lemma 29, we may assume

A_{1} ⊣⊢ _{i∈I}^{⨁} M_{i}^{1} and A_{2} ⊣⊢ _{j∈J}^{⨁} M_{j}^{2} .

We may furthermore assume I and J to be nonempty. Otherwise A_{1} ⊗ A_{2} ⊣⊢ F and so, as M is ⊕-free, M ⊬ A_{1} ⊗ A_{2} by lemma 30—a contradiction.

Therefore

M ⊢ (_{i∈I}^{⨁} M_{i}^{1}) ⊗ (_{j∈J}^{⨁} M_{j}^{2}),

so by distributivity,

M ⊢ _{(i,j)∈I×J}^{⨁} M_{i}^{1} ⊗ M_{j}^{2} .

Hence, by lemma 30,

M ⊢ M_{i}^{1} ⊗ M_{j}^{2} for some i ∈ I, j ∈ J

such that M_{i}^{1} ⊢ A_{1} and M_{j}^{2} ⊢ A_{2}. This plainly gives the required converse. □

Corollary 32 ⊧_{N} A iff ⊢ A, for any ⊸-free assertion A.

Thus we have completeness.

Because we only use the decomposition lemma (lemma 29) for the ⊗ case of the structural induction in lemma 31, we also get completeness for the larger fragment of assertions B given by:

B ::= A | A ⊸ B | T | F | 1 | a | B_{1} & B_{2} | B_{1} ⊕ B_{2}

where A lie in the ⊸-free fragment and a, as usual, ranges over atoms.

Lemma 33 For the larger fragment,

[[B]]_{N} = {M | M ⊕-free, M ⊢ B} .

Proof The proof proceeds by structural induction, as in lemma 31, but for a new case where the assertion has the form A ⊸ B. Because of its assumed form, by lemma 29, there is a decomposition

A ⊣⊢ _{i∈I}^{⨁} M_{i} .

Now, for ⊕-free M we argue that

M ∈ [[A ⊸ B]]_{N} ⇔ ∀M_{A} ∈ [[A]]_{N}. M + M_{A} ∈ [[B]]_{N} by definition,
⇔ ∀M_{A} ⊕-free. M_{A} ⊢ A ⇒ M ⊗ M_{A} ⊢ B by induction,
⇔ ∀M_{A} ⊕-free. M_{A} ⊢ ⨁_{i∈I} M_{i} ⇒ M ⊗ M_{A} ⊢ B
⇔ ∀M_{A} ⊕-free. (∃i ∈ I. M_{A} ⊢ M_{i}) ⇒ M ⊗ M_{A} ⊢ B by lemma 30,
⇔ ∀i ∈ I, ∀M_{A} ⊕-free. M_{A} ⊢ M_{i} ⇒ M ⊗ M_{A} ⊢ B
⇔ ∀i ∈ I. M ⊗ M_{i} ⊢ B.

Here “⇒” follows directly by taking M_{A} = M_{i}. The converse “⇐” makes use of the fact that if M_{A} ⊢ M_{i} and M ⊗ M_{i} ⊢ B then M ⊗ M_{A} ⊢ B. Now, continuing the argument,

M ∈ [[A ⊸ B]]_{N} ⇔ ∀i ∈ I. M ⊕ M_{i} ⊢ B
⇔ ⨁_{i∈I}(M ⊗ M_{i}) ⊢ B from the proof system,
⇔ M ⊗ (⨁_{i∈I} M_{i}) ⊢ B
⇔ M ⊗ A ⊢ B
⇔ M ⊢ A ⊸ B. □

Corollary 34 For the larger fragment, ⊧ B iff ⊢ B with the additional &-⊕- distributivity law.

Theorem 35 For the ⊸-free fragment,

Γ ⊧ A iff Γ ⊢ A

with the additional &-⊕-distributive law.

Proof Corollary 34 gives

⊧ ⨂ Γ ⊸ A iff ⊢ ⨂ Γ ⊸ A .

Hence

Γ ⊧ A iff Γ ⊢ A . □

14 Quantification and Atomic Nets

Definition 36 A net is atomic iff whenever M → \underline{0} then \underline{0} → M, for any marking M. □

This corresponds to 1 being atomic in the associated quantale. A sufficient condition for a net to be atomic is that every transition of it leads to a nonempty multiset of markings.

Notice that A & 1 plays the role of the exponential !A, and indeed according the net semantics, when the net N is atomic

[[!A]]_{N} = [[A & 1]]_{N} .

An other interesting consequence of dealing with an atomic net N is, that we no longer need the logical constant, ⊥, denoting linear-absurdity in order to express negative properties. Whatever property we could state before in terms of validity of a closed formula A, can now be stated negatively as ⊧_{N} A & 1 ⊸ F. Precisely:

Proposition 37 For an atomic net N and a closed formula A,

⊧_{N} A & 1 ⊸ F iff |̸=_{N} A .

Proof Notice that due to atomicity, the the denotation of A & 1 is that of 1 if the denotation of A contains 1 and empty otherwise. Hence [[A & 1 ⊸ F]]_{N} equals T in case |̸=_{N} A and equals F in case ⊧_{N} A. □

Abbreviating A & 1 ⊸ F by ^{∼}A, this means that all properties stated in section 10 as A^{⊥}, now can be stated as ^{∼}A. In exercise 49 in section 15 we shall see that ⊥ in fact can be expressed directly in the extended logic.

Syntax

Assume a countable set of atoms. Define the assertions over the atoms to be:

A ::= T | F | 1 | a | x | A_{1} ⊗ A_{2} | A_{1} ⊸ A_{2} | A_{1} & A_{2} | A_{1} ⊕ A_{2} | _{x}^{⨁} A | &_{x} A

where a ranges over the atoms and x ranges over countably many variables. The new constructions ⨁_{x} A and &_{x} A are forms of existential and universal quantification and bind accordingly. We adopt the traditional notions of free and bound variable and in particular use FV(A) for the set of free variables in A, and more generally FV(A_{1}, …, A_{n}) for FV(A_{1}) ∪ ⋯ ∪ FV(A_{n}). The variables x are to be thought of as standing for markings of a net.

Semantics

Given a net N, with markings (i.e. finite multisets of places) M, a (marking) environment is a function ρ from variables to markings M. Because of the presence of free variables we define the meaning of an assertion with respect to a marking environment. In particular,

\begin{matrix}[[ ⨁_{x} A]]_{N}ρ = & ⋃_{M∈M} [[A]]_{N}ρ[M/x], \\ [[ &_{x} A]]_{N}ρ = & ⋂_{M∈M} [[A]]_{N}ρ[M/x], \\ [[x]]_{N}ρ = & \{M ∈ M | M → ρ(x)\}. \end{matrix}

Atoms are interpreted as singletons of places of the net as in section 7 and similarly validity of a closed assertion A for the given net, N, can be expressed by:

⊧_{N} A iff \underline{0} ∈ [[A]]_{N}ρ .

This is generalized to open terms by taking the universal closure:

⊧_{N} A iff \underline{0} ∈ [[ &_{x_{1}} ⋯ &_{x_{k}} A]]_{N}ρ

where A has free variables x_{1}, …, x_{k} (here ρ can be arbitrary because &_{x_{1}} ⋯ &_{x_{k}} A is closed).

Let T be a subset of closed assertions in the syntax. Define B_{1}, …, B_{n} ⊧_{T} A iff for all atomic net valuations N such that (∀B ∈ T. ⊧_{N} B), ⊧_{N} (B_{1} ⊗ ⋯ ⊗ B_{n} ⊸ A).

Before proceeding with the proof rules we show how the new constructions can be used to express liveness.

A transition t is live iff ∀M ∈ [M_{0}⟩∃M′ ∈ [M⟩. M′ [t⟩.

This can be expressed by:

⊧_{N} &_{x}((M_{0} ⊸ x) & 1 ⊸ (x ⊸^{•}t ⊗ T)) .

Obviously liveness can then be expressed for finite nets.

Exercise 38 In this exercise we consider a logic for Petri nets inspired by branching-time logic. The syntax of the branching formulae is

φ ::= p | φ ∧ φ | φ ∨ φ | ¬φ | ∀G φ | ∃F φ  (12)

where p range over some atomic propositions. For a net N and a fixed valuation V_{N} yielding for each atomic proposition a set of markings for which it holds, we can recursively define when a marking M of N satisfies a formula φ, written M ⊧_{N} φ, as follows:

M ⊧_{N} p  iff M ∈ V_{N}(p)
M ⊧_{N} φ_{1} ∧ φ_{2} iff M ⊧_{N} φ_{1} and M ⊧_{N} φ_{1}
M ⊧_{N} φ_{1} ∨ φ_{2} iff M ⊧_{N} φ_{1} or M ⊧_{N} φ_{1}
M ⊧_{N} ¬φ  iff M |̸=_{N} φ
M ⊧_{N} ∀G φ iff ∀M′ ∈ [M⟩. M′ ⊧_{N} φ
M ⊧_{N} ∃F φ iff ∃M′ ∈ [M⟩. M′ ⊧_{N} φ .

As an example, a valuation V_{N} and an atomic proposition p_{t} could express the set of markings enabling t. I.e. V_{N}(p_{t}) = {M | ∃M′. M [t⟩ M′}.

Now, let M be some marking term and X an ordered infinite set of variables such that FV(M) ⊆ X. Furthermore, suppose a set Φ of formulae of (12) for which we, given a marking M and a φ ∈ Φ, have a translation A_{φ}(M) into linear logic, i.e. such that M ⊧_{N} φ iff ⊧_{N} A_{φ}(M). For p_{t} mentioned above, the translation A_{∃F p_{t}}(M) of ∃F p_{t} could be M ⊸^{•}t ⊗ T.

The translation can then be extended to cover all branching formulae over Φ by the following schema

\begin{aligned}[[φ]]_{X}^{M} & = A_{φ}(M), for φ ∈ Φ \\ [[φ_{1} ∧ φ_{2}]]_{X}^{M} & = [[φ_{1}]]_{X}^{M} & [[φ_{2}]]_{X}^{M} \\ [[φ_{1} ∨ φ_{2}]]_{X}^{M} & = [[φ_{1}]]_{X}^{M} ⊕ [[φ_{2}]]_{X}^{M} \\ [[¬φ]]_{X}^{M} & = ^{∼}[[φ]]_{X}^{M} \\ [[ ∀G φ]]_{X}^{M} & = &_{x}((M ⊸ x) & 1 ⊸ [[φ]]_{X∪\{x\}}^{x}) \\ [[ ∃F φ]]_{X}^{M} & = ⨁_{x}((M ⊸ x) & [[φ]]_{X∪\{x\}}^{x}) \end{aligned}

where x is the first variable not in X.

This gives another and easy way to see how to express in linear logic that a transition t is live or M-dead because

t live iff M_{0} ⊧ ∀G ∃F p_{t}
t is M-dead iff M ⊧ ∀G ¬p_{t} iff M ⊧ ¬ ∃F p_{t} .

Show that for a closed marking term M and branching formula φ over Φ we have:

M ⊧_{N} φ iff ⊧_{N} [[φ]]_{∅}^{M} . □

Proof rules

The proof rules are those of section 2 (without exponentials—they will become definable in the purely propositional logic), together with:

\frac{Γ ⊢ A}{Γ[θ] ⊢ A[θ]}  (Subst.)

where θ is a substitution of marking terms (i.e. assertions built up from variables, atoms and 1 purely by ⊗)—the usual care to avoid capture of free variables applies here.

\frac{Γ, B ⊢ A}{Γ, ⨁_{x} B ⊢ A} x ∉ FV(Γ, A)  (⨁⊢)
\frac{Γ ⊢ A[M/x]}{Γ ⊢ ⨁_{x} A} where M is a marking term  ( ⊢⨁)

Note these rules yield (and in the presence of (Subst.) are equivalent with)

\frac{\underline{Γ, ⨁_{x} B ⊢ A}}{Γ, B ⊢ A} x ∉ FV(Γ, A)  (⨁-adj.)

Assume (⨁⊢) and ( ⊢⨁). The upwards direction of the rule (⨁-adj.) is simply (⨁⊢).

The downwards direction viz.

\frac{Γ, ⨁_{x} B ⊢ A}{Γ, B ⊢ A} x ∉ FV(Γ, A)

is derivable in the following way. Clearly B ⊢ B so by application of ( ⊢⨁), B ⊢ ⨁_{x} B. Now by the cut rule from the assumption Γ, ⨁_{x} B ⊢ A we can conclude Γ, B ⊢ A.

By using (Subst.) we can also derive (⨁⊢) and ( ⊢⨁) from (⨁-adj.). The rule (⨁⊢) is simply the upwards reading of (⨁-adj.). Now we show ( ⊢⨁) follows from (⨁-adj.): Clearly ⨁_{x} A ⊢ ⨁_{x} A, from which A ⊢ ⨁_{x} A follows by (⨁-adj.); hence by (Subst.) A[M/x] ⊢ ⨁_{x} A, making ( ⊢⨁) derivable.

\frac{Γ, B ⊢ A}{Γ, &_{x} B ⊢ A}  (&⊢)

\frac{Γ ⊢ A}{Γ ⊢ &_{x} A} x ∉ FV(Γ)  ( ⊢&)

Note these rules are equivalent with

\frac{Γ ⊢ A}{\overline{Γ ⊢ &_{x} A}} x ∉ FV(Γ) .  (&-adj.)

In addition we have the following axioms valid of nets:

(A_{1} ⊕ A_{2}) & B ⊢ (A_{1} & B) ⊕ (A_{2} & B)  (&-⊕-dist.)
(_{x}^{⨁} A) & B ⊢ _{x}^{⨁}(A & B) where x ∉ FV(B)  (&-⨁-dist.)

In fact, in the presence of the atomicity, basis and primeness axioms, these distributivity laws are derivable from those in the special case where B is 1. The other distributive law,

&_{x}(A ⊕ B) ⊢ (&_{x} A) ⊕ B where x ∉ FV(B),

is also derivable (for general B).

⊢ (&_{x} B) ⊕ _{x}^{⨁}((B & 1) ⊸ F)  (Atomicity)

These entail sequents of the following form (by taking the variable x to not appear in B):

⊢ B ⊕ ((B & 1) ⊸ F) .

These hold because in an atomic net the denotation of a formula B & 1, in an environment for its free variables, only has two possibilities, to be the denotation of F or the denotation of 1.

A ⊢ _{x}^{⨁} x ⊗ ((x ⊸ A) & 1) where x ∉ FV(A)  (Basis)

These hold in an atomic net because an assertion denotes a set of markings; notice how the expression (x ⊸ A) & 1 is equivalent to 1 in the case the marking x satisfies A and F otherwise, so the effect in the whole expression is only to make a contribution of x when it satisfies A.

(x ⊸ F) ⊢ F
(x ⊸ B ⊕ C) ⊢ (x ⊸ B) ⊕ (x ⊸ C)
(x ⊸ ⨁_{y} A) ⊢ ⨁_{y}(x ⊸ A) where y and x are distinct.

(Primeness)

These axioms hold because if a marking is contained in union, denoting a disjunction, then it is clearly in a component of the union.

For clarity we have collected the new proof rules:

\frac{Γ ⊢ A}{Γ[θ] ⊢ A[θ]}  (Subst.)

\frac{Γ ⊢ A[M/x]}{Γ ⊢ ⨁_{x} A}  ( ⊢⨁)  \frac{Γ, B ⊢ A}{Γ, ⨁_{x} B ⊢ A} x ∉ FV(Γ, A) (⨁⊢)
\frac{Γ ⊢ A}{Γ ⊢ &_{x} A} x ∉ FV(Γ) ( ⊢&)  \frac{Γ, B ⊢ A}{Γ, &_{x} B ⊢ A}  (&⊢)
(A_{1} ⊕ A_{2}) & B ⊢ (A_{1} & B) ⊕ (A_{2} & B)  (&-⊕-dist.)
(_{x}^{⨁} A) & B ⊢ _{x}^{⨁}(A & B), x ∉ FV(B)  (&-⨁-dist.)
⊢ (&_{x} B) ⊕ _{x}^{⨁}((B & 1) ⊸ F)  (Atomicity)
A ⊢ _{x}^{⨁} x ⊗ ((x ⊸ A) & 1), x ∉ FV(A)  (Basis)
(x ⊸ F) ⊢ F
(x ⊸ B ⊕ C) ⊢ (x ⊸ B) ⊕ (x ⊸ C)
(x ⊸ ⨁_{y} A) ⊢ ⨁_{y}(x ⊸ A) where y and x are distinct

(Primeness)

The soundness of the basis and atomicity axioms follows from the fact that, in an atomic net,

[[A & 1]]_{N}ρ = \{ \begin{matrix}1 & if 1 ⊆ [[A]]_{N}ρ \\ F & otherwise \end{matrix} and [[A & 1 ⊸ F]]_{N}ρ = \{ \begin{matrix}F & if 1 ⊆ [[A]]_{N}ρ \\ T & otherwise. \end{matrix}

We have already remarked that in an atomic net, an exponential !A is represented by A & 1. In fact from the atomicity axioms and the rules for exponentials, there is a fairly direct proof of their equivalence, yielding

!A ⊣⊢ A & 1  (13)

—the syntax of exponentials can be eliminated in favour of the purely propositional connectives.

For the proof first remark that A & 1 ⊢ A and A & 1 ⊢ 1, simply by the rules for &. From A & 1 ⊢ (A & 1) & 1 and (Atomicity) we also get ⊢ (A & 1) ⊕ (A & 1 ⊸ F). Using A & 1 ⊢ A & 1 we then deduce

A & 1 ⊢ ((A & 1) ⊗ (A & 1)) ⊕ ((A & 1) ⊗ (A & 1 ⊸ F))

so that A & 1 ⊢ ((A & 1) ⊗ (A & 1)) ⊕ F, i.e.

A & 1 ⊢ (A & 1) ⊗ (A & 1) .

By (4) of section 3 this ensures A & 1 ⊢ !A, and clearly !A ⊢ A & 1, making (13).

Completeness

Prime theories play a key role in showing completeness. A prime theory arises as the set of all assertions true of some net, and conversely from a prime theory we can construct a net whose truths are precisely the prime theory. The completeness proof proceeds by showing that if an assertion is not provable then there is a prime theory, and so a net, for which it fails to hold.

In constructing prime theories we follow Henkin and extend the original syntax to include new atoms drawn from

c_{0}, c_{1}, …, c_{n}, …

a countably infinite enumeration of atoms not already present in the syntax. Suppose C is a subset of {c_{i} | i ∈ ω}. Suppose Γ, A are assertions from the syntax extended by C, and that F is a theory (i.e. a subset of assertions) of the extended syntax. We use

Γ ⊢_{F}^{C} A

to mean the sequent is provable in the proof system for the extended syntax, using the assertions in F as axioms. A judgment Γ ⊢ A means a sequent is provable in the proof system of the original assertion language, without extra atoms.

Lemma 39 Let B be a closed assertion and F a theory in a syntax extended by atoms C ⊆ {c_{i} | i ∈ ω}. Then

Γ ⊢_{F∪{B}}^{C} A iff Γ, B & 1 ⊢_{F}^{C} A .

Proof “⇒” By induction on the size of derivations of Γ ⊢_{F∪{B}}^{C} A, considering the final rule used.

“⇐” From ⊢_{F∪{B}} B and ⊢ 1 follows ⊢_{F∪{B}} B & 1 and so the results from hypothesis and cut. □

Definition 40 Let C ⊆ {c_{i} | i ∈ ω}. A subset F of closed assertions, in the syntax extended by atoms C, is called a prime theory iff

(i) F ∉ F, A_{1} ⊕ A_{2} ∈ F ⇒ A_{1} ∈ F or A_{2} ∈ F, ⨁_{x} A ∈ F ⇒ A[M/x] ∈ F, for some (necessarily closed) marking term M.

(ii) F is deductively closed, i.e. A closed and ⊢_{F}^{C} A ⇒ A ∈ F.

□

Lemma 41 (Existence of prime theories). Let A be an assertion and T a subset of closed assertions in the original syntax, for which

⊬_{T} A .

Then, there is a prime theory F, consisting of assertions over the syntax extended by some C ⊆ {c_{i} | i ∈ ω}, such that

T ⊆ F and ⊬_{F}^{C} A .

Proof As the atoms and variables form countable sets we can enumerate all the assertions

A_{0}, A_{1}, …, A_{n}, …

of the syntax extended by atoms {c_{i} | i ∈ ω}.

By induction, for n ∈ ω, we define a chain of deductively – closed theories F_{n} with new atoms C_{n}, such that

T ⊆ F_{n} and ⊬_{F_{n}}^{C_{n}} A .

Take F_{0} = {B | ⊢_{T} B}. Clearly T ⊆ F_{0} and, by assumption, ⊬_{F_{0}} A.

Assuming F_{n} is deductively closed, includes T, and ⊬_{F_{n}}^{C_{n}} A, define F_{n+1} according to the following cases:

(i) n is even, and there is an assertion B_{1} ⊕ B_{2} ∈ F_{n} with B_{1} ∉ F_{n}, B_{2} ∉ F_{n}.

(ii) n is odd, and there is an assertion ⨁_{x} B ∈ F_{n} with B[M/x] ∉ F_{n} for any closed marking terms M in the syntax over atoms extended by C_{n}.

(iii) neither (i) nor (ii) applies.

In case (iii), define C_{n+1} = C_{n} and F_{n+1} = F_{n}.

In case (i), take the earliest assertion in the enumeration B_{1}⊕B_{2} ∈ F_{n} and B_{1} ∉ F_{n} and B_{2} ∉ F_{n}. As F_{n} is deductively-closed, (B_{1} ⊕ B_{2}) & 1 ∈ F_{n}, so

(B_{1} & 1) ⊕ (B_{2} & 1) ∈ F_{n}

by the &-⊕-distributivity law. Suppose

⊢_{F_{n},B_{1}}^{C_{n}} A and ⊢_{F_{n},B_{2}}^{C_{n}} A .

Then, by lemma 39,

B_{1} & 1 ⊢_{F_{n}}^{C_{n}} A and B_{2} & 1 ⊢_{F_{n}}^{C_{n}} A .

Hence (B_{1} & 1) ⊕ (B_{2} & 1) ⊢_{F_{n}}^{C_{n}} A. But this implies ⊢_{F_{n}}^{C_{n}} A, a contradiction. Thus

⊬_{F_{n},B_{1}}^{C_{n}} A or ⊬_{F_{n},B_{2}}^{C_{n}} A .

Supposing, for instance, ⊬_{F_{n},B_{1}}^{C_{n}}, A, take F_{n+1} to be {D closed | ⊢_{F_{n},B_{1}}^{C_{n}}, D} and C_{n+1} = C_{n}.

In case (ii), take the earliest, according to the enumeration, ⨁_{x} B ∈ F_{n} for which B[M/x] ∉ F_{n} for all marking terms M, and where x is not a free variable of A. As F_{n} is deductively-closed, (⨁_{x} B) & 1 ∈ F_{n}, so

_{x}^{⨁}(B & 1) ∈ F_{n} .

Let c be the first new atom in the list c_{0}, c_{1}, … which is not in C_{n}. Define C_{n+1} = C_{n} ∪ {c} and F_{n+1} to consist of all closed assertions in the deductive closure of F_{n} ∪ {B[c/x]}, i.e.

F_{n+1} = {D closed | ⊢_{F_{n},B[c/x]}^{C_{n+1}} D} .

We must check that ⊬_{F_{n+1}}^{C_{n+1}} A. To this end, assume otherwise, that ⊢_{F_{n},B[c/x]}^{C_{n+1}} A. Then, by lemma 39,

B[c/x] & 1 ⊢_{F_{n}}^{C_{n+1}} A .

As c does not appear in C_{n} or F_{n},

B & 1 ⊢_{F_{n}}^{C_{n}} A .

To obtain the proof of this sequent, replace all occurrences of the new atom c in the proof of B[c/x] & 1 ⊢_{F_{n}}^{C_{n+1}} A by a new variable—one which does not appear anywhere in the proof—and finally use (Subst.) to replace this variable by x using the fact that renaming bound variables preserves logical equivalence. But now we can deduce

_{x}^{⨁}(B & 1) ⊢_{F_{n}}^{C_{n}} A .

But ⨁_{x}(B & 1) ∈ F_{n} and F_{n} is deductively-closed making ⊢_{F_{n}}^{C_{n}} A, a contradiction. Thus ⊬_{F_{n+1}}^{C_{n+1}} A, as required.

In this way, we inductively define a chain of theories F_{n} over the syntax extended by C_{n}, such that

C_{n} ⊆ C_{n+1} and F_{n} ⊆ F_{n+1},

with T ⊆ F_{0}. Finally take C = ⋃_{n∈ω} C_{n} and F = ⋃_{n∈ω} F_{n} to form the required prime theory. □

Assume a prime theory F with additional atoms C. Construct a net N from F by taking:

• Places to be the original atoms, including those of C. Atoms are be interpreted as their singleton markings.

• Transitions as those pairs (M, M′) of multisets of places for which M̂ ⊢_{F}^{C} M̂′.

We use M to represent the set of all markings of the net N. (Note the markings coincide with the closed marking terms of F.)

Lemma 42 For markings M, M′ in the net N,

M → M′ in N iff M ⊢_{F}^{C} M′ .

Furthermore N is atomic.

Proof The proof of “iff” is like that for lemma 23.

Regarding atomicity of the net, suppose M → \underline{0}, for M ∈ M. Then M ⊢_{F}^{C} 1. Certainly

M ⊕ (M & 1 ⊸ F) ∈ F

and as F is a prime theory

M ∈ F or M & 1 ⊸ F ∈ F .

The case M & 1 ⊸ F ∈ F is impossible. To see this assume otherwise, that M & 1 ⊸ F ∈ F. As M ⊢_{F}^{C} 1, and clearly M ⊢ M, it follows that M ⊢_{F}^{C} M & 1 and hence M ⊢_{F}^{C} F. This ensures ⊢_{F}^{C} (M ⊸ F) which together with the primeness axiom

(M ⊸ F) ⊢ F

yields ⊢_{F}^{C} F. I.e. F ∈ F—contradicting F being a prime theory. The case M & 1 ⊸ F ∈ F is thus impossible.

M ∈ F, where M ⊢_{F}^{C} 1. Thus M → \underline{0} in the net. The net N is therefore atomic.

□

We need the following facts:

Lemma 43

(i) Let B be an assertion with FV(B) ⊆ {x}. Let the assertions Γ not include x as a free variable. Then

(∀M ∈ M. Γ ⊢_{F}^{C} B[M/x]) ⇒ Γ ⊢_{F}^{C} &_{x} B .

(ii) Let B be an assertion with FV(B) ⊆ {x_{1}, …, x_{k}}, and Γ be assertions in which x_{1}, …, x_{k} are not free. Then

(∀M_{1}, …, M_{k} ∈ M. Γ ⊢_{F}^{C} B[M_{1}/x_{1}, …, M_{k}/x_{k}]) ⇒ Γ ⊢_{F}^{C} B .

Proof (i) We first prove the special case

(∀M ∈ M. ⊢_{F}^{C} A[M/x]) ⇒ ⊢_{F}^{C} &_{x} A,

where FV(A) ⊆ {x}, by contraposition. By atomicity,

⊢ (&_{x} A) ⊕ _{x}^{⨁}(A & 1 ⊸ F),

where both operands of ⊕ are closed, so as F is a prime theory

⊢_{F}^{C} &_{x} A or ⊢_{F}^{C} _{x}^{⨁}(A & 1 ⊸ F) .

Thus supposing ⊬_{F}^{C} &_{x} A we obtain ⊢_{F}^{C} ⨁_{x}(A&1⊸F). But as F is a prime theory, there is then M ∈ M, such that ⊢_{F}^{C} (A[M/x] & 1 ⊸ F) and thus ⊬_{F}^{C} A[M/x].

The more general statement of (i) above follows by taking A ≡ ⨂ Γ ⊸ B where Γ does not contain x free and B has at most x free. Note Γ ⊢ &_{x} B follows from ⊢ &_{x}(⨂ Γ ⊸ B).

(ii) follows by induction using (i) together with the fact that &_{x_{k}} B ⊢ B. □

Lemma 44 For assertions Γ, B and A suppose Γ, B[M/x] ⊢_{F}^{C} A for all M ∈ M. Assume FV(B) ⊆ {x}. Then

Γ, _{x}^{⨁} B ⊢_{F}^{C} A .

Proof We show that if B[M/x] ⊢_{F}^{C} A for all M ∈ M where FV(B) ⊆ x, then ⨁_{x} B ⊢_{F}^{C} A. The seemingly stronger result follows by ⊸-adjunction.

Assume B[M/x] ⊢_{F}^{C} A, for all M ∈ M, and FV(B) ⊆ {x}. Let some M ∈ M be given. Since FV(B[M/x]) ≠ ∅ (M is closed) we can use (⊢&) to get B[M/x] ⊢_{F}^{C} A′ where A′ ≡ &_{y∈FV(A)} A. I.e. FV(A′) = ∅ and ⊢_{F}^{C} B[M/x] ⊸ A′ for all M ∈ M. By (i) of lemma 43 we then get

⊢_{F}^{C} &_{x}(B ⊸ A′)

and by logic that

⊢_{F}^{C} (_{x}^{⨁} B) ⊸ A′ .

Here we used the logic deduction:

&_{x}(B ⊸ A′) ⊢ B ⊸ A′  holds by (&⊢) and (identity),
⇒ &_{x}(B ⊸ A′), B ⊢ A′
⇒ &_{x}(B ⊸ A′), ⨁_{x} B ⊢ A′  by (⨁⊢) as x ∉ FV(&_{x}(B ⊸ A′), A′),
⇒ &_{x}(B ⊸ A′) ⊢ (⨁_{x} B) ⊸ A′.

From ⊢_{F}^{C} (⨁_{x} B) ⊸ A′ we get ⨁_{x} B ⊢_{F}^{C} A′ and so ⨁_{x} B ⊢_{F}^{C} A by (&-adj.). □

Now we can relate semantics in the net N to provability in the prime theory F:

Lemma 45 For any assertion A, for any marking environment ρ, [[A]]_{N}ρ = {M ∈ M | M ⊢_{F}^{C} A[ρ]} .

Proof By structural induction on A. A ≡ T: [[T]]_{N}ρ = M = {M ∈ M | M ⊢_{F}^{C} T}. A ≡ F: [[F]]_{N}ρ = ∅ = {M ∈ M | M ⊢_{F}^{C} F}—as F ∉ F and (M ⊸ F) ⊢ F. A ≡ 1: [[1]]_{N}ρ = \{M ∈ M | M → \underline{0}\} = \{M ∈ M | M ⊢_{F}^{C} 1\} by lemma 42. A ≡ a: [[a]]_{N}ρ = {M ∈ M | M → a} = {M ∈ M | M ⊢_{F}^{C} a} by lemma 42. A ≡ x: [[x]]_{N}ρ = {M ∈ M | M → ρ(x)} = {M ∈ M | M ⊢_{F}^{C} ρ(x)} by lemma 42. A ≡ A_{1} ⊗ A_{2}: For M ∈ M,

M ∈ [[A_{1} ⊗ A_{2}]]_{N}ρ

⇔ ∃M_{1} ∈ [[A_{1}]]_{N}ρ, M_{2} ∈ [[A_{2}]]_{N}ρ. M → M_{1} + M_{2},
⇔ ∃M_{1}, M_{2} ∈ M. M_{1} ⊢_{F}^{C} A_{1}[ρ], M_{2} ⊢_{F}^{C} A_{2}[ρ] and M ⊢_{F}^{C} M_{1} ⊗ M_{2},
⇒ M ⊢_{F}^{C} (A_{1} ⊗ A_{2})[ρ].

To show “⇐” as well, we write A′_{1} ≡ A_{1}[ρ] and A′_{2} ≡ A_{2}[ρ], and use the basic facts that

A′_{1} ⊢ ⨁_{x_{1}} x_{1} ⊗ ((x_{1} ⊸ A′_{1}) & 1) and A′_{2} ⊢ ⨁_{x_{2}} x_{2} ⊗ ((x_{2} ⊸ A′_{2}) & 1) .

Assuming M ⊢_{F}^{C} A′_{1} ⊗ A′_{2}, we obtain M ⊢_{F}^{C} (_{x_{1}}^{⨁} x_{1} ⊗ ((x_{1} ⊸ A′_{1}) & 1)) ⊗ (_{x_{2}}^{⨁} x_{2} ⊗ ((x_{2} ⊸ A′_{2}) & 1)) .

By distributivity of ⊗ over ⨁, M ⊢_{F}^{C} _{x_{1}}^{⨁} _{x_{2}}^{⨁} x_{1} ⊗ ((x_{1} ⊸ A′_{1}) & 1) ⊗ x_{2} ⊗ ((x_{2} ⊸ A′_{2}) & 1) .

By primeness and because F is a prime theory,

M ⊢_{F}^{C} M_{1} ⊗ ((M_{1} ⊸ A′_{1}) & 1) ⊗ M_{2} ⊗ ((M_{2} ⊸ A′_{2}) & 1)  (*)

for some M_{1}, M_{2} ∈ M.

By atomicity and the fact that F is a prime theory

⊢_{F}^{C} (M_{1} ⊸ A′_{1}) or ⊢_{F}^{C} ((M_{1} ⊸ A′_{1}) & 1 ⊸ F) and
⊢_{F}^{C} (M_{2} ⊸ A′_{2}) or ⊢_{F}^{C} ((M_{2} ⊸ A′_{2}) & 1 ⊸ F) .

As M ⊬_{F}^{C} F and M_{i} ⊬_{F}^{C} F for i = 1, 2 (by the same argument as in the A ≡ F case above) we from (*) deduce (M_{i} ⊸ A′_{i}) & 1 ⊬_{F}^{C} F for i = 1, 2, and we must have ⊢_{F}^{C} (M_{1} ⊸ A′_{1}) and ⊢_{F}^{C} (M_{2} ⊸ A′_{2}), i.e. M_{1} ⊢_{F}^{C} A′_{1}, and M_{2} ⊢_{F}^{C} A′_{2}, as well as M ⊢_{F}^{C} M_{1} ⊗ M_{2}. This establishes the required reverse implication, and so equivalence.

A ≡ A_{1} ⊸ A_{2}: M ∈ [[A_{1} ⊸ A_{2}]]_{N}ρ ⇔ ∀M_{1} ∈ [[A_{1}]]_{N}ρ. M + M_{1} ∈ [[A_{2}]]_{N}ρ. ⇔ ∀M_{1} ⊢_{F} A_{1}[ρ]. M ⊗ M_{1} ⊢_{F}^{C} A_{2}[ρ] by induction, ⇔ ∀M_{1} ∈ M. M ⊗ M_{1} ⊗ ((M_{1} ⊸ A_{1}[ρ]) & 1) ⊢_{F}^{C} A_{2}[ρ]

where the last equivalence relies on atomicity and the fact that F is a prime theory. In more detail, writing A′_{1} ≡ A_{1}[ρ], A′_{2} ≡ A_{2}[ρ], we have

(i) ⊢_{F}^{C} M_{1} ⊸ A′_{1} or (ii) ⊢_{F}^{C} (M_{1} ⊸ A′_{1}) & 1 ⊸ F

for any M_{1} ∈ M. For case (i), (M_{1}⊸A′_{1})&1 ⊣⊢_{F}^{C} 1. In case (ii), (M_{1}⊸A′_{1})&1 ⊣⊢_{F}^{C} F.

It follows, by considering the two cases, that for any M ∈ M′

(M_{1} ⊢_{F}^{C} A′_{1} ⇒ M ⊗ M_{1} ⊢_{F}^{C} A′_{2}) iff M ⊗ M_{1} ⊗ ((M_{1} ⊸ A′_{1}) & 1) ⊢_{F}^{C} A′_{2} .

Now note that by lemma 44,

∀M_{1} ∈ M. M ⊗ M_{1} ⊗ ((M_{1} ⊸ A′_{1}) & 1) ⊢_{F}^{C} A′_{2}

⇔ M ⊗ ⨁_{x_{1}} x_{1} ⊗ ((x_{1} ⊸ A′_{1}) & 1)) ⊢_{F}^{C} A′_{2},
⇔ M ⊗ A′_{1} ⊢_{F}^{C} A′_{1} as A′_{1} ⊣⊢_{F}^{C} ⨁_{x} x_{1} ⊗ ((x_{1} ⊸ A′_{1}) & 1),
⇔ M ⊢_{F}^{C} A′_{1} ⊸ A′_{2} i.e. M ⊢_{F}^{C} A_{1}[ρ] ⊸ A_{2}[ρ], as required.

A ≡ A_{1} ⊕ A_{2}: \begin{matrix}M ∈ [[A_{1} ⊕ A_{2}]]_{N}ρ ⇔ & M ∈ [[A_{1}]]_{N}ρ or M ∈ [[A_{2}]]_{N}ρ \\ ⇔ & M ⊢_{F}^{C} A_{1}[ρ] or M ⊢_{F}^{C} A_{2}[ρ] \\ ⇔ & M ⊢_{F}^{C} A_{1}[ρ] ⊕ A_{2}[ρ]. \end{matrix}

where primeness and the fact that F is a prime theory is used in showing “⇐”; the other direction “⇒” follows directly from the proof system.

A ≡ A_{1} & A_{2}: M ∈ [[A_{1} & A_{2}]]_{N}ρ ⇔ M ∈ [[A_{1}]]_{N}ρ and M ∈ [[A_{2}]]_{N}ρ ⇔ M ⊢_{F}^{C} A_{1}[ρ] and M ⊢_{F}^{C} A_{2}[ρ] by induction, ⇔ M ⊢_{F}^{C} A_{1}[ρ] & A_{2}[ρ].

A ≡ ⨁_{x} B : M ∈ [[ ⨁_{x} B]]_{N}ρ ⇔ ∃M′ ∈ M. M ∈ [[B]]_{N}ρ[M′/x] ⇔ ∃M′ ∈ M. M ⊢_{F}^{C} B[ρ[M′/x]] by induction, ⇔ M ⊢_{F}^{C} (⨁_{x} B)[ρ]. where “⇒” follows directly from the proof system, whereas “⇐” relies on primeness and F being a prime theory.

A ≡ &_{x} B: M ∈ [[ &_{x} B]]_{N}ρ ⇔ ∀M′ ∈ M. M ∈ [[B]]_{N}ρ[M′/x] ⇔ ∀M′ ∈ M. M ⊢_{F}^{C} B[ρ[M′/x]] by induction, ⇔ M ⊢_{F}^{C} (&_{x} B)[ρ] by (i) of lemma 43.

□

Theorem 46 (Completeness). Let A, B and Γ ≡ B_{1}, …, B_{n} be assertions and T consist of closed assertions in the original syntax. Then,

Γ ⊧_{T} A iff Γ ⊢_{T} A .

Proof As ⊸ is present as a constructor on assertions it is clearly sufficient to show

⊧_{T} A iff ⊢_{T} A .

The “if” direction is shown by induction on the proof of ⊢_{T} A. To show the “only if” direction we prove its contraposition:

⊬_{T} A ⇒ |̸=_{T} A .

Suppose A is an assertion with free variables x_{1}, …, x_{k}. Suppose ⊬_{T} A. Then there is a prime theory F ⊇ T over additional constants C such that ⊬_{F}^{C} A. Let N be the net constructed from F; let M be the set consisting of its markings. As we now show, |̸=_{N} A. Suppose otherwise, that ⊧_{N} A. Recall

[[A]]_{N}ρ = {M ∈ M | M ⊢_{F}^{C} A[ρ]}

by lemma 45. Hence as ⊧_{N} A means \underline{0} ∈ [[A]]_{N}ρ for all environments ρ, we see

⊢_{F}^{C} A[ρ] for all environments ρ .

Therefore ⊢_{F}^{C} A[M_{1}/x_{1}, …, M_{k}/x_{k}] for all M_{1}, …, M_{k} ∈ M. Hence by (ii) of lemma 43, ⊢_{F}^{C} A, a contradiction. Thus N is an atomic net satisfying all axioms of the theory T and yet |̸=_{N} A. Hence |̸=_{T} A, as required. □

Exercise 47 (Infinite disjunctions) An alternative complete proof system with respect to countable atomic nets can be obtained by adding a countably infinite disjunction and infinitary rules for reasoning about it. More precisely, as the syntax of assertions take

A ::= T | F | 1 | a | A_{1} ⊗ A_{2} | A_{1} ⊸ A_{2} | A_{1} & A_{2} | _{i∈I}^{⨁} A_{i},

where a ranges over a countable set of atoms and I over countable indexing sets drawn from ω (this avoids our syntax becoming a proper class). When I = {1, 2}, we can write ⨁_{i∈I} A_{i} as A_{1} ⊕ A_{2}. We regard F as the empty disjunction. The semantics of assertions in an atomic net N is like that earlier in section 7, with the additional assumption that every place is named by an atomic proposition (this assumption ensures that we can describe all markings within the logic of assertions). The semantics of countable disjunctions ⨁_{i∈I} A_{i} is a slight extension of that in the finite case:

[[ _{i∈I}^{⨁} A_{i}]]_{N} = _{i∈I}^{⋃} [[A_{i}]]_{N}

All other semantic clauses are the same as in section 7. As proof rules we take those of earlier, in section 2, but replacing the rules for binary ⊕ by the following two proof rules, the second of which is infinitary:

\frac{Γ ⊢ A_{j}}{Γ ⊢ ⨁_{i∈I} A_{i}} for j ∈ I, \frac{Γ, B_{i} ⊢ C for all i ∈ I}{Γ, ⨁_{i∈I} B_{i} ⊢ C} .

In addition to these logical rules we also have rules specific to atomic nets:

\begin{matrix}(⨁_{i∈I} A_{i}) & B ⊢ & ⨁_{i∈I} (A_{i} & B) \\ ⊢ & B ⊕ (B & 1 ⊸ F) \\ A ⊢ & ⨁_{M∈M} M ⊗ ((M ⊸ A) & 1) \\ M ⊸ ⨁_{i∈I} A_{i} ⊢ & ⨁_{i∈I} (M ⊸ A_{i}) \end{matrix}

where M ∈ M. Here M denotes the set of finite multisets of atoms. As earlier, in the context of a assertions, we make the identification with such multisets and tensor formulae. Note that M is countable as the set of atoms is assumed countable. Note, for instance, that the last rule amounts to

(M ⊸ F) ⊢ F, for M ∈ M,

when the indexing set I is empty.

Show that the proof system described above is sound and complete with respect to atomic nets. [Hint: Mimic the completeness proof above, taking as a prime theory a deductively closed subset of assertions with the property that if it contains a disjunction then it contains a disjunct. To show that any theory not entailing A can be extended to a prime theory, define a suitable chain of theories F_{n} by transfinite induction on ordinals n, assuming inductively that F_{n} is deductively-closed and A ∉ F_{n}, and take the required prime theory as their union.] □

15 Decidability Issues

Here we show that the question of whether an assertion from the logic of section 14 belongs to the theory of a net is undecidable. We use the following proposition.

Proposition 48 In the logic of section 14, we define the following

⟨x | A⟩ ≡ _{x}^{⨁}[(A & 1) ⊗ x]

for an assertion A and variable x. Its denotation with respect to a net valuation N and environment ρ is given by:

[[⟨x | A⟩]]_{N}ρ = ↓\{M | \underline{0} ∈ [[A]]_{N}ρ[M/x]\} .

Exercise 49

(i) Prove proposition 48 above.

(ii) Show that linear absurdity ⊥ (cf. section 10) is definable for atomic nets,

in the following way:

⊥ ≡ ⟨x | x & 1 ⊸ F⟩

i.e., for an arbitrary environment,

[[⟨x | x & 1 ⊸ F⟩]]_{N}ρ = \{M | \underline{0} ↛ M in N\} .

(iii) Show that for an atomic net N,

[[⟨x | ^{∼}(M_{0} ⊸ x)⟩]]_{N}ρ = {M | M_{0} ↛ M in N} . □

Theorem 50 The property ⊧_{N} A is undecidable for a finite net N and assertion A of the of the logic of section 14 (assumed to have infinitely many atomic propositions).

Proof From Rabin’s work (described in [Hac76]), we know that the question of whether the reachable markings of one finite net are included in the reachable markings of another is undecidable. More precisely, for two finite nets N_{1} and N_{2}, over the same set of places, with markings M_{1}, M_{2}, it is undecidable whether or not all the markings reachable from M_{1} in N_{1} are included in those reachable from M_{2} in N_{2}. If ⊧_{N} A were decidable we could decide Rabin’s problem. From N_{1}, N_{2} we effectively construct another net N as follows: Its places are those in common to N_{1} and N_{2} plus two additional, distinct places a_{1} and a_{2}. Its transitions are obtained as a disjoint union of those of N_{1} and N_{2}; we adjoin a_{1} (with multiplicity 1) to the pre and post places of transitions originally is N_{1} and a_{2} to the pre and post places of those transitions originally of N_{2}:

[figure: .; .; .; .; .; .; .; .; t_{1}; a_{1}; .; .; .; .; .; .; .; .; t_{2}; a_{2}]

Above t_{1} is a transition of N_{1} and t_{2} is a transition of N_{2}.

Now, using proposition 48, we could decide Rabin’s problem if we could decide

⊧_{N} ⟨x | ^{∼}(M_{2} ⊗ a_{2} ⊸ x ⊗ a_{2})⟩ ⊸ ⟨x | ^{∼}(M_{1} ⊗ a_{1} ⊸ x ⊗ a_{1})⟩

Hence the property ⊧_{N} A is undecidable. □

Exercise 51 For this exercise suppose we modify ⊧_{N} A to be as before so that not only does every atomic proposition name a place of N, but also every place in N is named by some atomic proposition of the logic of section 14 (so every place of N receives a name).

(i) Show that with this modification we can not achieve strong completeness:

⊧_{T} A iff ⊢_{T} A

for an arbitrary theory T. Proceed as follows: For a finite net N the set of assertions

T_{N} = {M ⊸ M′ | M → M′ in N} ∪ {^{∼}(M ⊸ M′) | M ↛ M′ in N}

is recursively enumerable (see [May84]). Show that with our modified understanding of satisfaction

⊧_{N} A iff ⊧_{T_{N}} A.

Deduce that there is no effectively given sound and strongly complete proof system.

(ii) On the other hand, assuming the atomic propositions form an infinite set, show that there is a complete proof system in the sense that

⊢ A iff ⊧ A

where the proof rules are those of section 14.

[Hint: Its proof involves a slight modification of the notion of a prime theory.]

□

Although we feel sure the logic of section 14 is undecidable i.e. ⊢ A is not decidable for general A, we presently lack a proof (unfortunately, the techniques of [LMSN90] do not work directly because of our primeness axioms). There remain, in addition, the questions of decidability and complexity of weaker fragments of the logic than that of section 14 and their theories with respect to a specified finite net. However, directly from [LMSN90], it is known that the ⊕-free and ⊸-free fragments (without the law of &-⊕-distributivity) of section 13 are decidable.

16 Conclusion

Two questions emerge in our work:

(i) What can Petri nets contribute to linear logic?

(ii) What can linear logic contribute to Petri nets?

The expressiveness and completeness results that follow give answers to (i). For the ⊕-free fragment of linear logic (its syntax is given in Section 13), Petri nets are a good model; they give a sound and complete interpretation of this fragment of the logic without having to add any extra axioms or rules. For the other parts of linear logic that we treat, the answer must be more qualified, because we need to adjoin extra axioms to obtain completeness. Addressing (i), we hope the reader comes to share our view that Petri nets (with our semantics) are a helpful, intuitive and convincing model of linear logic—certainly Petri nets carry their own intuition and are models of interest, independently of linear logic.

Answering (ii) is harder at this stage. Linear logic is one of few logics for Petri nets which treat in a non-artificial way the fact that places can hold with multiplicities. The logic of section 14 is also very expressive and we have a complete proof system, although we pay through the theory of a net being non-recursive (see theorem 50). On the negative side, it’s sometimes very hard to see if and how a particular property can be expressed, though this criticism could also be levelled at the very useful modal μ-calculus and so cannot be taken too seriously. A fuller answer to (ii) would rest on a more detailed investigation, including that of fragments and variants of linear logic and whether they are useful in the study of Petri nets.^{4}

In summary, it is claimed that this paper helps in the understanding of linear logic. The paper exposes a possible role linear logic may have in reasoning about Petri nets and, through them, in concurrent computation.

4One possible irritation with the present semantics is that all atoms must name places, or more precisely their downwards closure with respect to reachability, possibly in a many-one way. Gian Luca Cattani has shown in [Cat] that the semantics can be relaxed to allow atoms to denote false at the slight cost of adding existence conditions to the logic and changing the substitution rule. Another extension would be to add transition names to the logic.

A Answers to exercises

Answer to exercise 1 The proofs are:

(i)

\frac{Γ ⊢ A & B \frac{\overline{A ⊢ A}}{A & B ⊢ A}}{Γ ⊢ A} and \frac{\frac{_{\overline{A ⊢ A} \overline{B ⊢ B}}}{A, B ⊢ A ⊗ B} Γ, A ⊗ B ⊢ C}{Γ, A, B ⊢ C}

(ii)

\frac{\frac{\frac{\frac{\overline{A ⊢ A}}{A ⊢ A ⊕ B} \overline{C ⊢ C}}{A, (A ⊕ B) ⊸ C ⊢ C}}{(A ⊕ B) ⊸ C ⊢ A ⊸ C} \frac{\frac{\frac{\overline{B ⊢ B}}{B ⊢ A ⊕ B} \overline{C ⊢ C}}{B, (A ⊕ B) ⊸ C ⊢ C}}{(A ⊕ B) ⊸ C ⊢ B ⊸ C}}{(A ⊕ B) ⊸ C ⊢ (A ⊸ C) & (B ⊸ C)}

(iii)

\frac{\frac{\frac{_{\overline{A ⊢ A} \overline{B ⊢ B}}}{A, B ⊢ A ⊗ B}}{A, B ⊢ (A ⊗ B) ⊕ (A ⊗ C)} \frac{\frac{_{\overline{A ⊢ A} \overline{C ⊢ C}}}{A, C ⊢ A ⊗ C}}{A, C ⊢ (A ⊗ B) ⊕ (A ⊗ C)}}{\frac{A, (B ⊕ C) ⊢ (A ⊗ B) ⊕ (A ⊗ C)}{A ⊗ (B ⊕ C) ⊢ (A ⊗ B) ⊕ (A ⊗ C)}} and

\frac{\frac{\overline{A ⊢ A} \frac{\overline{B ⊢ B}}{B ⊢ B ⊕ C}}{A, B ⊢ A ⊗ (B ⊕ C)}}{A ⊗ B ⊢ A ⊗ (B ⊕ C)} \frac{\frac{\overline{A ⊢ A} \frac{\overline{C ⊢ C}}{C ⊢ B ⊕ C}}{A, C ⊢ A ⊗ (B ⊕ C)}}{A ⊗ C ⊢ A ⊗ (B ⊕ C)}
(A ⊗ B) ⊕ (A ⊗ C) ⊢ A ⊗ (B ⊕ C)

Answer to exercise 4

(i) p ≤ q ⇔ p∨q = q ⇔ r⊗(p∨q) = r⊗q ⇔ r⊗p∨r⊗q = r⊗q ⇔ r⊗p ≤ r⊗q.

(ii) only if: r ⊗ p ≤ q ⇒ r ≤ ⋁{r′ | r′ ⊗ p ≤ q} = p ⊸ q. if: Notice that (p ⊸ q) ⊗ p = (⋁{r | r ⊗ p ≤ q}) ⊗ p = ⋁{r ⊗ p | r ⊗ p ≤ q} ≤ q and hence by monotonicity r ≤ p ⊸ q ⇒ r ⊗ p ≤ (p ⊸ q) ⊗ p ≤ q.

Answer to exercise 7 [[d]]_{N} = \{\underline{d}, \underline{a} + \underline{b}, \underline{c}\} [[d ⊗ e]]_{N} = \{\underline{d} + \underline{e}, \underline{a} + \underline{b} + \underline{c}, 2\underline{c}, \underline{a} + \underline{b} + \underline{e}, \underline{d} + \underline{c}, \underline{c} + \underline{e}\} [[d & e]]_{N} = \{\underline{c}\} [[b ⊸ d]]_{N} = \{\underline{a}\} [[c ⊸ d]]_{N} = \{\underline{0}\} Answer to exercise 9

(i) A ⊕ (B ⊗ C) ⊧ (A ⊕ B) ⊗ (A ⊕ C) does not hold in general. Take e.g. the net N without transitions, but with the places a, b and c. Then [[a]]_{N} = \underline{a} etc., so [[a ⊕ (b ⊗ c)]]_{N} = \{\underline{a}, \underline{b} + \underline{c}\} and [[(a ⊗ b) ⊕ (a ⊗ c)]]_{N} = \{\underline{a} + \underline{b}, \underline{a} + \underline{c}\}. That is ⊈.

(ii) From the same example it follows that (A ⊕ B) ⊗ (A ⊕ C) ⊧ A ⊕ (B ⊗ C)

cannot hold neither. Answer to exercise 12

(i) The following statements hold:

⊧ (c_{1} ⊸ w_{1}) ⊸ F, because [[c_{1} ⊸ w_{1}]]_{N} = ∅ |̸= (w_{1} ⊸ c_{1}) ⊸ F, because [[w_{1} ⊸ c_{1}]]_{N} ⊇ \{\underline{a}, \underline{b}, \underline{c} + 2\underline{a}, …\} |̸= (m_{0} ⊸ c_{1} ⊗ c_{2}) ⊸ F, because [[m_{0} ⊸ c_{1} ⊗ c_{2}]]_{N} ⊇ \{m_{0} + \underline{a}, …\}

(ii)

\frac{\frac{\frac{_{\overline{w_{1} ⊢ w_{1}} \overline{a ⊢ b}}}{w_{1}, a ⊢ w_{1} ⊗ b} \overline{w_{1} ⊗ b ⊢ c_{1}}}{w_{1}, a ⊢ c_{1}} \frac{\overline{w_{1} ⊗ b ⊢ c_{1}}}{w_{1}, b ⊢ c_{1}}}{w_{1} ⊗ (a ⊕ b) ⊢ c_{1}} \overline{w_{2} ⊢ w_{2}}

\frac{\frac{w_{1} ⊗ (a ⊕ b), w_{2} ⊢ c_{1} ⊗ w_{2}}{w_{1} ⊗ (a ⊕ b) ⊗ w_{2} ⊢ c_{1} ⊗ w_{2}}}{⊢ w_{1} ⊗ (a ⊕ b) ⊗ w_{2} ⊸ c_{1} ⊗ w_{2}}

Answer to exercise 13 The statements can be expressed as (i) ⊧_{N_{V}} a^{2} ⊸ (k ⊕ t ⊕ c) (ii) ⊧_{N_{V}} a^{2} ⊸ (k & c) (iii) ⊧_{N_{V}} f ⊸ k ⊗ t ⊗ a (iv) ⊧_{N_{V}} a ⊗ (k & t) ⊗ T ⊸ c ⊗ T

(v) For five pence one can get two cup of coffee and a penny back: ⊧_{N_{V}} f ⊸k^{2}⊗a Answer to exercise 19 ⊧_{N} (a ⊸ b)^{⊥} ⊕ (a ⊸ c).

References

[AD93] G. T. Allwein and J. M. Dunn Dunn. Kripke models of linear logic. The Journal of Symbolic Logic, 58(2):514–545, 1993.

[AJ92] Samson Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. In Rudrapatna Shyamasundar, editor, FST and TCS 12, Foundations of Software Technology and Theoretical Computer Science, New Delhi, India, December 18–20, pages 291–301. Springer-Verlag (LNCS, 652), 1992.

[Asp87] Andrea Asperti. A Logic for Concurrency. manuscript, November 1987.

[AV88] Samson Abramsky and Steve Vickers. Linear Process Logic. Notes by Steve Vickers, 1988.

[Ber78] G. Berry. Stable models of typed λ-calculi. In Fifth International Colloquium on Automata, Languages and Programs, pages 72–89. Springer-Verlag (LNCS 62), 1978.

[Bla92] A. Blass. A game semantics for linear logic. Annals of Pure and Applied Logic, 56:183–220, 192.

[Bro89] Carolyn Brown. Relating Petri Nets to Formulae of Linear Logic. Technical Report ECS LFCS 89-87, University of Edinburgh, 1989.

[Cat] Gian Luca Cattani. An existence predicate for a linear logic of Petri net.

[CGW89] T. Coquand, C. Gunter, and G. Winskel. Domain theoretic models of polymorphism. Information and Computation, 81(2), 1989.

[EW90] Uffe Henrik Engberg and Glynn Winskel. Petri Nets as Models of Linear Logic. In CAAP ’90, Coll. on Trees in Algebra and Programming Copenhagen, Denmark, May 15–18, pages 147–161. Springer-Verlag (LNCS 431), 1990. Appears as Technical Report, DAIMI PB–301.

[EW93] Uffe Henrik Engberg and Glynn Winskel. Completeness Results for Linear Logic on Petri Nets (Extended Abstract). In MFCS ’93, Mathematical Foundations of Computer Science, Gdańsk, Poland, August 30 - September 3. Springer-Verlag (LNCS 711), 1993. Appears as Technical Report, DAIMI PB–435.

[GG89a] Carl Gunter and Vijay Gehlot. A Proof-Theoretic Operational Semantics for True Concurrency. Preliminary Report, 1989.

[GG89b] Carl Gunter and Vijay Gehlot. Nets as Tensor Theories. Technical Report MS-CIS-89-68, University of Pennsylvania, October 1989.

[Gir86] Jean-Yves Girard. The system F of variable types, fifteen years later. Theoretical Computer Science, 45, 1986.

[Gir87] Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50(1):1–102, 1987.

[GL87] Jean-Yves Girard and Yves Lafont. Linear Logic and Lazy Computation. In Proc. TAPSOFT 87 (Pisa), vol. 2, pages 52–66. Springer-Verlag (LNCS 250), 1987.

[Hac76] M. H. T. Hack. Decidability questions for Petri nets. PhD thesis, MIT, 1976.

[Laf88] Yves Lafont. The Linear Abstract Machine. Theoretical Computer Science, 59:157–180, 1988.

[LMSN90] P. Lincoln, J. Mitchell, A. Scedrov, and Shankar N. Decision problems for propositional linear logic. In Foundations of Computer Science (FOCS’90), volume II, pages 662–671, St. Louis, MO, October 1990.

[May84] E. W. Mayr. An algorithm for the general Petri net reachability problem. SIAM Journal of Computing, 13(3):441–459, 1984.

[MOM89] Narciso Martí-Oliet and José Meseguer. From Petri Nets to Linear Logic. In Category Theory and Computer Science, Manchester, UK. Springer-Verlag (LNCS 389), 1989.

[MOM91] Narciso Martí-Oliet and José Meseguer. From Petri Nets to Linear Logic: a Survey. International Journal of Foundations of Computer Science, 2(4):297–399, 1991.

[Rei85] Wolfgang Reisig. Petri Nets, An Introduction, volume 4 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.

[Ros89] Kimmo I. Rosenthal. A Note on Girard Quantales. To appear in: Cah. de Top. et G. D., 1989.

[Sam] G. Sambin. . Manuscript reported to us by Per Martin-Löf.

[Yet] D. Yetter. Quantales and Non-Commutative Linear Logic. (preprint).

Recent Publications in the BRICS Report Series

RS-94-1 Glynn Winskel. Semantics, Algorithmics and Logic: Basic Research in Computer Science. BRICS Inaugural Talk. February 1994, 8 pp.

RS-94-2 Alexander E. Andreev. Complexity of Nondeterministic Functions. February 1994, 47 pp.

RS-94-3 Uffe H. Engberg and Glynn Winskel. Linear Logic on Petri Nets. February 1994, 54 pp.

RS-94-4 Nils Klarlund and Michael I. Schwartzbach. Graphs and Decidable Transductions based on Edge Constraints. February 1994, 19 pp. Appears in: Trees in Algebra and Programming CAAP ’94 (ed. S. Tison), LNCS 787, 1994.

RS-94-5 Peter D. Mosses. Uni�ed Algebras and Abstract Syntax. March 1994, 21 pp. To appear in: Recent Trends in Data Type Speci�cation (ed. F. Orejas), LNCS 785, 1994.

RS-94-6 Mogens Nielsen and Christian Clausen. Bisimulations, Games and Logic. April 1994, 37 pp. Full version of paper to appear in: New Results and Trends in Computer Science, LNCS, 1994.