[std-interval] More on interval computations as proofs

[R. Baker Kearfott]

At 07:54 AM 9/22/2006 +0200, Guillaume Melquiond wrote:
>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.
.
.
.
>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)})$.
>

Yes.  Actually, I think you are right that the main priority should
be to get the specification right in cases that will occur in practice,
and I think John is right in the sense that the system should be
logically coherent and consistent.  (For one thing, we might not
anticipate all cases of practical importance.)

In the above rewording what does "close to" mean in this context?  Also,
"is" does not sound very normative, and I assume you want it to be normative.
How is the following rewording?

"When \texttt{x} is a bounded interval, the result will be an approximation
        to the real number $\frac{1}{2}(\texttt{inf(x)} +
        \texttt{sup(x)})$."

??

Of course, the above would be correct if midpoint were intended to be
a of real type, but I see you have it is of <class T>.  in that case,
how would the following wording work?

"When \texttt{x} is a bounded interval, the result will be an enclosure
        to the real number $\frac{1}{2}(\texttt{inf(x)} +
        \texttt{sup(x)})$."

By the way, in implementations of interval arithmetic with which I
am familiar, "midpoint" is a real type.  However, I do not have a
strong opinion about whether it should be a real approximation or
an enclosure.

Best regards,

Baker


---------------------------------------------------------------
R. Baker Kearfott,    rbk at louisiana.edu   (337) 482-5346 (fax)
(337) 482-5270 (work)                     (337) 993-1827 (home)
URL: http://interval.louisiana.edu/kearfott.html
Department of Mathematics, University of Louisiana at Lafayette
(Room 217 Maxim D. Doucet Hall, 1403 Johnston Street)
Box 4-1010, Lafayette, LA 70504-1010, USA
---------------------------------------------------------------