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
Preface
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
This thesis is an investigation into axiomatic categorical domain theory as needed for the denotational semantics of deterministic programming languages.
To provide a direct semantic treatment of non-terminating computations, we make partiality the core of our theory. Thus, we focus on categories of partial maps. We study representability of partial maps and show its equivalence with classifiability. We observe that, once partiality is taken as primitive, a notion of approximation may be derived. In fact, two notions of approximation, contextual approximation and specialisation, based on testing and observing partial maps are considered and shown to coincide. Further we characterise 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 present a characterisation of colimits of diagrams of total maps; study order-enriched partial cartesian closure; and provide conditions to guarantee the existence of the limits needed to solve recursive type equations. Concerning the semantics of recursive types, we motivate the study of enriched algebraic compactness and make it the central concept when interpreting recursive types. We establish the fundamental property of algebraically compact categories, namely that recursive types on them admit canonical interpretations, and show that in algebraically compact categories recursive types reduce to inductive types. Special attention is 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. xi - xivPublisher: Cambridge University PressPrint publication year: 1996