coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Machine floats in Coq
- Date: Mon, 6 Jul 2015 09:25:11 +0000
- Accept-language: de-DE, en-US
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.
- [Coq-Club] Machine floats in Coq, Abhishek Anand, 07/04/2015
- Re: [Coq-Club] Machine floats in Coq, Eric Mullen, 07/05/2015
- Re: [Coq-Club] Machine floats in Coq, Laurent Théry, 07/05/2015
- RE: [Coq-Club] Machine floats in Coq, Soegtrop, Michael, 07/06/2015
- RE: [Coq-Club] Machine floats in Coq, Christophe Bal, 07/06/2015
- Re: [Coq-Club] Machine floats in Coq, Guillaume Melquiond, 07/06/2015
- RE: [Coq-Club] Machine floats in Coq, Soegtrop, Michael, 07/06/2015
- Re: [Coq-Club] Machine floats in Coq, Guillaume Melquiond, 07/06/2015
- RE: [Coq-Club] Machine floats in Coq, Soegtrop, Michael, 07/06/2015
- Re: [Coq-Club] Machine floats in Coq, Bas Spitters, 07/05/2015
- Re: [Coq-Club] Machine floats in Coq, Eric Mullen, 07/05/2015
Archive powered by MHonArc 2.6.18.