Partializing Stone Spaces using SFP domains

Fabio Alessi, Paolo Baldan, Furio Honsell Dipartimento di Matematica ed Informatica via delle Scienze 208, 33100 Udine, Italy  

Abstract:

In this paper we investigate the problem of ``partializing'' Stone spaces by SFP domains. More specifically, we introduce a suitable subcategory SFPm of SFP, which is naturally related to the special category of Stone spaces 2-Stone, by the functor MAX, which associates to each object of SFPm the space of its maximal elements. The category SFPm is closed under limits as well as many domain constructors, such as lifting, sum, product and Plotkin powerdomain. The functor MAX preserves limits and commutes with these constructors. Thus SFP domains which ``partialize'' solutions of a vast class of domain equations in 2-Stone, can be obtained by solving the corresponding equations in SFPm. Furthermore, we compare two classical partialization of the space of Milner's Synchronization Trees using SFP domains, (see S. Abramsky. A domain Equation for Bisimulation. , Information and Computation, 92(2),1991 and M. Mislove, L. Moss, F. Oles. Non-well-founded Sets modeled as Ideal Fixed Points. Information and Computation, 93(1)). Using the notion of ``rigid'' embedding projection pair, we show that the two domains are not isomorphic, thus providing a negative answer to an open problem raised in their paper by Mislove, Moss and Oles.