Linear logic and Petri nets : categories, algebra and proof
Carolyn T. Brown · ERA · 1990
This thesis explores three ways in which linear logic may be used to define a specification language for Petri nets, by giving precise correspondences, at different levels, between linear logic and Petri nets.Firstly, we define categories NC by analogy with de Paiva's dialectica categories GC.The category Met has objects-the elementary Petri nets and morphisms refinement maps.We show that GC induces in NC sufficient structure for NC to be a sound model of linear logic.We demonstrate the computational significance of the net constructors induced by the interpretation in NSet of the linear connectives ®, A, -o, ED and (_)1• Our framework unifies several existing approaches to categories of nets, and gives a model of full linear logic based on nets.Secondly, we show that the possible evolutions of a net generate a quantale.Quantales are algebraic models of linear logic.Further, we show that certain restrictions on nets, including being safe or bounded, arise as subquantales induced by suitable conuclei.This approach allows us to give a sound semantics for linear logic using sets of markings of a given net.Thus the provability of certain assertions in linear logic corresponds to properties of nets.Thirdly, we define a semantics for a fragment of linear logic f o in terms of nets, by giving a partial function from formulae of linear logic to nets.This semantics is complete and sound where defined.Further, we show that whenever a net N can evolve to a net N', there is a canonical proof in L o that the formula interpreted by N entails the formula interpreted by N'.A canonical proof expresses the causal dependencies of a net in a precise way, using the (Cut) rule.This approach allows us to use the techniques of proof theory to study the evolution of nets.I would like to thank my first supervisor, Stuart Anderson, for being a unique and wonderful person, for giving me much support, countless lively discussions and a sane philosophy.I also owe a great debt to my second supervisor, the inimitable John Power, for his expert guidance and assiduous attention.I greatly appreciate all that Stuart and John have done for me, and the commitment they have both shown to the welfare of post-graduate students.I would also like to thank Martin Hyland for his inspiration