[std-interval] More on interval computations as proofs

[Dr John Pryce]

Guillaume and all

At 07:14 19/09/06, Guillaume Melquiond wrote:
>Le dimanche 17 septembre 2006 à 23:49 +0100, Dr John Pryce a écrit :
>[...]
> > Guillaume, I think I understand your reasoning.
> > But does not interval computation requires a 
> uniquely precise specification?
>[...]
> > Each elementary interval calculation is justified
> > by some mathematical result - most of them fairly
> > shallow, but sometimes a profound one as in the
> > appeal to a fixed-point theorem, central in the
> > solution of differential equation systems. If
> > EVEN ONE STEP in this chain breaks down, the whole proof breaks down.
>
>Given intervals in input, the proposal guarantees that any sequence of
>interval operations will lead to interval results and their properties
>are perfectly defined (from an interval arithmetic point of view). This
>is a strong guarantee: as long as you don't mess with the intermediate
>results somehow, your "proof" holds.
>
>Now, the proposal flags some behaviors as undefined. None of them
>happens in the situation above. It can only happen when the programmer
>introduces objects that are not intervals among the computations.
>Moreover, note that we are talking about data that are not specified by
>the Standard.

I want to tease out how far this is true of your 
present standard text. Here is a first example, 
using the following code fragment.

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 1. Normal case
Input V = [3,4]
       m = (3 + 4)/2.0 = 3.5              by 26.6.12#5 & defs of inf, sup.
       W = [3,4] - 3.5
By 26.6.6#6 (Oops, there is a typo, but what it 
SHOULD do is) convert the 3.5 to interval<T>(3.5) and then subtract, giving
        W = [-0.5, 0.5].
OK.

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".

On a different issue (numeric, not semantic) the 
formula (inf(x)+sup(x))/T(2.0) for midpoint is 
flawed on a non-binary machine such as the old 
IBMs. It can give a midpoint lying outside the 
interval. For instance if the arithmetic is 4 sig 
fig decimal, and V=[9.997,9.999] we get 
(inf(V)+sup(V)) = T(19.996) = 20.00 if rounding 
to nearest is used, so m = 10.00.

Away to a couple of reunion dinners, but more on 
these lines to follow after the weekend, hopefully.

Regards

John
Dr John and Mrs Kate Pryce
142 Kingshill Rd
Swindon, Wiltshire SN1 4LW
UK
Tel (+44)1793-331062