Solving Recursive Domain Equations with Enriched Categories.
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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 aconverging sequence of complete domainsspaces with continuousretraction pairs between them has a limit in the category of complete domainsspaces with retraction pairs as morphisms. The pre-order version was discovered first by Scott in 1969, and is referred to as Scotts 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 Scotts 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.
- Computer Programming and Software
- Operations Research
- Theoretical Mathematics