Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Machine floats in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Machine floats in Coq


Chronological Thread 
  • 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

Le 6 juil. 2015 08:54, "Soegtrop, Michael" <michael.soegtrop AT intel.com> a écrit :

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,

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.




Archive powered by MHonArc 2.6.18.

Top of Page