Solving Recursive Domain Equations with Enriched Categories.
Abstract
Both pre-orders and metric spaces have been used at various times as a foundation for the solution of recursive domain equations in the area of denotational semantics. In both cases the central theorem states that a'converging' sequence of 'complete' domains/spaces with 'continuous'retraction pairs between them has a limit in the category of complete domains/spaces with retraction pairs as morphisms. The pre-order version was discovered first by Scott in 1969, and is referred to as Scott's inverse limit theorem. The metric version was mainly developed by de Bakker and Zucker and refined and generalized by America and Rutten. The theorem in both its versions provides the main tool for solving recursive domain equations. The proofs of the two versions of the theorem look astonishingly similar, but until now the preconditions for the pre-order and the metric versions have seemed to be fundamentally different. In this thesis we establish a more general theory of domains based on the notions of enriched categories, and prove Scott's inverse limit theorem in this theory. The metric and pre-order versions are special cases, obtained just by using different logics as parameter to the general theory.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1994
- Accession Number
- ADA289358
Entities
People
- Kim R. Wagner
Organizations
- Carnegie Mellon University