Betr.: [clean-list] IEEE floating point and Clean

[Siegfried Gonzi]

M.Kesseler@aia.nl wrote:

 
> So, some computations with exceptional values yield ordinary results.


I have been confused, because the following snippet from:

http://www.cs.berkeley.edu/~demmel/cs267/lecture21/lecture21.html

(and therein the last chapter) says (citation):

==
  count = 0
       b(0) = 0
       d = 1
       for i = 1 to n
           d = a(i) - s - b(i-1)^2/d
           if (d<0) count = count + 1
       end for

To make this code robust, we must take into account exceptions in the
inner loop. For example, if s were an
eigenvalue of the leading k-by-k submatrix of T, then (in exact
arithmetic) the k-th value of d would be
exactly zero. Assuming we prescale T so its largest entry is neither too
large nor too small (making ||T||
equal to the fourth root of the overflow threshold is a good value),
then the following code is robust across
all machines, and is currently in LAPACK routine slaebz.f (called by
sstebz): 

       count = 0
       b(0) = 0
       d = 1
       pivmin = sqrt(underflow_threshold)
       for i = 1 to n
           d = a(i) - s - b(i-1)^2/d
           if (abs(d) < pivmin) d = -pivmin  ... guarantees division
					     ....by |d| not too small
           if (d < 0) count = count + 1
       end for

However, this runs about 14% to 47% slower than the simpler algorithm
above. With IEEE arithmetic, it
turns out that the first algorithm is perfectly correct even when d
becomes zero. The result is that the next d
will be +-infinity, and on the subsequent iteration -b(i-1)^2/d will be
zero again. One can show that this
yields accurate and reliable results; see the reference below. 
==

Therefore I thought it is enough in order to pleasure the IEEE rules
when the computation does not break (especially the last few sentences;
see above).


> This can be dangerous. Java provides no built-in way to check that
> such a situation has occured. Clean does not either (as far as I know).

Clean would behave the same as Java in this respect? And the paper could
also be called?:

"Why Clean's floating point hurts everyone everywhere"


This is my motivation to figure this out whether it is true or not. And
also to discuss whether Kahan is exaggeration the problem.


S. Gonzi