[Prev][Next][Index][Thread]
automata run schedules
Date: Sun, 6 Jan 91 21:51:29 PST
On Friday I wrestled with the question of which side of The Mirror
(Alice's looking glass) to locate this theory that I've been writing
about, namely concurrent automata (state spaces) and schedules (event
spaces). Which are the objects and which are their duals, the function
spaces to a dualizing object?
If the subject matter had been vector spaces, one would know right away
that this kind of question had no mathematical content. A vector space
is a vector space, whether it is doing duty as an object or a function
space.
It's the same thing here. Only the application cares.
Since I want this theory not just for its mathematics but for a
programming language I'm designing, I do care which are the vector
spaces and which their duals in this application.
On Friday I voted that automata, or state spaces, were vector spaces.
That is, I said that the automata were the objects in the "real world,"
and were the things that product and coproduct and tensor were to be
applied to. Schedules or event spaces were then their duals.
After reflecting on this for a couple of days I now want to change my
vote. I really do want to treat schedules, or event spaces, as the
objects and to regard the automata as the reflection or dual of
schedules.
This has the advantage to me of putting me back in the framework I have
grown accustomed to for nearly a decade, in which concurrence is sum,
a+b. We (my students and I) didn't have choice then, but with this
recent move of certain sups out of automata and into schedules we now
do: choice is the product axb, an operation which previously had no
application except in situations where it inadvertently equaled the
tensor product.
Interaction reverts to being tensor product instead of the dual tensor,
in full agreement both with our previous usage and with Girard's
orientation and even usage of the term "interaction" (even in the title
of one of his papers, "Towards a Geometry of Interaction").
Also debug(a), the free (choice) schedule a on the underlying set of a,
becomes ?a, while verify(a), the free (concert) (in the sense of acting
in concert) schedule becomes !a. This matches Girard's "of course" and
"why not" intuition much better; the mismatch was what confused me when
I first realized !a and ?a were free automata and free schedules and
guessed that ? should be choice and ! concert. My guess was
appropriate for how Girard and I have been oriented for a number of
years, ten in my case, but wrong for my somewhat arbitrary choice on
Friday of automata as objects, which I now regret. I will fix this in
the paper in a few days.
But this does mean we've gone through The Mirror. If you wanted to
match up computers and programs the way you understand words and
objects, how would *you* match them up?
-v