View source for Constructive metric space

The concept of metric space used in constructive mathematics. The notion of recursive metric space has nearly the same meaning.

A list <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c0253501.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c0253502.png" /> is some set of constructive objects (usually words over some alphabet) and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c0253503.png" /> is an algorithm converting any pair of elements of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c0253504.png" /> into a constructive real number (see [[Constructive analysis|Constructive analysis]]), is called a constructive metric space if for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c0253505.png" /> the following properties hold: 1) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c0253506.png" />; 2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c0253507.png" /> (here and in what follows the term  "algorithm"  is used in the sense of one of the precise notions of algorithm). The set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c0253508.png" /> and the algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c0253509.png" /> are respectively called the carrier and metric algorithm of the constructive metric space, and the elements of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535010.png" /> are the points of this constructive metric space. The axioms 1), 2) imply that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535011.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535012.png" />. Two points <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535013.png" /> are called equivalent (respectively, distinct) in the constructive metric space <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535014.png" /> if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535015.png" /> (respectively, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535016.png" />).

Examples of constructive metric spaces. a) The space of natural numbers <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535017.png" />. The carrier of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535018.png" /> is the set of natural numbers (the natural numbers are treated as words of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535019.png" />), while the metric algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535020.png" /> is given by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535021.png" />. The spaces <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535022.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535023.png" /> of rational and constructive real numbers, respectively, are defined similarly.

b) The <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535024.png" />-dimension Euclidean space <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535025.png" />. The carrier of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535026.png" /> is the set of words of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535027.png" />, where the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535028.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535029.png" />, are constructive real numbers, and the metric algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535030.png" /> is constructed so that

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535031.png" /></td> </tr></table>

c) The space <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535032.png" /> of uniformly-continuous constructive functions on the unit interval. The carrier of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535033.png" /> is the set of words of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535034.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535035.png" /> is a constructive function defined throughout the unit interval and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535036.png" /> is an algorithm taking each natural number into a natural number so that

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535037.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535038.png" /></td> </tr></table>

(<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535039.png" /> denotes the description (code) of the algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535040.png" />). The metric algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535041.png" /> is constructed so that

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535042.png" /></td> </tr></table>

The complicated form of the carrier of the space <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535043.png" /> is necessary for the effective computability of the metric.

d) The Baire space of general recursive functions. The carrier of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535044.png" /> is the set of Gödel numbers of general recursive functions and the metric algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535045.png" /> is constructed so that if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535046.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535047.png" /> are general recursive functions with numbers <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535048.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535049.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535050.png" /> if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535051.png" /> for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535052.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535053.png" /> if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535054.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535055.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535056.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535057.png" /> be a constructive metric space. An algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535058.png" /> is called a sequence of points of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535059.png" /> if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535060.png" /> for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535061.png" />. The sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535062.png" /> is called regular if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535063.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535064.png" />. A regular sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535065.png" /> converges to the point <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535066.png" /> of the constructive metric space <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535067.png" /> if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535068.png" /> for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535069.png" />. A constructive metric space <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535070.png" /> is called complete if there exists an algorithm that finds for each regular sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535071.png" /> (of points of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535072.png" />) a point of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535073.png" /> to which <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535074.png" /> converges. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535075.png" /> is called separable if there exists algorithms <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535076.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535077.png" /> is a sequence of points of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535078.png" /> and for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535079.png" /> and any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535080.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535081.png" /> is a natural number where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535082.png" />. All the spaces <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535083.png" /> of the examples a)–d) are separable, the spaces <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535084.png" /> are complete as well. An example of a non-separable constructive metric space is given by considering a subspace of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535085.png" /> induced by a non-recursively enumerable set. Many of the results of the classical theory of metric spaces can be stated in terms of constructive metric spaces; in particular, the constructive variant of Hausdorff's theorem, stating that for any constructive metric space its completion can be constructed, is of great importance.

The process of completing a constructive metric space is a powerful means for introducing certain structures in constructive mathematics. Constructive real numbers are introduced in this way, and the natural analogues of the classical notions of measurable sets and functions, Lebesgue-integrable functions, etc., can be defined. One of the fundamental aims of the theory of constructive metric spaces is the study of algorithmic mappings that are well-defined with respect to some or other computable metrics.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535086.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535087.png" /> be two constructive metric spaces. By an algorithmic operator of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535089.png" /> is meant an algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535090.png" /> satisfying the following properties: a) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535091.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535092.png" /> is defined, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535093.png" />; and b) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535094.png" /> are equivalent points of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535095.png" /> (that is, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535096.png" />) and if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535097.png" /> is defined, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535098.png" /> is defined and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c02535099.png" /> are equivalent points of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350100.png" />. Algorithmic operators of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350101.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350102.png" /> are constructive functions of one, respectively, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350103.png" />, variables; algorithmic operators of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350104.png" /> are conventionally called effective functionals (or effective operations).

A fundamental result in the theory of algorithmic operators is Tseitin's theorem, which states that in the case of a complete separable constructive metric space <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350105.png" /> one can, for any algorithmic operator <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350106.png" /> of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350107.png" />, construct for each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350108.png" /> an algorithmically (recursively) enumerable set of balls covering the domain of definition of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350109.png" /> such that the oscillation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350110.png" /> on any ball of this set does not exceed <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350111.png" />. This theorem implies the well-known result on the extendability of effective functionals to partial recursive functionals. Another important corollary of the above result is the theorem on the continuity of algorithmic operators: If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350112.png" /> is a complete separable constructive metric space and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350113.png" /> is an arbitrary constructive metric space, then for any algorithmic operator <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350114.png" /> of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350115.png" /> one can construct an algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350116.png" /> such that for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350117.png" /> in the domain of definition of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350118.png" /> and any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350119.png" />, the number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350120.png" /> is a natural number, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350121.png" /> implies that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025350/c025350122.png" />.

Using the same general methods as for the case of constructive metric spaces, one can develop a theory of constructive normed spaces and Hilbert spaces.

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  G.S. Tseitin,   "Algorithmic operators in constructive metric spaces"  ''Trudy Mat. Inst. Steklov.'' , '''67'''  (1962)  pp. 295–361  (In Russian)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  Y.N. Moschovakis,   "Recursive metric spaces"  ''Fund. Math.'' , '''55''' :  3  (1964)  pp. 215–238</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  N.A. Shanin,   "Constructive real numbers and constructive function spaces"  ''Trudy Mat. Inst. Steklov.'' , '''67'''  (1962)  pp. 15–294  (In Russian)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  B.A. Kushner,   "Lectures on constructive mathematical analysis" , Amer. Math. Soc.  (1984)  (Translated from Russian)</TD></TR></table>



====Comments====
The article above is only concerned with constructive analysis in the narrow sense of the Soviet school (see also [[Constructive mathematics|Constructive mathematics]]). A different approach can be found in [[#References|[a1]]], [[#References|[a2]]]. For the notion of a recursive metric space see [[#References|[a3]]].

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  E. Bishop,   D.S. Bridges,   "Constructive analysis" , Springer  (1985)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  M.J. Beeson,   "Foundations of constructive mathematics" , Springer  (1985)</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  O. Alberth,   "Computable analysis" , McGraw-Hill  (1980)</TD></TR></table>