The Directed Probabilistic Powerspace

TL;DR

This paper extends the probabilistic powerdomain concept to directed spaces, constructing a free directed space-cone and exploring its relation to classical probabilistic powerdomains, advancing semantics modeling for probabilistic nondeterminism.

Contribution

It introduces a novel probabilistic powerspace for directed spaces, linking domain theory with directed space structures and classical probabilistic powerdomains.

Findings

Constructed the probabilistic powerspace as a free directed space-cone.

Established relationships between the new construction and classical probabilistic powerdomains.

Extended domain-theoretic semantics to directed spaces with probabilistic features.

Abstract

Probabilistic powerdomain in domain theory plays an important role in modeling the semantics of nondeterministic functional programming languages with probabilistic choice. In this paper, we extend the notion of powerdomain to directed spaces, which is equivalent to the notion of the T0 monotone-determined space [4]. We construct the probabilistic powerspace of the directed space, which is defined as a free directed space-cone. In addition, the relationships between our construction and classical probabilistic powerdomain are studied.