From: Thomas S. <st...@re...> - 2010-08-21 07:20:31
Attachments:
smime.p7s
|
Are there IEEE Floats available as a domain in Reduce? If not, could I implement this on the Reduce level in such a way that existing hardware support is directly used? The idea is to perform symbolic computations involving such floats for software verification. Thomas -- Dr. habil. Thomas Sturm Departamento de Matematicas, Estadistica y Computacion Universidad de Cantabria, Santander, Spain Avda. Los Castros s/n, Room 1072, +34 693 251058 http://personales.unican.es/sturmt/ |
From: Arthur N. <ac...@ca...> - 2010-08-21 07:51:01
|
On Sat, 21 Aug 2010, Thomas Sturm wrote: > Are there IEEE Floats available as a domain in Reduce? If not, could I implement this on the Reduce level in such a way that existing hardware support is directly used? > > The idea is to perform symbolic computations involving such floats for software verification. > > Thomas > If you merely go "on float" but do not mess with "precision" then Reduce uses whatever floating point data type is natively provided by the underlying Lisp. I EXPECT that on most systems and both Lisps that this is IEEE double precision. But eg if you had built the CSL version on an old IBM mainframe or (in some circumstances) on a VAX you just got whatever was native there. In CSL you can investigate to see if things do what you want at the bit level because the Lisp function "rational" should convert a Lisp float either to an integer or to a cons of a numerator and denominator, with the denominator a power of 2 - giving you a bit-precise version of the value. On just trying this it is OK for modest size numbers but fails on numbers that are either very large or very small - teh code is in cslbase/arith04.c as the function rationalf() and with luck I will fix it over the weekend. If other hooks to access the raw parts of the IEEE representation would help they could probably easily go in. Obviously in almost any Lisp you will find floating point values have to be "boxed" for use so that their type is recorded along with them. Also any use of them will depend on the competence of the read and print code that maps between them and character strings. In CSL that copnversion is done by whatever C library you have - and you can NOT assume that everybody uses the same C library or that it will perform well either on trig functions or on input/output conversion. If you look at the main Reduce test logs you see an effect of different numeric libraries on different platforms, in that numeric.tst/.rlg show LSB-style variation when you try on Mac/Linux/Solaris/BSD/Windows and no doubt when you use different C compilers and libraries on Windows. You should not instantly believe that you own platform is the one that is definitively correct! CSL has all the code framework in there to support IEEE 32-bit floats as well as the 64-bit ones mostly used, and it has SOME code ready to allow for 80-bit ones. But at present those are all guarded by "#ifdef COMMON" and Reduce would not know what to do with them. I will go away and mend the "rational" function... Reduce (Free CSL version), 20-Aug-10 ... 1: lisp; nil 2* rational 19.0; 19 3* rational 0.3333333333; (6004799502560181 . 18014398509481984) 4* rational 0.125; (1 . 8) 5* Arthur |
From: Arthur N. <ac...@ca...> - 2010-08-22 09:17:36
|
CSL now has some more functions to help with floating point. To get access to these you will need to rebuild your Reduce image I expect. These are in the lastest subversion. Reduce (Free CSL version), 21-Aug-10 ... 1: lisp; nil 2* decode!-float (-1024.0); (-1.0 11 0.5) This is basically FREXP and gives you sign, exponant and mantissa. There ought not be to any rounding etc in the process. 3* integer!-decode!-float (-1024.0); (4503599627370496 -42 -1) Much the same except that the mantissa is returned as an integer of 52 bits. Except of course when the input is 0.0. This gives access to the bitwise representationof the float. 4* scale!-float(1.0, 10); 1024.0 This one is as in ldexp and scales by a factor of 2 by addint in exponent bits. 5* rational 3.125; (25 . 8) If the float concerned denotes a neat rational numbet the dotted pair you get back will be that. 6* rational exp 1.0; (6121026514868073 . 2251799813685248) Note that the quotient of those two integers is close to "e", and the second of them is a power of 2. So this is rather like doing integer-decode-float but then using the exponent to get an integer power of 2. 7* rational 1.0e22; 10000000000000000000000 This may return an integer not a dotted pair if a fraction is not needed. 8* rational 1.0e77; 99999999999999998278261272554585856747747644714015897553975120217811154108416 The exact integer value denoted by the floating point representation. Which is a 52-bit number multiplied by 2^21, as integer-decode-float would tell you. If there were documentation anywhere I might merge this email into it! Arthur |
From: Rainer S. <rai...@gm...> - 2010-08-24 23:19:44
|
Just for the record: I have a lisp implementation of the Cody/Waite elementary function test package. Given the state of the art of floating point implementations, these tests are probably obsolete, but they still give some information about the accuracy of the computation. Unfortunately, the license status is unclear, so I cannot put it into the public repository. Rainer Schöpf |
From: Arthur N. <ac...@ca...> - 2010-08-25 06:22:31
|
Excellent! Indeed it is not liable to know about gradual underflow. I spent a lot of time with thst stuff 20 odd years ago! Arthur On Wed, 25 Aug 2010, Rainer Schöpf wrote: > Just for the record: I have a lisp implementation of the Cody/Waite elementary > function test package. Given the state of the art of floating point > implementations, these tests are probably obsolete, but they still give some > information about the accuracy of the computation. > > Unfortunately, the license status is unclear, so I cannot put it into the public > repository. > > Rainer Schöpf |
From: Rainer S. <rai...@gm...> - 2010-08-25 08:21:07
|
I think I wrote this to test the DEC Alpha Lisp implementation, nearly forgotten like the architecture itself. More recently, Nelson Beebe collected floating point test routines, see http://www.math.utah.edu/~beebe/software/ieee/ Rainer On Wed, 25 Aug 2010, Arthur Norman wrote: > Excellent! Indeed it is not liable to know about gradual underflow. I spent a > lot of time with thst stuff 20 odd years ago! Arthur > > On Wed, 25 Aug 2010, Rainer Schöpf wrote: > > > Just for the record: I have a lisp implementation of the Cody/Waite > > elementary > > function test package. Given the state of the art of floating point > > implementations, these tests are probably obsolete, but they still give > > some > > information about the accuracy of the computation. > > > > Unfortunately, the license status is unclear, so I cannot put it into the > > public > > repository. > > > > Rainer Schöpf Rainer |