Dear Will,
thank you for your most recent post; I find it very helpful. Also for the possible benefit of other readers, let me rephrase what you call the "double rounding problem", which doesn't need large numbers to be explained:
Let M and N be two sets of (real) numbers where the result of the rounding of a real number x should lie. E.g., M and N can be the sets of floating-point numbers with mantissa widths m and n. Let us assume that M is a subset of N. If x = y - eps where y in N and eps > 0 sufficiently small, rounding of x to N will yield y. Assuming that y is not in M but y +/- d are, a rounding algorithm from N to M will have to decide with no further information whether it maps y to y + d or y - d, both being equidistant to y. Now, a direct rounding of x to M is y - d. The two-step rounding, first to N and then to M would achieve this if the rounding algorithm from N to M maps y to y - d. This is not universal, however. If it were that x = y + eps, it would have to map y to y + d instead.
The simplest example is probably given when M and N are the sets of floating-point numbers with mantissa widths 1 and 2. Let x = 1011 in binary notation. Rounding to N gives y = 1100. We have d = 0100. So, rounding to M is either 10000 (round to even or round to infinity) or 1000 (round to zero). Now a direct rounding of x = 1011 to M gives 1000. Finally, play the same game with x = 1101.
While the "double-rounding" problem is, according to the specialist, the main reason making converting decimal scientific notation to binary floating-point non-trivial, it is noteworthy that it is independent of any decimal (or other) printing format.
One might want to explain the "double-rounding" problem by the discontinuity of the rounding function. In fact, when the numbers in M and N are sufficiently evenly spaced, remembering a sign, i.e. writing y +/- 0 where +/- is a signed zero instead of y is enough to make the double rounding equivalent to the single rounding, which I make more precise below. Incidentally, one can see this as a hint that the IEEE floating point format is unbalanced in a certain sense; as branch cuts, for example, can appear everywhere in the complex plane, not only 0 but all floating-point numbers should remember whether they are constructed by a limit from below or from above.
Now let's make the previous remark more precise with the following proposition concerned with binary floating-point approximations.
Proposition: Let x be a real number. Let m < n be natural numbers. Let y be a rounding of x to n significant bits. Then there exists a rounding z of y to m significant bits such that z is also a rounding of x to m significant bits.
Proof: Let M and N be the set of numbers with m and n, respectively, significant bits. There exists t0 and t1 in M such that M does not intersect the open interval ]t0, t1[ and such that x in [t0, t1]. We distinguish two cases: In the first case, N does not intersect ]t0, t1[. In this case, any rounding of x to n significant bits is a rounding of x to m significant bits and vice versa (and equal to t0 or t1). In the second case, N does intersect ]t0, t1[. In this case, t = (t0 + t1)/2 is in N. If x in [t0, t], we therefore have y in [t0, t]. From that it follows that t0, which is a rounding of x to m significant bits, is a rounding of y to m significant bits. If x in [t, t1], we argue similarly.
After these preliminary remarks, let me finally come to the two claims in Will's previous email.
Claim 1 is about how SRFI 77/R6RS is to be read. Unless I misinterpret anything in Will's text, Claim 1 is more or less literally what's in the two documents, is consistent with Mike's paper from where the x|p idea came from, and is also how Mike as the author of SRFI 77 who was responsible for the x|p notation reads the text. I, therefore, stand by Claim 1.
I would also like to add that the term "double rounding" might be slightly misleading in this context. In the notation 1.1|54, the first rounding from the mathematical number 1.1 to the actual mathematical number represented by 1.1|54 is of a slightly different semantic quality than the the rounding of mathematical number 1.1|54 to an IEEE double. The precise decimal number 1.1 plays no role in the lexical notation as long as for any other decimal number x the mathematical number x|54 is the same as 1.1|54.
Claim 2, different from Claim 1, is ultimately not about how to read SRFI 77/R6RS. Whether Claim 2 holds or not does not touch the original topic of this thread. The original context of Claim 2 was a discussion on ways to implement the semantics of Claim 1 efficiently. If Claim 2 does not have to be retracted, Will's method cited in Mike's paper seems to be an efficient way to implement the semantics of Claim 1. If Claim 2 has to be retracted, reading numbers with an explicitly given mantissa width may not be as efficient as reading numbers without, but this wouldn't make explicit mantissa widths unviable because (1) some important implementations like Chez Scheme have always used bigint arithmetic so there would be no difference in efficiency and (2) the vast majority of number literals in practice do not have an explicitly given mantissa width and can be read as efficiently as before.
I made Claim 2 in response to an earlier post by Will in the context that I didn't understand his argument that arbitrary precision would be needed to process the x|p notation. If Claim 2 has to be retracted, it will mean that I have understood his argument. (Given your helpful examples, I think I already have understood your line of thinking, Will.)
That said, I don't think that Claim 2 in the way I intended it has to be retracted, though. The reason is the Proposition I formulated above. The point is that R6RS does not prescribe how ties are to be resolved when a number has to be approximated by a number object with limited precision (i.e., no rounding mode is specified). In other words, a binary approximation of x|53 in the IEEE floating point format is a suitable binary approximation of x|p for any p > 53. The only thing we lose in an implementation that makes use of the statement of Claim 2 is that the expression (inexact #ex|p) does not evaluate to the same number object as x|p, but I can't find a statement that it must. (That said, if I were an implementer, I would choose the slower method using bigints so that the invariant still holds.)
I can illustrate this point with the example 99999999999999983222783|54. By Claim 1, this number literal describes the mathematical number 99999999999999983222784, which now has to be represented by IEEE double. The two different methods ("double rounding" versus "single rounding") give, as shown in Will's post, the approximations 99999999999999991611392 and 99999999999999974834176. The point is now that both approximations differ from the mathematical number 99999999999999983222784 by exactly the same absolute value, namely 8388608, so both approximations are equally good approximations and both methods give results allowed by R6RS.
Let me conclude by saying that we haven't touched on whether the x|p notation is particularly helpful or useful or not. This is outside the scope of this thread. The only thing we can conclude from this thread is that it does not touch the efficiency of the rest of the number system, in particular, the reading and writing of numbers without an explicitly given mantissa width.
Marc