Lower power structures of directed spaces

Abstract:

Powerdomains in domain theory play an important role in modeling the semantics of nondeterministic functional programming languages. In this paper, we extend the notion of powerdomain to the category of directed spaces and define the notion of lower powerspace of a directed space in the way of free algebras. Then we prove the existence of the lower powerspace over any directed space exists and give its concrete structure. Generally, the lower powerspace of a directed space is different from the lower powerdomain of a dcpo endowed with the Scott topology and the observationally-induced lower powerspace introduced by Battenfeld and Schoder in 2015.