Computable metrization

Every second-countable regular topological space X is metrizable. For a given "computable" topological space satisfying an axiom of computable regularity M. Schroder [10] has constructed a computable metric. In this article we study whether this metric space (X, d) can be considered computationally as a subspace of some computable metric space [15]. While Schroder's construction is "pointless", i.e., only sets of a countable base but no concrete points are known, for a computable metric space a concrete dense set of computable points is needed. But there may be no computable points in X. By converging sequences of basis sets instead of Cauchy sequences of points we construct a metric completion ((X) over tilde, (d) over tilde) of a space (X, d) together with a canonical representation. We show that there is a computable embedding of (X, d) in ((X) over tilde, (d) over tilde) with computable inverse. Finally, we construct a notation of a dense set of points in ((X) over tilde, (d) over tilde) with computable mutual distances and prove that the Cauchy representation of the resulting computable metric space is equivalent to. Therefore, every computably regular space has a computable homeomorphic embedding in a computable metric space, which topologically is its completion. By the way we prove a computable Urysohn lemma. (C) 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.