Namespaces
Variants
Actions

Difference between revisions of "Constructive metric space"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
Line 1: Line 1:
 +
<!--
 +
c0253501.png
 +
$#A+1 = 121 n = 0
 +
$#C+1 = 121 : ~/encyclopedia/old_files/data/C025/C.0205350 Constructive metric space
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
 +
 +
{{TEX|auto}}
 +
{{TEX|done}}
 +
 
The concept of metric space used in constructive mathematics. The notion of recursive metric space has nearly the same meaning.
 
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" />).
+
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|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 <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.
+
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 <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
+
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
  
<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>
+
$$
 +
\rho ( x _ {1} * \dots * x _ {n} , y _ {1} * \dots * y _ {n} )  = \
 +
\sqrt {
 +
\sum _ { i= } 1 ^ { n }
 +
( x _ {i} - y _ {i} )
 +
^ {2} } .
 +
$$
  
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
+
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
  
<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>
+
$$
 +
\forall n , x _ {1} ,\
 +
x _ {2}  ( ( 0 \leq  x _ {1} , x _ {2} \leq  1 \& | x _ {1} - x _ {2} | < 2 ^ {- \gamma ( n) } ) \supset
 +
$$
  
<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>
+
$$
 +
\supset \
 +
{}| f ( x _ {1} ) - f ( x _ {2} ) | < 2  ^ {-} n )
 +
$$
  
(<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
+
( $  \epsilon \mathfrak A \epsilon $
 +
denotes the description (code) of the algorithm $  \mathfrak A $).  
 +
The metric algorithm $  \rho $
 +
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>
+
$$
 +
\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 <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.
+
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 <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" />.
+
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 <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.
+
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.
 
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).
+
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 <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" />.
+
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.
 
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.
Line 35: Line 178:
 
====References====
 
====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>
 
<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====
 
====Comments====

Revision as of 20:31, 4 June 2020


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)
How to Cite This Entry:
Constructive metric space. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Constructive_metric_space&oldid=18953
This article was adapted from an original article by B.A. Kushner (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article