The denotation map

As above, we only consider fractional numbers, ignoring the decimal point and the leading zero in decimal notation. A numeral is an infinite sequence over the digit alphabet 25#25. A numeral 27#27 denotes the number

28#28

The denotation map 29#29 is the fundamental link between the operational and denotational semantics of real number computation as discussed in Chapter 4--but notice that different operational semantics will use different notation spaces. Our denotation map is a surjection

30#30

It is not an injection because the decimal rationals 31#31 have two decimal notations--the reason is that we consider infinitely long runs of digits 9 as legitimate as infinitely long runs of digits 0, because there is no way of ruling out the former by computational means.