Book contents
- Frontmatter
- Contents
- Preface
- Notation
- 1 Continuity and computability
- 2 Syntactic theory of the λ-calculus
- 3 D∞ models and intersection types
- 4 Interpretation of λ-calculi in CCC's
- 5 CCC's of algebraic dcpo's
- 6 The Language PCF
- 7 Domain equations
- 8 Values and computations
- 9 Powerdomains
- 10 Stone duality
- 11 Dependent and second order types
- 12 Stability
- 13 Towards linear logic
- 14 Sequentially
- 15 Domains and realizability
- 16 Functions and processes
- Appendix 1 Summary of recursion theory
- Appendix 2 Summary of category theory
- References and bibliography
- Index
5 - CCC's of algebraic dcpo's
Published online by Cambridge University Press: 05 November 2011
- Frontmatter
- Contents
- Preface
- Notation
- 1 Continuity and computability
- 2 Syntactic theory of the λ-calculus
- 3 D∞ models and intersection types
- 4 Interpretation of λ-calculi in CCC's
- 5 CCC's of algebraic dcpo's
- 6 The Language PCF
- 7 Domain equations
- 8 Values and computations
- 9 Powerdomains
- 10 Stone duality
- 11 Dependent and second order types
- 12 Stability
- 13 Towards linear logic
- 14 Sequentially
- 15 Domains and realizability
- 16 Functions and processes
- Appendix 1 Summary of recursion theory
- Appendix 2 Summary of category theory
- References and bibliography
- Index
Summary
In this chapter, we provide a finer analysis of algebraicity. The central result – which was conjectured by Plotkin and was first proved in [Smy83a] – is that there exists a maximum cartesian closed full subcategory (full sub-CCC) of ω Acpo (the category of ω-algebraic cpo's). Jung has extended this result: he has characterized the maximal cartesian closed full subcategories of Acpo and Adcpo (and of ω Adcpo as well).
In section 5.1, we define continuous dcpo's, which are dcpo's where approximations exist without being necessarily compact. Continuous lattices have been investigated in depth from a mathematical perspective [GHK+80]. Our interest in continuous dcpo's arises from the fact that retracts of algebraic dcpo's are not algebraic in general, but are continuous. Much of the technical work involved in our quest of maximal full cartesian closed subcategories of (d)cpo's involves retracts. In section 5.2, we introduce two cartesian closed categories: the category of profinite dcpo's and the category of L-domains, both with continuous functions as morphisms. In section 5.3, we show that the algebraic L-domains and the bifinite domains form the two maximal cartesian closed full subcategories of Acpo, and derive Smyth's result for ωAcpo with little extra work. In section 5.4, we treat more sketchily the situation for Adcpo. The material of sections 5.3 and 5.4 is based on [Jun88]. In section 5.5, we show a technical result needed in section 5.3: a partial order is a dcpo if and only if all its well-founded subsets have a lub.
- Type
- Chapter
- Information
- Domains and Lambda-Calculi , pp. 105 - 123Publisher: Cambridge University PressPrint publication year: 1998