[Prev][Next][Index][Thread]
Corrections to "Concurrent Automata and their Logic"
Date: Fri, 4 Jan 91 00:46:20 PST
With regard to the paper "Concurrent Automata and their Logic" that I
announced yesterday, I included in it a brief treatment of !a and ?a
which I thought pretty much covered things. On reflection today it was
apparent I'd botched this badly due to not having thought much about
these odd creatures before. Now that I've rethought this I see a lot
more clearly what's going on, and have redone it as follows.
To begin with, ! and ? should be interchanged. !a should be FU(a), the
free automaton on the underlying set of states of a, and ?a is its
dual, at least as an object; you need the dual to be ?a' for the maps
to be oriented correctly.
For example if a has 2 states then ?a and !a are respectively the
diamond and the steeple, denoting concurrency and choice.
?a: !a:
* *
/ \ |
* * *
\ / / \
* * *
I call these respectively verify(a) and debug(a). (I badly wanted
verify(a) to be called !a ("of course it works"), and debug ?a ("why
does it not work?"), for obvious reasons. Unfortunately one can only
achieve this if one takes schedules as the basic sort and automata
their looking glass reflection, which I am reluctant to do.)
I'm using p.376 of Robert Seely's 1987 Boulder paper (Contemporary
Math. 92) for the following, specifically his simplifications of
Girard's rules, par.2.1. (If there are any problems with these
simplifications I'd certainly appreciate hearing about them.)
The thing about free automata is that they are closed under tensor
product. They are also closed under coproduct, which may be good for
something. Let me write !m for the free automaton on m generators; it
has m leaves and 2^m states. Then !m@!n = !(mn) while !m+!n = !(m+n)
(cute; that's numeric m+n, not automaton +).
So noting that the number of states in axb is the product of those in a
and b, we infer !a@!b = !(axb), and similarly that !1 is 2 (using the
naming system 1-9 of my 9-automaton example (1)).
Our main goal is to construct the following morphisms in Seely's
paper. The following depends on the fact that the leaves of !a freely
generate !a, whence a morphism f:!a->b is uniquely specified by mapping
the leaves of !a to anywhere in b.
!a -> a leaf i to i in a
!a -> I every leaf to the leaf of I (I is 2, the 2-state automaton)
!a -> !a@!a leaf i to leaf (i,i) (leaves of !a@!b are (i,j))
!a -> !!a leaf i to leaf [i] (leaves in !!a are nodes=terms in !a)
Given f:a->b, form !a->!b by sending leaf i of !a to leaf f(i) in !b.
As far as I can tell that pretty much takes care of it. If anyone more
used to hacking this linear logic stuff than I sees any residual
problems I'd appreciate hearing about them.
I will incorporate the above into my draft.
Vaughan Pratt