## From term models to domains

**Wesley Phoa**
*Abstract:* Let **B** be the closed term model of the
lambda-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**.

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

We illustrate the theory by discussing an interpretation of PCF,
and proving a computional adequacy theorem. None of the usual
counterexamples to full abstraction are applicable to our
model.

*LFCS report
ECS-LFCS-92-214*

Previous |

Index |

Next