Next: Inequality tests in real
Up: Numerical order in signed-digit
Previous: Numerical order in signed-digit
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: Inequality tests in real
Up: Numerical order in signed-digit
Previous: Numerical order in signed-digit
Martin Escardo
2000-10-02