Computer Science Department
School of Computer Science, Carnegie Mellon University
Profinite Solutions for Recursive Domain Equations
Carl Gunter - Thesis
The purpose of the dissertation is to introduce and study the category of profinite domains. The study emphasizes those properties which are relevant to the use of these domains in a semantic theory, particularly the denotational semantics of computer programming languages. An attempt is made to show that the profinites are an especially natural and, in a sense, inevitable class of spaces. It is shown, for example, that there is a rigorous sense in which the countably based profinites are the largest category of countably based spaces closed under the function space operation. They are closely related to other categories which appear in the domain theory literature, particularly strongly algebraic domains SFP which form a significant subcategory of the profinites. The profinites are bicartesian closed - a noteworthy property not possessed by SFP because it has no coproduct . This gives rise to a rich type structure on the profinites which makes them a pleasing category of semantic domains.
However, there are problems that arise with respect to the solution of recursive domain equations over the profinites which do not apply to the strongly algebraic domains. For the purposes of semantics, the solution of such equations is essential because it is the primary technique of data type specification. There are continuous functors over the profinite which have no profinite solution. The usual universal domain technique for solutions to such equations will not work for the profinites because there is no universal profinite domain. Instead a kind of "multi-universal domain" technique is devised which uses an infinite class of "almost universal" spaces. These make it possible to show that an equation of the on profinites has a solution if and only if a related equation has a finite solution. For a continuous computable functor the decision problem for the used to prove properties of solutions. For example, it is shown that a countably based fixed point of the diagonal of the function space operation must have a least element.