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