Re: roundTiesToEven in precision 1

[John R Harrison <johnh@xxxxxxxxxxxxxxxx>]

Hi Vincent,

| FYI, the precision-1 problem in binary is something that has been
| known for quite a long time by us, MPFR developers, and that's the
| only reason why the minimal precision in MPFR is 2, and not 1 (we
| also thought that 1 was not really useful, and that's why we did
| not try to fix the problem).

I'd hit the same thing when formalizing floating-point arithmetic.
For example, see the first text paragraph on page 8 of this paper:

  http://www.cl.cam.ac.uk/~jrh13/papers/fparith.pdf

Many of the formal theorems about round-to-nearest carry an extra
"2 <= precision fmt" hypothesis. And yet, I had seen this as the
typical pedantry forced on one by formalization, and never imagined a
context in which anyone would really care about precision-1 rounding.
I must admit, I still didn't see the point after your first message
until the later mention of character output.

John.