Book contents
- Frontmatter
- Contents
- Preface
- 1 Introduction
- 2 Categorical Preliminaries
- 3 Partiality
- 4 Order-Enriched Categories of Partial Maps
- 5 Data Types
- 6 Recursive Types
- 7 Recursive Types in Cpo-Categories
- 8 FPC
- 9 Computational Soundness and Adequacy
- 10 Summary and Further Research
- A Lemma 8.4.4
- B Theorem 8.6.6
- C Lemma 9.1.3
- D Propositions D.0.1 and D.0.2
- Bibliography
- Index
- Symbol Index
10 - Summary and Further Research
Published online by Cambridge University Press: 23 November 2009
- Frontmatter
- Contents
- Preface
- 1 Introduction
- 2 Categorical Preliminaries
- 3 Partiality
- 4 Order-Enriched Categories of Partial Maps
- 5 Data Types
- 6 Recursive Types
- 7 Recursive Types in Cpo-Categories
- 8 FPC
- 9 Computational Soundness and Adequacy
- 10 Summary and Further Research
- A Lemma 8.4.4
- B Theorem 8.6.6
- C Lemma 9.1.3
- D Propositions D.0.1 and D.0.2
- Bibliography
- Index
- Symbol Index
Summary
We have initiated an abstract approach to domain theory as needed for the denotational semantics of deterministic programming languages. To provide an explicit semantic treatment of non-termination, we decided to make partiality the core of our theory. Thus, we focussed on categories of partial maps. We have studied the representability of partial maps and shown its equivalence with classifiability. We have observed that, once partiality is taken as primitive, a notion of approximation may be derived. In fact, two notions of approximations based on testing and observing partial maps have been considered and shown to coincide. Further we have characterised when the approximation relation between partial maps is domain-theoretic in the (technical) sense that the category of partial maps Cpo-enriches with respect to it.
Concerning the semantics of type constructors in categories of partial maps we have: presented a characterisation of colimits of diagrams of total maps due to Gordon Plotkin; studied order-enriched partial cartesian closure; and provided conditions to guarantee the existence of the limits needed to solve recursive type equations. Concerning the semantics of recursive types we have: made Peter Freyd's notion of algebraic compactness the central concept; motivated the compactness axiom; established the fundamental property of parameterised algebraically compact categories (slightly extending a previous result of Peter Freyd); and shown that in algebraically compact categories recursive types reduce to inductive types. Special attention has been paid to Cpo-algebraic compactness, leading to the identification of a 2-category of kinds with very strong closure properties.
- Type
- Chapter
- Information
- Axiomatic Domain Theory in Categories of Partial Maps , pp. 191 - 201Publisher: Cambridge University PressPrint publication year: 1996