The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Guillaume,

thanks for clarifying, this is what I expected. Just out of curiosity: do you 
know if the behavior of signed 0 is specified by the IEEE standard? In python 
3.4 I get this:

>>> (-0.0)+(0.0)
0.0
>>> (0.0)+(-0.0)
0.0
>>> (-0.0)+(-0.0)
-0.0

>>> (-0.0)*(0.0)
-0.0
>>> (0.0)*(-0.0)
-0.0
>>> (-0.0)*(-0.0)
0.0

So it is commutative, but I don't know if it is specified. For infinities I 
don't see a problem.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Guillaume Melquiond
Sent: Monday, July 06, 2015 10:51 AM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Machine floats in Coq

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
HTML Version:

---------------------------------------------------------------------
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

This e-mail and any attachments may contain confidential material for the 
sole use of the intended recipient(s). Any review or distribution by others 
is strictly prohibited. If you are not the intended recipient, please contact 
the sender and delete all copies.