[std-interval] More on interval computations as proofs

[Guillaume Melquiond]

Le vendredi 22 septembre 2006 à 00:43 +0100, Dr John Pryce a écrit :

> Input is V, which is an interval known to be 
> valid (not NaI) and nonempty, but perhaps infinite. Do:
>        m = midpoint(V);
>        W = V-m; //centre V about its midpoint.
> 
> Aim:
> To see if the current standard stops one getting 
> nonsense results without warning.

> Case 2.
> Input V = [3,Inf)
>        m = (3 + Inf)/2.0 = Inf
>        W = [3,Inf) - Inf
> The Inf is converted to interval<T>(Inf) = 
> [REALMAX, Inf) probably, by 26.6.4#7. So
>         W = (-Inf, Inf).
> 
> Case 3.
> Input V = (-Inf,Inf)
>        m = (-Inf + Inf)/2.0 = NaN
>        W = (-Inf,Inf) - NaN
> The NaN is converted to interval<T>(Inf) = empty, by 26.6.4#7. So
>         W = empty.
> 
> I may have made a slip in these calculations. If 
> not, I am not happy about either of cases 2 & 3 
> which to my mind are both "nonsense results without warning".

Both cases 2 and 3 are actually forbidden by the proposal. But the code
can be modified a bit (namely do an explicit conversion from the number
to an interval) so that it becomes defined and matches your
interpretation. Now, for case 3, it would end up throwing an exception
according to our recent discussions.

Anyway, what happens is not really relevant, it seems to me that the
flaw is in the specification of midpoint, both for cases 2 and 3. I
admit that I had not considered the situation of using midpoint on
unbounded intervals, because in practice (mine at least), you always end
up intersecting your interval with a bounded interval before computing
the midpoint.

Still, the specification is a bit poor. Both in the divide-by-2 as you
already mentioned, and in the addition as it could overflow for bounded
intervals far from zero. This kind of wording may be more satisfactory:

        Returns: a finite number included in \texttt{x} when \texttt{x}
        is not empty, an implementation-defined value otherwise.
        Note: when \texttt{x} is a bounded interval, the result is close
        to the real number $\frac{1}{2}(\texttt{inf(x)} +
        \texttt{sup(x)})$.

Best regards,

Guillaume