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 $ \{ \mathfrak M , \rho \} $, where $ \mathfrak M $ is some set of constructive objects (usually words over some alphabet) and $ \rho $ is an algorithm converting any pair of elements of $ \mathfrak M $ into a constructive real number (see Constructive analysis), is called a constructive metric space if for any $ X , Y , Z \in \mathfrak M $ the following properties hold: 1) $ \rho ( X , X ) = 0 $; 2) $ \rho ( X , Y ) \leq \rho ( X , Z ) + \rho ( Y , Z ) $( here and in what follows the term "algorithm" is used in the sense of one of the precise notions of algorithm). The set $ \mathfrak M $ and the algorithm $ \rho $ are respectively called the carrier and metric algorithm of the constructive metric space, and the elements of $ \mathfrak M $ are the points of this constructive metric space. The axioms 1), 2) imply that $ \rho ( X , Y ) \geq 0 $ and $ \rho ( X , Y ) = \rho ( Y , X ) $. Two points $ X , Y \in \mathfrak M $ are called equivalent (respectively, distinct) in the constructive metric space $ \{ \mathfrak M , \rho \} $ if $ \rho ( X , Y ) = 0 $( respectively, $ \rho ( X , Y ) \neq 0 $).

Examples of constructive metric spaces. a) The space of natural numbers $ H $. The carrier of $ H $ is the set of natural numbers (the natural numbers are treated as words of the form $ 0 , 01 , 011 ,\dots $), while the metric algorithm $ \rho $ is given by $ \rho ( m , n ) = | m - n | $. The spaces $ R $ and $ E _ {1} $ of rational and constructive real numbers, respectively, are defined similarly.

b) The $ n $- dimension Euclidean space $ E _ {n} $. The carrier of $ E _ {n} $ is the set of words of the form $ x _ {1} * \dots * x _ {n} $, where the $ x _ {i} $, $ 1 \leq i \leq n $, are constructive real numbers, and the metric algorithm $ \rho $ is constructed so that

$$ \rho ( x _ {1} * \dots * x _ {n} , y _ {1} * \dots * y _ {n} ) = \ \sqrt { \sum _ { i= } 1 ^ { n } ( x _ {i} - y _ {i} ) ^ {2} } . $$

c) The space $ C $ of uniformly-continuous constructive functions on the unit interval. The carrier of $ C $ is the set of words of the form $ \epsilon f \epsilon * \epsilon \gamma \epsilon $, where $ f $ is a constructive function defined throughout the unit interval and $ \gamma $ is an algorithm taking each natural number into a natural number so that

$$ \forall n , x _ {1} ,\ x _ {2} ( ( 0 \leq x _ {1} , x _ {2} \leq 1 \& | x _ {1} - x _ {2} | < 2 ^ {- \gamma ( n) } ) \supset $$

$$ \supset \ {}| f ( x _ {1} ) - f ( x _ {2} ) | < 2 ^ {-} n ) $$

( $ \epsilon \mathfrak A \epsilon $ denotes the description (code) of the algorithm $ \mathfrak A $). The metric algorithm $ \rho $ is constructed so that

$$ \rho ( \epsilon f _ {1} \epsilon * \epsilon \gamma _ {1} \epsilon ,\ \epsilon f _ {2} \epsilon * \epsilon \gamma _ {2} \epsilon ) = \ \max _ {0 \leq x \leq 1 } | f _ {1} ( x) - f _ {2} ( x) | . $$

The complicated form of the carrier of the space $ C $ is necessary for the effective computability of the metric.

d) The Baire space of general recursive functions. The carrier of $ B $ is the set of Gödel numbers of general recursive functions and the metric algorithm $ \rho $ is constructed so that if $ \phi _ {n} $ and $ \phi _ {m} $ are general recursive functions with numbers $ n $ and $ m $, then $ \rho ( n , m ) = 0 $ if $ \phi _ {n} ( i) = \phi _ {m} ( i) $ for any $ i $, and $ \rho ( n , m ) = 2 ^ {-} k $ if $ \phi _ {n} ( i) = \phi _ {m} ( i) $ for $ i < k $ and $ \phi _ {n} ( k) \neq \phi _ {m} ( k) $.

Let $ M = \{ \mathfrak M , \rho \} $ be a constructive metric space. An algorithm $ \beta $ is called a sequence of points of $ M $ if $ \beta ( n) \in \mathfrak M $ for every $ n $. The sequence $ \beta $ is called regular if $ \rho ( \beta ( m) , \beta ( n) ) < 2 ^ {-} n $ for $ m \geq n $. A regular sequence $ \beta $ converges to the point $ X $ of the constructive metric space $ M $ if $ \rho ( X , \beta ( n) ) \leq 2 ^ {-} n $ for any $ n $. A constructive metric space $ M $ is called complete if there exists an algorithm that finds for each regular sequence $ \beta $( of points of $ M $) a point of $ M $ to which $ \beta $ converges. $ M $ is called separable if there exists algorithms $ \alpha , \delta $ such that $ \alpha $ is a sequence of points of $ M $ and for any $ x \in M $ and any $ n $, $ \delta ( X * n ) $ is a natural number where $ \rho ( \alpha ( \delta ( X * n ) ) , X ) < 2 ^ {-} n $. All the spaces $ H , R , E _ {1} , E _ {n} , C , B $ of the examples a)–d) are separable, the spaces $ H , E _ {1} , E _ {n} , C $ are complete as well. An example of a non-separable constructive metric space is given by considering a subspace of $ H $ 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 $ M _ {1} = \{ \mathfrak M _ {1} , \rho _ {1} \} $, $ M _ {2} = \{ \mathfrak M _ {2} , \rho _ {2} \} $ be two constructive metric spaces. By an algorithmic operator of type $ M _ {1} \rightarrow M _ {2} $ is meant an algorithm $ \psi $ satisfying the following properties: a) if $ X \in \mathfrak M _ {1} $ and $ \psi ( X) $ is defined, then $ \psi ( X) \in \mathfrak M _ {2} $; and b) if $ X , Y $ are equivalent points of $ M _ {1} $( that is, $ \rho _ {1} ( X , Y ) = 0 $) and if $ \psi ( X) $ is defined, then $ \psi ( Y) $ is defined and $ \psi ( X) , \psi ( Y) $ are equivalent points of $ M _ {2} $. Algorithmic operators of type $ E _ {1} \rightarrow E _ {1} $, $ E _ {n} \rightarrow E _ {1} $ are constructive functions of one, respectively, $ n $, variables; algorithmic operators of type $ B \rightarrow H $ 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 $ M _ {1} $ one can, for any algorithmic operator $ \psi $ of type $ M _ {1} \rightarrow M _ {2} $, construct for each $ n $ an algorithmically (recursively) enumerable set of balls covering the domain of definition of $ \psi $ such that the oscillation of $ \psi $ on any ball of this set does not exceed $ 2 ^ {-} n $. 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 $ M _ {1} $ is a complete separable constructive metric space and $ M _ {2} $ is an arbitrary constructive metric space, then for any algorithmic operator $ \psi $ of type $ M _ {1} \rightarrow M _ {2} $ one can construct an algorithm $ \alpha $ such that for any $ X , Y $ in the domain of definition of $ \psi $ and any $ n $, the number $ \alpha ( X , n ) $ is a natural number, where $ \rho _ {1} ( X , Y ) < 2 ^ {- \alpha ( X , n ) } $ implies that $ \rho _ {2} ( \psi ( X) , \psi ( Y) ) < 2 ^ {-} n $.

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

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

Comments

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

References

[a1]	E. Bishop, D.S. Bridges, "Constructive analysis" , Springer (1985)
[a2]	M.J. Beeson, "Foundations of constructive mathematics" , Springer (1985)
[a3]	O. Alberth, "Computable analysis" , McGraw-Hill (1980)