A quantitative computational model for complete partial metric spaces via formal balls

Given a partial metric space (X, p), we use (BX, subset of(dp)) to denote the poset of formal balls of the associated quasi-metric space (X,d(p)). We obtain characterisations of complete partial metric spaces and sup-separable complete partial metric spaces in terms of domain-theoretic properties of (BX, subset of(dp)) In particular, we prove that a partial metric space (X, p) is complete if and only if the poset (BX, subset of(dp)) is a domain. Furthermore, for any complete partial metric space (X,p), we construct a Smyth complete quasi-metric q on BX that extends the quasi-metric d(p) such that both the Scott topology and the partial order subset of(dp) are induced by q. This is done using the partial quasi-metric concept recently introduced and discussed by H. P. Kunzi, H. Pajoohesh and M. P. Schellekens (Kunzi et, al. 2006). Our approach, which is inspired by methods due to A. Edalat and R. Heckmann (Edalat and Heckmann 1998), generalises to partial metric spaces the constructions given by R. Heckmann (Heckmann 1999) and J. J. M. M. Rutten (Rutten 1998) for metric spaces.