3rd Irish Workshop on Formal Methods (IWFM)
1st - 2nd July 1999
The notion of a semivaluation has been introduced in [Sch98]. Aside from providing a novel concept generalizing valuations on lattices to the context of semilattices, semivaluations shed new light on the notion of a “partial metric” well known from theoretical computer science (e.g. [Mat94], [Mat95], [O’N97], [BS97] and [BSh97]).
As discussed in [Sch98], the characterization of partial metrics in terms of semivaluations is non-trivial and involves the solution of an open problem of the Survey Paper “Non-symmetric Topology” (Problem 7 of [Kün93]) for the class of quasi-uniform semilattices.
We recall from [Sch98] that the traditional domain theoretic examples, including the well known class of totally bounded Scott domains (e.g. [Smy91]), all correspond to semivaluation spaces. As such it is possible to study Quantitative Domain Theory (e.g. [FSW96]) in this simplified context, similar to the study of metric lattices (uniform lattices) in the more basic context of valuation spaces (cf. [Bir84] and also [Web91]). Hence the notion of a semivaluation is of sufficient interest to merit an independent study.
The main purpose of this short note is to provide a basic introduction to the notion of a semivaluation independent of the domain theoretic considerations of [Sch98] and to discuss a recently obtained characterization of valuations in terms of semivaluations.