"Event Spaces and Their Linear Logic," which I promised way back in February, is now a more or less complete 19-page paper, see abstract below. It is available as pub/es.tex from Boole.Stanford.EDU by anonymous ftp, and will appear in the AMAST'91 proceedings (AMAST is in Iowa City late next month, May 22-25). It supersedes "Concurrent Automata and Their Logic". See pub/README on Boole for abstracts of related papers. The intended application of event spaces is to modelling concurrency. In January I claimed that they were incidentally "the best model of linear logic to date". The guardians of posterity were understandably shocked. Let me try to attenuate my obvious proprietor's bias a bit by listing the criteria for "best" that I have in mind. Only criterion 2 has the force of a theorem, but the other two are surely clear enough that one could reasonably hope for some sort of consensus. Event spaces are 1. simple: the category is just posets with all nonempty joins and a top, and their homomorphisms. 2. nondegenerate: the sums and products are four distinct operations; 3. useful: their primary raison d'etre is not as a model of linear logic but as a model of concurrency that in comparison to event structures is more general and has a cleaner algebraic structure, namely that of full linear logic. If you have a model of full linear logic that meets all three criteria as well or better I am likely to be among your first and most enthusiastic customers (unless it turns out to require inaccessible cardinals). The closest competitor seems to be Girard's original model, coherent spaces and their linear morphisms. However the objects are a very special case of state spaces (dual to event spaces), while the morphisms require the conditions of monotonicity, continuity, stability, and linearity, whereas event space morphisms are merely homomorphisms. Those models of full linear logic that purport to model concurrency all seem very complicated to me, though I'd be very happy to be set straight if I've overestimated the complexity of someone's model. Other features of the paper: What linear logic is about (answer: it combines elementary and categorical logic in the one system). Applications of event spaces to family planning (no connection with risque computers). Herewith the abstract. ABSTRACT Boolean logic treats disjunction and conjunction symmetrically and algebraically. The corresponding operations for computation are respectively nondeterminism (choice) and concurrency. Petri nets treat these symmetrically but not algebraically, while event structures treat them algebraically but not symmetrically. Here we achieve both via the notion of an event space as a poset with all nonempty joins representing concurrence and a top representing the unreachable event. The symmetry is with the dual notion of state space, a poset with all nonempty meets representing choice and a bottom representing the start state. The algebra is that of a parallel programming language expanded to the language of full linear logic, Girard's axiomatization of which is satisfied by the event space interpretation of this language. Event spaces resemble vector spaces in distinguishing tensor product from direct product and in being isomorphic to their double dual, but differ from them in distinguishing direct product from direct sum and tensor product from tensor sum.
participants (1)
-
Vaughan Pratt