Building domains from graph models

Wesley Phoa

Abstract: In this paper we study partial equivalence relations (PERs) over graph models of the lambda-calculus. We define categories of PERs that behave like predomains, and like domains. These categories are small and complete; so inside them, we can solve domain equations and construct polymorphic types. Upper, lower and convex powerdomain constructions are also available, as well as interpretations of subtyping and bounded quantification. Rather than performing explicit calculations with PERs, we work inside the appropriate realizability topos: this is a model of constructive set theory in which PERs can be regarded simply as special kinds of sets. In this framework, most of the definitions and proofs become quite simple and attractive. They illustrate some general techniques in `synthetic domain theory' that rely heavily on category theory; using these methods, we can obtain quite powerful results about classes of PERs even when we know very little about their internal structure.

LFCS report ECS-LFCS-92-215

Previous | Index | Next