Domain Theory in Realizability Toposes

[an error occurred while processing this directive]An error occured whilst processing this directive

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 An error occured whilst processing this directive