scientific article; zbMATH DE number 194122

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

Denotational semantics, as developed by Scott and Strachey (see \textit{J. Stoy}, MIT Press 1977; Zbl 0503.68059) for a systematic presentation) is essentially a framework in which properties of programs can be determined by formal proof techniques. In particular, we are interested in properties such as program correctness and program equivalence. In fact, when a program is transformed, for example by an automatic program manipulation system which aims at optimizing it, a fundamental request is that at each step a program equivalent to the previous one is obtained. Hence, notions of program equivalence are fundamental to the theory and practice of programming languages, and are the semantic basis for program optimization based on correctness-preserving transformations. A way for formally dealing with program equivalence is to reduce the equivalence between two programs (defined as directly executable terms in a given language) to the equality of their semantic values in appropriate models. Models with the ideal property that only equivalent terms are identified are called (equationally) correct, while if exactly the equivalent terms are identified the model is called fully abstract. A clear and mathematically self-contained survey of the research on full abstraction is contained in this short monograph, a revision of the author's Ph.D. thesis. The monograph presents a language independent theory of fully abstract denotational semantics of programming languages, dealing both with the synthesis and analysis of natural models and with the theoretical study of the conditions under which fully abstract models exist. First of all, since the study of the existence of fully abstract models is carried on within the framework of initial algebra semantics, Chapter 2 introduces the definitions and theorems concerning universal algebras and complete ordered algebras [\textit{J. Goguen}, \textit{J. Thatcher}, \textit{E. Wagner} and \textit{J. Wright}, J. Assoc. Comput. Machin. 24, 68-95 (1977; Zbl 0359.68018)]. Programming language syntax is specified in this framework by many-sorted signatures, whose sorts and operators correspond to the syntactic categories and constructs, respectively, of programming languages, and moels are many-sorted universal algebras whose carriers are sort-indexed families of complete partial orders with least element \(\Omega\), with continuous functions as operations. Then, Chapter 3 is devoted to the definitions and elementary properties of full abstraction and least fixed point models. Three kinds of correctness and full abstraction are considered: equational, inequational and contextual. Formally, any congruence \(\approx\) over the term algebra T generated by a signature \(\Sigma\) defines a notion of program equivalence, and \(\approx\)- equationally correct models are those algebras A which induce on T a congruence \(\approx_ A\subseteq \approx\). If \(\approx_ A=\approx\), then we have fully abstract models: in other terms, ground equations hold in A exactly when they hold in \(\approx\). In an analogous way, A is contextually fully abstract iff universally quantified equations hold in A exactly when they hold in \(\approx\). The notion of inequational full abstractness is given in the same way, considering an \(\Omega\)-least substitutive pre-ordering \(\leq\) over T instead of the congruence \(\approx\). Then, the notion of least fixed point model is introduced, i.e. complete ordered algebras which satisfy some least fixed point constraints. The constraints specify that the meaning of certain terms should be least upper bounds of the meaning of certain directed subsets of the ordered term algebra. Two kinds of least fixed points models are considered: ordinary and contextual. The latter is the natural generalization of the former from terms to contexts or, more precisely, to derived operators. In these models, it is possible to assign meanings to iteration and recursion constructs. In Chapter 4, the above notions are applied to define the denotational semantics of two programming languages: the combinatory logic version of PCF and an imperative language, called TIE, with explicit storage allocation and higher and recursive types. Notions of programs ordering and equivalence are defined and it is shown that the models for both languages are inequationally correct with reference to these notions of ordering. In contrast, the model of PCF is already known not to be fully abstract, and the same is conjectured for the model of TIE. The next chapter is devoted to state necessary and sufficient conditions for the existence of correct and fully abstract, least fixed point, complete ordered algebras. Since there are three notions of correctness and fully abstraction and two of least fixed point models, six possible combinations are considered. The main result concerns a necessary and sufficient condition for the existence of inequationally full abstract least fixed point complete ordered algebras. Furthermore, it is shown that, if the category of such algebras and continuous homomorphisms is nonempty, then it has an initial object. Conditions for the existence of equationally fully abstract (resp., equationally correct) least fixed point complete ordered algebras follows as a corollary, and it is shown that equationally correct, complete ordered algebras always exist. As far as contextual full abstraction is concerned, it is shown that contextually fully abstract, contextually least fixed point complete ordered algebras exist exactly when fully abstract, least fixed point complete ordered algebras do. The chapter concludes with several theorems concerning the existence of initial objects and the nonexistence of terminal objects in various categories of models. Chapter 6 contains simplified proofs of known results about the nonexistence of fully abstract models of two nondeterministic imperative programming languages: one with random assignment and the other with finite output streams. The results are given by using the conditions for the existence of equationally fully abstract, least fixed point, complete ordered algebras, without any model-theoretic reasoning. In Chapter 7, two approaches to obtaining fully abstract models from correct ones are investigated. In particular, the possibility of collapsing correct models, via continuous homomorphisms, to fully abstract ones is considered, and useful sufficient conditions are given. The monograph concludes with a short section in which the limitations of the monograph and the corresponding possibilities for further research are discussed.

Recommendations

Cited in

(40)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4040912)