Domain theory

Paul Taylor

Please note that, although this page was created in June 2003, the abstracts have been copied from the papers as they were written at the time.

Recursive Domains, Indexed Category Theory and Polymorphism

PDF (1039 kb)
DVI (877 kb)
PostScript (compressed) (522 kb)
A5 PS booklet (compressed) (512 kb)
What are these?
[12 Feb 2009] 		Ph.D. thesis, Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, 1983-7.

Applications of Continuous Lattices to Lambda Calculus and Denotational Semantics

PDF (4 MB)
What are these?
[12 Feb 2009] 		Part III ( ∼  Master's) thesis, Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, 1983.
Warning: this is a 4MB scanned PDF file.

Homomorphisms, Bilimits and Saturated Domains

PDF (315 kb)
DVI (98 kb)
PostScript (compressed) (107 kb)
A5 PS booklet (compressed) (99 kb)
What are these?
[12 Feb 2009]
The most powerful feature of categories of posets with directed sups is the ability to solve domain equations such as D ≅ DD. A crucial ingredient of this technique is the fact that for certain kinds of diagrams (in particular sequences of "projection pairs") the limit and colimit are isomorphic. This much is known to everyone in the subject: what appears not to be generally known is

    (i) that we only use the fact that the maps are adjoint (not that they are respectively epi and mono) and
    (ii) what the corresponding results for other limits (such as pullbacks) are.
I propose to set out the basic definitions and results here, introducing the following terms:

    (i) homomorphism, for a continuous map with a left adjoint (projections being a special case),
    (ii) comparison, for this left adjoint (embeddings being a special case),
    (iii) bilimit, for the common limit and colimit of filtered diagrams of homomorphisms,
    (iv) bifinite, for a domain expressible as a bilimit of finite posets and
    (v) saturated, for a domain of which any other is a retract.
I shall justify my strongly-held view that the last two should replace the existing terms "profinite" and "universal".
We begin by recalling the basic ideas of the domain-theoretic solution of equations such as D ≅ DD, and showing that homomorphisms (not just projections) arise frequently. We look briefly at general limits and colimits and explain the difference between bifinite and profinite posets. Then the proof of the limit-colimit coincidence for cofiltered diagrams of homomorphisms is given. Working with cofiltered diagrams is cleaner and no more difficult than working with sequences. Although the case for sequences of projections is sufficient for solving domain equations, this general form arises naturally from "indexed retracts". We then seek limits of other kinds of diagrams of special classes of maps, in particular pullbacks and simply-connected limits of projections. Finally we apply this to finding saturated domains.

The Limit-Colimit Coincidence for Categories

PDF (257 kb)
DVI (128 kb)
PostScript (compressed) (111 kb)
A5 PS booklet (compressed) (103 kb)
What are these?
[12 Feb 2009]
Scott noticed in 1969 that in the category of complete lattices and maps preserving directed joins, limit of a sequence of projections (maps with preinverse left adjoints) is isomorphic to the colimit of those left adjoints (called embeddings). This result holds in any category of domains and is the basis of the solution of recursive domain equations. Limits of this kind (and continuity with respect to them) also occur in domain semantics of polymorphism, where we find that we need to generalise from sequences to directed or filtered diagrams and drop the "preinverse" condition. The result is also applicable to the proof of cartesian closure for stable domains.
The purpose of this paper is to express and prove the most general form of the result, which is for filtered diagrams of adjoint pairs between categories with filtered colimits. The ideas involved in the applications are to be found elsewhere in the literature: here we are concerned solely with 2-categorical details. The result we obtain is what is expected, the only remarkable point being that it seems definitely to be about pseudo- and not lax limits and colimits.
On the way to proving the main result, we find ourselves also performing the constructions needed for domain interpretations of dependent type polymorphism.

Internal Completeness of Categories of Domains

PDF (211 kb)
DVI (91 kb)
What are these?
[12 Feb 2009] 		presented at Category Theory and Computer Programming 1, University of Surrey (Guildford), September 1985, published in Springer-Verlag Lecture Notes in Computer Science 240 (1986) 449-465.
One of the objectives of category theory is to provide a foundation for itself in particular and mathematics in general which is independent of the traditional use of set theory. A major question in this programme is how to formulate the fact that Set is "complete", i.e. it has all "small" (set- rather than class-indexed) limits (and colimits). The answer to this depends upon first being able to express the notion of a "family" of sets, and indexed category theory was developed for this purpose.
This paper sets out some of the basic ideas of indexed category theory, motivated in the first instance by this problem. Our aim, however, is the application of these techniques to two categories of "domains" for data types in the semantics of programming languages. These are Retr(Λ), whose objects are the retracts of a combinatory model of the λ-calculus, and bcContω, which consists of countably-based boundedly-complete continuous posets. They are (approximately) related by Scott's [1976] Pω model.
In the case of Set we would like to be able to define an indexed family of sets as a function from the indexing set to the "set" of all sets. Of course Russell showed long ago that we cannot have this. However there is a trick with disjoint unions and pullbacks which enables us to perform an equivalent construction called a fibration.
Retr(Λ) and bcContω do not have all pullbacks. This of course means that they're not strictly speaking complete however we formulate smallness: what we aim to show is that they have all "small" products. More importantly, this pullback trick is on the face of it not available to us. They do, on the other hand, have a notion of "universal" set (of which any other is a retract), and indeed of a "set" of sets, though space forbids discussion of this. These we use in stead to provide the indexation.
Having constructed the indexed form of Retr(Λ) we discover that it does after all have enough pullbacks to present it as a fibration in the same way as Set. However whereas in Set any map may occur as a display map, in this case we have only a restricted class of them. We then identify this class for bcContω and find that it consists of the projections (continuous surjections with left adjoint) already known to be of importance in the solution of recursive domain equations.
We formulate the abstract notion of a class of display maps and define relative cartesian closure with respect to it. The maximal case of this (as applies in Set, where all maps are displays, is known as local cartesian closure. The minimal case (where only product projections are displays) is known in computer science as (ordinary) cartesian closure, though in category theory it is now more common to use this term only when all pullbacks exist, though not necessarily as displays.

This is www.PaulTaylor.EU/domains/index.php and it was derived from domains/index.tex which was last modified on 2 June 2007.