Ben Smith wrote: > On 13/11/06, Rhythmic Fistman <[EMAIL PROTECTED]> wrote: > >>> Well .. of course the distributive law doesn't hold for >>> floats. The question is .. what to do about it? >>> >>> Options: >>> >>> 1. Change 'eq' for floats >>> >>> 2. Change the axiom for floats to be >>> >>> axiom distrib (x:t,y:t,z:t): close (x * ( y + z), x * y + x * z); >>> >> 3. not expect that axiom to hold for floats. >> > > I like 3). 2) is asking for trouble, but so is using 'eq' with floats > anyway, so I vote for doing both 1) and 3).:) > > ben > > I'm with 3. floats are just tricky. The fact that a large number x plus a small number y can result in x just makes it hard to apply normal mathematical axioms. I did a quick google, and here's how Intel used HOL Light to verify their floating point math. Perhaps there are some simple axioms or other mathematical structures we could use from it:
http://www.cl.cam.ac.uk/~jrh13/papers/iday.html One thing that would be really *really* interesting for engineers is a mechanism to automatically calculate the error of floating point mathematical operations. One of the tricky things with analyzing things like this is that you have to know what the language does to optimize your expressions, as each of these may modify your precision. If we had some way of the felix optimizer to generate the expression as calculating the error according to the IEEE spec, it could be very interesting. Not sure exactly how it could work though. Perhaps something like this: val result, error = witherror (x * (y * z)); Either way, here's another document all about dealing with floating point stuff. Maybe it'll also give some ideas on how to deal with this stuff. http://docs.sun.com/source/806-3568/ncg_goldberg.html Finally, here's a reference to a paper that talks about some floating point axioms: Brown, W. S. 1981. A Simple but Realistic Model of Floating-Point Computation, ACM Trans. on Math. Software 7(4), pp. 445-480. Extra-finally, here's another: http://citeseer.ist.psu.edu/barrett89formal.html -e ------------------------------------------------------------------------- Using Tomcat but need to do more? Need to support web services, security? Get stuff done quickly with pre-integrated technology to make your job easier Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642 _______________________________________________ Felix-language mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/felix-language
