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
7 - Domain equations
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
This chapter presents general techniques for the solution of domain equations and the representation of domains and functors over a universal domain. Given a category of domains C we build the related category Cip (cf. chapter 3) that has the same objects as C and injection-projection pairs as morphisms (section 7.1). It turns out that this is a suitable framework for the solution of domain equations. The technique is applied in section 7.2 in order to solve a predicate equation. In turn, the solution of the predicate equation is used in proving an adequacy theorem for a simple declarative language with dynamic binding.
The category of injection-projection pairs is also a suitable framework for the construction of a universal homogeneous object (section 7.3). The latter is a domain in which every other domain (not exceeding a certain size) can be embedded. Once a universal object U is built, it is possible to represent the collection of domains as the domain FP(U) of finitary projections over U, and functors as continuous functions over FP(U). In this way, one obtains a rather handy poset theoretical framework for the solution of domain equations (section 7.4). If, moreover, FP(U) is itself (the image of a) projection, then projections can be used to give a model of second order typed λ-calculus (see exercise 7.4.8 and section 11.3).
A third approach to the solution of domain equations consists in working with concrete representations of domains like information systems, event structures, or concrete data structures (introduced in definitions 10.2.11, 12.3.3 and 14.1.1, respectively).
- Type
- Chapter
- Information
- Domains and Lambda-Calculi , pp. 144 - 167Publisher: Cambridge University PressPrint publication year: 1998