Tensor Products and Powerspaces in Quantitative Domain Theory
Philipp Sünderhauf · Electronic Notes in Theoretical Computer Science · 1997
One approach to quantitative domain theory is the thesis that the underlying boolean logic of ordinary domain theory which assumes only values in the set {true, false} is replaced by a more elaborate logic with values in a suitable structure Ν. (We take Ν to be a value quantale.) So the order ⊑ is replaced by a generalised quasi-metric d, assigning to a pair of points the truth value of the assertion x ⊑ y. In this paper, we carry this thesis over to the construction of powerdomains. This means that we assume the membership relation ∈ to take its values in Ν. This is done by requiring that the value quantale Ν carries the additional structure of a semiring. Powerdomains are then constructed as free modules over this semiring. For the case that the underlying logic is the logic of ordinary domain theory our construction reduces to the familiar Hoare powerdomain. Taking the logic of quasi-metric spaces, i.e. Ν = [0, ∞] with usual addition and multiplication, reveals a close connection to the powerdomain of extended probability measures. As scalar multiplication need not be nonexpansive we develop the theory of moduli of continuity and m-continuous functions. This makes it also possible to consider functions between quantitative domains with different underlying logic. Formal union is an operation which takes pairs as input, so we investigate tensor products and their behavior with respect to the ideal completion.