Home
 

Domain Theory in Realizability Toposes

Wesley Phoa

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

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