# [std-interval] More on interval computations as proofs

Hervé Brönnimann hbr at poly.edu
Wed Sep 27 00:37:25 PDT 2006

Sorry to catch up this thread late.  I read everything, but don't
usually have the resources to weigh in on the issues.

On Sep 22, 2006, at 8:07 AM, Guillaume Melquiond wrote:
> Le vendredi 22 septembre 2006 à 06:41 -0500, R. Baker Kearfott a
> écrit :
>> At 07:54 AM 9/22/2006 +0200, Guillaume Melquiond wrote:
>>> 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)})$.
>> 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)})$."
>> ??
>
> I have used "close" to mean "approximation" in my sentence. Your
> wording
> looks less confusing to me.

I agree with all the points, but I would slightly rephrase Baker's
proposed wording to (should instead of will, as this is more a
statement of intention, and guideline to the implementor, than a
normative text):

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

I am glad to see the wording converge.
--
Hervé Brönnimann
CIS, Polytechnic University
hbr at poly.edu