×

Extension of valuations. (English) Zbl 1067.68089

Summary: Continuous valuations have been proposed by several authors as a way of modelling probabilistic nondeterminism in programming language semantics. Let \((X,{\mathcal O})\) be a topological space. A quasi-simple valuation on \(X\) is the sup of a directed family of simple valuations. We show that quasi-simple valuations are exactly those valuations that extend to continuous valuations to the Alexandroff topology on the specialisation preordering of the topology \({\mathcal O}\). A number of applications are presented. In particular, we recover Jones’ result that every continuous valuation is quasi-simple if \(X\) is a continuous dcpo – in this case there is a least extension to the Alexandroff topology. We show that this can be refined if \(X\) is algebraic, where every continuous valuation is the sup of a directed family of simple valuations based on finite elements. We exhibit another class of spaces in which every continuous valuation is quasi-simple, the so-called finitarily coherent spaces – in this case there is a largest extension to the Alexandroff topology. In general, the extension to the Alexandroff topology is not unique, unless, for example, the original valuation is bicontinuous. We also show that other natural spaces of valuations, namely those of discrete valuations and point-continuous valuations, can be characterised by similar extension theorems.

MSC:

68Q55 Semantics in the theory of computing
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
06B35 Continuous lattices and posets, applications
PDFBibTeX XMLCite
Full Text: DOI