Approximation of Metric Spaces by Partial Metric Spaces

Partial metrics are generalised metrics with non-zero self-distances. We slightly generalise Matthews' original definition of partial metrics, yielding a notion of weak partial metric. After considering weak partial metric spaces in general, we introduce a weak partial metric on the poset of formal balls of a metric space. This weak partial metric can be used to construct the completion of classical metric spaces from the domain-theoretic rounded ideal completion.