Cancellation and Level-1 overflowed intervals
Nate's main argument is, if I interpret correctly, the following:
> Date: Wed, 11 Apr 2012 10:03:43 -0500
> ...
> For me, it is more important that the Level 1 arithmetic is cancellative,
> and the current P1788 model with unbounded intervals does not have this
> property.
Yet I fail to see how A + X = B + X
can imply A = B
when X = [x, OVR]
even when we interpret the latter to denote a family of intervals.
No matter how you quantify over the family, I see no way to tie the
instance of X that is added to A to the one that is added to B.
This is perhaps a subtle point, because after all the same X is used.
The trouble is that in an actual application we really have:
A + X = B + Y
and we want to derive A=B from X=Y. That however requires
attaching the entire computation history to X and Y; we cannot
tell that [x,OVR] = [y,OVR] (in the sense needed here) from x=y.
Just as with x+oo = y+oo in Rbar, we have x+OVR = y+OVR for all finite x,y.
I'm reasoning at Level 1 here, to be clear. At level 2 cancellation does
not apply anyway, as we all know (including Nate), just as it does not
apply even in F (finite FP numbers), never mind Fbar.
Michel.
---Sent: 2012-04-26 16:09:32 UTC