Partializing Stone Spaces Using SFP Domains
Fabio Alessi, Paolo Baldan, Furio Honsell · 1997
In this paper we investigate the problem of "partializing" Stone spaces by "Sequence of Finite Posets" (SFP) domains. More specifically, we introduce a suitable subcategory SFP m 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 SFP m the space of its maximal elements. The category SFP m 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 SFP m . Furthermore, we compare two classical partializations of the space of Milner's Synchronization Trees using SFP domains (see [3], [15]). Using the notion of "rigid" embedding projection pair, we show that the two domains are not isomorphic, thus providing a negative a...