JAIST Repository

JAIST Repository

https://dspace.jaist.ac.jp/

Title

Author(s)

Citation

Issue Date

Type

Text version

URL

Rights

Description

by

Keiko Ishihara

submitted to

Japan Advanced Institute of Science and Technology

in partial fulllment of the requirements

for the degree of

Doctor of Philosophy

Supervisor: Professor Kunihiko Hiraishi

School of Information Science

Japan Advanced Institute of Science and Technology

August 28, 2001

Copyright2001byKeikoIshihara

The connection between linear logic and Petri nets has recently been a subject of great

interest. In theseresearches, the propositionalfragment of intuitionisticlinearlogic with

exponential! was considered, and Petri nets were related to linear logic as follows: each

place of a Petri net is regarded as an atomic proposition of linear logic, and transitions

as provabilityrelation.

Soundness and completenessof linearlogic are proved for algebraicstructures, called

quantales. Engberg and Winskel showed soundness of linear logic for quantales induced

fromPetrinets,butforthesequantalescompletenesswasnotvalid. Soundnessstatesthat

all provable properties (formulas) in linear logic hold in Petri nets, while completeness

states that properties which hold in any Petri net can be proved in linear logic. When

both of soundness and completenessare validinsome quantales induced fromPetri nets,

wecansaythatapropertyisprovableinlinearlogicifand onlyifitisacommonproperty

of Petri nets, i.e., itholds in any Petri net.

Recently Engberg and Winskelhavealsoproved completeness of at-freefragmentof

linearlogicandlinearlogicwithdistributivity. OneofdiÆculties inprovingcompleteness

forfulllinearlogicliesindistributivityofuovert,i.e.,Au(BtC))(AuB)t(AuC),

whichdoesnotholdinlinearlogic. ThequantalesconstructedbyEngbergandWinskelare

distributive lattices, i.e., distributivity is always valid. Therefore, to prove completeness

usingtheirquantales,wehavetodealwiththet-freefragmentortoaddthedistributivity

to linear logic as an axiom. However these are not what we intend to do. Although

there should be argument about which of full linear logic or a logic with distributivity

is appropriate for representing properties of Petri nets, we here concentrate on proving

completenessforfulllinearlogic. TondadequatelogicsforwhichthemodelsofEngberg

and Winskel are complete is another interesting problem.

In this thesis, we rst construct non-distributive quantales, i.e., quantales in which

distributivity is not always valid, from Petri nets, and prove completeness of linear logic

withoutexponentialfor the quantales. Inlinear logic, exponential! isadded tocompen-

sate the absence of the rules of weakening and contraction. For example, !A indicates

that we may extract as many data of type A as we like, i.e., a datum of type !A is a

nitecollectionof dataof typeA. ForPetri nets, we canregard aplacewith exponential

! as a place which can supply arbitrary many but nite resources (tokens, in petri net

terminology) by ring transitions. We extend the construction of the quantales to those

with exponential, and prove completenessof linearlogic for the quantales. It meansthat

properties which hold in any Petri nets with such exponential places can be proved in

linear logic.

We also give an impression on the meaning of the logic on the proposed Petri net

model, comparing with that by Engberg and Winskel.

1 Introduction 1

2 Preliminaries 6

2.1 BasicAlgebraic Structures . . . 6

2.1.1 Multisets . . . 6

2.1.2 Monoids and Ordered Structures . . . 7

2.1.3 Meets and Joins . . . 9

2.1.4 Lattices . . . 12

2.2 Fixed Point Theorem . . . 16

3 Petri Nets 19 3.1 Petri Nets and Multisets . . . 19

3.2 Reachability Relation . . . 21

4 Quantales and Closure Operations 24 4.1 IL-algebrasand Quantales . . . 24

4.1.1 IL-algebras . . . 24

4.1.2 Quantales . . . 26

4.2 ClosureOperations onIL-algebrasand Quantales . . . 28

4.2.1 ClosureOperation . . . 28

4.2.2 ClosureOperation onIL-algebras . . . 29

4.2.3 ClosureOperation onQuantales . . . 30

4.2.4 ClosureOperation C 1 and C 2 . . . 33

4.3 Quantales with Exponential . . . 35

4.3.1 Exponentialon Quantales . . . 35

4.3.2 FS-quantales and Quantales with Exponential . . . 36

5 Intuitionistic Linear Logic without Exponential 40 5.1 Syntax . . . 40

5.1.1 Formulas. . . 40

5.1.2 Sequents . . . 41

5.1.3 Axioms(initial sequents) and Rules . . . 41

5.1.4 Examples of Proofs . . . 42

5.1.5 Relationbetween Linear Logic and Petri Nets . . . 44

5.2 Semantics . . . 46

5.2.1 ValuationonQuantale . . . 46

5.2.2 Validity . . . 46

5.2.3 Soundness . . . 47

6 Intuitionistic Linear Logic 57

6.1 Syntax . . . 57

6.1.1 Formulas. . . 57

6.1.2 Sequents . . . 58

6.1.3 Axioms(initial sequents) and Rules . . . 58

6.1.4 Examples of Proofs . . . 60

6.1.5 Relationbetween the exponential and Petri Nets. . . 62

6.2 Semantics . . . 63

6.2.1 ValuationonQuantale . . . 63

6.2.2 Validity . . . 64

6.2.3 Soundness . . . 64

6.3 Completeness . . . 67

6.3.1 Completeness for FS-Linear Logic . . . 69

6.3.2 Completeness for Linear Logic . . . 72

7 Interpretation on Petri Nets 76 7.1 Interpretation of C 1 and C 2 . . . 76

7.2 Dierence between C 1 and C 2 . . . 77

7.3 Interpretation of Exponential! . . . 84

7.4 Another Interpretation . . . 85

7.5 Relationof Linear Logic, Models and Petri Nets . . . 87

8 Concluding Remarks 89

Introduction

Linear Logic, introducedby J.Y. Girard in1987 [19], isinteresting fromapurely logical

point of view, and potentially of considerable interest for computer science [20, 24, 26,

27, 30, 45]. Linear logic (intuitionistic, classical and predicate) are obtained by deleting

the contraction and the weakening rules from standard sequent calculus formulations of

corresponding logics. Linear logic may be viewed as an example of a resource conscious

logic, where the formulas represent types of resource, and resources cannot be used ad

libitum. That is to say, asserting a sequent A;A ) B means something like: we use

two data (resources) of type Ato obtain one datumof type B. In Gentzen-style 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 formulas A

1

;:::;A

n

(we shall use capital

Greek letters as an abbreviation for a sequence of formulas). The calculus has the two

structuralrulesforaddingavacantassumptionandremovingofaduplicateofassumption,

)B

;A)B

(weakening )

;

;A;A)B

;A)B

(contraction)

:

In the presence of these rules the following two rules for conjunction

)A )B

;)AuB (1)

;

)A )B

)AuB (2)

become interderivable in the sense that the rst rule can be derived from the second by

weakening,andthesecondfromtherstbycontraction. Inintuitionisticlinearlogicthese

rules (weakening and contraction) are deleted and the rule of (1) and (2) are no longer

interderivable. Withoutthem, propositions cannotbeintroducedarbitrarilyintoalistof

assumptionand aduplicationinthe listcannotberemoved. It isinthissense thatlinear

logic is aresource conscious logic.

In theyears 1960-1962,CarlAdam Petri dened Petrinets whichisageneralpurpose

mathematicalmodel fordescribing relations existing between conditions and events [40].

Petri nets consist of two types of elements, places and transitions. Each place models a

process in terms of types of resources, and can hold arbitrary nonnegative multiplicity.

orproducedby actions. Theyaredescribedusingthenotionofmultisets. Amultisetover

a set P isa function, m:P !N [9,18,32, 41].

Theconnectionbetween linearlogicandPetrinetshas recentlybeenasubjectofgreat

interest [7, 8, 15, 16, 17, 29, 34, 35]. Girard's linear logic has a great deal of interest in

how might be useful in the theory of parallelism. In these researches, the propositional

fragmentofintuitionisticlinearlogicwithexponential! [47]wasconsidered,andPetrinets

were relatedto linear logic as follows: each place of a Petri net is regarded as an atomic

propositionsoflinear logic,and transitionsasprovability relation. Inthe sequel, weshall

simply use the word \linear logic" to denote the propositional fragment of intuitionistic

linear logic.

Soundness and completenessof linearlogic are proved for algebraicstructures, called

quantale [1,5, 19, 21, 22, 39, 47]. Engberg and Winskel [15] showed soundness of linear

logic forquantales induced fromPetri nets, but forthese quantalescompleteness wasnot

valid. Soundness theorem states that all provable properties (formulas) in linear logic

hold in Petri nets, while completeness theorem states that properties which hold in any

Petri net can be proved in linear logic. When both of soundness and completeness are

validinsome quantales inducedfromPetri nets,wecan saythat apropertyisprovable in

linear logic if and only if itis acommon property of Petri nets, i.e., it holds inany Petri

net.

Recently Engberg and Winskel have also proved completeness of a t-free fragment

of linear logic and linear logic with distributivity [16, 17]. One of diÆculties in proving

completenessforfull linearlogic liesindistributivityofu overt. Althoughthe following

proof shows that

(AuB)t(AuC))Au(BtC)

is derivable in linearlogic,

A)A

AuB )A

(u1))

B )B

B )BtC

()t1)

AuB )BtC

(u2))

AuB )Au(BtC)

()u) (a)

;

A)A

AuC )A

(u1))

C )C

C )BtC

()t2)

AuC )BtC

(u2))

AuC )Au(BtC)

()u) (b)

;

and from (a)and (b), we can get

AuB )Au(B tC) AuC )Au(BtC)

(AuB)t(AuC))Au(BtC)

(t))

;

we cannotprove the sequent

Au(BtC))(AuB)t(AuC):

That is,the distributivityof uover tdoesnot hold inlinearlogic. Withthe contraction

and weakening rules, we can prove this as follows:

A;B )A

(weakening )

A;B )B

(weakening )

A;B )AuB

()u)

A;B )(AuB)t(AuC)

()t1) (a)

;

A)A

A;C )A

(weakening)

C )C

A;C )C

(weakening)

A;C )AuC

()u)

A;C )(AuB)t(AuC)

()t2) (b)

;

and from (a)and (b), we can get

A;B )(AuB)t(AuC) A;C )(AuB)t(AuC)

A;BtC )(AuB)t(AuC)

Au(BtC);Au(BtC))(AuB)t(AuC)

(u1and u2))

Au(BtC))(AuB)t(AuC)

(contraction)

(t))

:

The quantales constructed in [15, 16, 17] are distributive lattices. Therefore, to prove

completeness using their quantales, we have to deal with the t-free fragment or to add

the distributivity to linear logic as an axiom. However these are not what we intend to

do.

Thereisafamilyofsubstructurallogics,suchasrelevantlogics,inwhichdistributivity

isvalid. Ithas been pointed outthat semanticconsiderationsofsubstructurallogicstend

towardvalidatingdistribution,andprooftheoreticconsiderationstendtowardinvalidating

it (see [13]). Although there should be argument about which of full linear logic or a

logic with distributivity is appropriate for representing properties of Petri nets, we here

concentrateonprovingcompletenessforfulllinearlogic. Tondadequatelogicsforwhich

the models of [15, 16, 17] are complete isanotherinteresting problem.

The key element is the way of the construction of quantales. When we construct

the quantales, we use a closure operation. We introduce two closure operations C

1 and

C

2

. Let X = hM;;;ei be a preordered commutative monoid. We dene two closure

operations C

1

and C

2

onP(X). C

1

is anoperation onP(X)such that

C

1

X :=fy2M j9x2X(y x)g;

and C

2

isan operationon P(X)such that

C

2

X :=(X

!

) ;

where

X

!

:=fy 2M j8x2X(xy)g

and

X :=fy2M j8x2X(y x)g:

C

1

isusedin[15,16,17],andC

2

,whichiscalledtheMacNeillecompletionofX [23,31],is

used inthis thesis. In the quantales constructed from Petri nets using C

1

, distributivity

2

is not always valid.

In this thesis, we rst construct non-distributive quantales, i.e., quantales in which

distributivity is not always valid, from Petri nets, and prove completeness of linear logic

withoutexponentialfor the quantales.

Moreover, we extend the quantales to the quantales with exponential. In linearlogic,

exponential ! is added to compensate the absence of the rules of weakening and con-

traction. For example, !A indicates that we may extract as many data of type A as we

like, i.e., a datum of type !A is a nite collection of data of type A. For Petri nets, we

can regard a place with exponential ! as a place which can supply arbitrary many but

nite resources (tokens, in Petri net terminology) by ring transitions. We extend the

constructionof the quantales tothose withexponential,and prove completenessoflinear

logic for the quantales. It means that properties which hold in any Petri nets with such

exponentialplaces can be proved in linearlogic.

There are two approaches to construct a Petri net model in which completeness of

linear logic holds; one is introducing distributivity in the logic, and the other is the

approach taken in this thesis, i.e., making anon-distributivemodel by usingappropriate

closure operation.

From the practical point of view, the former approach may be useful in dealing with

propertiesofPetrinet. ThequantaleconstructedinthisthesisseemsstrangefromaPetri

net point of view, because the closure operation takes both of forwards and backwards

reachability into account. However, the motivation of this thesis is to nd an answer to

the following problem: Is there a Petri net model which is sound and complete for full

linear logic? And the problemhas been solved aÆrmatively.

Of course, the signicance of the result depends on the meaningof the logic in Petri

nets. For the proposed Petri net model, we give an interpretation of the logic which

may be acceptable froma Petri net point of view, comparing with that by Engberg and

Winskel [15].

The organization of this thesis is asfollows.

In Chapter 2, we review basic algebraic structures and xed point theorem. In the

discussionofthis thesis,weshalloftenneedtheconcepts ofbasicalgebraicstructures (for

example a multiset and ordered structures) and xed point theorem. In these notes we

do not intend to go very deeply in to these; we limit ourselves to a brief description of

basic algebraicstructures and xed point theorem.

In Chapter 3, we review Petri nets. First we discuss Petri net simply. Then we

introduce the relation between Petri net and multiset,and reachabilityrelation.

InChapter4,wediscussIL-algebrasandquantales. Thenweintroducetwoclosureop-

erationsC

1

andC

2

onthealgebras,whichplayacrucialrole inthe proofofcompleteness.

Moreover, we discuss exponential and quantales with exponential.

In Chapter 5, we discuss linear logic without exponential (its syntax and semantics)

and then prove soundness theorem for quantales generated by Petri nets. Next we show

why wecannotprovecompletenessforthe quantales usedin[15, 16,17]. Finallywe show

howtoconstructquantales inwhichthedistributivityisnotalways validfromPetrinets,

and then prove completenessof linear logic withoutexponentialfor the quantales.

In Chapter 6, we discuss linearlogic with exponential(itssyntax and semantics) and

then prove soundness theorem for the quantales generated by Petri nets. And then we

showhowtoconstructquantaleswithexponentialinwhichthedistributivityisnotalways

quantales.

In Chapter 7, we give an impression on the meaning of the logic on the proposed

Petri net model, comparing withthat by [15]. Weconsider a dierenceof interpretations

between closureoperationsC

1

and C

2

,and weshowadierentinterpretationof formulas

under the closure operationC

2 .

In Chapter 8, we consider classical quantales for classical linear logic generated by

Petri nets.

Preliminaries

In this chapter, we review basic algebraicstructures and xed pointtheorem. Forback-

ground material on basic algebraic structures, see [3, 6, 14, 28, 46, 48, 49] and on xed

point theorem, see [37].

2.1 Basic Algebraic Structures

Inthe discussionof thisthesis, weshalloftenneedthe concepts ofamultisetand ordered

structures. Inthesenoteswedonotintendtogoverydeeplyintothese;welimitourselves

toa briefdescription ofthe theory of multiset and the puretheory of ordered structures.

2.1.1 Multisets

Intuitively,amultisetisasetwith(nite)multiplicities;theremaybenitelymanycopies

of a single element. As a formaldenition we use

Denition 2.1.1 (multiset) A multiset over aset S isamappingm : S !N,where

m(a)=n meansthat a occurswith multiplicity n. Ifm(a)=0,a isnot an elementof m

(that isto say, a occurs with multiplicity0).

The operation+on multisetsis dened by (m+m 0

)(a)=m(a)+m 0

(a)forall a2S,

and [] denotes the empty multiset.

We shall denote the set of all multisets over a set S by M

S

, and use fg for a set

and [] for amultiset.

Example 2.1.2 Leta and b beelementsof S. Then

fag;fbg;fa;bg;:::are sets and

fag =fa;ag and fag[fa;bg=fa;bg,

[a];[b];[a;b];::: are multisets and

[a] 6=[a;a] and [a]+[a;b]=[a;a;b].

Denition 2.1.3 (monoid) A structure M = hX;;ei is a monoid with the identity e

if is abinary operation onX and e is anelement of X such that forevery a;b;c2X,

1. a(bc) =(ab)c,

2. ae=ea=a.

Remark 2.1.4 When the structure satises only 1 of Denition 2.1.3, it is called a

semigroup.

Denition 2.1.5 (commutative monoid) A structure M=hX;;eiis acommutative

monoidwith the identitye if

1. hX;;ei isa monoid,

2. ab=ba forevery a;b2X.

Denition 2.1.6 (partially ordered set) AstructureX=hX;iisapartiallyordered

set if isa binary relation onX suchthat for every a;b;c2X,

1. aa (reexive),

2. if ab and bc, then ac (transitive),

3. if ab and ba, then a=b (antisymmetric).

Let P be a partially ordered set and X P. y 2 X is the greatest element of X if

and only if

if x2X; then xy;

and y 0

2X is the least element of X if and only if

if x2X; then y 0

x:

Let P be a partially ordered set and X P. y 2X is the maximal element of X if

and only if

if yx and x2 X; then x=y;

and y 0

2X is the minimal elementof X if and onlyif

if xy 0

and x2 X; then x=y 0

:

Let P and Q be partially ordered sets. Then a function f : P ! Q is monotone if

and only if for alla;b 2P,

if ab; then f(a)f(b):

Sof preserves order.

We shall think of the elements of a partially ordered set as being propositions, and

of as meaning \)", or \entails", or \is logicallystronger than". Then it is precisely

antisymmetry that says that if two propositionsare logicallyequivalent (each entailsthe

other) then they are equal: weidentify them.

a

b c

d

e

f

g h

Figure2.1: Partiallyordered set.

Here each line represents an inequality. For instance, b a, because b is at the

bottom end of the line, e b. We can deduce other inequalities, such as f f,

ea, fromthe partiallyordered set axioms, reexiveand transitive,i.e., eb and

ba, or ecand ca.

Example 2.1.8 Let X be a set and P(X) its power set, i.e., the set of all subsets of

X. Taking tomean , P(X)is a partially ordered set. Antisymmetry corresponds to

the extensional denition of set equality, which says that equality between sets is to be

determined entirelyby what elementsthey have.

Denition 2.1.9 (preordered set) A structure X = hX;i isa preordered set if is

a binary relationon X such that for every a;b;c2X,

1. aa (reexive),

2. if ab and bc, then ac (transitive).

Proposition 2.1.10 Let P be a preordered set. We dene a binary relation on P by

a b if and only if ab and ba:

Then isanequivalence relation, andthe equivalenceclasses [a]form a partiallyordered

set P=, with

[a][b] ifand only if ab:

Denition 2.1.11 (preordered commutative monoid) A structure X = hX;;;ei

is apreordered commutative monoidif,

1. hX;;ei isa commutative monoid,

2. hX;iis a preordered set,

3. if xx 0

and yy 0

,then xyx 0

y 0

for allx;x 0

;y;y 0

2X.

Thinkingofasmeaning\)", wenext wishtodescribewhat correspondsto\and"and

\or".

First, we denemeets, which correspond to\and".

Denition 2.1.12 (meet) LetP bea partiallyordered set, X P and y2P. Then y

is ameet (orgreatest lower bound orinmum) for X if and only if

1. y is alower bound for X, i.e., if x2X then yx, and

2. if z is any other lowerboundfor X then z y.

In symbols, we write y= V

X.

Example 2.1.13 Let P be a partially ordered set, X P and y 2 P. A meet, or a

greatest lowerbound yand lower bounds of X can bedrawn asfollows:

P

meet, or greatest lower bound

x

y

lower bounds of X

Figure2.2: Meet and lower bounds.

Ifx2X, then yx, and then y is alowerboundfor X,

if z is any other lowerboundfor X, then z y.

Proposition 2.1.14 Let P be a partially ordered set and X a subset. Then X can have

at most one meet.

Proof. Let y and y 0

be two meets of X. Since y is a meet and y 0

is a lower bound,

y 0

y. Similarly,yy 0

. By antisymmetry,y=y 0

.

Next, we dene joins,whichcorrespond to\or".

is ajoin (or least upper bound or supremum) for X if and onlyif

1. y is anupperbound for X, i.e., if x2X then yx and

2. if z is any other upper bound for X then zy.

In symbols, we write y= W

X.

Remark 2.1.16 > and ? are dened as follows:

> isthe greatest element,

? isthe least element.

a_b and a^b denote W

fa;bg and V

fa;bg, respectively.

Proposition 2.1.17 Let P be a partially ordered set. Thenfor ally 2P,

1. y is the empty meet if and only if it is a top (greatest) element and

2. y is the empty join if and only if it is a bottom (least) element.

Proof.

1. Suppose y= V

;. Every z 2P isa lower bound of ;: forthe condition

if x2; then z x

is satised vacuously. Therefore z y, so y is greater than every other element of

P. Conversely, if y istop then itis alowerboundfor ;(because everything is)and

itis greaterthan all the other lower bounds (becauseit's greaterthan everything),

so

y=

^

;:

2. Suppose y= W

;. Every z 2P isa upperbound of ;: for the condition

if x2; then xz

is satised vacuously. Therefore y z, so y is less than every other element of P.

Conversely, if y is bottom then it is an upper bound for ; (because everything is)

and itisless than allthe other upper bounds(becauseit'sless than everything), so

y= _

;:

Empty meets and joins need not exist. Wehave already seen an example(see Figure

2.1) thathadtwominimalelementsg andh, butnoleastelement. Aleast elementwould

have to be less than everything else. Thus this example does not have an empty join,

althoughit doeshave anempty meet, namely a.

An empty meet (top) isoften writtenas >,and anempty join (bottom) as?.

thinking of asmeaning).

meets.

{ First, P uQ= V

fP;Qg,a meet for the set fP;Qg. Wecheck

P uQ)P and P uQ)Q

so that P uQ isa lower bound for fP;Qg.

{ Next, if R isanother lower bound for fP;Qg, inother words

R)P and R)Q;

then R)P uQ.

Trueiseasilyseentobeatop element: itholds unconditionally,soanything implies

true: P )true.

joins.

{ First, P tQ= W

fP;Qg,a joinfor the set fP;Qg. Wecheck

P )P tQ and Q)P tQ

so that P tQ isan upper bound for fP;Qg.

{ Next, if R isanother upperbound for fP;Qg,in other words

P )R and Q)R ;

then P tQ)R .

Falseisbottombecauseofthestandardlogicalideathatifweassumeacontradiction

then we can proveanything: false)P.

Example 2.1.19 In set theory, meets are intersections and joins are unions. We work

with subsets of a\universe" U, and is set inclusion,.

First, meets. Clearly if each X

i

is a subsetof U, then

{ T

i X

i X

i

for alli.

{ IfY X

i

foralliand y2Y,then y2X

i

foralli andsoy2 T

i X

i

. Therefore

Y T

i X

i .

{ The empty meet is the top subset, U itself.

Next, joins. Clearly if each X

i

is asubset of U, then

{ X

i

S

i X

i

for alli.

{ If X

i

Y for all i and x 2 S

i X

i

, then x 2 X

i

for some i and so x 2 Y.

Therefore S

i X

i Y.

{ The empty join is the bottom subset,;.

Orders Logic Sets

)

= , =

top, >, true universe

empty meet, V

;

bottom, ?, false ;

empty join, W

;

meet, V

, conjunction, intersection, \

greatest lower bound, glb, and, ^

inmum, inf

join, W

, disjunction, union, [

least upper bound,lub, or,_

supremum, sup

Figure2.3: The relation of orders,logic and sets.

2.1.4 Lattices

Denition 2.1.20 (lattice) A partially ordered set P is alattice if and onlyif alltwo-

element subsets have meets and joins.

Let v be abinary relation ona latticedened by

xvy if and only if x_y=y:

Remark 2.1.21 Letastructure L=hL;vibealattice. Thenfora;b 2L,thefollowing

are equivalent.

1. avb,

2. a_b =b and

3. a^b =a.

Proof.

avb if and onlyif a_b =b.

Suppose avb. Thenb isanupperboundof fa;bg. Ifcisanupperbound offa;bg,

b v c from denition. It means that b is the least upper bound of fa;bg, i.e., b is

the supremum. Therefore a_b=b. Conversely suppose a_b =b. Then

ava_b=b;

and hence avb.

Suppose a v b. Then a is a lower bound of fa;bg. If c is a lower bound of fa;bg,

cv a from denition. It means that a is the greatest lower bound of fa;bg, i.e., a

is the inmum. Therefore a^b =a. Conversely suppose a^b =a. Then

a=a^b vb;

and hence avb.

Proposition 2.1.22 LetastructureL=hL;_;^ibealattice. Thenforeverya;b;c2L,

it satises the following conditions.

1. a_a=a , a^a=a (idempotence),

2. a_(b_c) =(a_b)_c , a^(b^c) =(a^b)^c(associativity),

3. a_b =b_a , a^b=b^a (commutativity),

4. a_(a^b)=a , a^(a_b)=a (absorption).

Proof. 1and 3 are immediate. We show 2and 4.

1. (associativity).

(a) a_(b_c)=(a_b)_c.

Suppose thata_(b_c) =d. ItsuÆces toshowthatdistheleast upperbound

of fa_b;cg. First, since a v d and b_c vd, a vd, b v d and cv d. From

a vd andb vd,a_bvd, and thend is one of the upper boundof fa_b;cg.

Next, suppose thateisanarbitraryone oftheupperboundoffa_b;cg. Then

a ve,b veand cve. From bve andcve,b_cve, and thene isalsoone

of the upperbound offa;b_cg. Since disthe least upperbound offa;b_cg,

d ve. Therefore d is the least upperbound of fa_b;cg, and then

a_(b_c) =d=(a_b)_c:

(b) a^(b^c)=(a^b)^c.

Suppose that a^(b^c) = d. It suÆces to show that d is the greatest lower

bound of fa ^b;cg. First, since d v a and d v b ^c, d v a, d v b and

d vc. From dva and dvb, dva^b, and then d is one of the lower bound

of fa^b;cg. Next, suppose that e is an arbitrary one of the lower bound of

fa^b;cg. Then eva, evb and evc. From evb and evc, evb^c, and

then e isalsooneof thelowerbound offa;b^cg. Sincedis thegreatest lower

boundoffa;b^cg,evd. Therefore disthegreatest lowerboundof fa^b;cg,

and then

a^(b^c) =d=(a^b)^c:

2. (absorption).

a_(a^b)=a meansa^bva, and itis trivial.

(b) a^(a_b)=a.

a^(a_b)=a meansa va_b, and itis alsotrivial.

Denition 2.1.23 (distributive) A lattice L is distributive if and only if for every

a;b;c2L wehave

a^(b_c)=(a^b)_(a^c);

i.e., ^distributesover_,inthe sameway as,fornumbers,multiplicationdistributes over

addition.

Proposition 2.1.24 In a distributive lattice L, _ alsodistributes over ^.

Proof.

(a_b)^(a_c) = f(a_b)^ag_f(a_b)^cg

= a_fc^(a_b)g

= a_f(c^a)_(c^b)g

= fa_(c^a)g_(b^c)

= a_(b^c)

Remark 2.1.25 A lattice doesnot satisfy the distributivityof _ and ^ ingeneral, i.e.,

(a^b)_(a^c)va^(b_c), but does not hold

a^(b_c) v(a^b)_(a^c)

and

a_(b^c) v(a_b)^(a_c), but does not hold

(a_b)^(a_c)va_(b^c):

Example 2.1.26 If U is a set, then we have already seen that its power set P(U) is a

lattice (itactually has all meetsand joins,not just the nite ones). It isdistributive.

Example 2.1.27 A partially ordered set P is linearly ordered if any two elements are

comparable:

if x;y2P then either xy oryx (or both, if and only if x=y):

Sucha partially ordered set has allbinary meets and joins, for instance

x^y=min(x;y)=x if xy,

x^y=min(x;y)=y if yx.

as follows:

a

b

c a ^{b c}

d

e

d

e

1

1

2

2

Figure 2.4: Distributivelattices.

1. Cconsider the left-hand example. First of all,itis alattice. The nullarymeets and

joins are d

1

and e

1

, and we know binary meets and joins of comparable elements

alwaysexist. Allthatislefttocheck aremeetsand joinsforthe incomparablepairs

fa;cgand fb;cg. These are as writtenin the diagram,i.e., d

1 and e

1

,and they are

d

1

=a_c=b_c and

e

1

=a^c=b^c

respectively. However, the latticeis not distributive,because

a^(b_c)=a^d

1

=a6=b =b_e

1

=(a^b)_(a^c):

2. Considerthe right-handexample. Thenullarymeetsandjoinsare d

2 ande

2

. Meets

and joins for the incomparable pairs fa;bg, fa;cg and fb;cg are as written in the

diagram,i.e., d

2 and e

2

,and they are

d

2

=a_b=a_c=b_c and

e

2

=a^b =a^c=b^c

respectively. However, the latticeis not also distributive,because

a^(b_c)=a^d

2

=a6=e

2

=e

2 _e

2

=(a^b)_(a^c):

Proposition 2.1.29 Let P be a partially ordered set in which every subset has a join.

Then every subset has a meet.

Proof. Let S P, and letL be the set of its lower bounds. If a meet (greatest lower

bound) of S exists, then it must be W

L. Thus all we need toshow is that W

L is alower

bound of S. But if x2S and y 2L, then yx, so W

Lx.

and only if every subset has a joinand ameet.

Example 2.1.31 Foragiven set U, astructure P(U) = hP(U);[;\iforms acomplete

lattice,where [ and \ are the usualset theoretic operations,union and intersection.

Remark 2.1.32 In a complete lattice hX;_i, the greatest and the least element exist:

in fact

>:=

W

X,

?:=

V

X.

Remark 2.1.33 We can dene a mapping^ (the inmum) of P(X) intoX by

^

Y :=

_

fz jz vy for ally2Yg:

2.2 Fixed Point Theorem

In the discussion of interpretation for the exponential !, Engberg and Winskel use the

xed point theorem. For an element a of a quantale (it is given in Chapter 4), as an

interpretationof !a, they requireanelement xsuchthat itis thegreatest xed pointof a

function. Therefore, we introduce the basic xed pointtheorem here.

Firstwediscussmonotoneandxed point,andthenweshowthe least(greatest)xed

point theorem below.

monotone:

Given acomplete latticeL, a functionh : L !Lis monotone if and only if

if xvy; then h(x)vh(y)for allx;y2L:

xed point:

An element x2L is a xed point of h if and only if

x=h(x):

Theorem 2.2.1 (xed point) LetLbeacompletelatticeandhbeamonotonemapping

on L. Thenh has a xed point.

Proof. Suppose

D=fx2Ljh(x)vxg

and maximum of L is 1. Then D is not empty since 1 2 D is immediate, and so ^D

exists. Therefore, we may assume a=^D, and itsuÆces to show that a is a xed point

of h. Suppose that x2D,then a vx. Since h is monotone,

h(a)vh(x)vx;

h(a)va;

and usingmonotone ofh, h(h(a))vh(a). This meansh(a)2D. Sincethe inmum ofD

is a,

avh(a):

It follows that h(a)=a, and hence a (=^D)is a xed point of h.

Theorem 2.2.2 (least xed point) Let L be a complete lattice and h be a monotone

mapping on L. Then h has the least xed point:

^

fx2Ljh(x)vxg:

Proof. Suppose

D=fx2Ljh(x)vxg:

Since we have shown that h has at least one xed point in Theorem 2.2.1, we show a

xed point a in 2.2.1 is the least xed point. Suppose that b is a xed point of h, then

h(b) =b, and hence b 2D. Since a is the inmum of D, a v b, and hence a is the least

xed point.

Theorem 2.2.3 (greatest xed point) Let L be a complete lattice and h be a mono-

tone mapping on L. Then h has a xed point, and especially,

_

fx2Ljxvh(x)g

is the greatest xed point of L.

Proof. We can prove similarly. Suppose

D=fx2Ljxvh(x)g

and minimum of L is ?. Then D is not empty since ? 2 D is immediate, and so _D

exists. Therefore, we may assume a=_D, and itsuÆces to show that a is a xed point

of h. Suppose that x2D,then xva. Since h is monotone,

xvh(x)vh(a);

and hence h(a) isan upperbound of D. Since a is the supremum of D,

avh(a);

and using monotone of h, h(a)vh(h(a)). This means h(a)2D. Sincethe supremum of

D is a,

h(a)va:

It follows that a=h(a),and hence a(=_D)is a xed pointof h.

Next we show a xed point a is the greatest xed point. Suppose that b is a xed

point of h, then b = h(b), and hence b 2 D. Since a is the supremum of D, b v a, and

hence a is the greatest xed point.

complete lattice L,weuse the greatest xed point theorem.

The monotone mapping his

h:x !a^1^(xx):

Then the greatest xed point p isdened as

_

fx2Ljxva^1^(xx)g:

Petri Nets

In thischapter,wediscuss Petri nets. ForbackgroundmaterialonPetri nets, see [40, 41]

and on the relationbetween Petri nets and multisets, see [9,18, 32].

3.1 Petri Nets and Multisets

Petri nets is a general purpose mathematical model for describing relations existing be-

tween conditions and events.

Petri nets consistof twotypesof elements, placesand transitions. Eachplace models

a process interms of typesof resources, and can hold arbitrarynonnegative multiplicity.

Each transitionrepresents a state transition rule,i.e., howthose resources are consumed

orproduced by actions. They are described using the notion of multisets.

First we dene Petri nets, and then we discuss the relation between Petri nets and

multisets with some examples.

Denition 3.1.1 (Petri net) A Petri netN isa quadruplehP;T;

( );( )

i such that

1. P isa set (of places),

2. T is a set (of transitions),

3.

( );( )

are mappings of T into M

P

(i.e., the set of all multisets over a set P),

where for t2T,

(a)

(t) iscalled the pre-multisetof t and

(b) (t)

iscalled the post-multiset of t

respectively. Each element of M

P

is called a marking, and in the sequel, we shall

use simply Mfor M

P .

A ring of transitions transforms the given marking into anotherone; ring a single

transitiont subtracts (adds)n from(to) the markm inplace A if thereis anarrowwith

label n from A to t (t toA). Firing of transitions givesthe result of ring transitions in

some other.

tions assquares, and anarrow fromplaceA totransitiont (fromtransitiont toplaceA)

labeled with n 2N n0 if (A;t)2

( ) ((t;A)2( )

)with multiplicity n (n =1 usually

omitted) (respectively). A marking can be indicated in a graphical representation of a

Petri net by inscribingthe multiplicitiesinthe circles.

For understanding of the relation between Petri nets and multisets, We give the fol-

lowing examples.

Example 3.1.2 Consider the followingtwonets, net-1 and net-2.

a

c b

t a

c b

t

t

1

2

net-2 net-1

Figure3.1: Petri net - I.

net-1:

We show a Petri net N = hP;T;

( );( )

i with P = fa;b;cg and T = ftg. Pre-

multiset

(t) is [a;b] and post-multiset (t)

is [c] respectively. Graphically this be-

comes like net-1.

{ Supposethatthereareonetokeninaandinbrespectively. Aringoftransition

t changes the marking from[a;b] to [c].

{ Suppose that there are two tokens in a and in b respectively, then a ring of

transition t changes the marking from[a;a;b;b] to[a;b;c].

net-2:

We show a Petri net N = hP;T;

( );( )

i with P = fa;b;cg and T = ft

1

;t

2 g.

Pre-multiset

(t

1 ) and

(t

2

) are [a] and [b], and post-multiset (t

1 )

and (t

2 )

are [c]

respectively. Graphicallythis becomeslikenet-2.

{ Supposethatthereareonetokeninaandinbrespectively. Aringoftransition

t

1

changesthe markingfrom[a;b] to[b;c], and aring of transitiont

2

changes

the marking from[b;c] to[c;c].

{ Supposethattherearetwotokensinaandonetokeninb. Aringoftransition

t

1

changes the marking from [a;a;b] to [a;b;c], and a ring of transition t

2

changesthe markingfrom [a;b;c] to[a;c;c].

a

c

b t

t 2

1

net-3

Figure3.2: Petri net -II.

We show a Petri net N = hP;T;

( );( )

i with P = fa;b;cg and T = ft

1

;t

2 g.

Pre-multiset

(t

1 ) and

(t

2

) are [a;b] and [c], and post-multiset (t

1 )

and (t

2 )

are

[c] and [a] respectively. Graphicallythis becomeslike net-3.

Suppose that thereare two tokens in a and one token inb. A ring of transitiont

1

changes the marking from[a;a;b] to [a;c], and aring of transitiont

2

changes the

marking from[a;c] to [a;a].

3.2 Reachability Relation

Next, we discuss the reachability relation <>. It is the reexive and transitive relation

dened as follows.

Denition 3.2.1 (reachability relation) Let N = hP;T;

( );( )

i be a Petri net.

Then we denea relation<>onM called the reachabilityrelationof N as follows:

1. Fort 2T, let[ti bea relationon Msuch that

m[tim 0

if and only if m=m 00

+

t and t

+m 00

=m 0

for some m 00

2M.

2. Let<>be arelation onM suchthat

m<>m 0

if and onlyif m[t

1 im

1 [t

2 im

2 [t

3

i [t

n im

n

=m 0

for some t

1

;t

2

;:::;t

n

2T, m

1

;m

2

;:::;m

n

2Mand n 0.

We show the reachabilityrelation <> usingthe net-3of Figure 3.2.

Example 3.2.2 Consider the net-3 of Figure3.2.

Suppose that thereare one token inaand inb. Aring oftransitiont

1

changesthe

marking from[a;b] to [c], and a ringof transitiont

2

changes the marking from[c]

to[a]. This means that

[a;b][t

1 i[c][t

2 i[a]

and we have

[a;b]<> [a]:

t

1

changesthemarkingfrom[a;b;b]to[b;c], andaringoftransitiont

2

changesthe

markingfrom[b;c] to[a;b]. Then aringof transitiont

1

changes themarking from

[a;b] to [c], and a ring of transition t

2

changes the marking from [c] to [a]. This

means that

[a;b;b][t

1

i[b;c][t

2

i[a;b][t

1 i[c][t

2 i[a]

and we have

[a;b;b]<>[a]:

For aPetri net N, we dene structures M

N

=hM;+;[]iand X

N

=hM;<>;+;[]i.

Proposition 3.2.3 A structure M

N

=hM;+;[]i isa commutative monoid.

Proof. In fact,wecan showthat astructure dened asabove satisesthe conditionsof

Denition 2.1.5, forevery m;m 0

;m 00

2M,

1. m+(m 0

+m 00

)=(m+m 0

)+m 00

,

2. m+[]=[]+m=m,

3. m+m 0

=m 0

+m.

Proposition 3.2.4 AstructureX

N

=hM;<>;+;[]iisapreorderedcommutativemonoid.

Proof. In fact,wecan showthat astructure dened asabove satisesthe conditionsof

Denition 2.1.11,for everym;m 0

;m 00

2M,

1. hM;+;[]iis a commutative monoid,

2. a structure hM;<>i holds Denition2.1.9 since

(a) m <>m,

(b) if m<>m 0

and m 0

<>m 00

,then m <>m 00

,

3. if x<>x 0

and y<>y 0

, then x+y <>x 0

+y 0

.

We show the conditions 2(b) and 3 of Proposition 3.2.4 with the example net-3 of

Figure3.2.

Example 3.2.5 Consider the net-3 of Figure3.2.

Suppose that m=[a;a;a;b;b;b], and then m 0

=[c;c;c] and m 00

=[a;a;a], i.e.,

[a;a;a;b;b;b] <>[c;c;c] and [c;c;c] <>[a;a;a]:

Sincem<>m 0

=[a;a;a;b;b;b]<>[c;c;c] andm 0

<>m 00

=[c;c;c]<>[a;a;a],then

[a;a;a;b;b;b]<>[a;a;a], i.e.,

if m <>m 0

and m 0

<>m 00

; then m<>m 00

:

Suppose that x=[a;b] and y=[a;a;b;b], and then x =[c] and y =[c;c], i.e.,

[a;b] <>[c] and [a;a;b;b] <>[c;c]:

Since x+y = [a;b]+[a;a;b;b] = [a;a;a;b;b;b] and x 0

+y 0

= [c]+[c;c] = [c;c;c],

then [a;a;a;b;b;b]<>[c;c;c], i.e.,

x+y <>x 0

+y 0

:

Quantales and Closure Operations

In this chapter,we discuss IL-algebras (intuitionisticlinearalgebras) and quantales, and

introduce closure operations on the algebras. Moreover, we discuss exponential ! and

quantales with exponential. For background material on the algebras, see [2, 4, 38, 39,

42,43, 50].

4.1 IL-algebras and Quantales

Algebraic semantics for linear logic, as presented here, is for linear logic what Boolean-

valued models are for classical logic, and Heyting-valuedmodels for intuitionisticlogic.

4.1.1 IL-algebras

Denition 4.1.1 (IL-algebra) A structureA =hA;^;_;?; ;;1iisanIL-algebraif

1. hA;^;_;?iis a lattice with the least element ?,

2. hA;;1iis a commutative monoidwith unit 1,

3. if xvx 0

, yvy 0

, then xyvx 0

y 0

and x 0

yvx y 0

,

4. xyvz if and only if xvy z forall x;y;z 2A.

Lemma 4.1.2 In any IL-algebra A = hA;^;_;?; ;;1i, for all x;y;z in A,

1. z(x_y)=(zx)_(zy), andmoreover,ifthejoin W

i2I y

i

exists,thenx W

i2I y

i

=

W

i2I (xy

i ),

2. x (y z)=xy z,

3. ? ? is top of A (>:=? ?).

Proof.

1. Suppose thatz(x_y)vv. Sincex_yvz v,xvz vandyvz v. Therefore

xzvv and yz vv, and hence (zx)_(zy)vv. We can prove the converse

similarly.

uvxy z. Similarlywe can prove the converse.

3. Since ?vx ?,?xv?. Therefore xv? ?, and hence >=? ?.

Proposition 4.1.3 A denition of IL-algebra is obtained replacing Denition 3 of 4.1.1

by z(x_y)=(zx)_(zy).

Proof. Assume Denition1,2and 4of4.1.1and z(x_y)=(zx)_(zy). Ifxvx 0

,

then x_x 0

=x 0

. Therefore

z(x_x 0

) = (zx)_(zx 0

)

= zx 0

;

and hence zx vz x 0

. Also assume x vx 0

. Since z vx 0

y if and only if zx 0

vy,

zxvy. Therefore z vx y, and so x 0

yvx y.

Denition 4.1.4 (complete IL-algebra) AstructureA=hA; ;_;^;;1iisacomplete

IL-algebra if

1. hA;^;_iis a complete lattice,

2. hA;;1iis a commutative monoidwith unit 1,

3. ( W

x

i

)y= W

(x

i

y) for allx

i

;y2A,

4. xyvz if and only if xvy z forall x;y;z 2A.

Proposition 4.1.5 Let M =hM;;ei be a commutative monoidwith the identity e, and

for each X;Y M, dene sets XY and Y Z of M by

1. XY :=fxyj x2X;y2Yg,

2. Y Z :=fx2M jxy 2Z for ally2Yg.

Then the structure

P(M)=hP(M); ;[;\;;fegi;

where [ and \ are the usual set-theoretic operations, isa complete IL-algebra.

Proof.

1. 1 and 2of Denition 4.1.4 are trivial.

2. For3 of Denition 4.1.4, weshow that

( [

X

i

)Y = [

(X

i Y):

Suppose that x 2 ( S

X

i

)Y. Then x = yz for some y 2 S

X

i

and some z 2 Y.

Therefore y 2 X

i

for some i, and so x 2 X

i

Y. Since x

i

Y

S

(X

i Y),

x 2 S

(x

i

Y). Conversely suppose that X

j

S

X

i

. Then X

j

Y ( S

X

i )Y.

Therefore S

(X

j

Y)( S

X

i )Y.

XY Z if and onlyif XY Z:

If x2X, then xy2 XY for all y2 Y. Therefore xy 2Z, and sox 2Y Z.

ThusX Y Z. Conversely forallx2X and y2Y,since X Y Z,xy2Z.

Therefore XY Z.

Remark 4.1.6 The structure P(M)=hP(M); ;[;\;;fegisatises alawnot gener-

ally validin IL-algebras: distributivity of the lattice operations.

The simplest way to see that distributivity of the lattice operations does not hold in

general,is toverify that the sequent

Au(BtC))(AuB)t(AuC)

isnotderivable,sincethismeansthattheIL-algebraconstructedfromIntuitionisticlinear

logic or classical linear logic by means of the Lindenbaum construction does not obey

distributivity.

4.1.2 Quantales

Denition 4.1.7 (commutative quantale) A structure Q = hQ;_;;1i is a commu-

tative quantale if

1. hQ;_iis a complete lattice,

2. hQ;;1iis acommutativemonoid,

3. ( W

x

i

)y= W

(x

i

y) for allx

i

;y2Q.

We shall use simplyquantale for commutativequantale with unit.

Remark 4.1.8 Dene a binary operation on Q by

y z :=

_

fxjxyvzg:

Then

xvy z if and only if xyvz:

Proposition 4.1.9 Let M =hM;;ei be a commutative monoidwith the identity e, and

for each X;Y M, dene a subset XY of M by

XY :=fxyjx2X;y2Yg:

Then the structure

P(M)=hP(M);[;;fegi

is a quantale.

Proof.

2. For3 of Denition 4.1.7,weshow that

( [

X

i

)Y = [

(X

i Y):

Suppose that x 2 ( S

X

i

)Y. Then x = yz for some y 2 S

X

i

and some z 2 Y.

Therefore y 2 X

i

for some i, and so x 2 X

i

Y. Since x

i

Y

S

(X

i Y),

x 2 S

(x

i

Y). Conversely suppose that X

j

[X

i

. Then X

j

Y ( S

X

i )Y.

Therefore S

(X

j

Y)( S

X

i )Y.

Remark 4.1.10 In the quantale P(M),

Y Z :=

[

fX jXY Zg

= fx2M jxy2Z for all y2Yg:

Remark 4.1.11 Itiseasytoshowthatacomplete IL-algebraisjustaquantale, inwhich

y z is dened by

y z :=

_

fxjxyvzg:

Proposition 4.1.12 A structure is a complete IL-algebra if and only if it is a quantale.

Proof. It is trivial that if a structure is a complete IL-algebra, then it is a quantale.

Weshow that if a structure isa quantale, then it isa complete IL-algebra. Dene

y z :=

_

fxjxyvzg:

Then we show that a commutative quantale is always acomplete IL-algebra.

1. 1,2 and 3 of Denition4.1.4 are trivial.

2. For4 of Denition 4.1.4,weshow that

xyvz if and only if xvy z:

Suppose that y z :=

W

fujuy v zg. If xy vz, then x 2 fu juy v zg, and

hence xvy z. Conversely if xvy z, then

xy v (y z)y

= ( _

fujuyvzg)y

= _

fuy juyvzg

v z;

and hence xyvz.

The proposition shows that complete IL-algebras and quantales amount to the same

thing.

Corollary 4.1.13 A structure P(M

N

):=hP(M);[;;f[]gi is a quantale, where

XY :=fm+m 0

jm 2X;m 0

2Yg:

(Note that a structure M

N

=hM;+;[]iis a commutative monoid.)

Remark 4.1.14 In the quantale P(M

N ),

Y Z :=

[

fXj XY Zg

= fm2Mjm+m 0

2Z for all m 0

2Yg:

Next, we discuss closure operations on the IL-algebras and the quantales which play a

crucial role inthe proof of completeness.

4.2.1 Closure Operation

Denition 4.2.1 (closure operation) An operation C on a quantale Q =hQ;_;;1i

is aclosure operation onQ if

1. xvCx,

2. if xvy then CxvCy,

3. CCxvCx,

4. CxCy vC(xy).

An element x of Q is C-closed if x = Cx holds. C(Q) denotes the set of all C-closed

elements of Q.

Lemma 4.2.2 C(Cx_Cy)=C(x_y)holds for every x;y2Q.

Proof. SinceC(x_y)vC(Cx_Cy)is trivial,we show that

C(Cx_Cy)vC(x_y):

xvx_y and yvx_y,thenCxvC(x_y)andCyvC(x_y). Therefore (Cx_Cy)v

C(x_y),and hence

C(Cx_Cy) v CC(x_y)

= C(x_y):

Lemma 4.2.3 C(CxCy)=C(xy) holdsfor every x;y2Q.

Proof. SinceC(xy)vC(CxCy)is trivial,we show that

C(CxCy)vC(xy):

Since CxCy vC(xy)(4of Denition 4.2.1),

C(CxCy) v CC(xy)

= C(xy):

Proposition 4.2.4 IfC isaclosureoperationonanIL-algebraA=hA;^;_;?; ;;1i,

then

C(A)=hC(A);^;_

C

;C?; ;

C

;C1i

is also an IL-algebra, where _

C

and

C

are dened by

1. _

C x

i

:=C(_x

i ),

2. x

C

y:=C(xy).

Proof. We showthat a structure hC(A);^;_

C

;C?; ;

C

;C1i dened as above holds

Denition 4.1.1. The proof of that if a;b 2 C(Q), then a^b 2 C(Q), a_

C

b 2 C(Q),

a

C

b2C(Q)and a b2C(Q), and 1 of denition willbe shown later (see the proof of

Proposition 4.2.5. Nowwe show 2,3 and 4 of denition.

1. We show that a structure hC(A);^;_

C

;C?; ;

C

;C1i is a commutative monoid

with unit 1.

(a) Fora

C (b

C

c) =(a

C b)

C c, a

C (b

C

c) =C(aC(bc))=C(CaC(bc)) =

C(a(bc)) =C((ab)c)=C(C(ab)Cc)=C(C(ab)c)=C((a

c

b)C)=

(a

C b)

C c.

(b) Fora

C

C1=C1

C

a=a, C1

C

a =C(C1a)=C(C1Ca)=C(1a) =

C(a 1) = C(CaC1) = C(a C1) = a

C

C1, and C(1a) = Ca = a.

Therefore C1is the unit.

(c) Fora

C

b=b

C a, a

C

b=C(ab)=C(ba)=b

C a.

2. We show z

C (x_

C

y)=(z

C x)_

C (z

C y).

z

C (x_

C

y) = C(z(x_

C y))

= C(zC(x_y))

= C(CzC(x_y))

= C(z(x_y))

= C((zx)_(zy))

= C(C(zx)_C(zy))

= (z

C x)_

C (z

C y):

3. We show x

C

yvz if and only if xvy z.

x

C

y = C(xy)

= C(CxCy)

v Cz;

then CxCyvCz, and hence xvy z.

Proposition 4.2.5 If C is a closure operation on a quantale Q=hQ;_;;1i, then

C(Q)=hC(Q);_

C

;

C

;C1i

is also a quantale, where _

C

and

C

are dened by

1. _

C x

i

:=C(_x

i ),

2. x

C

y:=C(xy).

Proof. Firstweshowthatifa;b 2C(Q),thena^b 2C(Q),a_

C

b 2C(Q),a

C

b 2C(Q)

and a b 2C(Q).

For a^b 2 C(Q), since a^b v a, C(a^b) v Ca = a. Similarly since a^b v b,

C(a^b)vCb=b. Therefore C(a^b) va^bvC(a^b), and so a^b2C(Q).

For a _

C

b 2 C(Q), C(a_

C

b) = C(C(a_b)) = C(a_b) = a _

C

b. Therefore

a_

C

b2C(Q).

For a

C

b 2 C(Q), C(a

C

b) = C(C(a b)) = C(a b) = a

C

b. Therefore

a

C

b2C(Q).

Fora b2C(Q),

C(a b)

C

a = C(a b)

C Ca

= C(C(a b)Ca)

= C((a b)a)

v b

(since we can get (a b)a vb froma bva b). Therefore

C(a b) v a b

v C(a b);

and so a b2C(Q).

Next we show that a structure C(Q) = hC(Q);_

C

;

C

;C1i dened as above holds

Denition 4.1.7.

1. hC(Q);_

C

i isa complete lattice.

We show that a structure hC(Q);_

C

i is a lattice and holds Denition 2.1.30. It is

enoughto prove for _

C .

First we show that hC(Q);_

C

i holds Denition2.1.20.

(a) Fora_

C

a=a, a_

C

a=C(a_a)=Ca=a.

C C C C

a_

C (b_

C

c) = C(a_C(b_c))

= C(Ca_C(b_c))

v C(C(a_(b_c)))

= C(a_(b_c))

v C(a_C(b_c))

= a_

C (b_

C c):

Therefore a_

C (b_

C

c)=C(a_(b_c))=C((a_b)_c) =(a_

C b)_

C c.

(c) Fora_

C

b=b_

C

a, a_

C

b=C(a_b)=C(b_a) =b_

C a.

(d) Fora_

C

(a^b)=a,a_

C

(a^b) =C(a_(a^b))=Ca=a. Fora^(a_

C

b) =a,

a w a^(a_

C b)

= a^C(a_b)

w a^(a_b)

= a:

Next we show that the maximum element : > and the minimum element : C?

exist.

(a) > 2C(Q) since C>v>vC>.

(b) Since ?va for all a2Q,C?vCa=a.

2. hC(Q);

C

;C1i is acommutativemonoid.

Weshowthat astructurehC(Q);

C

;C1iisamonoidand holdsDenition2.1.5,for

every a;b;c2C(Q).

First we show that hC(Q);

C

;C1iholds Denition 2.1.3.

(a) Fora

C (b

C

c) =(a

C b)

C c, a

C (b

C

c) =C(aC(bc))=C(CaC(bc)) =

C(a(bc)) =C((ab)c)=C(C(ab)Cc)=C(C(ab)c)=C((a

c

b)C)=

(a

C b)

C c.

(b) Fora

C

C1=C1

C

a=a, C1

C

a =C(C1a)=C(C1Ca)=C(1a) =

C(a 1) = C(CaC1) = C(a C1) = a

C

C1, and C(1a) = Ca = a.

Therefore C1is the unit.

Next we showthat hC(Q);

C

;C1iholds 2 of Denition 2.1.5.

Fora

C

b=b

C a, a

C

b=C(ab)=C(ba)=b

C a.

3. We show that

C

distributes over _

C .

( _

C S)

C

b = C(C( _

S)b)

= C(C( _

S)Cb)

= C( Sb)

= C(

_

a2S

(ab))

= C(

_

a2S

C(ab))

= _

a2S

C (a

C b):

Therefore for every SC(Q) and a2S,( W

C S)

C b =

_

a2S

C (a

C b).

4. We show that for every a;b;c2C(Q), a

C

b v cif and only if a v b c. Suppose

that a

C bvc.

ab = CaCb

v C(ab)

= a

C b

v c;

and hence avb c. Conversely, suppose that avb c. Then ab vc. Therefore

a

C

b =C(ab)vCc=c, andhencea

C

bvc. Therefore foreverya;b;c2C(A),

a

C

bvcif and onlyif a vb c.

Lemma 4.2.6 Inthe quantaleC(Q), x^y and x y are C-closed whenever xand y are

C-closed. Hence operations ^ and coincide with the original operations on Q.

Proof.

1. Cx CyvC(Cx Cy) is trivial. We showC(Cx Cy)vCx Cy).

C(Cx Cy)vCx Cy if and only if C(Cx Cy)CxvCy:

But

C(Cx Cy)Cx v C(C(Cx Cy)Cx)

= C((Cx Cy)Cx)

v CCy

= Cy;

using (u v)uvv and 1,2, 3and 4 of Denition 4.2.1.

2. Cx^Cy vC(Cx^Cy) istrivial. WeshowC(Cx^Cy)vCx^Cy. Cx^Cy vCx

and Cx^Cy v Cy, hence C(Cx^Cy) v Cx and C(Cx^Cy) v Cy, therefore

C(Cx^Cy)vCx^Cy.

1 2

LetX =hM;;;ei be apreordered commutativemonoid. Wedene twoclosure opera-

tions C

1

and C

2

on P(X).

Proposition 4.2.7 Let X =hM;;;ei be a preordered commutative monoid anddene

an operation # on P(X) such that

#X :=fy2M j9x2X(y x)g:

Thenitiseasytoseethat#isaclosureoperationonthequantaleP(X)=hP(M);[;;fegi

(see the proof of Proposition 4.2.10).

Denition 4.2.8 Let X = hM;;;ei be a preordered commutativemonoid and dene

anoperation C

1

on P(X)by

C

1

X :=#X:

Denition 4.2.9 Let X = hM;;;ei be a preordered commutativemonoid and dene

two operations !and on P(X)by

X

!

:=fy2M j8x2X(xy)g;

X :=fy2M j8x2X(y x)g;

and let C

2

be the operation onP(X) dened by

C

2

X :=(X

!

) :

(C

2

is called the MacNeille completion of X,see [14, 23,31, 36]).

We can easilyshow the followingpropositions(see e.g. [47]).

Proposition 4.2.10 C

1

is a closure operation on the quantale

P(X)=hP(M);[;;fegi:

Proof. We showthat a function C

1

dened asabove holds Denition 4.2.1.

1. If x 2 X, then x x, and hence 9y 2 X(x y). Therefore x 2 C

1

X, and so

X C

1 X.

2. If z 2C

1

X, then 9x 2X(z x), and since X Y, so 9x2 Y (z x). Therefore

z 2C

1

Y,and hence C

1

X C

1 Y.

3. If x 2 C

1 C

1

X, then 9y 2 C

1

X(x y) and 9z 2 X(y z). Therefore x z,

so x C

1

X, and hence C

1 C

1

X C

1

X. Since C

1

X C

1 C

1

X (1 of denition),

C

1 C

1

X =C

1 X.

4. We show that if x 2 C

1

X and y 2 C

1

Y, then xy 2 C

1

(X Y). Since x 2 C

1 X,

9x 0

2X(xx 0

). Sincey2C

1 Y,9y

0

2Y (y y 0

). Bydenition,sincexyx 0

y 0

,

xy2 XY. Therefore 9x 0

9y 0

2XY (xyx 0

y 0

). Thusxy 2C

1

(X Y),

and hence C

1 XC

1

Y C

1

(X Y).

2

P(X)=hP(M);[;;fegi:

Proof. We showthat a function C

2

dened asabove holds Denition 4.2.1.

1. If x 2 X, then 8y 2 X

!

(x y). Therefore x 2 (X

!

) = C

2

X, and hence

X C

2 X.

2. First we show that

if X Y; then Y

!

X

!

(1):

If z 2 Y

!

, then 8y 2 Y (y z). Therefore 8x 2 X(x z), and hence z 2 X

!

.

Next we showthat

if X Y; then Y X (2):

Ifz 2Y ,then 8y2Y (z y). Therefore 8x 2X(z x),and hence z 2X . By

(1) and (2), if X Y, then Y

!

X

!

. and if Y

!

X

!

, then (X

!

) (Y

!

) .

Therefore if XY then (X

!

) (Y

!

) , and hence C

2

X C

2 Y.

3. X (X

!

) by 1,then by 2,

((X

!

) )

!

=(C

2 X)

!

X

!

(1):

Ifx2X

!

,then bydenition, 8y2(X

!

) (y x). Therefore x2((X

!

) )

!

,and

hence

X

!

((X

!

) )

!

=(C

2 X)

!

(2):

By (1) and (2), ((X

!

) )

!

=(C

2 X)

!

=X

!

. Therefore C

2 C

2

X = ((C

2 X)

!

) =

(X

!

) =C

2

X,then C

2 C

2

X =C

2 X.

4. We show that

if x2C

2

X and y 2C

2

Y; then xy2C

2

(X Y):

Suppose that z 2 (X Y)

!

. Then 8u 2 X and 8v 2 Y (uv z), and hence

8u 2 X(u v z). Since u 2 X is arbitrary, 8v 2 Y (v z 2 X

!

). Therefore

x v z, and hence we have v x = xv z. Thus v x z. Since v 2 Y is

arbitrary, we have x z 2 Y

!

, and hence y x z. Therefore xy = yx z,

and hence xy2((X Y)

!

) =C

2

(X Y). Thus C

2 XC

2

Y C

2

(X Y).

Remark 4.2.12 C

1

is the closure operation used in [15]. In the quantales constructed

fromPetri nets using C

1

, since C

1

-closed sets are downwards closed, form; m 0

2M

C

1

(m)C

1 (m

0

) if and onlyif m<>m 0

:

Therefore C

1

adequates for the reachability relation of Petri nets. Similarly,since every

C

2

-closedset isdownwards closed,C

2

alsoadequates forthe reachability relation.

N

structed from a Petri net using C

2

closure operation. Then for all x 2M, the following

holds.

C

2

(fxg)=fyjyvxg:

Proof.

First we showthat if m 2C

2

(fxg), then mvx. Suppose that m2C

2

(fxg). Since

v isreexive, then x2fxg

!

, and hence mvx.

Next we showthat if mvx, then m 2C

2

(fxg). Suppose that m vx. Ifm 0

2x

!

,

then xvm 0

. Since v istransitive,then m vm 0

, and hence

m 2(fxg

!

) =C

2 (fxg):

4.3 Quantales with Exponential

Weextendthequantalesgivenabovetothequantaleswithexponential,whichcorrespond

tothe logicalconnective !.

The following denition of quantales with exponential will naturally arise from the

syntactic properties of ! in linear logic.

4.3.1 Exponential on Quantales

Denition 4.3.1 (exponential) Let Q = hQ;_;;1i be a quantale. An exponential !

onQ is anunary operatorsuch that

1. !xvxfor all x2Q,

2. if !xvy, then !xv!y for all x;y2Q,

3. 1=!>,

4. !x!y =!(x^y) for allx;y2Q.

Lemma 4.3.2 Clause2 of the denition is equivalentto the following:

if xvy,then !xv!y and !xv!!y:

Proof. We show that if !x v y, then !x v!y. Since !x v y, !!x v!y, and since x v x,

!xv!!x. Therefore !xv!y. Next we showif xvy,then !xv!y and !xv!!y. Since xvy,

!xvy by 1 of the denition, and hence !xv!y and !xv!!y by 2of the denition.

Lemma 4.3.3 In every quantale with exponential,the following holds:

1. !!x=!x,

2. 1=!1.

1. !!xv!xby 1of the denition. Since !xv!x, !xv!!x by 2 of the denition.

2. !1v 1by 1 ofdenition. Since 1=!> and 1v1,!>=1v1, and hence1v!1by 2

of the denition.

Lemma 4.3.4 In every quantale with exponential,the following holds:

1. !xv1,

2. !xv!x!x,

3. !x!y v!(!x!y),

4. if xvy, then !xv!y.

Proof.

1. Since x v >, !x v > by 1 of the denition, and !x v!> by 2 of the denition, so

!xv1by 3of the denition.

2. !x=!(x^x)=!x!x by 4 of the denition.

3. !x!y =!(x^y)by 4of thedenition. Since!(x^y)v!(x^y),!(x^y)v!!(x^y)by

2 ofthe denition. Therefore !x!y v!!(x^y)=!(!x!y).

4. Sincewehave!xvyfromxvy by1ofthe denition,!xv!y by 2ofthedenition.

4.3.2 FS-quantales and Quantales with Exponential

Here we discuss two denitions of the quantale with exponential !. The former denition

isusedin[15, 16,17]. Usingthisdenition, wecouldnotprovethecompletenessoflinear

logic for Petri net models with exponential. Therefore we use the latter denition and

prove it.

In this thesis,wecallthe quantale dened by theformer denition \FS-quantalewith

exponential",and callthequantale dened by thelatter denitionsimply\quantalewith

exponential".

1. FS-quantales with exponential

In linearlogic, given apropositiona, the assertionof !ahas the possibilityof being

instantiated by the proposition a, 1 or!a!a.

The denition of FS-quantales with exponential will naturally arise from the fol-

lowing syntactic properties of ! in linearlogic, the rules of (1)and (2). The formal

denition of exponential! of linear logic willbe given in Chapter 6.

!a)au1u!a!a(1);

from the rule of free storage,

b )a b)1 b )bb

b)!a

(2)

:

As an interpretation of !a, for an element a of a lattice, we require an element x

from(1) such that

xva^1^(xx):

This will not in general characterize a unique value of the lattice. For instance

taking x tobe the bottom element ? of the lattice will always do. How ever from

(2) itfollowsthat anyx satisfyingxva^1^(xx)shouldbebelow!a. Therefore

!a should bethe greatest xed pointof the monotone mapping

x !a^1^(xx)

inthe complete latticegiven together withthe quantale.

(InChapter2,wehaveshownthatforacompletelatticeLandamonotonemapping

h onL, there exists xed point,and especially,

_

fx2Ljxvh(x)g

is the greatest xed pointof L.)

Sucha solutionensures the soundness of the proof rules extended by those for!a.

We dene FS-quantale with exponentialQ

!

=hQ;_;;1;!ias follows:

Denition 4.3.5 (commutative FS-quantale with exponential) Aquantalewith

exponentialQ

!

=hQ;_;;1;!i isa commutative FS-quantale with exponentialif

bva;b v1and b vbb implies b v!a:

WeshallusesimplyFS-quantalewithexponentialforcommutativeFS-quantalewith

exponential.

Proposition 4.3.6 Let Q = hQ;_;;1i be a quantale, and for each a2 Q, dene

an operator ! on Q by

!a:=

_

fx2Qjxva^1^(xx)g:

Then Q

!

=hQ;_;;1;!i is an FS-quantale with exponential.

Proof. It is immediate fromthe denition of exponential.

This denition of !a is dierent from one in [15, 16, 17]. They dene !a for the

linearlogic with the rule of freestorage[47], and tobethe greatest xed pointof a

mappingcorresponding tothe freestorage rule.

We dene quantale with exponentialQ

!

F

=hQ;_;;1;!;Fias follows:

Denition 4.3.7 (commutative quantale with exponential) LetQ=hQ;_;;1i

be aquantale, and Fbe a subsetof Q such that

(a) if x;y 2F, then xy2F,

(b) xx=x for allx2F,

(c) 12F and xv1for allx2F.

Then astructure Q

!

F

=hQ;_;;1;!;Fi isa commutative quantale with exponential

!a= _

fx2Fjxvag:

We shalluse simplyquantalewith exponentialforcommutativequantale withexpo-

nential.

Proposition 4.3.8 !a= W

fx2Fjxvag denes an exponentialover Q.

Proof. We show that !a= W

fx2Fjxvag holds Denition4.3.1.

(a) !xvx isimmediatefromconditionof denition. Since!x= W

fy2Fjy vxg,

then !xvx.

(b) We showthat if !xvy, then !xv!y. Suppose that !xvy. From denition

!x= _

fz 2F jz vxg and

!y= _

fz 2F jz vyg:

Since!x= W

fz 2F jz vxgvy,ifz vx,thenzvy,forallz 2F. Therefore

wehave !xv!y.

(c) We show1=!>. Since

!>= _

fx2F jxv>g;

and fromcondition ofthe denition, itisimmediate. Becausesince 12F and

x v1 for allx2F, !>v1, and since 1v> and 12F, 1v!>.

(d) We showthat !x!x=!(x^y)for allx;y2Q.

First we show that !x!yv!(x^y). Since!y v!>=1,

!x!y v !x!>

= !x1

= !x:

from1ofdenition, !x!y vxand!x!y vy,and then!x!y vx^y. Also

!x!y = _

z;z 0

2F fzz

0

jz vx;z 0

vyg

(by distributivity of _over )

v _

z;z 0

2F fzz

0

jz v!x;z 0

v!yg

(sincez 2F and z vu impliesz v!u)

v _

fz 2F jz v!x!yg

= !(!x!y);

hence !x!y v!(!x!y)v!(x^y).

Next we show the converse, !(x^y)v!x!y. On the other hand,

!(x^y)= _

fz2F jz vx^yg:

For all z 2 Q, if z v x^y, then z v x and z vy, which in turn implies

z v!x and z v!y, and hence z =zz v!x!y. Therefore !(x^y)v!x!y.