He99 : Abstract
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.