Electronic Notes in Theoretical Computer Science ?? (2000)

URL: http://www.elsevier.nl/locate/entcs/volume??.html 15 pages

Quantales as completions of ordered monoids: Revised semantics for Intuitionistic Linear Logic

D. Larchey-Wendling and D. Galmiche

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

Abstract The aim of this paper is to propose a unified analysis of the relationships between the notions of order and closure and to relate it to different semantics of Intuitionistic Linear Logic (ILL). We study the embedding of ordered monoids into quantales and then we propose general constructions and results about such an embedding. Therefore we obtain a new semantics based on ordered monoids and also new completeness results for ILL.

1 Introduction

Linear logic (denoted LL) [8] is a powerful and expressive logic with connections to a variety of topics in computer science as logic programming, concurrency or functional programming [2]. In this context, Intuitionistic Linear Logic (ILL) [4,14] and some of its sub-fragments are often used as the underlying logic of logical frameworks. There exists different semantics of ILL based on phases spaces [8], quantales [20] and Petri nets [15]. The completeness for ILL with respect to Petri nets as a model has been studied in [6]. For instance, Petri nets form a sound and complete model for the ⊕-free fragment of ILL and in the case of the ⊸-free fragment an extra axiom (of distributivity of & over ⊕) is necessary for the completeness. In fact with the classical interpretation of [6] one cannot establish the non-distributivity of & over ⊕, namely that (X ⊕ Y) & Z ⊢ (X ⊕ Z) & (Y ⊕ Z) is not provable in ILL. It is important to understand if it is due to the nature of Petri nets or to other semantical reasons. Thus, to have a better understanding of ILL semantics and their relationships with IL semantics, we have developed an analysis of ILL semantics from the point of view of the relationships between the notions of order and closure. Then we propose a general construction of quantales from ordered monoids based on a particular analysis of closure. It naturally leads to the

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

A ⊢ A id  \begin{matrix}Γ ⊢ A & A, Δ ⊢ B \\ Γ, Δ ⊢ B \end{matrix} cut
{Γ ⊢ A \atop Γ, 1 ⊢ A} 1_{L} ⊢ 1 1_{R} Γ, ⊥ ⊢ A ⊥_{L} Γ ⊢ ⊤ ⊤_{R}
{Γ, A, B ⊢ C \atop Γ, A ⊗ B ⊢ C} ^{⊗^{L}}  \begin{matrix}Γ ⊢ A & Δ ⊢ B \\ Γ, Δ ⊢ A ⊗ B \end{matrix} ^{⊗^{R}}
\begin{matrix}Γ ⊢ A & Δ, B ⊢ C \\ Γ, Δ, A ⊸ B ⊢ C \end{matrix} ^{⊸^{L}}  {Γ, A ⊢ B \atop Γ ⊢ A ⊸ B} ^{⊸^{R}}
{Γ, A ⊢ C \atop Γ, A & B ⊢ C} ^{&^{L}} {Γ, B ⊢ C \atop Γ, A & B ⊢ C} ^{&^{L}} \begin{matrix}Γ ⊢ A & Γ ⊢ B \\ Γ ⊢ A & B \end{matrix} ^{&^{R}}
\begin{matrix}Γ, A ⊢ C & Γ, B ⊢ C \\ Γ, A ⊕ B ⊢ C \end{matrix} ^{⊕^{L}} {Γ ⊢ A \atop Γ ⊢ A ⊕ B} ^{⊕^{R}} {Γ ⊢ B \atop Γ ⊢ A ⊕ B} ^{⊕^{R}}

Fig. 1. The IMALL sequent calculus

definition of a new closure operator such that the new class of quantales we define is 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 [16] and its consequences on proof search or refutation search in these logics.

2 Intuitionistic Linear Logic

Linear logic (LL) and its intuitionistic fragment are used in several areas of computer science. Some works tried to find optimizations in functional programming language implementations by using linear logic as a type system [1,14]. Other applications deal with concurrent logic programming [3,10,11]. From the specification point of view, ILL provides a natural and simple encoding of Petri net reachability [15]. The sequent calculus of the propositional multiplicative and additive fragment of ILL is presented in figure 1. For a complete presentation of the system we refer to [8].

Our main interest consits of an unified analysis of ILL semantics, having in mind the relationships between the notions of order and provability through the soundness theorem. Then, we will consider the provability or non-provability problems from a semantical point of view. In fact, the phase semantics [9] and Petri net semantics of ILL [6] will be latter mentioned as important examples to illustrate our results on the embedding of ordered monoids into quantales.

3 Ordered monoid extensions

In this section, we describe a method to build quantales [20] from weaker structures that are ordered monoids. Such structures, compared to quantales, lack a complete lattice structure, i.e. least upper and greatest lower bounds. We describe a method to enrich an ordered monoid with a complete lattice structure. This method is based on the notion of closure and has already been studied [17,18]. We provide an algebraic characterization of our construction in a category of completions.

For the sake of clarity, we will start by presenting the partial order case before we add a monoidal structure. This will lead us to a generalization of the Mac-Neille construction [5].

3.1 Basic definitions and notations

In this section we recall the notions of poset, embedding, complete lattice, monoid, ordered monoid and quantale. Here are some notational conventions.

The calligraphic letters K, P, L, Q, … usually denote sets with some additional structure. Uppercase letters X, Y, … denote subsets of these sets with usually no additional structure. The symbol ℙ(K) denotes the powerset of the set K, i.e. the set of all the subsets of K. Finally, lowercase letters x, y, … denote elements of sets K or subsets X.

The symbol ℕ denotes the set of natural numbers, ℤ the set of integers, ℚ the set of rational numbers and ℝ the set of reals.

Definition 3.1 (Poset) A pair (P, ⩽) is called a poset (partially ordered set) if P is a set and ⩽ is an order relation over P, i.e. a relation which is reflexive, antisymmetric and transitive.

For example, (ℕ, ⩽) where ⩽ is the natural ordering on natural numbers is a poset. By an abuse of language, we will often speak of the poset P, omitting the order. We will also write X ⩽ y for ∀x ∈ X, x ⩽ y, i.e. when y is an upper bound of X. Conversely, we write y ⩽ X when y is a lower bound of X.

Definition 3.2 (Embedding) Let P and Q be two posets, a function i : P → Q is an embedding if for any x, y ∈ P we have x ⩽ y ⇔ i(x) ⩽ i(y).

In other words, i is an monotonic function which is also injective. If P is embedded into Q by i then the image i(P) is isomorphic to P and the isomorphism is the restriction of i. For example, the identity map is an embedding of (ℕ, ⩽) into (ℚ, ⩽).

Definition 3.3 (Complete lattice) A pair (L, ⩽) is called a complete lattice if it is a poset and L has all least upper bounds, i.e. for any subset X ⊆ L, X has a least upper bound in L denoted by ⋁X.

For example, the set of subsets (ℙ(X), ⊆) ordered by inclusion is a complete lattice where the least upper bound is simply the union of subsets.

Proposition 3.4 If (L, ⩽) is a complete lattice then any subset X ⊆ L also has a greatest lower bound.

The reader is reminded that greatest lower bounds are obtained by the following identity: ⋀Y = ⋁{z | z ⩽ Y }. For a more detailed introduction to lattices, see [5].

Definition 3.5 (Monoid) A pair (M, •) is called a (commutative) monoid if • is a binary operator on the set M, which is (commutative,) associative and has a neutral element denoted by 1.

For example, (ℕ, +) is a (free) commutative monoid with neutral element 0. We remind the reader that the neutral element is unique and is also called the unit of the monoid. The operation • can be extended to subsets of M by the following definition: X • Y ≜ {x • y | x ∈ X and y ∈ Y }. This is the same definition as the concatenation of the set of words in the free non-commutative monoid.

Definition 3.6 (Ordered monoid) A triplet (M, •, ⩽) is called a (commutative) ordered monoid if (M, ⩽) is a poset, (M, •) is a (commutative) monoid and (x, y) ↦ x • y is monotonic in x and y.

For example, (ℕ, +, ⩽) is an ordered monoid. Any monoid may be extended an ordered monoid by putting the flat order^{1} on it.

Definition 3.7 (Quantale) A triplet (Q, •, ⩽) is called a (commutative) quantale if it is a (commutative) ordered monoid, (M, ⩽) is a complete lattice and for any a, (b_{i})_{i} in Q, a • ⋁_{i} b_{i} = ⋁_{i}(a • b_{i}).

This last condition is called infinite distributivity and expresses a kind of continuity for •. For example, ({⊥} ∪ ℕ ∪ {∞}, +, ⩽) and ([0, n], max, ⩽) are two quantales.

3.2 Closures

In this section we present the notion of closure which is widespread in many areas of mathematics. It is very simple and general and it will help us in extending a poset to a complete lattice, a process known as completion.

Definition 3.8 (Closure) Let K be a set, a closure on K is an unary operator (·)^{⋆} : ℙ(K) → ℙ(K) such that for all subsets X, Y and K,

X ⊆ Y^{⋆} ⇔ X^{⋆} ⊆ Y^{⋆}

A closed subset is a subset X of the form Y^{⋆}.

By an abuse of notation we will often denoted the subset {x}^{⋆} by x^{⋆} identifying the point x with the singleton {x}. In general it does not lead to ambiguities. Closures are very common in different domains; for example we can mention the transitive closure, logical closure, topological closure, algebraic closure, normalization processes, modal operators …

Proposition 3.9 If (·)^{⋆} is a closure on a set K then for any X and Y, the following three properties hold: X ⊆ X^{⋆}, X ⊆ Y ⇒ X^{⋆} ⊆ Y^{⋆} and X^{⋆}^{⋆} ⊆ X^{⋆}.

1 By definition x ⩽ y ⇔ x = y, i.e. x is only comparable to x.

The proof is trivial. A closed subset is of the form X^{⋆}. It is then equivalent to X = X^{⋆}. The set of closed subsets will be denoted by K^{⋆}. It is naturally ordered by inclusion of subsets.

Theorem 3.10 Let K be a set and (·)^{⋆} be a closure on K, let K^{⋆} be the set of closed subsets then (K^{⋆}, ⊆) is a complete lattice.

Proof. Let (X_{i})_{i} be a family of closed subsets of K. Then ⋁_{i} X_{i} = (⋃_{i} X_{i})^{⋆} is the least upper bound of the X_{i}’s.

As a remark, the greatest lower bound is the intersection ⋂_{i} X_{i}. The least element is ∅^{⋆} and the greatest is K considered as a closed subset of K.

Definition 3.11 (Compatible closure) Let (P, ⩽) be a poset and (·)^{⋆} be a closure on P, (·)^{⋆} is said to be compatible if for any x ∈ P, x^{⋆} = {z | z ⩽ x}.

We define ↓X ≜ {z | ∃x ∈ X, z ⩽ x}, the initial segment of the subset X. It is important to notice that ↓X is not the set of lower bounds of X. Then ↓(·) is a compatible closure. Moreover, (·)^{⋆} is compatible if and only if ↓x = x^{⋆} and then if and only if for any subset ↓X ⊆ X^{⋆}.

We can also defined X^{n} ≜ {x | ∀z ∈ P, X ⩽ z ⇒ x ⩽ z} which is known as the Mac-Neille closure. See [5] for more details on closures.

Theorem 3.12 The set of compatible closure ordered point-wise by inclusion is a complete lattice. The least compatible closure is ↓(·) and the greatest compatible closure is (·)^{n}.

Proof. The point-wise non-empty intersection of compatible closures is a compatible closure so we have a complete lattice.^{2} ↓(·) is the least because ↓X = ⋃_{x∈X} ↓x ⊆ ⋃_{x∈X} x^{⋆} ⊆ X^{⋆}. Let (·)^{⋆} be any compatible closure, let us now show that X^{⋆} ⊆ X^{n}. Let x ∈ X^{⋆} and k be such that X ⩽ k. Then X^{⋆} ⊆ k^{⋆} and x ∈ k^{⋆} i.e. x ⩽ k. Consequently x ∈ X^{n}.

Now we consider a central point of the paper. Given a compatible closure, one can embed a poset into a complete lattice preserving some properties.

Lemma 3.13 Let (P, ⩽) be a poset and (·)^{⋆} be a compatible closure. Then the function i : P → P^{⋆} defined by i(x) ≜ x^{⋆} is an embedding of P in the complete lattice P^{⋆}. This embedding preserves greatest lower bounds provided they exist in P.

Proof. For any x, y ∈ P we have x^{⋆} ⊆ y^{⋆} ⇔ x ∈ y^{⋆} ⇔ x ⩽ y. Moreover let a = ⋀_{k} b_{k} exist in P, we prove that i(a) = ⋀_{k} i(b_{k}). Let X be a subset of P, X^{⋆} ⊆ ⋀_{k} i(b_{k}) ⇔ ∀k X ⊆ b_{k}^{⋆} ⇔ ∀k X ⩽ b_{i} ⇔ X ⩽ a ⇔ X^{⋆} ⊆ i(a).

Proposition 3.14 The Mac-Neille closure (·)^{n} also preserves least upper bounds which exist.

2 To be precise, we also need a greatest element for the empty intersection but it is provided a few lines later.

Proof. Let us suppose a = ⋁_{k} b_{k}. For any subset X of P, we have a ∈ X^{n} ⇔ ∀k b_{k} ∈ X^{n} — this is not always true for any compatible closure. We suppose ∀k b_{k} ∈ X^{n} then X ⩽ z implies ∀k b_{k} ⩽ z and we have a ⩽ z. Thus a ∈ X^{n} and finally ⋁_{k} i(b_{k}) ⊆ X^{n} ⇔ ∀k b_{k} ∈ X^{n} ⇔ a ∈ X^{n} ⇔ i(a) ⊆ X^{n}.

Let us give an example to compare the Mac-Neille closure and the initial segment closure. On this example, we can see that ↓(·) does not preserve the least upper bound 3 = 1 ∨ 2.

⟵^{↓(·)}  ⟶^{(·)^{n}}

3.3 The category of ⋁-completions

In this section we define the notion of ⋁-completion from an abstract point of view. We show that the use of closures is a very natural and generic way to build completions. In this section (P, ⩽) is a fixed poset.

Definition 3.15 (⋁-completions and their morphisms) A pair (i, L) is a ⋁-completion of P if L is a complete lattice and i : P → L is an poset embedding such that ∀l ∈ L, ∃X ⊆ P, l = ⋁i(X). A function f : L_{1} → L_{2} is a ⋁-completion morphism f : (i_{1}, L_{1}) → (i_{2}, L_{2}) if f is monotonic, preserves least upper bounds and commutes with i_{1} and i_{2}, i.e. i_{2} = f ∘ i_{1}.

[figure: L_{1}; f; L_{2}; P; ⊂; i_{2}; i_{1}; ⊃]

The condition ∀l ∈ L, ∃X ⊆ P, l = ⋁i(X) expresses the fact that the process of extending P does not add unreachable points.

Proposition 3.16 If a morphism f : (i_{1}, L_{1}) → (i_{2}, L_{2}) exists then it is unique.

Proof. Let l ∈ L_{1}, there exist a subset X of P such that l = ⋁i_{1}(X). Then we have f(l) = f(⋁i_{1}(X)) = ⋁f ∘ i_{1}(X)) = ⋁i_{2}(X). This last value is independent of f.

Theorem 3.17 (Equivalence) ⋁-completions of P form a category which is equivalent to the poset of compatible closures over P.

Proof. We prove the equivalence according to [12]. We define the function 𝔽(i, L)(X) ≜ {z | i(z) ⩽ ⋁i(X)}. It is easy to show that this is a compatible closure and therefore we have a map from ⋁-completions to compatible closures. If f : (i_{1}, L_{1}) → (i_{2}, L_{2}) is a morphism then we can easily show that for any X 𝔽(i_{1}, L_{1})(X) ⊆ 𝔽(i_{2}, L_{2})(X) holds. Thus, 𝔽 is a functor between two posets (which are a particular case of category). Moreover, this functor is full and faithfull (always true for posets.) Let (·)^{⋆} be a compatible closure and let us consider the embedding i : (P, ⩽) → (P^{⋆}, ⊆) defined in proposition 3.13. We have 𝔽(i, (P^{⋆}, ⊆))(X) = X^{⋆}. Indeed z ∈ 𝔽(i, (P^{⋆}, ⊆))(X) ⇔ i(z) ⩽ ⋁i(X) ⇔ z^{⋆} ⊆ ⋁_{x∈X} x^{⋆} ⇔ z^{⋆} ⊆ X^{⋆} ⇔ z ∈ X^{⋆}. It concludes the proof that 𝔽 is an equivalence of categories (in fact of posets in our case).

As a conclusion, we have provided an algebraic characterization of the notion of compatible closure in terms of ⋁-completion. The Mac-Neille closure corresponds to the terminal element of this category.

We can now extend the notion of completion to ordered monoids and then deduce an extension of the Mac-Neille construction in that case.

3.4 Completion of ordered monoids

In this section we adapt the previous results to the case of ordered monoids.

Definition 3.18 (Stable closure) A closure on the monoid (M, •) is stable if for any X, Y ⊆ M, X • Y^{⋆} ⊆ (X • Y)^{⋆} holds.

The stability condition can be compared to the condition for X ⊸Y^{⋆} to be closed^{3} that arises in the phase space semantics of linear logic. In fact, both notions are the same. Moreover, stability can also be related to the continuity axiom [19]: in this case, continuity is equivalent to stability of (·)^{n} but we will discuss this point in section 5.4.

Definition 3.19 (Pretopology) A closure on the ordered monoid (M, •, ⩽) which is compatible and stable is called a pretopology [18].

For example, the initial segment closure ↓(·) is a pretopology. The Mac-Neille closure is not a pretopology. A counter example will be provided in section 4.2. Let us now introduce an extension of the Mac-Neille closure.

Lemma 3.20 Let (·)^{⋆} be a pretopology on the ordered monoid (M, •, ⩽), the set of closed subsets (M^{⋆}, •, ⊆) is a quantale. If i is defined by i(x) ≜ x^{⋆} then i : M → M^{⋆} is an ordered monoid embedding.

Proof. As (X^{⋆} • Y^{⋆})^{⋆} = X^{⋆} • Y^{⋆}, • is a monoidal operation over M^{⋆} with unit 1^{⋆}. Since proposition 3.10, we already know that (M^{⋆}, ⊆) is a complete lattice. It is also clear that • is increasing. Thus, it remains to prove the infinite distributivity. Let X, Y be arbitrary subsets of M.

X^{⋆} • ⋁_{i} Y_{i}^{⋆} = X^{⋆} • (⋃_{i} Y_{i})^{⋆} = (X • ⋃_{i} Y_{i})^{⋆} = (⋃_{i} X • Y_{i})^{⋆} = ⋁_{i} X^{⋆} • Y_{i}^{⋆}

3 Where ⊸ is defined by X ⊸ Y ≜ {z | ∀x ∈ X, z • x ∈ Y }.

We already know that i is a poset embedding and i is also a monoid morphism because i(x • y) = (x • y)^{⋆} = ({x} • {y})^{⋆} = {x}^{⋆} • {y}^{⋆} = i(x) • i(y).

Thus, we can view pretopologies as a convenient way to build quantales. Examples will be provided later. Is there a structure on the set of pretopologies as it is the case with posets and compatible closures?

Theorem 3.21 If there is a greatest pretopology, the set of pretopologies ordered point-wise by inclusion is a complete lattice. The least element is ↓(·).

Proof. The (point-wise) non-empty intersection of stable closures is a stable closure.

The next result provides us the greatest element. The pretopology which is introduced has already been presented in previous papers [7,17] but the following characterization is new.

Theorem 3.22 Let (M, •, ⩽) be an ordered monoid, we define the operator (·)^{∘} by X^{∘} = {z | ∀a, b ∈ M, a • X ⩽ b ⇒ a • z ⩽ b}. Then (·)^{∘} is the greatest pretopology.

Proof. (·)^{∘} is a closure. If z ∈ x^{∘} then since 1 • x ⩽ x we have 1 • z ⩽ x i.e. z ⩽ x. Thus x^{∘} ⊆ ↓x. If z ⩽ x and a • x ⩽ b then a • z ⩽ a • x ⩽ b. Therefore ↓x = x^{∘} and the closure (·)^{∘} is compatible.

Let x ∈ X and y ∈ Y^{∘}, we show that x • y ∈ (X • Y)^{∘}. Let a, b be such that a•(X •Y) ⩽ b. Then (a•X)•Y ⩽ b and so (a•x)•Y ⩽ b. Since y ∈ Y^{∘}, we deduce (a • x) • y ⩽ b and so a • (x • y) ⩽ b. Thus, X • Y^{∘} ⊆ (X • Y)^{∘}. The closure (·)^{∘} is stable.

We prove now that we have the greatest pretopology. Let (·)^{⋆} be any pretopology and x ∈ X^{⋆}. Let a, b be such that a • X ⩽ b. Then a • X^{⋆} ⊆ (a • X)^{⋆} ⊆ b^{⋆} because of stability and consequently a • x ∈ b^{⋆}. Then by compatibility, a • x ⩽ b. This proves that x ∈ X^{∘} and then X^{⋆} ⊆ X^{∘}.

We point out the fact that when the monoidal translation x • (·) has a right adjoint x⊸(·) in the ordered monoid, then X^{∘} = X^{n} for any X. That is the reason why it is possible to use the Mac-Neille closure in the phase space completion.

Definition 3.23 (⋁-completion) A pair (i, Q) is a ⋁-completion of the ordered monoid M if Q is a quantale and (i, Q) is a ⋁-completion of the poset (M, ⩽). Moreover i has to be a monoid morphism, i.e. i(x • y) = i(x) • i(y). A morphism f : (i_{1}, Q_{1}) → (i_{2}, Q_{2}) is a ⋁-completion morphism for the poset case which is also a monoid morphism.

This defines a category and a morphism between two completions is unique. The proof is the same as in proposition 3.16. This category is the algebraic counterpart of the notion of pretopology.

Theorem 3.24 (Equivalence) The category of ⋁-completions of the ordered monoid M is equivalent to the poset of pretopologies over M.

Proof. 𝔽 is defined exactely as before. Then 𝔽(i, Q)(·) is a compatible closure. We prove it is also stable. Let x ∈ X and y ∈ 𝔽(i, Q)(Y). Then i(y) ⩽ ⋁i(Y). i(x • y) = i(x) • i(y) ⩽ i(x) • ⋁i(Y) ⩽ ⋁i(x) • i(Y) ⩽ ⋁i(X • Y). Then x • y ∈ 𝔽(i, Q)(X • Y) and we have stability X • 𝔽(i, Q)(Y) ⊆ 𝔽(i, Q)(X • Y). The rest of the proof, i.e. proving that 𝔽 is an equivalence of categories, is the same as in the proof of theorem 3.17.

Now from our algebraic characterization, we can study our greatest pretopology (·)^{∘} in deeper details and analyse if the good properties of the Mac-Neille closure for posets are inherited by (·)^{∘}.

4 Properties of the greatest pretopology

In this section we are going to prove that the greatest pretopology (·)^{∘} preserves a lot of the initial structure of the ordered monoid M. From a semantical point of view, if we interpret ILL-formula then it means that their meaning can almost be evaluated inside M.

4.1 Preservation properties

Proposition 4.1 Let (M, •, ⩽) by an ordered monoid, we have

(1) If a = ⋀_{i} b_{i} then a^{∘} = ⋀ b_{i}^{∘}

(2) 1^{∘} = 1 and (b • c)^{∘} = b^{∘} • c^{∘}

(3) If a = b ⊸ c then a^{∘} = b^{∘} ⊸ c^{∘}

(4) If ⊤ exists then ⊥^{∘} is the greatest element

Proof. (1) and (4) are straightforward. (2) comes from stability. Now suppose that a = b ⊸ c exist, i.e. for any x, x • b ⩽ c ⇔ x ⩽ a. Then for any X, X^{∘} • b^{∘} ⊆ c^{∘} ⇔ (X • b)^{∘} ⊆ c^{∘} ⇔ X • b ⩽ c ⇔ X ⩽ a ⇔ X^{∘} ⊆ a^{∘} and then (3) is proved.

It only remains the cases of least upper bounds and the greatest element. As a first observation, we point out the fact that they cannot always be preserved because infinite distributivity does not always hold in ordered monoids. Thus preserved lubs should at least verify infinite distributivity. This necessary condition is in fact a sufficient condition.

Lemma 4.2 If a = ⋁_{i} b_{i} exists in M and is distributive, i.e. for all x in M we have x • a = ⋁_{i} x • b_{i} then a^{∘} = ⋁_{i} b_{i}^{∘}.

Proof. Let us first prove that a ∈ X^{∘} ⇔ ∀i b_{i} ∈ X^{∘}. The direct side is trivial. The reverse is more tricky. Suppose α • X ⩽ β. Then, as b_{i} ∈ X^{∘}, we have α • b_{i} ⩽ β and so ⋁_{i} α • b_{i} ⩽ β. By distributivity, we obtain α • ⋁_{i} b_{i} ⩽ β and we obtain α • a ⩽ β. This is for any α, β and so a ∈ X^{∘}. We finally obtain a^{∘} ⊆ X^{∘} ⇔ a ∈ X^{∘} ⇔ ∀i b_{i} ∈ X^{∘} ⇔ ⋃_{i} b_{i}^{∘} ⊆ X^{∘} ⇔ ⋁_{i} b_{i}^{∘} ⊆ X^{∘}. Consequently a^{∘} = ⋁_{i} b_{i}^{∘}.

As a remark, we observe that ⊥ may not be preserved. We obtain the condition x • ⊥ = ⊥ which is not always true in ordered monoids — but it is true in quantales.

4.2 Examples

In this section we apply our greatest pretopology construction to build examples of quantales. The proofs are not given.

\begin{matrix}(ℕ, +, ⩽) & ⟶^{(·)^{∘}} & (\{[0, n[ | n ∈ ℕ\}, +, ⊆) \\ (ℚ, +, ⩽) & ⟶^{(·)^{∘}} & (ℝ ∪ \{−∞, +∞\}, +, ⩽) \end{matrix}

The case of ℕ is interesting because the least element 0 is not preserved as an example of what we said in section 4.1.

A trivial method to build ordered monoids is to consider the flat order structure on any monoid. Even though the order is the same in all cases, the obtained lattice is not always the same when completed with (·)^{∘}.

Proposition 4.3 If the flat monoid M is regular then M^{∘} = M ∪ {⊥, ⊤} with ⊥ • x = ⊥ and for x ≠ ⊥, ⊤ • x = ⊤.

A monoid is regular if • is erasable, i.e. a • x = b • x implies a = b. This is the case for free monoids (multisets) like ℕ or for groups like ℤ/pℤ but there exist non-regular monoids. The structure obtained by completion is described by the following figure.

\begin{aligned}⊥ • & ⊤ & = & ⊥ \\ m • & ⊤ & = & ⊤ \\ m • & ⊥ & = & ⊥ \end{aligned}

As an example of non-regular flat monoid, we can consider for a fixed natural n the monoid ([0, n], max). It is not regular because max(0, n) = max(1, n). The structure obtained is described in the next figure for n = 3. We can show that ∅^{∘} = ∅, x^{∘} = {x} and if X has more than two elements then X^{∘} = [0, max X].

([0, 3], max, flat)^{∘}

This last example is interesting because the Mac-Neille closure (·)^{n} is not stable on ([0, 3], max, flat). Indeed, {0, 1}^{n} = [0, 3] because 0 and 1 have no common upper bound in the flat order. But {2}max{0, 1} = {2}. So

{2}max{0, 1}^{n} = {2, 3} ⊈ {2} = ({2}max{0, 1})^{n}

5 Semantics of ILL

In this section we present completeness results for a semantics based on the completion-as-pretopology method we have presented. This result and our methodology are compared to previous results. The important point is that our methodology generalises other approaches.

5.1 Completeness

We observe that the greatest pretopology has very nice preservation properties. It partially conserves the initial structure.

Lemma 5.1 If Q is a quantale then it can be viewed as an ordered monoid and in this case, we can complete it with (·)^{∘}. In this case (Q^{∘}, ⊆) is isomorphic to Q.

The proof is trivial because all the structure is preserved and since anything in the completion is a lub, the embedding is surjective. This result gives rise to completeness results for ILL derived from the fact that quantales are a complete algebraic semantic for ILL.

Theorem 5.2 The classes of ordered monoids, Petri nets, finite ordered monoids and finite Petri nets are all complete classes of models for ILL.^{4}

These results have already been proved in previous papers [7,13]. They are compared in section 5.3 to the completeness results obtained for Petri nets in which the semantics is (unfortunately) distributive [6]. In contrast, our semantics is not distributive as shown by the following proposition.

Proposition 5.3 The quantale (ℤ/3ℤ, +, flat)^{∘} obtained by completion of the flat cyclic group, is a counter-model of (A ⊕ B) & C ⊢ (A & C) ⊕ (B & C).

Proof. Indeed, as shown in proposition 4.3, this quantale is not distributive as a lattice.^{5} Then let us define ⟦A⟧ ≜ 0^{∘}, ⟦B⟧ ≜ 1^{∘}, ⟦C⟧ ≜ 2^{∘}. Then ⟦A⊕B⟧ = ⊤ and ⟦(A⊕B)&C⟧ = 2^{∘}. But ⟦A&C⟧ = ⟦B &C⟧ = ⊥ and thus ⟦(A⊕B)&C ⊢ (A & C)⟧ = ⊥. Or 2^{∘} ⩽̸ ⊥.

5.2 Phase spaces

Phases spaces form the initial complete semantics for ILL[9]. The algebraic semantics based on quantales [20] appeared later. However the completeness

4 ILL without exponentials. 5 In fact, it is exactly one of the two minimal non-distributive lattices.

theorem for phase spaces can be viewed as the construction of a quantale using the well known Lindenbaum construction.

In the case of (commutative) linear logic, we view the set of contexts (multisets of formulae) as a (pre)ordered monoid, the order being logical deductibility. Linear implication ⊸ provides a right adjoint to the addition of contexts (the monoidal operation) and so X^{∘} = X^{n} (see section 5.4).

Then it is possible to build a quantale on the top of this ordered monoid using the Mac-Neille closure as a pretopology. And in this quantale, it is possible to interpret contexts as themselves (as it is the case for the Lindenbaum construction) providing a semantics equal to logical deductibility.

Then completeness for phase spaces can be viewed as a particular case of completion of an ordered monoid of contexts into a quantale.

5.3 Petri nets

In [6], a semantics of ILL based on Petri nets is presented. As explained in [13], Petri nets can be viewed as a graphical representation of (pre)ordered monoids if we ignore their operational aspects. A quantale is built on the top of these Petri nets to provide a semantical interpretation of ILL.

But this semantics is not fully complete because distributivity holds in their quantales. Therefore completeness is only achieved at the price of removing one of the two operators ⊕ or & to ILL. One may argue that this feature is related to the choice of Petri nets as a basis for the semantics. In the light of our based-on-closure completion, we can prove that this is not founded. Indeed in [6], the pretopology ↓(·) is used to build quantales on the top of Petri nets. Distributivity is inevitable because lubs are unions with this closure. But choosing another closure, namely (·)^{∘}, leads to completeness for all ILL, even if we start from ordered monoids coming from Petri nets.

5.4 Continuity axiom

The continuity axiom is introduced in [19] to ensure that a quantale can be obtained as the completion of an ordered monoid using the Mac-Neille completion. Continuity is a property of an ordered monoid expressed by:

For all a, b, p if ∀q(∀z(a • z ⩽ b ⇒ z ⩽ q) ⇒ p ⩽ q) then a • p ⩽ b

Continuity is related to stability by the following lemma.

Lemma 5.4 An ordered monoid is continuous if and only if its Mac-Neille closure is stable.

Proof. We rewrite continuity in a more readable form. Let us define

X_{a,b} ≜ {x | a • x ⩽ b}

We point out the fact that X_{a,b} is often written a ⊸ b. Then continuity can be read as

For all a, b, p if ∀q(X_{a,b} ⩽ q ⇒ p ⩽ q) then p ∈ X_{a,b}

Using the Mac-Neille closure, we rewrite this as ∀a, b X_{a,b}^{n} ⊆ X_{a,b}. Then continuity corresponds to X_{a,b} being Mac-Neille closed for all a, b.

For any subset X, we also have the identity

X^{∘} = ⋂{X_{a,b} | X ⊆ X_{a,b}}

As an intersection of Mac-Neille closed subsets, X^{∘} is Mac-Neille closed, i.e. X^{∘} = X^{∘}^{n} which leads to X^{n} ⊆ X^{∘}^{n} ⊆ X^{∘}. The converse inclusion being trivial. And so the Mac-Neille closure is stable if continuity holds.

Conversely, if (·)^{n} is stable then it is a pretopology and as X^{∘} ⊆ X^{n} and (·)^{∘} is the greatest pretopology, X^{∘} = X^{n}. Or X_{a,b}^{∘} = X_{a,b} and so X_{a,b}^{n} = X_{a,b} which is equivalent to continuity.

We can then read the semantical developments of [19] as a particular case of our order monoid completion, i.e. when the Mac-Neille closure is the greatest pretopology.

6 Conclusion

In this paper, we have considered an alternative and unified analysis of semantics of ILL that leads to new results about completeness and also nonprovability in this logic. It is developed from the point of view of the relationships between the notions of order and closure and leads to a general construction of quantales from ordered monoids based on a fine analysis of closure. A new closure operator is defined in such a way we can propose a complete class of models for ILL. To complete these results, we have proved in [13] that every ordered monoid can be obtained from a Petri net and that the finiteness is preserved during the construction. Therefore, as a natural consequence, Petri nets form a complete class of models for ILL. Moreover these results can be extended to the case of non-commutative logic. As consequences, we have shown how ordered monoids or Petri nets can provide concise counter-examples revealing the non-provability of formulae of ILL such as the distributivity property that was not feasible with the initial Petri net semantics [6,7]. In fact, the search of counter-models is a complementary and powerful tool for proof-search and in this context, the based-on semantics considerations are important. 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 [16] 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] V. Alexiev. Applications of Linear Logic to Computation: An Overview. Logic Journal of the IGPL, 2(1):77–107, 1994.

[3] J.M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992.

[4] 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.

[5] B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge Mathematical Textbooks. Cambridge University Press, 1990.

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

[7] D. Galmiche and D. Larchey-Wendling. Provability in intuitionistic linear logic from a new interpretation on petri nets - extended abstract. Electronic Notes in Theoretical Computer Science, 17, 1998.

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

[9] J.Y. Girard. Linear logic: its syntax and semantics. In J.Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 1–42. Cambridge University Press, 1995.

[10] J. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. Journal of Information and Computation, 110:327–365, 1994.

[11] N. Kobayashi and A. Yonezawa. ACL - a concurrent linear logic programming paradigm. In Int. Symposium on Logic Programming, pages 279–294, Vancouver, October 1993.

[12] S. Mac Lane. Categories for the Working Mathematicians. Graduate Texts in Mathematics. Springer-Verlag, 1971.

[13] D. Larchey-Wendling and D. Galmiche. From ordered monoids to quantales and petri nets: Revised semantics and completeness results in intuitionistic linear logic. Submitted for publication, Oct. 1998.

[14] 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.

[15] J. Meseguer and N. Marti-Oliet. From Petri nets to Linear Logic. Math. Struct. in Comp. Science, 1:69–101, 1991.

[16] S. Negri. Semantical observations on the embedding of Intuitionistic Logic into Intuitionistic Linear Logic. Math. Struct. in Comp. Science, 5:41–68, 1995.

[17] H. Ono. Substructural Logics, volume 2 of Studies in Logic and Computation, chapter Semantics for Substructural Logics. Oxford Science Publications, 1993.

[18] G. Sambin. Substructural Logics, volume 2 of Studies in Logic and Computation, chapter Semantics of Pretopologies. Oxford Science Publications, 1993.

[19] A. Ursini. Semantical Investigations of Linear Logic.

   http://www.csl.sri.com/linear/ursini-paper.dvi.gz.

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