[std-interval] More on interval computations as proofs
Dr John Pryce
j.d.pryce at ntlworld.com
Fri Sep 22 01:43:53 PDT 2006
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
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.
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].
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).
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.
Dr John and Mrs Kate Pryce
142 Kingshill Rd
Swindon, Wiltshire SN1 4LW
More information about the Std-interval