Summary of Objectives and Approach.
Detailed Summary of Technical Progress.
P ::= STOP | SKIP | a -> P | P;P | P + P | P || P | x | rec x.PThis syntax is based on CSP, in which STOP denotes the deadlocked process, and SKIP the processes which immediately terminates normally. The process a -> P is first engages in the atomic action a (from the set A of atomic actions), and then acts like the process P, P;Q is the sequential composition of P followed by Q, P + Q denotes the nondeterministic choice of P and Q, and P || Q is the synchronous parallel composition of P and Q. The symbol x denotes a process variable, and the term rec x.P denotes a recursive process. It is important to notice that languages like the one given above are first order, and to note that we can use universal algebra to analyze the language if we view the BNF-like production rules as giving the signature of a (single sorted) algebra. The object of study is then the family of closed terms from the full language, a term being closed is each occurrence of a variable x is bound by some recursive operator rec x.
Our research has focused on how to build operational models and related denotational models for languages such as the one given above so that a denotational model is adequate and fully abstract with respect to the given operational model. An operational model is meant to show how programs act on an abstract machine, and it usually is given by a set of transition rules which describe the "next steps" that a process can undertake. The model is defined by assigning to each program from the language under study a behavior using the transition rules and perhaps some additional relations such as a divergence predicate.
A denotational model is one given as a mapping from the language viewed as the universal algebra the production rules define to an algebra with the same signature so that the mapping preserves the operations in the syntax; such a map is called compositional. The denotational model is adequate and fully abstract with respect to the operational model if two programs are identified by the denotational mapping if and only if the programs have the same behavior in the operational model when considered in every context (which can be viewed as an abstract version of an environment in which to run the program).
A focal point of our research has been how to enlarge models for the finitary fragment of a given language to ones for the language of closed terms from the language with recursion operators while retaining the relationship of full abstraction. For example, for the language given above the finitary sublanguage has BNF-production rules
P ::= STOP | SKIP | a -> P | P;P | P + P | P || P.The idea is to begin by crafting an operational model and a related fully abstract denotational model for this fragment, and then to "complete" these to models for the language of closed terms with recursion operators added so that the resulting denotational model still is fully abstract with respect to the operational model for the full language.
In an earlier paper [MO93], it was shown that, under mild conditions on the operational and denotational models, it is possible to add unnested recursion to the finitary sublanguage. Unnested recursion allows one to solve systems of equations in the finitary language with process variables added; it is a limited form of recursion, but one that has been used extensively (cf. [RT94]).
Last year, we reported on an extension of this result that showed that recursion operators can be added to the finitary sublanguage, again assuming some conditions on the models of the finitary sublanguage with which one begins. To be more precise, if the finitary language has an operational model B : L -> O that is an ordered space, and a denotational model M : L -> D that is a domain all of whose compact elements are denotable by terms in the finitary sublanguage L, then we say the denotational model is order adequate with respect to the operational model if whenever M[P] <= M[Q] in the denotational model, then B[P] <= B[Q], in the operational model. Likewise, the denotational model is order fully abstract with respect to the operational model if, whenever B[C[P]] <= B[C[Q]] for all contexts C, then M[P} <= M[Q], for all terms P, Q in the language under study. (These concepts generalize the usual notions of adequacy and full abstraction to the ordered setting.) We showed in [MO95] that an additional condition - strong order full abstraction - allows one to extend the ordered operational model and associated ordered denotational model to an ordered operational model and associated ordered denotational model for the language of closed terms that also is order adequate and strongly order fully abstract with respect to the extended operational model. While technically a weaker condition, strong order full abstraction holds if the image of each term of the finitary language under the behavior mapping is compact in the operational model.
Since that report, the result has been extended. The results just described applied to any finitary language (i.e., they do not assume the language is a free or an initial algebra), but the model for the language of closed terms produced by the theory does not satisfy any equations, even if the original language satisfied them. For example, even if the sequential composition operation ";" in the denotational model for the finitary model were assumed to be associative, the same would not be true of this operation in the denotational model for the language of closed terms.
The extension we now report allows us to conclude that the denotational model can be crafted so that it satisfies any equations (or in-equations) that the original finitary language satisfies. Thus, the denotational model for the language of closed terms resides in the same category of continuous algebras as the one for the finitary language. This provides models that are natural for the extended language, rather than forcing one to work in a class of algebras where equations that held in the finitary model no longer can be assumed to hold for the extended language.
The thrust of these results, all of which are contained in [MO95], is to allow one to focus on the finitary sublanguage as the place for crafting operational and denotational models, and then to "turn the crank" to extend these models to ones for the language of closed terms with recursion that retain the desired full abstraction relations. Thus recursion no longer needs to be carried along from the start of the modeling process - it can be added at the end after the "correct" models for the finitary sublanguage have been crafted. Since the latter process focuses more on algebra and doesn't require being concerned with continuity arguments, the whole process of crafting models is greatly simplified.
We have previously reported on the theory of local cpo's begun in joint work with Roscoe and Schneider. The results in that paper apply the theory to derive a denotational model for a dialect of Timed CSP without recourse to an external operational model to prove that least fixed points exist. In last year's report, we indicated some preliminary results that the theory of local cpo's could be generalized beyond the limited one that was aimed specifically at the dialect of Timed CSP.
We also reported that demonic nondeterminism - in which divergence is catastrophic - is the only one of the three common forms of nondeterminism that can be extended in a uniform manner to a theory to support unbounded choice. The basis for evaluating such a general theory is whether it can provide a denotational model for unbounded nondeterminism that can discriminate between a process from the simple language given under 1) above that does any finite number of a's from one that also can do infinitely many a's. Because of the fact that the two orders - the order of nondeterminism and the order of recursion (both of which are defined in [M95]) - on any model for angelic nondeterminism coincide, we easily conclude that there is no uniform model for unbounded angelic nondeterminism. What is surprising is that, despite the fact that our theory provides a model for demonic nondeterminism that meets our test, there is no such theory for what we call conventional nondeterminism.
The theory we derive relies on the fact that the finitely nondeterministic processes have a well-defined model for demonic nondeterminism - the so-called Smyth power domain. We then use a generalization of spectral theory that guarantees that a needed dominated convergence theorem holds is a category of local cpo's an monotone maps that preserve all infima. This result shows that those closed terms that can be refined to deterministic ones are guaranteed to have a well-defined meaning in the model, despite the fact that the model is not directed complete and the operations are not continuous. These are the same conditions that were at play in the earlier work on CSP.
What is different about the theory presented in [M95] is that we actually show there is a cartesian closed category of local cpo inf semilattices that support unbounded infima in which all monotone maps that preserve all infima and that also are bounded above have least fixed points. This allows a uniform treatment of recursion in the model, even though the objects are not directed complete and the maps are not continuous.
What remains to be investigated is the possibility of generalizing the results on full abstraction to this setting. Specifically, the goal is to give a full abstraction result along the lines of the one provided in [MO95], so that one could begin in principle with an operational and related fully abstract model for a language supporting bounded demonic nondeterminism and extend the language to include unbounded nondeterminism and the models to support this new operation, and still retain the full abstraction result. Since we already know that demonic nondeterminism is the only form that allows a general theory, by providing such a full abstraction result we would provide a complete theory for the one form of unbounded nondeterminism amenable to a general theory.
Wide Varieties of Topological Groups: In 1993 Professor Mislove visited the University of Wollongong, Australia, and a result of that visit was collaborative work with a number of colleagues on varieties of topological groups. A variety is an equational class, and in the case of pure algebra, Birkhoff's Theorem says each is the class of models of some set of algebraic laws. Taylor in 1977 showed that an analogous result holds for topological algebras, in that the set of algebraic laws must be augmented by a (perhaps proper) class of limit laws. Such classes of topological algebras are called wide varieties because they are closed under the formation of subgroups, products and continuous homomorphic images. In the paper [KMMNS] a simple necessary and sufficient for the class of limit laws to be a set in the case of topological groups is presented. In addition, two closely related wide varieties of topological groups that depend on a fixed infinite cardinal are studied. A detailed analysis of certain simple limit laws is given for the case of locally compact abelian groups.
Electronic Notes in Theoretical Computer Science: Lastly, we report the founding of a new electronic series that began in with the goal of providing more rapid dissemination of high-quality proceedings, lecture notes and monographs than is afforded with the print media. The Initial algebra and final co-algebra semantics for concurrency, CWI Technical Report CS-R9409 (January, 1994).
Transitions and DOD Interactions.
Software and Hardware Prototypes.
Invited and Contributed Presentations.
Honors, Prizes or Awards Received.