[Next][Index][Thread]
Concurrency and linear logic paper
Date: Wed, 2 Jan 91 23:03:40 PST
The following extended abstract can be retrieved by anonymous ftp from
boole.stanford.edu, IP address 36.8.0.65. Instructions for retrieving
this and other papers may found in /pub/README. Contact me,
pratt@cs.stanford.edu, if you need further assistance or would prefer
to receive a copy by email.
Concurrent Automata and Their Logic
Vaughan Pratt
Stanford University
A concurrent automaton is a poset with a top (the global initial state)
and all nonempty sups (the local initial states). These form a
nondegenerate self-dual category Aut admitting universally definable
operations constituting a concurrent programming language and
additional operations yielding a linear logic of concurrency. The
cofree automaton !a is a power set whose dual ?a is a free automaton by
self-duality, obtainable from !a by moving the empty set to the top.
The linear logic theory Th(CSLat) of complete semilattices strictly
extends Th(Aut), having no counterexample to !a=?a since !a and ?a are
power sets on the underlying set of a but for dual reasons. Both
theories strictly extend linear logic with such howlers as 0=1; these
but not !a=?a are removable by intersecting with classical logic,
equivalent to taking both sides of the respective dualities as a single
model. This makes Aut the best model of linear logic to date. The
self-duality of both categories facilitates a noncategorical account
requiring only elementary lattice theory for a complete understanding.