The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 06/07/2015 08:53, Soegtrop, Michael wrote:
> Dear Eric,
>
> is it really so that floats don’t commute? I thought floats are
> commutative under addition and multiplication, but not associative. But
> maybe there are some exceptions I didn’t see as yet.

It depends the kind of inputs you consider. For non-NaN results, 
addition and multiplication are commutative operations. When given NaN 
as inputs, they no longer are. Imagine "NaN(1) + NaN(2)", what is the 
result? NaN(1) or NaN(2) or some other NaN? This case is underspecified 
in the IEEE-754 standard and depends on the implementation.

Best regards,

Guillaume