Effective and sequential definition by cases on the reals via infinite signed-digit numerals
Martı́n Hötzel Escardó · Electronic Notes in Theoretical Computer Science · 1998
The lexicographical and numerical orders on infinite signed-digit numerals are unrelated. However, we show that there is a computable normalization operation on pairs of signed-digit numerals such that for normal pairs the two orderings coincide. In particular, one can always assume without loss of generality that any two numerals that denote the same number are themselves the same. We apply the order-normalization operator to easily obtain an effective and sequential definition-by-cases scheme in which the cases consist of inequalities between real numbers.