Re: I vote NO on: Motion P1788/M0032:midpoint
On 2012-04-02 14:04:22 +0200, Vincent Lefevre wrote:
> I vote NO on: Motion P1788/M0032:midpoint
>
> The main problems (mentioned in my mail on 15 Mar 2012 15:51:29 +0100)
> are:
[...]
A third problem I've just noticed (this one is new): the motion says
that for any X and Y that live at Level 2,
"X \subset Y ==> if (inf_F(X)==inf_F(Y)) then mid_F(X) <= mid_F(Y)"
However I don't think one necessarily wants mid_F(X) <= mid_F(Y).
This inequality is not satisfied on the following counter-example
anyway.
Let F be a radix-10, 1-digit precision floating-point system.
Let the interval type be based on a triplex representation
<mid,rad1,rad2>. Let's choose:
X = <20,-5,-3> = [15,17]
Y = <20,-9,-3> = [11,17]
One has: "X \subset Y and inf_F(X) = inf_F(Y) = 10, so that the
conditions of the properties are satisfied.
Then:
mid_F(X) = round2Nearest_F(mid(X)) = round2Nearest_F(16) = 20,
mid_F(Y) = round2Nearest_F(mid(Y)) = round2Nearest_F(14) = 10.
The inequality mid_F(X) <= mid_F(Y) doesn't hold! Actually, I don't
see anything wrong by having mid_F(X) > mid_F(Y) here, since X >= Y.
The problem comes from the fact that the midpoint is based on a
Level 1 definition (then mid(X) is rounded) while the property
is based on Level 2 lower bounds of the intervals.
--
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <http://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <http://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)