A category of compositional domain-models for separable Stone spaces

• Published in: Theoretical computer science 2003, Vol.290 (1), p.599-635
• Main Authors: Alessi, Fabio, Baldan, Paolo, Honsell, Furio
• Format: Article
• Language: English
• Subjects: Algebra; Category theory, homological algebra; Denotational semantics; Domain theory; Exact sciences and technology; General topology; Mathematics; Sciences and techniques of general use; Stone spaces; Topology. Manifolds and cell complexes. Global analysis and analysis on manifolds; Totality
• ISSN: 0304-3975; 1879-2294
• DOI: 10.1016/S0304-3975(02)00037-3

In this paper we introduce SFP M , a category of SFP domains which provides very satisfactory domain-models, i.e. “partializations”, of separable Stone spaces (2- Stone spaces). More specifically, SFP M is a subcategory of SFP ep , closed under direct limits as well as many constructors, such as lifting, sum, product and Plotkin powerdomain (with the notable exception of the function space constructor). SFP M is “structurally well behaved”, in the sense that the functor MAX , which associates to each object of SFP M the Stone space of its maximal elements, is compositional with respect to the constructors above, and ω-continuous. A correspondence can be established between these constructors over SFP M and appropriate constructors on Stone spaces, whereby SFP M domain-models of Stone spaces defined as solutions of a vast class of recursive equations in SFP M , can be obtained simply by solving the corresponding equations in SFP M . Moreover any continuous function between two 2-Stone spaces can be extended to a continuous function between any two SFP M domain-models of the original spaces. The category SFP M does not include all the SFP's with a 2-Stone space of maximal elements (CSFP's). We show that the CSFP's can be characterized precisely as suitable retracts of SFP M objects. Then the results proved for SFP M easily extends to the wider category having CSFP's as objects. Using SFP M we can provide a plethora of “partializations” of the space of finitary hypersets (the hyperuniverse N ω (Ann. New York Acad. Sci. 806 (1996) 140). These includes the classical ones proposed in Abramsky (A Cook's tour of the finitary non-well-founded sets unpublished manuscript, 1988; Inform. Comput. 92(2) (1991) 161) and Mislove et al. (Inform. Comput. 93(1) (1991) 16), which are also shown to be non-isomorphic, thus providing a negative answer to a problem raised in Mislove et al.