next up previous contents
Next: Inequality tests in real Up: Numerical order in signed-digit Previous: Numerical order in signed-digit

Order normalization

A pair 74#74 of numerals is order-normal it its lexicographical order coincides with its numerical order, in the sense that
1.
57#57 and 75#75, or
2.
76#76, or
3.
77#77 and 78#78.
Thus, for order-normal pairs 74#74, the condition 52#52 implies 76#76. In order to emphasize that order-normality is a property of pairs of numerals and not of single numerals, we observe that the pair 79#79 is always order-normal.

Theorem 9.1   There is a computable, denotation-preserving idempotent map

80#80

whose fixed-points are order-normal pairs.

That is, 81#81 implies that
1.
82#82,
2.
83#83 is order-normal, and
3.
  84#84.
In particular, one can always assume w.l.o.g. that any two numerals that denote the same numbers are themselves the same, despite the fact that single numerals don't have effectively determinable canonical forms. Since one can effectively translate between the notation systems of real numbers discussed in Chapter 7, all of them have the same property.

Lemma 8.1 is the fundamental ingredient of the proof of the theorem, which is not included here. Together with topology, the identities of the lemma actually capture all identities induced by the denotation function. Let 85#85 be the least equivalence relation such that

86#86,          87#87.
The relation 85#85 is strictly weaker than the relation 50#50. For example, 88#88, because both numerals denote the number 0, but they are not related by 85#85, because it is not possible to obtain one from the other by finitely many applications of the above identities. But if we add limits to 85#85 then we get 50#50.

Proposition 9.2   The relation 50#50 is the topological closure of the relation 85#85 in the product space 89#89.

(Notice that 50#50 has to be closed because the denotation quotient map is continuous and 26#26 and [-1,1] are Hausdorff spaces.)


next up previous contents
Next: Inequality tests in real Up: Numerical order in signed-digit Previous: Numerical order in signed-digit
Martin Escardo
2000-10-02