Power structures of directed spaces

TL;DR

This paper extends the concept of powerdomains to directed spaces, defining and constructing upper, lower, and convex powerspaces, and comparing them to existing notions in domain theory.

Contribution

It introduces new definitions of powerspaces for directed spaces via free algebras and provides their concrete structures, expanding the theoretical framework.

Findings

Existence of upper, lower, and convex powerspaces for any directed space.

Concrete structures of these powerspaces are explicitly constructed.

Differences identified between these powerspaces and traditional powerdomains in dcpos.

Abstract

Powerdomains in domain theory plays 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,\ which is equivalent to the notion of the\ $T_0$\ monotone-determined space\ \cite{EN2009}.\ We define the notion of upper,\ lower and convex powerspace of a directed space by the way of free algebras.\ We show that the upper,\ lower and convex powerspace over any directed space exist and give their concrete structures.\ Generally,\ the upper,\ lower and convex powerspaces of a directed spaces are different from the upper,\ lower and convex powerdomains of a dcpos endowed with the Scott topology and the observationally-induced upper and lower powerspaces introduced by Battenfeld and Sch\"{o}der in 2015. Keywords: powerdomain,\ directed lower powerspace of directed spaces,\ directed upper powerspace of directed spaces,\ directed convex powerspace of directed spaces,\ observationally-induced lower powerspace,\ observationally-induced lower powerspace