From term models to domains

Abstract

Let B be the closed term model of the λ-calculus in which terms with the same Böhm tree are identified. We investigate which partial equivalence relations (PERs) on B can be regarded as predomains or domains. Working inside the realizability topos on B, such PERs can be regarded simply as sets in a particular model of constructive set theory.

No well-behaved partial order has been identified for any class of PERs; but it is still possible to isolate those PERs which have ‘suprema of chains’ in a certain sense, and all maps between such PERs in the model preserve such suprema of chains. One can also define what it means for such a PER to have a ‘bottom’; partial function spaces provide an example. For these PERs, fixed points of arbitrary endofunctions exist and are computed by the fixed point combinator y. There is also a notion of meet-closure for which all maps are stable.

The categories of predomains are closed under the formation of total and partial function spaces, polymorphic types and convex powerdomains. (Subtyping and bounded quantification can also be modelled.) They in fact form reflective subcategories of the realizability topos; and in this set-theoretic context, these constructions are very simple to describe.