|
| Author(s) | Stoughton, Allen |
|---|---|
| Title | Fully Abstract Models of Programming Languages |
| Publisher |
Pitman Publishing, John Wiley & Sons |
| Year of publication | 0 |
| Reviewed by | Z. Kasa |
Abstraction is very important in science. In computer science, where there are a lot of concrete models, programming languages and systems, the abstraction gets a leading part.
In the world of diverse programming languages the problem of optimal programs is of great importance. The optimality may be approached in different ways, but in any cases the notions of program equivalence are fundamental. Once the notion of program equivalence is defined, parts of programs can be replaced by anothers without affecting the program behaviours. The equivalence of programs is reduced to the equality of their semantic values in appropiate models. "Thus it is necessary to work with models that are "equationally correct" (or simply "correct") in the sense that only equivalent terms are identified (mapped to the same semantic value). Models with the ideal property that exactly the equivalent terms are identified are called "equationally fully abstract" (or simply "fully abstract"). Similarly, one can judge denotational semantics with reference to notion of program ordering. A model is said to be inequationally correct with reference to a program ordering if and only if one term is less than another in the program ordering whenever the meaning of the first is less than that of the second in the model, and "inequationally fully abstract" if and only if one term is less than another in the program ordering exactly when the meaning of the first is less than that of the second in the model."
The chapters of the book are the followings:
- Introduction,
- Universal Algebras and Ordered Algebras,
- Full Abstraction and Least Fixed Point Models,
- Example Correct Models,
- Conditions for the Existence of Fully Abstract Models,
- Negative Results,
- Obtaining Fully Abstract Models from Correct Models,
- Conclusion.
The book ends with 32 bibliographical titles and index.
Two special programming languages (PCF, TIE) are used to illustrate the theory presented. The author considers three kinds of correctness and full abstractions: equational (ordinary), inequational and contextual. Negative results (nonexistence of fully abstract models) are given for two nondeterministic imperative programming laguages (one with random assignment, another with infinite output streams).