## 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