Summary of Objectives and Approach.
The application focus of the work is the language CSP originally crafted by members of the Programming Research Group at Oxford. The aim is to relate the operational and denotational models built up using the uniform methods we devise to the models that have proved so successful for the PRG.
The theory of local cpos has been developed and shown to provide denotational models for languages supporting unbounded nondeterminism. In addition, we are exploring methods of building truly concurrent models for concurrent programs, and relating these models to the interleaving models that are more conventionally used.
Ultimately, the established models for untimed CSP - the failures model and the failures-divergences model - will be analyzed from these viewpoints.
Detailed Summary of Technical Progress.
On the other hand, denotational models for programming languages are most easily described in mathematical terms. If we regard a programming language as a universal algebra, then a denotational model for the language is nothing more than an algebra with the same signature together with an algebra homomorphism from the language to the model. Such a model is inherently modular or compositional, in that the meaning of any program is given by combining the meanings of its components. Such models allow one to analyze how programs interact with one another.
A denotational model for a programming language is said to be fully abstract with respect to an operational model for the same language if and only two programs have the same meaning in the denotational model if and only they have the same behavior in the operational model, no matter what environment they are placed in when running them in the operational model. Here an environment is nothing more than a one-variable polynomial in the language viewed as a universal algebra. The sine qua non in semantics is to have both an operational model and a related, fully abstract denotational model for the language in question.
In [MO95] Oles and I showed that, in certain circumstances, a somewhat stronger notion -- strong order full abstraction -- can be lifted from a language without variables or recursion operators to models for the language of closed terms when identifiers and recursion operators are added to the language. Moreover, the models for the extended language arise naturally from the original models. These results are applicable in particular to languages like CSP that support concurrent computation.
More recently, my work has focused on enhancing the theory underlying this result and showed how to simplifying the process of building models, so that the work occurs "at the poset level". Domains that are used as semantic models are algebraic, which means they are the ideal completion of a poset with properties similar to those that are required for the domain. For example, power domains provide models for the traditional method of understanding parallel composition in terms of the ``simpler'' constructs of sequential composition and nondeterministic choice. The three standard power domains are defined in terms of the set of compact elements of the underlying domain, which is nothing more than a partially ordered set. As previously reported, my work has shown that the functorial construction of a power domain is the ideal completion of a related construction at the poset level, as reported at MFPS 11 (1996).
The problem with the approach just described is that not all continuous maps between algebraic cpos preserve compact elements, so the object-level association of a domain to its set of compact elements does not extend to a functor between the category of algebraic cpos and continuous maps and the category of posets and monotone maps. But For example, a large number of domain equations have solutions which arise using a limit of lower adjoints, and so these solutions also can be obtained by considering the associated upper adjoints, restricting them to the posets of compact elements, finding the initial algebra satisfying this system (i.e., finding the colimit in poset), and then lifting back to domains to solve the original equation. The three power domains are examples here - they each arise using associated free semilattice constructions over posets, and following them by the ideal completion functor.
In the past year we have investigated which domain equations can be solved using this approach. In a paper presented at MFPS 12, we showed that a number of domain equations can be solved using duality. The duality referred to here is that of domains and continuous maps that have "upper adjoints". The objects of both categories are algebraic cpos (and continuous cpos more generally, as described below), and maps in one category are those continuous mappings that have "dual mappings" which go in the opposite direction in the other category, and for which the pair of mappings form a Galois adjunction. In this situation, each mapping determines the other completely, so information encoded in one is also encoded in the other. But, upper adjoints between algebraic cpos preserve compact elements, so these mappings are liftings to the cpo-level of mappings between the compact elements of the underlying domains. While not all continuous maps between domains are lower adjoints, enough of them satisfy this criterion to support a viable theory which can be used to account for a number of constructions at the domain level. To solve a domain equation in the category of algebraic cpos and lower adjoints, one can thus
Gastin and I have been developing truly concurrent models for concurrent programming languages. This theory is more general than the traditional interleaving approach to modeling concurrent computation in which parallel composition is a derived operator which is defined in terms of sequential composition and nondeterministic choice. The truly concurrent approach supports individual actions or events being able to commute with one another, if they are independent, and this is used to develop more expressive models. The goal of our work is to provide insight into the relationship between truly concurrent semantics and interleaving semantics.
So far, we have devised a simple, truly concurrent language that supports concatenation of processes (the true concurrency analogue to sequential composition), restriction of processes to a subset of the set of possible actions according to the resources that are required, and of course recursion. While the work is still in the formative stages, we have a full abstraction result for our initial language, and some further results for the language extended to include parallel composition of processes. The language itself has some interesting and appealing properties. It is deterministic, and also fair. This last means that actions that are infinitely often enabled in any trace are executed infinitely often. Full abstraction results for languages supporting fairness are difficult to come by, and we are hopeful that our approach will provide a simple yet effective means to support this notion. We also are interested in understanding the exact relationship between interleaving models for concurrent languages and the truly concurrent ones we are devising. In particular, we would like to find more definitive information about the oft-made claim that true concurrency is more expressive than the interleaving approach can be.
There are several potential applications of the models we are devising. One is security work, where results have recently been devised by Roscoe showing that determinism in CSP captures a wide range of security properties. The aim here is to generalize Roscoe's results so that security can be assured in a trusted network even if the low-level user's viewpoint is nondeterministic.
A second potential application for this approach is in object-based programming. Here, it is hoped that the truly concurrent language and its models will provide natural setting in which to model concurrent object-based programming.
More details about this research can be found in the report on the principal investigator's visit to the Universitè de Paris 7 in June, 1997.
Work at Tulane in this area has centered on the PhD thesis of Keye Martin, who is working under the direction of the Principal Investigator. Mr. Martin's approach to computational models incorporates the notion of a measurement function on a domain, which is a Scott continuous map from the domain to the non-negative reals ordered under the greater-than-or-equal-to order. Additional assumptions are needed of this function, including the fact that it induces the Scott topology "near the top" of the domain, and that the points that have measure 0 are among the maximal elements of the domain. There are many examples of such situations, including lists over a fixed set, with the length of the list as the measurement, and the closed, bounded intervals of real numbers, ordered by reverse inclusion and with the length of the interval as the measurement function. In both these cases (and, in fact, in most cases) the measurement function actually induces the Scott topology on the whole domain, rather than just near the top. This approach provides a uniform setting in which one can analyze both
Mr. Martin also has developed the notion of a derivative of a selfmap of a domain with measurement. For a selfmap f of the reals, one can induce a selfmap F of the compact intervals, and F has domain-theoretic derivative at each maximal element {x} of the domain of intervals for which f is differentiable at x, and F's derivative at {x} is equal to the absolute value of the derivative of f at x, for each real number x. This work allows one to define the rate of convergence of an algorithm which generalizes the usual notion from numerical analysis. It also can be used to analyze the number of iterations an algorithm takes to get within epsilon accuracy of its limiting value.
We are investigating applications of these results as a theoretical basis for work of T. Peters (University of Connecticut) which is aimed at resolving discrepancies between the theoretical structure of objects such as aircraft and their implementation with computer-aided design and manufacturing. Professor Peters has been collaborating with Pratt & Whitney and with Boeing in an effort to better understand and analyze the inconsistencies between the representations of objects designed and manufactured using CAD/CAM and other computer-based technologies, and their theoretically precise structure.
Transitions and DOD Interactions.
Software and Hardware Prototypes.
Invited and Contributed Presentations.
Honors, Prizes or Awards Received.
I will be on sabbatical during the Spring, 1998 term. My plans include three trips abroad. These will include: