coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Christophe Bal <projetmbc AT gmail.com>
- To: coq-club AT inria.fr
- Subject: RE: [Coq-Club] Machine floats in Coq
- Date: Mon, 6 Jul 2015 09:23:41 +0200
Hello.
I am not an expert but I really think that this operations aren't commutative. There are potential roundings at each step.
The problem is that I can give you an example.
Christophe BAL
HTML Version: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.
Best regards,
Michael
From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Eric Mullen
Sent: Sunday, July 05, 2015 1:12 AM
To: coq-club
Subject: Re: [Coq-Club] Machine floats in Coq
There's Flocq, which is used by CompCert to formalize floating point: http://flocq.gforge.inria.fr/
As for relating it to rationals, that will be tough. Rational arithmetic is quite fundamentally different than floating point: e.g. addition commutes in the rationals, but doesn't in the floats.
Best of luck!
Eric
On Sat, Jul 4, 2015 at 2:32 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:
Hi,
Some of my Coq programs need to interoperate (after extraction to Haskell)
with some Haskell libraries which use floating points (Prelude.Float).
Has someone axiomatized an interface to Haskell floats,
along with extraction-directives to realize those axiomatic operations with Haskell functions?
If so, I would be grateful to reuse that code and benefit from their experience.
It would be awesome if this interface also includes a logical specification of the floating point operations, perhaps in terms of Coq rationals (Coq.QArith.QArith_base.Q).
Thanks,
-- Abhishek
---------------------------------------------------------------------
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.