On Computable Metrization

Every second-countable regular topological space X is metrizable. For a given “computable” topological space satisfying an axiom of computable regularity M. Schröder [M. Schröder, Effective metrization of regular spaces, in: K.-I. Ko, A. Nerode, M. B. Pour-El, K. Weihrauch and J. Wiedermann, editors, Computability and Complexity in Analysis, Informatik Berichte 235 (1998), pp. 63–80, cCA Workshop, Brno, Czech Republic, August, 1998.] 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 [K. Weihrauch, Computable Analysis, Springer, Berlin, 2000]. While Schröder'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. By partial completion we extend (X,d) to a metric space (X˜,d˜) with computable metric and canonical representation. We construct a computable sequence (xi)i∈N of points which is dense in (X˜,d˜). The isometric embedding of X into X˜ is computable. Its inverse is computable if some further computability axiom holds true. The space (X˜,d˜) can be embedded computationally into the computable metric space generated by the sequence (xi)i∈N of points. The inverse of this embedding is continuous