## Domain Theory in Realizability Toposes

**Wesley Phoa**
*Abstract:* This thesis describes some new categories of
domains. These categories have two novel, and important,
features:

- They are
*full subcategories* of certain toposes. A topos
can be regarded as a model of constructive set theory; so our
domains are simply sets, with no extra structure. This makes it
much simpler to describe constructions on domains: for instance,
exponentials are ordinary set-theoretic function spaces.
- They are
*small complete categories* (in an appropriate
sense). This makes it simple to define polymorphic types; it also
means that convex powerdomains, for example, exist for quite
trivial reasons. The use of category theory, and the internal
language of a topos, makes most of the results quite easy to
formulate and prove.

The first part of the thesis is a brief review of Hyland's theory
of realizability toposes - in particular, the

*effective
topos,* the world of recursive mathematics. Inside each
realizability topos is the small compelte category of

*modest
sets*, the counterpart of the PER model. We can use it to model
various polymorphic typed lambda-calculi, including ones with
subtyping.

In the next few chapters, we study domains in the effective
topos. Following Scott and Rosolini, we base the theory on the
notion of *r.e. subobject*; we use it to define an intrinsic
preorder on every object of the topos. Our predomains are the
*complete Sigma-spaces*: the objects for which this preorder
is a chain-complete partial order. Every map between two complete
Sigma-spaces is automatically monotone and preserves suprema of
chains; they form a complete full subcategory for the modest
sets.

There is a natural notion of lifting for predomains, namely the
`computable partial map classifier'; this defines a monad on the
category, whose algebras are the complete Sigma-spaces with a
bottom element - the domains. The categories of predomains and
domains have many other attractive properties.

In the last couple of chapters, we find categories of domains in
other realizability toposes: those based on the Plotkin/Scott graph
models, and on the term model of the untyped lambda-calculus in
which two terms are identified if they have the same Böhm
tree. The methods used are rather different, and the results here
are still a little mysterious.

**PhD Thesis - Price £8.50**

*LFCS report LFCS-91-171 (also published as CST-82-91)*

Previous |

Index |

Next