Fabio Alessi, Paolo Baldan, Furio Honsell

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 {\bf SFP}$^m$ of {\bf SFP} which is naturally related to the special category of Stone spaces {\bf 2-Stone} by the functor {\sf MAX}, which associates to each object of {\bf SFP}$^m$ the space of its maximal elements. The category {\bf SFP}$^m$ is closed under limits as well as many domain constructors, such as lifting, sum, product and Plotkin powerdomain. The functor {\sf MAX} preserves limits and commutes with these constructors. Thus, SFP domains which ``partialize'' solutions of a vast class of domain equations in {\bf 2-Stone}, can be obtained by solving the corresponding equations in {\bf SFP}$^m$. Furthermore, we compare two classical partializations of the space of Milner's Synchronization Trees using SFP domains (see \cite{AbramskyS:bisim}, \cite{MisloveMO91:nwfs}). 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 \cite{MisloveMO91:nwfs}.