Electronic Notes in Theoretical Computer Science 17 (1998)

URL: http://www.elsevier.nl/locate/entcs/volume17.html 18 pages

Provability in Intuitionistic Linear Logic from a New Interpretation on Petri nets - extended abstract -

D. Larchey-Wendling and D. Galmiche

LORIA UMR 7503 - Univ. Henri Poincaré Campus Scientifique, BP 239 54506 Vandœuvre-lès-Nancy, France

Abstract

Linear logic is a logic of actions which seems well suited to various computer science applications. From its intrinsic ability to reflect computational resources, it is possible to refine different programming paradigms like formulae-as-types (proofsas-programs) or formulae-as-states (proofs-as-computations) with a finer control on resource management. In the latter case, the correspondence between Intuitionistic Linear Logic (ILL) and Petri nets illustrates the interest of efficient proof search methods for proving specifications or properties of distributed systems. In contrast to existing methods, for instance based on canonical proofs, we propose here to revisit the semantics of ILL and its interpretation on Petri nets to provide new proof techniques for proving or disproving properties. From the relationships between the notions of ordered monoid and of quantale we define a new interpretation of ILL on Petri nets that is complete and verifies the property of finite models. Possible issues would be to derive a new algebraic semantics as basis of proof search and to propose a calculus to effectively build counter-models for ILL.

1 Introduction

Linear logic (denoted LL) [7] is a powerful and expressive logic with connections to a variety of topics in computer science as logic programming, concurrency or functional programming. Works have been devoted to term assignment for Intuitionistic Linear Logic (ILL) [2,11] and classical LL [1] with proposals of linear lambda calculi having important properties as subjectreduction or substitution property. From natural deduction and sequent calculus proof systems of ILL (see appendix A for the ILL sequent calculus) we can investigate the problems of type inference and type safety [11] but also apply the programming with proofs paradigm with possible mechanized program extraction from proofs. In this case, proof search corresponds to

\begin{matrix}c \\ ◯ \end{matrix}1998 Published by Elsevier Science B. V.

Larchey-Wendling and Galmiche

program synthesis and proof normalisation to computation. The correspondence between ILL and Petri nets [12] or predicate ILL and high-level nets [10] justifies the necessity of adequate proof search methods for proving specifications (and synthesising programs). Let us mention that works on linear logic programming [8] and on concurrent programming based on proof-search-as-computation involve also specific logical fragments from ILL. Therefore the study of proof search methods for automatic or interactive theorem proving is essential for such logical frameworks or type-theoretic languages. We have previously studied proof search in ILL that was based on the definition of canonical proofs that are complete w.r.t. provability [5]. In the opposite side from this constructive approach, it could be also very important to be able to capture unprovability for ILL with a new calculus for this logic that could be used effectively to build counter models as it is already done in Intuitionistic Logic (IL) [14]. Here we focus on the relationships between ILL and the Petri nets that can naturally be made into models of ILL in such a way that many properties of nets (one might wish to state) become expressible in the logic [3]. Completeness for the logic with respect to nets as a model has been studied in [4]. For instance, Petri nets form a sound and complete model for the ⊕-free fragment and in the case of the ⊸-free fragment an extra axiom (of distributivity of & over ⊕) is necessary for the completeness. In fact with the given interpretation one cannot state the non-distributivity of & over ⊕, namely that (X ⊕ Y) & Z ⊢ (X ⊕ Z) & (Y ⊕ Z) is not provable in ILL. Then we propose, from a study of the relationships between the notions of ordered monoid and of quantale, to define a new interpretation of ILL on Petri nets that is complete, by opposition to the one of [4], and that can lead to the property of finite models. It is based on the specific construction of a quantale from a commutative monoid with an order and on the definition of a new closure operator such that the new class of quantales we define forms a complete class of models for ILL. Moreover this new closure allows to naturally give a counter example to show that (X ⊕ Y) & Z ⊢ (X ⊕ Z) & (Y ⊕ Z) is not provable in ILL. To complete the result that a Petri net can be viewed as an ordered monoid [4], we show that every ordered monoid can be obtained from a Petri net and that the finiteness is preserved during the construction. Then, as a consequence, Petri nets form a complete class of models for ILL.

Possible issues would be to derive a new algebraic semantics as basis of proof search and to propose a calculus to effectively build counter-models for ILL. Moreover, we could study, from these semantical considerations, a possible and alternative embedding of ILL into IL [13] and its consequence on proof search or refutation search in these logics.

2 From ordered monoids to quantales

Quantales are to ILL what complete Boolean algebras are to classical logic, or what complete Heyting algebras are to intuitionistic logic. They all form a complete class of models for their respective logic, namely ILL in the case of quantales [13,17,20]. In the case of classical logic, there is a very simple way to obtain Boolean algebras from a simple structure by taking the powerset of any set. In the case of IL, constructions also exist like the open sets of a topology, orelse Kripke models [15,19]. In the case of ILL, one may construct a quantale from an intuitionistic phase model [6] and one has a commutative monoid together with a closure operator such that the linear implication ⊸ preserves closed subsets. But it is not easy to build a non-trivial closure with this property on a given commutative monoid.

Here we present another general construction of a quantale starting from a commutative monoid with an extra structure: an order (a preorder would also work) which is compatible with the monoidal operations. We first recall the basic definitions of ordered monoids and quantales and introduce the construction starting from a flat monoid. This general construction is presented with all its properties. It involves the notion of closure which is used to build a complete lattice structure. We define conditions on closure to ensure the preservation of the properties in the quantale and we present a new closure operator derived from the MacNeille completion. We explain why the construction is enough general to ensure the completeness and therefore such quantales form a complete class of models of ILL.

2.1 Some definitions

Ordered monoids have a simple structure. It is mainly a monoid together with an order relation such that the monoidal operation is increasing in both arguments. We will denote by OM the class of ordered monoids.

Definition 2.1 A triplet M = (M, •, ⩽) is called an ordered monoid OM if i) (M, ⩽) is an ordered set. ii) (M, •) is a commutative monoid. iii) (x, y) ↦ x • y is increasing.

We will denote by 1 the unit of the monoid (M, •). Condition iii) is equivalent to the following one: for any x, a, b such that a ⩽ b, we have x•a ⩽ x•b. The commutativity ensures that • is increasing in its two parameters. Let us note that (ℕ, +, ⩽) is an ordered monoid.

Quantales have a richer structure. Indeed, a quantale is already a ordered monoid, but its order structure has all joins and meets (even infinite ones) and consequently it is also a complete lattice. Moreover, the monoidal operation preserves meets. We will denote by Qa the class of quantales.

Definition 2.2 The triplet Q = (Q, ⩽, •) is called a quantale Qa, if

i) (Q, ⩽) is a complete lattice. ii) (Q, •) is a commutative monoid. iii) For all a, (b_{i})_{i} in M, a • (⋁_{i} b_{i}) = ⋁_{i}(a • b_{i}).

\begin{aligned}⊥ • & ⊤ & = & ⊥ \\ m_{i} • & ⊤ & = & ⊤ \\ m_{i} • & ⊥ & = & ⊥ \\ m_{i} • & m_{j} & = & m_{i+j} \end{aligned}

Fig. 1. A simple quantale

Condition iii) is sufficient to prove that • is increasing^{1} . It is known as infinite distributivity and can be compared with intuitionistic infinite distributivity: a ∧ (⋁_{i} b_{i}) = ⋁_{i}(a ∧ b_{i}). In the context of condition i) and ii), condition iii) is equivalent to the existence of a right adjoint to x ∈ Q ↦ a • x, usually denoted y ↦ a ⊸ y, for all a in Q.

The aim consists in building a quantale Q, given an ordered monoid M. The construction should preserve as much as possible structures from M, the most important being the monoidal structure. This preservation is important from the point of view of completeness theorems [19] but also if we want to compute the semantics of formulae. For example, if we want to compute the semantic ⟦A & B⟧ of A & B from the semantics ⟦A⟧ of A and ⟦B⟧ of B, we must compute ⟦A⟧ ∧ ⟦B⟧ in Q. If this last value exists in M and if meets are preserved by the construction then this is the semantics of A & B in Q.

2.2 An example

A first idea consists in starting from a monoid M without an “a priori” order and in putting the flat order on it, therefore identifying the quantales that embed this ordered monoid^{2} .

Let us consider M = ℤ/kℤ = ({m_{0}, …, m_{k−1}}, •), the integers modulo a fixed natural k and let • be the addition of class, hence m_{3} • m_{k−2} = m_{1} for example. This is of course a commutative monoid and even a commutative group. If we consider Q = {m_{0}, …, m_{k−1}} ∪ {⊥, ⊤} with the obvious lattice structure: ⊥ is the least element and ⊤ the greatest, the order on the m_{i} (being flat) is then preserved. The monoidal structure is preserved but it should be extended to ⊥ and ⊤. We can observe that only one extension gives a valid quantale. It is given in figure 1.

What are the applications of such a simple construction? We point out that we already have non-trivial ones. Indeed, if we take the following valuation: ⟦X⟧ = m_{1}, then, the semantics of X^{p} = X ⊗ ⋯ ⊗ X (p times) is m_{p}. Hence, ⟦X^{k}⟧ ⩽ ⟦X^{q}⟧ if and only if m_{0} ⩽ m_{q mod k} if and only if q mod k = 0.

1 Indeed, if a ⩽ b then x • b = x • (a ∨ b) = x • a ∨ x • b. So x • a ⩽ x • b. 2 In this case the preservation of the lattice structure is not the main point because it will be trivially verified.

Proposition 2.3 The sequent X^{k} ⊢ X^{q} is provable in ILL only if we have k divides q.

The simplicity of this construction should not be misleading. Building a quantale from a “flat monoid” is not always so simple as only considering a top and bottom element. Indeed, the preceding construction succeeded because the underlying monoid was regular^{3} . However, it seems that a slight modification would be necessary in case of non regularity to keep the lattice structure.

Let us now compare this construction with the one for Petri nets in [3]. In this case, one used the downward closed subsets of the underlying (pre)order. In case of a flat order, these are all subsets of the monoid and one has a much bigger number of elements in the quantale. But there should exist another general method for such construction leading to smaller quantales than the downward closed subsets method.

2.3 Building complete lattices

There exists a general method to build a complete lattice that is based on the notion of closure [18].

Definition 2.4 A closure ⋆ on a set K is a function that maps a subset X of K to a subset X^{⋆} of K and such that X ⊆ Y^{⋆} ⟺ X^{⋆} ⊆ Y^{⋆}.

There are many examples of closures. For instance, the topological closure where X^{⋆} is the smallest closed set containing X. If you have a (pre)order, we obtain another closure if we take X^{⋆} as the smallest initial segment containing X. The MacNeille completion is also a very important closure operation.

Given a closure ⋆ on a set K, the closed subsets are subsets X of K such that X = X^{⋆} or equivalently subsets of the form X^{⋆}. The set of closed subsets, together with subset inclusion, forms an ordered set which is in fact a complete lattice. We do not give all the details but we simply notice that the meet operation is the subset intersection. We note K^{⋆} for the set of closed subsets.

2.4 How to choose a closure for ordered monoids

Therefore we have a closure ⋆ on the set M, (M, ⩽, •) being an ordered monoid. We introduce two natural conditions to ensure that the complete lattice (M^{⋆}, ⊆) is an extension of (M, ⩽) and we extend the • monoidal operation to M^{⋆}. We first choose a “natural” possible embedding and study the conditions on the closure ⋆ so that this function is indeed an embedding, and also a faithful embedding. Then we introduce an operation ⊗ on M^{⋆} and assume that (M^{⋆}, ⊆, ⊗) forms a quantale. Moreover we require that our previous embedding is a monoidal embedding from (M, •) to (M^{⋆}, ⊗).

3 A monoid is regular if the following property holds: x • y = x • z implies y = z.

2.4.1 A natural embedding of M into M^{⋆} The first point is how can we embed M into M^{⋆}. This is done by taking the closed subset {x}^{⋆} where {x} denotes the singleton set, that is in fact the smallest closed subset containing x. We will also denote this set by x^{⋆} identified with {x}^{⋆}. But what are the conditions such that x ↦ x^{⋆} is an embedding ? We aim at first to have the following one: x ⩽ y implies x^{⋆} ⊆ y^{⋆}, that implies that the downward closure {m ∈ M | m ⩽ x} of x, denoted by ↓x, is included in x^{⋆}. Then for a subset X we have ↓X ⊆ X^{⋆} where

↓X = {m ∈ M | ∃x ∈ X, m ⩽ x}

The reader may notice that X ↦ ↓X is also a closure operator. Then the condition ↓X ⊆ X^{⋆} expresses that X ↦ ↓X is the smallest closure with respect to the family of embedding we have chosen.

We also want x ↦ x^{⋆} to be faithful and consequently to be effectively used in counter examples. Thus the condition becomes: x ⩽ y if and only if x^{⋆} ⊆ y^{⋆}. This condition leads to x^{⋆} = ↓x. Indeed, x ∈ ↓y iff x ⩽ y iff x^{⋆} ⊆ y^{⋆} iff x ∈ y^{⋆}. Then x ↦ ↓x is a faithful embedding. Moreover, any closure that has a faithful embedding must coincide with X ↦ ↓X on singletons. This is the condition we need for our closure.

Proposition 2.5 For any closure ⋆, the function x ↦ x^{⋆} is a faithful ordered embedding if and only if x^{⋆} = ↓x.

2.4.2 Extending the monoidal structure Now we have the condition for x ↦ x^{⋆} to be a monomorphism of ordered sets, i.e. a monotone function. What is the additional condition to obtain a monomorphism of monoids ? We have to define a monoidal operation denoted ⊗ on M^{⋆} assuming that (M^{⋆}, ⊆, ⊗) is a quantale.

Since x ↦ x^{⋆} is a monoid embedding, we have x^{⋆} ⊗ y^{⋆} = (x • y)^{⋆}. Then we observe that for any subset X of M we have X^{⋆} = ⋁ {x^{⋆} | x ∈ X} and consequently X^{⋆} ⊗ Y^{⋆} = ⋁ {(x • y)^{⋆} | x ∈ X, y ∈ Y }. Finally X^{⋆} ⊗ Y^{⋆} = {x • y | x ∈ X, y ∈ Y }^{⋆}. Denoting {x • y | x ∈ X, y ∈ Y } by X •Y, we obtain:

Proposition 2.6 Let ⋆ be a closure, if (M^{⋆}, ⊆, ⊗) is a quantale and the function x ↦ x^{⋆} is a faithful ordered monoid embedding then X^{⋆} ⊗Y^{⋆} = (X • Y)^{⋆}.

Moreover as (M^{⋆}, ⊆, ⊗) is supposed to be a quantale, we have the following: x^{⋆}⊗Y^{⋆} = ⋁ {x^{⋆} ⊗ y^{⋆} | y ∈ Y } = ⋁ {(x • y)^{⋆} | y ∈ Y } = (x • Y)^{⋆} and X •Y^{⋆} ⊆ ⋃ {x^{⋆} ⊗ Y^{⋆} | x ∈ X} ⊆ ⋃ {(x • Y)^{⋆} | x ∈ X} ⊆ (X • Y)^{⋆}.

Proposition 2.7 Let ⋆ be a closure, if (M^{⋆}, ⊆, ⊗) is a quantale and the function x ↦ x^{⋆} is a faithful ordered monoid embedding then X • Y^{⋆} ⊆ (X • Y)^{⋆}.

Let us remind the conditions we have obtained. First, we have

x^{⋆} = ↓x for any x ∈ M  (1)

With this condition, we already know that x ↦ x^{⋆} is a faithful order embedding and that there is at most one possible definition of ⊗ so that it is also an ordered monoid embedding from (M, ⩽, •) to the quantale (M^{⋆}, ⊆, ⊗). The second condition is

X • Y^{⋆} ⊆ (X • Y)^{⋆} for any X, Y ⊆ M  (2)

With these two conditions, we are in position to demonstrate that our hypothesis is verified, i.e., x ↦ x^{⋆} is a faithful ordered monoid embedding and that (M^{⋆}, ⊆, ⊗) is indeed a quantale.

2.5 The construction

Let ⋆ be a closure on M where M = (M, ⩽, •) is an ordered monoid. We suppose that the properties (1) and (2) are verified. M^{⋆} is the set of closed subsets of M with respect to ⋆ and is a complete lattice structure under the subset inclusion ⊆. We define the monoidal operation to be X⊗Y = (X • Y)^{⋆}. Let us prove that (M^{⋆}, ⊗) is a commutative monoid. Then we will prove infinite distributivity and we finally show that x ↦ x^{⋆} is an ordered monoid embedding and that it preserves arbitrary meets.

Let us verify that this ⊗ is indeed a monoidal operation. As 1 is the unit of (M, •), it is clear that 1^{⋆} is the unit of (M^{⋆}, ⊗). Moreover, ⊗ is commutative since • is. The associativity requires our second property: X • (Y ⊗ Z) = X • (Y • Z)^{⋆} ⊆ (X • Y • Z)^{⋆} and so X ⊗ (Y ⊗ Z) ⊆ (X • Y • Z)^{⋆}. The converse is trivial. We obtain X ⊗ (Y ⊗ Z) = (X • Y • Z)^{⋆} and by symmetry (X ⊗ Y) ⊗ Z = (X • Y • Z)^{⋆} which proves associativity.

Infinite distributivity also requires our second property. X • ⋁_{i} Y_{i} = X • (⋃_{i} Y_{i})^{⋆} ⊆ (⋃_{i}(X • Y_{i}))^{⋆} ⊆ ⋁_{i}(X ⊗ Y_{i}). Then we get X ⊗ ⋁_{i} Y_{i} ⊆ ⋁_{i}(X ⊗ Y_{i}). Again the converse is trivial.

It remains to show that x ↦ x^{⋆} is a monoid morphism. Our first condition is needed: x^{⋆} • y^{⋆} ⊆ (x • y)^{⋆} is true because it is the same as ↓x • ↓y ⊆ ↓(x • y) which exactly says that (x, y) ↦ x•y is increasing. And then x^{⋆}⊗y^{⋆} ⊆ (x • y)^{⋆} is true. The converse inclusion is trivial. x ↦ x^{⋆} preserves meets because in any ordered set we have ↓ ⋀_{i} x_{i} = ⋀_{i} ↓x_{i}. With our first condition, we get (⋀_{i} x_{i})^{⋆} = ⋀_{i} x_{i}^{⋆} provided ⋀_{i} x_{i} exists in (M, ⩽).

Theorem 2.8 Let ⋆ be a closure on M where M = (M, ⩽, •) is an ordered monoid, if x^{⋆} = ↓x and X •Y^{⋆} ⊆ (X • Y)^{⋆} then Q = (M^{⋆}, ⊆, ⊗) is a quantale and φ : M → Q defined by φ(x) = x^{⋆} is a faithful ordered monoid embedding that preserves arbitrary meets.

In fact join preservation is more subtle and joins must verify (infinite) distributivity in Q. But no reason imposes this property in the more general case of an ordered monoid. This is the key point of the next section.

One might want to know how to compute the linear implication in Q. Let us recall that in the case of phase semantic [7], this operator is the starting point. Normally, this operator should have the same expression,

X ⊸ Y = {z ∈ M | ∀x ∈ M, x • z ∈ Y }

as for phase semantics and this is indeed the case. For this, we prove that A ⊗ X ⊆ Y ⟺ A ⊆ X ⊸ Y. For the ⇒ case, let a ∈ A. We have to prove a ∈ X ⊸ Y. Let consider x ∈ X, we have a • x ∈ A ⊗ X and then a • x ∈ Y as required. For the ⇐ case, A ⊆ X ⊸ Y ⇒ A • X ⊆ X ⊸ Y • X ⊆ Y. Thus A • X ⊆ Y and as Y is closed, we have A ⊗ X ⊆ Y as required.

2.6 A new closure operator

We have already observe that X ↦ ↓X is a closure. It also satisfies our two properties. Therefore we can built a quantale with this closure and obtain a model of ILL. A similar construction was done in [4] for Petri nets, which can be considered as ordered monoids. But as a semantic of ILL, this closure has two major drawbacks: the first one is that joins are interpreted by unions because the union of initial segments is an initial segment — ↓ ⋃_{i} ↓A_{i} = ⋃_{i} ↓A_{i}. Then as joins “are” unions (in this case) and meets “are” intersections (this is always true), joins and meets distribute over each other. This is the reason why the semantic of Winskel and Engberg is not complete with respect to ILL [4].

Theorem 2.9 For the closure X ↦ ↓X, the quantale obtained from any ordered monoid is distributive as a lattice.

This is not true in general for any quantale. In fact one could think that this is because of the nature of ordered monoids — orelse Petri nets — but we are going to show that it is not the case. The choice of another closure removes the lattice distributivity and then leads to the ILL-completeness.

The MacNeille completion is a well known completion technique that is useful for many completeness theorems. For example, it is used in [18] to prove the completeness of quantales with respect to ILL. We start with it but the initial structure is richer: the Lindenbaum algebra (the algebra of equivalent class of formulae) that enjoys the structure of an ILS-algebra and for which the monoidal operator has a right adjoint. In fact our second property (2) is verified whereas it is not in the more general case of an ordered monoid. Thus the completed structure is indeed a quantale — see [18], algebraic semantic section.

The MacNeille closure is defined as

X^{n} = {z ∈ M | ∀m ∈ M, X ⩽ m ⇒ z ⩽ m}  (3)

where X ⩽ m means that m is above any element of X. X ↦ X^{n} does not verify property (2) in the general case but counter-examples are difficult to find. We will show such counter-example built from a Petri net in section 4.3. Analyzing the failure of the proof is very interesting because it leads us to a generalisation of the MacNeille operator.

Suppose we want to prove the property (2) for X ↦ X^{n}, i.e. X • Y^{n} ⊆ (X • Y)^{n}. Then we take an element x ∈ X and z ∈ Y^{n} and try to prove that x • z ∈ (X • Y)^{n}. We know that for any m, Y ⩽ m ⇒ z ⩽ m. Assuming that X • Y ⩽ m, we aim to obtain x • z ⩽ m. But now we are blocked because we cannot use Y ⩽ m ⇒ z ⩽ m unless the monoidal operator has a right adjoint.

We slightly modify the definition of the MacNeille closure to obtain the following definition:

X^{∘} = {z ∈ M | ∀a, m ∈ M, a • X ⩽ m ⇒ a • z ⩽ m}  (4)

Now we do not need a right adjoint anymore. Indeed, let us prove property (2). Thus we take an element x ∈ X and z ∈ Y^{∘} and try to prove that x • z ∈ (X • Y)^{∘}. We know that for any a, m, a • Y ⩽ m ⇒ a • z ⩽ m. Assuming a • (X • Y) ⩽ m, we want to obtain a • (x • z) ⩽ m that is also (a • x) • z ⩽ m and then, using the hypothesis, it is sufficient to prove (a • x) • Y ⩽ m which is also a • (x • Y) ⩽ m. This is weaker than a • (X • Y) ⩽ m. The property (2) is proved and the property (1) is easy to prove.

Lemma 2.10 The closure ∘ has the two required properties (1) and (2) that lead to a quantale.

In fact the definition (4) is equivalent to the definition (3) if y ↦ x • y as a right adjoint y ↦ x ⊸ y. Then we have obtained another closure operator X ↦ X^{∘} which gives rise to a quantale, like X ↦ ↓X. Let us explore some properties of this closure. We know that the MacNeille completion preserves arbitrary joins in some good cases. As already mentioned, the preservation of all joins cannot be true here for any closure because ordered monoids do not enjoy infinite distributivity. But some joins might be preserved, namely those which distribute over • and these are the joins preserved by our new closure.

Indeed, let x = ⋁_{i} x_{i} in (M, ⩽) (recall that it does not always exist) and suppose that for any a ∈ M, we have a • x = ⋁_{i}(a • x_{i}). We prove that x^{∘} = ⋁_{i} x_{i}^{∘} in (M^{∘}, ⊆). ⋁_{i} x_{i}^{∘} ⊆ x^{∘} is trivial because y ↦ y^{∘} is monotone. Now assume that we have another upper bound X^{∘} of all the x_{i}^{∘} in M^{∘}. Then, for all i, x_{i} ∈ X^{∘}. Let us prove x ∈ X^{∘}. Assuming that a • X ⩽ m, we have to prove a • x ⩽ m. Since x_{i} ∈ X^{∘}, we have a • x_{i} ⩽ m for all i and then ⋁_{i}(a • x_{i}) ⩽ m. Then, using our hypothesis we get a • x ⩽ m as required.

Lemma 2.11 The embedding x ↦ x^{∘} preserves all the joins that distribute over •^{4} .

4 The join x = ⋁_{i} x_{i} distributes over • if for any a ∈ M, we have a • x = ⋁_{i}(a • x_{i}).

2.7 Completeness

We are now in position to give a completeness result for the quantales which are generated using the new closure ∘. In fact, any quantale is isomorphic to a quantale of this kind.

Lemma 2.12 Let Q = (Q, ⩽, •) be a quantale, x ↦ x^{∘} is an isomorphism from Q to (Q^{∘}, ⊆, ⊗).

To prove it we only need to prove that x ↦ x^{∘} is a surjective. Thus we have to prove that any X^{∘} is of the form x^{∘} for some x. This x can be chosen to be ⋁ X. First prove that ⋁ X ∈ X^{∘}. Then assuming that a • X ⩽ m we want to prove a • ⋁ X ⩽ m. But a • ⋁ X = ⋁ a • X because Q is a quantale and since a • X ⩽ m, we obtain ⋁ a • X. We have ⋁ X ∈ X^{∘} and (⋁ X)^{∘} ⊆ X^{∘}. On the other hand, X ⩽ ⋁ X. Thus we have X ⊆ (⋁ X)^{∘} and finally X^{∘} ⊆ (⋁ X)^{∘}.

Theorem 2.13 The class of quantales of the form (M^{∘}, ⊆, ⊗) is a complete class of models of ILL.

Moreover, finiteness is preserved by our construction. From [9], we know that ILL is complete with respect to finite quantales and thus we can deduce another complete class of quantales.

Theorem 2.14 The class of finite quantales of the form (M^{∘}, ⊆, ⊗), where M is finite, is complete class of models of ILL.

2.8 Back to the example

Remember the example of figure 1 in section 2.2. It is easy to prove that this is the quantale you obtain by our construction starting from the flat monoid ℤ/kℤ. In fact, as ℤ/kℤ is a group, • has a right adjoint and as a consequence, we obtain the MacNeille completion.

This example is also interesting in case k ≥ 3. Indeed, in this case you have (m_{0} ∨ m_{1}) ∧ m_{2} = ⊤ ∧ m_{2} = m_{2} and (m_{0} ∧ m_{2}) ∨ (m_{1} ∧ m_{2}) = ⊥ ∨ ⊥ = ⊥ and then the lattice distributivity is not verified.

Proposition 2.15 (X ⊕ Y) & Z ⊢ (X & Z) ⊕ (Y & Z) is not provable in ILL.

As we have already observed, no counter example can be found using the simple closure X ↦ ↓X whereas a very simple one is constructed with X ↦ X^{∘}.

3 Ordered monoids and Petri nets

In this section, we show that the concept of Petri net is more general than the one of ordered monoid. First we show how a Petri net can be viewed like an ordered monoid as in [4]. Then, we show that every ordered monoid can be obtained from a Petri net using this construction. Moreover the finiteness is preserved during this process.

Fig. 2. Example of Petri net.  Fig. 3. Another Petri net.

3.1 Definition and properties of Petri nets

We recall the basics of the theory of Petri nets. They form a model of processes in terms of resources, represented by places which can hold to arbitrary nonnegative multiplicity, and of production or consumption of resources by actions, represented by transitions — see [16] for more details.

Definition 3.1 Let P be a set, we denote by M_{f}(P) the set of finite multisets of elements of P and its elements are called markings. The elements of P are called places. A marking is a distribution of tokens over the places of P. We will generally write M instead of M_{f}(P) for the set of markings. A Petri net is a quadruple R = (P, T,^{•}(·), (·)^{•}) where P is a set of places, T is a set of transitions, and ^{•}(·), (·)^{•} are two functions from T to M_{f}(P).

M_{f}(P) is naturally a structure of commutative monoid, + representing the union of multisets and 0, the empty multiset. In fact, it is the free commutative monoid over P. The behaviour of a net is expressed by describing how markings change as transitions occur. For the markings m, m′ and the transition t ∈ T, we define the firing relation by :

m [t⟩ m′ if ∃e ∈ M, m = e +^{•}t and m′ = t^{•} + e

Intuitively, this means that when one reach the marking m′ from the marking m with a transition t, you have to remove ^{•}t tokens from m getting e and put t^{•} tokens in e getting m′. We now introduce the reachability relation ⇝ which is the preorder induced by [·⟩, that is

m ⇝ m′ if ∃t_{1}, …, t_{n}, m_{1}, …, m_{n−1} such that m [t_{1}⟩ m_{1} … m_{n−1} [t_{n}⟩ m′

In other words, m ⇝ m′ means on can reach m′ from m by a finite number of transitions. As an example, in the Petri net of figure 2, we have the property \underline{a} ⇝ 3\underline{a} by the following transitions \underline{a} [t_{1}⟩ \underline{a} + \underline{b} [t_{3}⟩ 3\underline{a}.

The reachability relation ⇝ is the reflexive and transitive closure of the firing relation and then it is a preorder on M_{f}(P). Moreover, we have the following property expressing that the monoidal operation + is increasing with respect to the ⇝ preorder.

Proposition 3.2 For any marking m_{0}, m, m′ we have m ⇝ m′ implies m_{0} + m ⇝ m_{0} + m′.

3.2 Universal construction of an ordered monoid

From the Petri net, we have a preorder ⇝ and a monoidal structure + respecting the preorder because of proposition 3.2 that can justify the construction by quotient. Let us define the equivalence of markings by:

m ≃ m′ if m ⇝ m′ and m′ ⇝ m

It is easy to prove that ≃ is a congruence. Then the following definitions are correct: [a] ⩽ [b] if a ⇝ b and [a] • [b] = [a + b]. We will denote by M the quotient M_{f}(P)/≃, i.e. the set of markings modulo the ≃ equivalence. Then we have the following:

Lemma 3.3 Let R be a Petri net, 𝔽(R) = (M, ⩽, •) is an ordered monoid where M is the quotient M_{f}(P)/≃.

Let us show that this construction is universal: up to an isomorphism, any ordered monoid can be obtained this way. The method can be described as follows: starting from an (resp. finite) ordered monoid M, we build a (resp. finite) Petri net R and prove that the induced monoid 𝔽(R) is isomorphic to M.

Let M = (M, ⩽, •) be an ordered monoid. We build a Petri net R = (M, T,^{•}(·), (·)^{•}) where places are copies of the elements of M and transitions are of five kinds. For the sake of clarity, we will use the following shape for the elements of M: a, b, c, 1 ∈ M. Places will be denoted by underlining the elements of M like \underline{a}, \underline{b}. Let us recall that 0 denotes the empty multiset and + the union of multisets.

t_{1} ∈ T_{1} \underline{a} [t_{1}⟩ \underline{b}  for a ⩽ b
t_{2} ∈ T_{2} \underline{a} [t_{2}⟩ \underline{b} + \underline{c} for a = b • c
t_{3} ∈ T_{3} \underline{b} + \underline{c} [t_{3}⟩ \underline{a} for a = b • c

t_{4} ∈ T_{4} 0 [t_{4}⟩ \underline{1}_{t_{5} ∈ T_{5} \underline{1} [t_{5}⟩ 0}

Notice that there is only one transition of kind 4 (resp. 5) whereas there are as many transitions of kind 1 as there are pairs (a, b) such that a ⩽ b. The reader may also have noticed that the disjoint union T_{1} ∪ ⋯ ∪ T_{5} is finite if M is a finite set. Then R having a finite number of places which are the elements of M, also has a finite number of transitions. Now we can prove that 𝔽(R) is isomorphic to M. For this, we need two lemmas:

Lemma 3.4 We have \underline{a}_{1} + ⋯ + \underline{a}_{n} ≃ \underline{a_{1} • ⋯ • a_{n}} and as an immediate consequence, the classes [\underline{a}_{1} + ⋯ + \underline{a}_{n}] and [\underline{a_{1} • ⋯ • a_{n}}] are equal.

12 Lemma 3.5 \underline{a}_{1} + ⋯ + \underline{a}_{n} ⇝ \underline{b}_{1} + ⋯ + \underline{b}_{m} in R if and only if a_{1} • ⋯ • a_{n} ⩽ b_{1} • ⋯ • b_{m} in M.

Lemma 3.4 is proved by induction on n using transitions of kind T_{2} and T_{3}. The only if case of lemma 3.5 is proved by induction on the number of transitions while the if case is trivial using lemma 3.4 and one transition of kind T_{1}. The final result is the following:

Lemma 3.6 The function i : M ⟶ M_{f}(M)/ ≃ defined by i(a) = [\underline{a}] is an isomorphism of ordered monoids from M to 𝔽(R).

Indeed, i is an faithful embedding of ordered set because we have a ⩽ b ⟺ \underline{a} ⇝ \underline{b} ⟺ [\underline{a}] ⩽ [\underline{b}] ⟺ i(a) ⩽ i(b). Moreover, i is full because of lemma 3.4: [\underline{a}_{1} + ⋯ + \underline{a}_{n}] = i(a_{1} • ⋯ • a_{n}) and then i is an isomorphism of ordered sets. Moreover, [\underline{a}] • [\underline{b}] = [\underline{a} + \underline{b}] = [\underline{a • b}] and thus i(a) • i(b) = i(a • b). Then i is also a morphism of monoids.

Theorem 3.7 Let M = (M, ⩽, •) be an ordered monoid and R be the Petri net (M, T,^{•}(·), (·)^{•}) previously defined with transitions in T_{1} ∪ ⋯ ∪ T_{5}, 𝔽(R) is an isomorphic copy of M. Moreover, if M is finite then R is a finite Petri net.

We pointed out that another construction is presented in [4] but it does not preserve the finiteness: the constructed Petri net always has an infinite number of transitions. But in fact this point is not so important because having no general completeness, the finite model property was not a priority in [4].

To summarize, we have shown in this section that given a (finite) ordered monoid M, we are able to find a (finite) Petri net, R the underlying ordered monoid 𝔽(R) of which being an exact copy of M. It means that in any construction involving an ordered monoid, it is safe to consider that this ordered monoid comes from a Petri net.

What does this mean in the context of quantales ? We have seen in section 2 that OM is a complete class of models of ILL. But ordered monoids can be replaced by Petri nets and consequently Petri nets are a complete class of models for ILL.

4 From Petri nets to quantales

In this section, we combine the two preceding results to obtain a completeness theorem for Petri nets and the finite model property.

4.1 Comparison with the existing semantics

In [3], Winskel and Engberg presented a semantics of ILL using Petri nets. In section 2, we presented a new semantics of ILL from ordered monoid and in section 3, we explained how to replace ordered monoids by Petri nets. We now compare the two semantics. Let (P, T,^{•}(·), (·)^{•}) be a Petri net. Here are both definitions for which the interpretations are different:

Semantic of Winskel and Engberg

⟦⊥⟧ ∅
⟦A ⊕ B⟧ ⟦A⟧ ∪ ⟦B⟧
⟦A ⊗ B⟧ {m | ∃(a, b) ∈ ⟦A⟧ × ⟦B⟧, m ⇝ a + b}

New semantic derived from OM-semantic

⟦⊥⟧ {m | ∀a, a + m ⇝ 0}
⟦A ⊕ B⟧ {m | ∀k, n, k + (⟦A⟧ ∪ ⟦B⟧) ⇝ n ⇒ k + m ⇝ n}
⟦A ⊗ B⟧ {m | ∀k, n, k + ⟦A⟧ + ⟦B⟧ ⇝ n ⇒ k + m ⇝ n}

For the other connectives, the definitions are the same:

\begin{matrix}⟦⊤⟧ & M_{f}(P) \\ ⟦1⟧ & \{m | m ⇝ 0\} \\ ⟦\underline{a}⟧ & \{m | m ⇝ \underline{a}\} \end{matrix}  \begin{matrix}⟦A & B⟧ & ⟦A⟧ ∩ ⟦B⟧ \\ ⟦A ⊸ B⟧ & \{m | ∀a ∈ ⟦A⟧ a + m ∈ ⟦B⟧\} \end{matrix}

This does not mean that a formula of type A & B has the same semantic in both models. In fact, the semantic ⟦A⟧ and ⟦B⟧ might already be different in case we have an internal ⊕ for example.

In figure 3, there is an example of Petri net for which the two semantics are different. Indeed, let us define X to be the smallest closed set containing the marking \underline{a}, i.e. ⟦X⟧ = (3ℕ + 1)\underline{a} and Y be the smallest containing 2\underline{a}, ⟦Y ⟧ = (3ℕ + 2)\underline{a}. The semantics of X and Y are the same in both cases — Winskel and Engberg or the new semantic. But the semantics of X ⊕ Y is not the same anymore. Indeed, in Winskel and Engberg’s case, we get ⟦X ⊕Y ⟧ = (3ℕ+\{1, 2\})\underline{a} whereas in the new semantics, we get ⟦X ⊕Y ⟧ = ℕ\underline{a}. For that, we observe that the number of occurrences of \underline{a} in the markings is preserved modulo 3 by any transition t_{1} or t_{2}. Then, for any natural k, there is no natural n such that (3ℕ + \{1, 2\} + k)\underline{a} ⇝ n\underline{a}.

4.2 Completeness

The previous results from section 2 and 3 can be combined to obtain a completeness result for Petri nets as well as a finite model property. Indeed, given a (finite) quantale Q, we find a (finite) Petri net R representing its underlying ordered monoid 𝔽(R) ≃ Q. The semantics of ILL within this Petri net R is

Fig. 4. A Petri net that does not satisfy property (2) for the MacNeille closure.

the same as the semantics for the underlying ordered monoid 𝔽(R) and by isomorphism, it is the same as the semantics in Q.

Theorem 4.1 A formula A of ILL is provable if and only if its semantics verifies ⟦1⟧ ⊆ ⟦A⟧ in every Petri net. This property is still true if we only consider finite Petri nets.

4.3 Some examples

Let us come back to the example of figure 3. We also define Z to be the smallest closed set containing 0, ⟦Z⟧ = ⟦1⟧ = 3ℕ \underline{a}. Then we have ⟦X & Y ⟧ = ⟦X⟧ ∩ ⟦Y ⟧ = ∅ and ⟦X & Y ⟧ ⊕ Z = ⟦Z⟧ = 3ℕ \underline{a}. On the contrary, ⟦X ⊕ Z⟧ = ⟦Y ⊕ Z⟧ = ℕ \underline{a} as already noticed. Then ⟦(X ⊕ Z) & (Y ⊕ Z)⟧ is not included in ⟦(X & Y) ⊕ Z⟧.

Proposition 4.2 (X ⊕ Z) & (Y ⊕ Z) ⊢ (X & Y) ⊕ Z is not provable in ILL.

Let us present now a last example. We remind that we were obliged to modify the MacNeille closure to obtain the property X • Y^{⋆} ⊆ (X • Y)^{⋆}. We exhibit in figure 4 a Petri net that does not satisfy this property for the MacNeille closure X ↦ X^{n}. In this case the monoidal operation • is usually denoted by + because it is the “sum” of multisets.

We define X = \{\underline{a}\} and Y = \{\underline{b}_{1}, \underline{b}_{2}\}. Then after a computation, we obtain: X^{n} = ↓\underline{a} = \{\underline{a}\} and Y^{n} = \{\underline{k}, \underline{b}_{1}, \underline{b}_{2}\}. Moreover, we have X + Y^{n} = \{\underline{a} + \underline{k}, \underline{a} + \underline{b}_{1}, \underline{a} + \underline{b}_{2}\}. Now, let us evaluate (X + Y)^{n} = \{\underline{a} + \underline{b}_{1}, \underline{a} + \underline{b}_{2}\}^{n}. It is clear that \{\underline{a} + \underline{b}_{1}, \underline{a} + \underline{b}_{2}\} ⇝ \underline{c}. It is also true that \underline{a} + \underline{k} ⇝̸ \underline{c} even if it is less clear how to prove it. Then \underline{a} + \underline{k} ∉ \{\underline{a} + \underline{b}_{1}, \underline{a} + \underline{b}_{2}\}^{n} and we have X + Y^{n} ⊈ (X + Y)^{n}.

Proposition 4.3 There are ordered monoids for which the MacNeille closure does not satisfy the property X • Y^{n} ⊆ (X • Y)^{n}. The Petri net of figure 4 is such an example.

5 Concluding remarks

What about the computation of the semantics function? For Winskel and Engberg’s semantics, we had an intuitive understanding of what the semantics represents. It does not seem as obvious with our new semantics. Moreover, computing the semantics function is not easy in many cases since we have to verify a property for an infinite number of markings k: k + A ⇝ m implies k + z ⇝ m. However, we could directly consider the closure of Winskel and Engberg’s semantics as a lower approximation of the new semantics to have an idea of what it might be. All along this paper, we have shown how ordered monoids or Petri nets can provide concise counter examples revealing the unprovability of formulae of ILL. Small examples were presented to show that ⊕ and ⊗ do not distribute over each other in ILL for example, something that was not feasible with the initial Petri net semantics. The search of counter models is a complementary tool to proof search and in this context, the semantical considerations are important, especially when only simple structures like Petri nets are involved.

Possible issues of this revision of the ILL semantics would be to derive a new algebraic semantics as basis of proof search and to propose a calculus to effectively build counter-models for ILL. Moreover, we could study, from these semantical considerations, a possible and alternative embedding of ILL into IL [13] and its consequences on proof search or refutation search in these logics.

References

[1] S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1-2):3–58, 1993.

[2] N. Benton, G. Bierman, V. de Paiva, and M. Hyland. A term calculus for intuitionistic linear logic. In Int. Conference on Typed Lambda Calculi and Applications, LNCS 664, pages 75–90, Utrecht, The Netherlands, March 1993.

[3] U. Engberg and G. Winskel. Petri Nets as Models of Linear Logic. In CAAP 90, LNCS 431, pages 144–161, Copenhagen, Denmark, May 1990.

[4] U. Engberg and G. Winskel. Completeness results for linear logic on Petri nets. Annals of Pure and Applied Logic, 86:101–135, 1997.

[5] D. Galmiche and E. Boudinet. Proof search for programming in Intuitionistic Linear Logic. In CADE-12 Workshop on Proof Search in Type-Theoretic Languages, Nancy, France, June 1994.

[6] Jean-Yves Girard. Linear Logic, its syntax and semantics. In Lafont Girard and Regnier, editors, Advances in Linear Logic. Cambridge University Press, 1995.

[7] J.Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–102, 1987.

[8] J.S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In 6th IEEE Symposium on Logic in Computer Science, pages 32–42, Amsterdam, The Netherlands, July 1991.

[9] Yves Lafont. The finite model property for various fragments of linear logic. Journal of Symbolic Logic, 62(4):1202–1208, 1997.

[10] J. Lilius. High-level nets and linear logic. In 13th Int. Conference on Applications and Theory of Petri Nets, LNCS 616, pages 310–327, Sheffield, UK, 1992.

[11] P. Lincoln and J. Mitchell. Operational aspects of linear lambda calculus. In 7th IEEE Symposium on Logic in Computer Science, pages 235–246, Santa-Cruz, California, 1992.

[12] J. Meseguer and N. Marti-Oliet. From Petri nets to Linear Logic. Mathematical Structures in Computer Science, 1:69–101, 1991.

[13] Sara Negri. Semantical observations on the embedding of Intuitionistic Logic into Intuitionistic Linear Logic. Mathematical Structures in Computer Science, 5:41–68, January 1995.

[14] L. Pinto and R. Dyckhoff. Loop-free construction of counter-models for intuitionistic propositional logic. In Behara and al., editors, Symposia Gaussiana, pages 225–232, 1995.

[15] H. Rasiowa and R. Sikorski. The Mathematics of Metamathematics, volume 41 of Monografie Matematyczne. Polska Akademia Nauk, Warszawa, 1963.

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

[17] Kimmo I. Rosenthal. Quantales and their applications. Research Notes in Mathematics, 1990.

[18] A. S. Troelstra. Lectures on Linear Logic, volume 29 of Center for the Study of Language and Information. CSLI, 1992.

[19] A. S. Troelstra and D. van Dalen. Constructivism in Mathematics, an Introduction, volume 2 of Studies in Logic and the foundations of Mathematics, pages 705–719. North-Holland, 1988.

[20] D. N. Yetter. Quantales and (noncommutative) Linear Logic. Journal of Symbolic Logic, 55:41–64, 1990.

Larchey-Wendling and Galmiche

A Sequent calculus for ILL

Identity / Cut rules

A ⊢ A Id  \begin{matrix}Γ, A ⊢ B & Δ ⊢ A \\ Γ, Δ ⊢ B \end{matrix} Cut

Logical rules

\begin{matrix}Γ ⊢ A \\ Γ, 1 ⊢ A \end{matrix} 1-L  ⊢ 1 1-R
Γ, ⊥ ⊢ A ⊥-L  Γ ⊢ ⊤ ⊤-R
\begin{matrix}Γ, A, B ⊢ C \\ Γ, A ⊗ B ⊢ C \end{matrix} ⊗-L  \begin{matrix}Γ ⊢ A & Δ ⊢ B \\ Γ, Δ ⊢ A ⊗ B \end{matrix} ⊗-R
\begin{matrix}Γ, A ⊢ C & Δ, B ⊢ C \\ Γ, Δ, A ⊕ B ⊢ C \end{matrix} ⊕-L  \begin{matrix}\begin{matrix}Γ ⊢ A \\ Γ ⊢ A ⊕ B \end{matrix} & ⊕-R_{1} \\ \begin{matrix}Γ ⊢ B \\ Γ ⊢ A ⊕ B \end{matrix} & ⊕-R_{2} \end{matrix}
\begin{matrix}\begin{matrix}Γ, A ⊢ C \\ Γ, A & B ⊢ C \end{matrix} & &-L_{1} \\ \begin{matrix}Γ, B ⊢ C \\ Γ, A & B ⊢ C \end{matrix} & &-L_{2} \end{matrix}  \begin{matrix}Γ ⊢ A & Γ ⊢ B \\ Γ ⊢ A & B \end{matrix} &-R
\begin{matrix}Γ ⊢ A & Δ, B ⊢ C \\ Γ, Δ, A ⊸ B ⊢ C \end{matrix} ⊸-L  \begin{matrix}Γ, A ⊢ B \\ Γ ⊢ A ⊸ B \end{matrix} ⊸-R