[Prev][Next][Index][Thread]
automata or schedules !?
Date: Fri, 4 Jan 91 09:49:58 PST
As my confusion over which way round to make ! and ? highlights, there
is an interesting question as to whether automata or schedules
constitute the real world. This is a theme I elaborate on in the
repaired paper, which I have just released now. (*Please* throw away
your buggy version, very sorry about the nuisance.)
Let me go into additional detail here. This is too long to go in the
paper, but a few concurrency specialists and/or philosophers may find
these ruminations of some interest.
Let me list the appropriate choice of linear logic symbols for certain
programming constructs, as a function whether one takes automata or
schedules for the models of one's logic (and hence the other for the
sentences). This assumes the particular category of my paper, posets
with top and all nonempty sups.
Since this note was motivated by concerns about ! and ?, for the sake
of minimizing notation changes in this note I'll use linear logic
notation throughout this note: & for Girard's additive product, ^8 for
inverted ampersand, + for additive plus (Girard's circle plus), and @
for tensor product. I will always assume & means product, + coproduct,
and @ tensor. I'm not sure what ! and ? should be, but I've taken the
equation !a@!b = !(a&b) as the orienting criterion and noting that the
tensor product of free automata in Aut is free.
Automata as models Schedules as models
concurrence & +
choice + &
cointeraction @ ^8
interaction ^8 @
debug ! ?
verify ? !
The arguments for choosing automata as models were the following.
1. a+b is standard in concurrency theory for choice
2. axb for concurrency is very familiar via the product construction
for concurrent finite state automata, modulo the concerns for
hollow-solid, i.e. homotopy, made explicit in my POPL-91 paper, also by
Christos Papadimitriou, as well as Mike Shields, and implicit elsewhere
in the concurrency literature.
3. I had the strong sense that the automaton-schedule duality was the
duality of models and theories. Furthermore, despite a decade spent
working with schedules as computational objects, when it came down to
comparing automata and schedules it seemed to me obvious that automata
were models and schedules were sentences expressing constraints on
events. In this mirror between the real world and its perfect
reflection, the models were real and the sentences were only the
reflection of reality. To take schedules as the objects of the theory
rather than the sentences seemed like a pretty basic word-object
confusion, amounting to going through the looking glass and declaring
you were now in the real world. (But of course! Why not? Who knows?)
The main counterargument I had at the time, besides having spent a
decade thinking of pomsets as real-world objects (I come from a land
down under) was that this entailed redefining interaction
(orthocurrence) from tensor product to its dual. (In 1985 I mistook
this tensor product for direct product. This error was due to Poset
being cartesian closed, i.e. the two products are equal. The error was
discovered late in 1987 when we moved to other categories more
appropriate to other notions of time than mere ordered time, e.g.
delayed time, real time, etc. See Casley et al in the Manchester
category conference, LNCS 389, pp.21-51, and to appear in Math.Struct.
in CS, Vol. 2., also ftp'able from Boole.Stanford.EDU.)
Now the question arises as to which should take priority in choosing
the proper side:
1. the symbols of linear logic;
2. the computational operations (on the left);
3. the issue of whether automata or schedules are more like objects; or
4. Girard's intuitions as to what his symbols really denote.
1. The symbols. I shall assume that the symbols stand for fixed
concepts of category theory: product etc. These are determined by the
category. An automaton is a poset with top and all nonempty sups,
which determines the category. So is a schedule. The equation !a@!b =
!(a&b) determines which is ! and which ? in each case, namely ! should
always be a free algebra. So there is nothing left to decide here.
2. The reality of computational operations. It has not escaped my
attention that Girard finished his thesis in the same year as I, 1971,
and I can well understand that at this stage of our respective careers
proofs would be as real to him as automata are to me.
Computational operations are completely fixed for me. I can tell the
difference between concurrence and choice. Furthermore interaction
(orthocurrence) has a very well-defined meaning. It is what happens
when a sequence of trains goes through a sequence of stations, signals
pass through circuits, a river along its bed, galaxies passing through
each. It is what Liggett's book "Interacting Particle Systems" is
about.
Interaction is also how you run programs on computers: the programs
pass through the computer, in a sense that you can see clearly in my
semilattice model. This point is discussed crisply (having the
inestimable benefit of a simple model to refer to!) in my present
paper. There I treat s -o a as the execution of schedule s on
automaton a, viewed from the automaton side (i.e. -o is the internal
hom of Aut, not of Sched, meaning that s -o a is an automaton). But
this execution takes place as an interaction. I first give an
operational account of this interaction (turn s into an automaton s'
oriented to agree with a, create the constantly initial map from s' to
a, then move s' and a past each other like little galaxies and record a
new map every time two points one from each poset pass each other
unless the previous map had already anticipated this passage). Then I
give the denotational version of this: s -o a = s' ^8 a (^8 for
interaction interpreted in Aut, namely dual tensor product). This of
course is one of the basic laws of linear logic. That it is so
classical is reflected in the model by the fact that it is meaningful
to stop the interaction anywhere and run it backwards.
Interaction is so tangible for me that a while ago I wrote the
following words about it as the abstract for a paper entitled "Flow
Geometry and Generalized Time."
We identify certain commonly occurring geometric structures
associated with flow-oriented processes. These structures
suggest an appropriate language for the specification of such
flows. Our thesis is that these geometric structures are quite
robust with respect to choice of temporal model: a given
process has the same basic shape whether describing it with
ordered time or various forms of real time. The geometric
structures suggest an appropriate language, while the
robustness demonstrates that this language is equally suited to
ordered time and various notions of real time. We characterize
the extent of this robustness in terms of sufficient conditions
on the temporal model for the language operations to be
well-defined. The resulting language constitutes a reasonable
generalization of extant serial programming language control
structures.
3. The reality of automata or schedules. Let me prove to you that
automata are more real *to you* than schedules. I want you to
visualize running each on the other. What running a schedule s on an
automaton a means is that the execution is itself a bigger automaton
whose states are assignments of states of a to events of s. Each event
evolves from the initial state to successively later states of the
automaton. Each change in state of an event generates another
assignment. Each assignment or map is then a state of the big
automaton s -o a which describes the entire execution.
If that didn't make sense, skip to 4 below. If it did, try to come up
with the dual notion a -o s, running an automaton on a schedule. I
think it means finding out just how closely automaton a meets
specification s, with the result represented as a schedule, but I'd
like to hear from others who have thought more about this. Meanwhile I
for one have far more difficulty making concrete sense of a -o s than I
do of s -o a, indicating to me that a's are real objects that one runs
schedules on to produce a real object running that schedule.
4. Girard's orientation. Interaction for Girard is tensor product.
His intuition and mine are then in perfect agreement if I take
schedules as the real objects and automata as their mirror image.
Moreover, his "of course" and "why not" match perfectly to "verify" and
"debug"; the other way round makes no sense at all to me.
One simple explanation for this comes to mind. Girard being a proof
theorist, proofs for him *are* the real world. They do not refer to
the weather, if the weather exists at all for Girard it refers to the
proofs! But Girard's duality may in fact not be that of word and
object at all but rather something deeper within proof theory, a
subject that I know little of but that seems to me to have successfully
detached itself from the real world and has been moving onto
successively higher planes of existence for some time.
I can understand why I thought interaction was tensor product: it was
because I was working with schedules. The reflection of that tensor
product in the real world is dual tensor product.
And I think I understand why my intuition about verify and debug are in
line with Girard. It is because one does not debug and verify the
world. The world is not broken, only one's theories about it can be
broken. Thus debugging and verification are operations on theories of
the world, not on the world itself. With this in mind I can reconcile
myself to these notions appearing reversed in a world of automata.
I would very much appreciate hearing from those with more understanding
of proof theory than I as to how my interpretation of the duality in my
paper relates to the world of proof theory. I am reasonably certain
that there is no mismatch with concurrency theory as it is understood
by the majority of people working in that area.
--Vaughan Pratt
PS. If you're wondering what Aut is about and don't have time to
retrieve and read my paper, here's the scoop.
The objects are posets with top and all nonempty sups. The category of
such and their homomorphisms turns out to be isomorphic to its dual
(opposite), i.e. self-dual. The isomorphism does not however fix the
objects but rather inverts all of the object leaving its top fixed.
This operation yields an object still in the category for a fascinating
variant of the reason why complete semilattices are complete lattices.
Here is a square and a church. They are the only nonselfdual objects
with at most four elements.
* *
/ \ |
* * *
\ / / \
* * *
Assuming these objects are on opposite sides of the duality (one is a
schedule, the other an automaton) they denote the same thing: true
concurrence if the square is an automaton, otherwise angelic choice, in
each case of two events (aka transitions). In either case the top * is
the start state (always entered) of the automaton and the final event
(never performed) of the schedule.
(People used to having only two incomparable points in a schedule
representing two truly concurrent events have to get used (a) to the
final event being a feature of every schedule, like the initial state
of every automaton and (b) the conflict-concurrency information
represented as a sup of two events, which denotes conflict when the sup
equals the final event and otherwise denotes concurrency.) These are
the price of automaton-schedule symmetry. I think the price is a
steal, but if you want to bargain you'll find me reasonable.
If you want more than this you will have to read the paper. It is a
most amazing category. I was completely blown away when I saw it. Yet
you don't have to know any category theory to read all of this paper,
which makes it all the more amazing. I am convinced that it is the
optimum category for the symmetric representation of the essence of
automata and schedules.
-v