PCF is a simply typed lambda -calculus with ground types iota (natural numbers) and omicron (Booleans); there are no type variables and implies is the only type constructor. There is a natural way to translate any PCF term t into an untyped lambda -expression Lambda (t), such that if t is a program, i.e. a closed term of ground type (say integer type) and t implies /sub N/ n then Lambda (t) implies /sub beta / c/sub n/, where implies /sub N/ denotes call-by-name evaluation and c/sub n/ denotes the nth Church numeral. This paper contains a proof of the converse: if Lambda (t) implies /sub beta / c/sub n/ then t implies /sub N/ n; this tells us that the translation is adequate. The proof is semantic, and uses synthetic domain theory to reduce the question to the original Plotkin/Sazonov adequacy theorem for standard domain models of call-by-name PCF. This argument generalises easily to extensions of PCF which can be translated into the untyped lambda -calculus: we illustrate this by proving an analogous result for a 'second-order' PCF with type quantification. We also discuss how to extend the result to versions of PCF with recursive types and subtyping.>

In this paper we study partial equivalence relations (PERs) over graph models of the λcalculus. We define categories of PERs that behave like predomains, and like domains. These categories are small and complete; so we can solve domain equations and construct polymorphic types inside them. 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 smple and attractives. They illustrative some general technicques 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.

Topos theory is the categorical analog of constructive set theory; and conveniently, PERs (partial equivalence relations) do sit inside a topos-the category of PERs can be (loosely speaking) identified with the full subcategory of modest sets in Hyland's effective topos. (The effective topos is the topos-theoretic version of recursive realizability.) Working in the effective topos is especially attractive since not only can set-theoretic reasoning be used, but one also has a lot of category-theoretic and topos-theoretic machinery at one's disposal. That is the point of view taken in this research. The basic theory of Sigma -spaces is discussed. A convex power domain is also presented. Modal operators are outlined. Parallelism and sheaves are examined. Finally, the fixed-point classifier is presented.>