Partializing stone spaces using SFP domains

Abstract

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 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 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. 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.