Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Axiomatic domain theory in categories of partial maps
Fiore M., Cambridge University Press, New York, NY, 1996. Type: Book (9780521571883)
Date Reviewed: Sep 1 1997

I began this reviewing assignment with more than usual interest, because its subject continues work I studied in the 1970s. It was good to see some of the major researchers from those days--Dana Scott, Saunders MacLane, and Haskell Curry--being quoted; that theoretical computer science is using notions from mathematics; and that work is being held to the same high standards.

Fiore wrote this thesis to fulfill a requirement for his 1994 Ph.D. in computer science from the University of Edinburgh. The thesis was subsequently selected by the British Computer Society to be published as a model for future students. Fiore expects mathematicians to be interested in the topic, and provides a detailed introduction relating theory to application. Applied computer scientists should also be able to understand it if they carefully read chapter 2, “Categorical Preliminaries,” which reviews the category-theoretic notions used throughout the book and which are not considered in MacLane [1]. Chapters 3 through 7 develop the necessary category theory. Chapters 8 and 9 consider the programming language enriched FPC (fixed point calculus). Chapter 10 discusses possible further research.

Domain theory is the primary tool for studying denotational semantics, the “true meanings” of programs. It has been used since 1969, when Scott applied the methods to give formal meaning to the &lgr;-calculus. There is, however, a difference in its use in computer science, commented on by Achim Jung [2]. In mathematics, the connection between a model (such as the &lgr;-calculus) and a theory (such as domain  theory)  has to be tight, including soundness and completeness theorems, before an approach is considered useful. Such a connection is known as full abstraction. In computer science this is not always the case. There are examples where the model of a theory is only loosely connected to a programming language that have led to better insights into the theory and to better applications of the language. The mere translation from one formalism, such as the syntax of a particular programming language, to another, a semantic model, has proven useful. Such a loose connection is judged by its adequacy.

Categorical domain theory uses categories as its fundamental tool. Fiore considers the category pCpo, of partial continuous functions over partially ordered set objects called posets. Posets are widely used to model types in semantic domains (see Gunter [3]). Cppo, the category of total continuous maps on pointed posets, those with least elements, had been used by Fiore’s thesis advisor, G. D. Plotkin, to model deterministic programming languages in which expressions always terminate. Fiore’s work can be used to model languages with expressions that may not terminate for some arguments. In particular, he models the metalanguage FPC, which includes products, sums, exponentials, and recursive types. There are operators to construct and destroy expressions, as well as a case expression. Fiore adds call-by-value operational semantics so FPC can function as a programming language. Poset models of FPC arising from domain structures are defined with a denotational semantics on top of them. Fiore proves the computational adequacy of the models, that is, that the evaluation of an FPC program terminates whenever its interpretation in a model is total, and that the model is computationally sound. Soundness is somewhat the reverse of adequacy, meaning here that FPC expressions whose evaluations terminate have total interpretations in the model.

Unfortunately, the indexes are almost useless, with references as much as six pages off. Even so, a nice graduate seminar on denotational semantics could be built using Gunter [3], Pierce [4], or both, followed by the thesis and Fiore et al. [1].

Reviewer:  D. Appleby Review #: CR120686 (9709-0655)
1) MacLane, S. Categories for the working mathematician. Springer, New York, 1971.
2) Fiore, M.; Jung, A; Moggi, E.; et al. Domains and denotational semantics: history, accomplishments, and open problems. Technical Report CSR-96-2, University of Birmingham, School of Computer Science. Available from ftp://ftp.cs.bham.ac.uk/pub/tech-reports/1996/CSR-96-02.ps.gz. Also to appear in the Bull. Eur. Assoc. Theor. Comput. Sci.
3) Gunter, C. Semantics of programming languages: structures and techniques. MIT Press, Cambridge, MA, 1992.
4) Pierce, B. C. Basic category theory for computer scientists. MIT Press, Cambridge, MA, 1993.
Bookmark and Share
 
Denotational Semantics (F.3.2 ... )
 
 
Semantics (D.3.1 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Denotational Semantics": Date
Category-sorted algebra-based action semantics
Even S., Schmidt D. (ed) Theoretical Computer Science 77(1-2): 73-95, 1990. Type: Article
Nov 1 1991
Domains for logic programming
Filippenko I., Morris F. Theoretical Computer Science 94(1): 63-99, 1992. Type: Article
Apr 1 1993
On the fixpoints of nondeterministic recursive definitions
Chen T. Journal of Computer and System Sciences 29(1): 58-79, 1984. Type: Article
May 1 1985
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy