Summary of Objectives and Approach.
Detailed Summary of Technical Progress.
P ::= STOP | SKIP | a -> P | P;P | P + P | P || P | x | rec x.P
Our research has focused on how to build operational models and related denotational models for languages such as the one given above so that the denotational model is adequate and fully abstract with respect to the given operational model.
Of particular interest has been the question of how to enlarge models for fragments of a given language to ones for the full language, while retaining the relationships of adequacy and full abstraction. An obvious place to start is with the finitary sublanguage whose BNF-production rules are
P ::= STOP | SKIP | a -> P | P;P | P + P | P || P,
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]).
This year, we have extended this result by showing that full recursion 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, suppose that 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. We than say that the denotational model is order adequate with respect to the denotational model if whenever M[P] is less than or equal to M[Q] in the denotational model, then B[P] is less than or equal to B[Q], in the operational model. Likewise, we say that the denotational model is order fully abstract with respect to the operational model if, whenever B[C[P]] is less than or equal to B[C[Q]] for all contexts C, then M[P} is less than or equal to 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 then show in [MO94] 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 full language of closed terms that also is order adequate and strongly order fully abstract with respect to the extended operational model.
In essence, these results allow one to focus on the finitary sublanguage as the place for crafting operational and denotational models, and then "turn the crank" to extend these models to ones for the language with some form of recursion added, and to that retain the desired full abstraction relations.
What remains to be investigated here is how these results can be applied to specific languages. As an example, we intend to exploit these results to shed further light on how to obtain the failures-divergences model for CSP from more "traditional" domain-theoretic models. We believe we can show how to construct fully abstract models for CSP using domain-theoretic techniques, and the failures-divergences model for CSP should be a quotient of the model we construct. We are interested in finding out if the process of factoring out the equivalence the failures-divergences model imposes on our model for CSP factors through the process of forming models for the finitary sublanguage and extending them to the language supporting recursion. If so, this would afford an alternative method for obtaining a full abstraction result for CSP .
We have previously reported on joint work with Roscoe and Schneider in which a theory of local cpo's was initiated. This work began in an effort to understand the common threads between existing models for unbounded nondeterminism in Timed and untimed CSP. The theory presented in that paper is a beginning, and we have since begun a fuller investigation of these objects and how they can be used to model other forms of unbounded nondeterminism. While the results we have to report currently are preliminary, they nonetheless show that some general results are available.
For example, we can show that, in general, demonic nondeterminism - in which divergence is catastrophic - is the only one of the three common forms of nondeterminism that can be extended to support unbounded choice. The theory we derive relies on the fact that the finitely nondeterministic processes have a well-behaved model, and we use a generalization of spectral theory that guarantees that a needed dominated convergence theorem holds. This result shows that those closed recursive 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.
Models of the untyped lambda calculus: We have extended the results about lambda models in the category K of Hausdorff k-spaces. One of the intriguing results about the untyped lambda calculus is that all known models are in the category of dcpo's and Scott continuous maps. Results also have been available that show that a number of the "obvious" Cartesian closed categories - Sets, Posets and Complete Ultrametric Spaces - cannot contain a nondegenerate model of the untyped lambda calculus. In the paper we have shown that no compact Hausdorff model of the untyped lambda calculus can be nondegenerate. More recently, we have extended this result to show that any Hausdorff k-space model X that is normal and contains a metric arc must be degenerate. While this is additional evidence that there are no nondegenerate models of the untyped lambda calculus in K, the question remains unsettled in general.
As an alternative approach to the question, we are investigating the validity of the methods that are used to construct models of the untyped lambda calculus in DCPO. Indeed, K is complete and co-complete, and so one path to showing models cannot exist there would be through a better understanding of what goes awry with the constructions that were used to obtain them elsewhere. This hinges on understanding the nature of the related category KR of Hausdorff k-spaces and retraction mappings (this corresponds to categories of dcpo's and embedding - projection pairs of mappings), and of the continuity properties of the endofunctor that assigns to an object its family of continuous selfmaps. Results about the nature of limits in KR already show this endofunctor cannot be continuous: indeed, if it were, we could construct a model starting with any Hausdorff k-space - eg, with the unit interval, and the resulting model would have the beginning space as a retract. Now, any model has a continuous fixed point picker, and a retract of a model also must satisfy this property. But, as is noted in our proof about normal spaces containing a metric arc, the fixed point picker on the unit interval is not continuous.
Linear FS-lattices: A selfmap f : L -> L on a complete
lattice L is finitely separated from the identity if
there is a finite subset M of L such that
f(x) is less than or equal to m is less than or equal to x for some
m in M, for each x in
L. A complete lattice L is a linear FS-lattice if
the identity map is the directed supremum of selfmaps each of which is
finitely separated from the identity. Linear FS-lattices and linear (ie,
sup-preserving) maps have recently been exploited (cf. [HJK94])
as models for game semantics and linear logic.
In the technical report, we have characterized the linear FS-lattices in terms of their spaces of Scott continuous and sup-preserving selfmaps. We also have characterized those FS-lattices that are completely distributive in a similar fashion.
References
Transitions and DOD Interactions.
Software and Hardware Prototypes.
Invited and Contributed Presentations.
Honors, Prizes or Awards Received.
Project Personnel Promotions Obtained.