[std-interval] More on interval computations as proofs

[Hervé Brönnimann]

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