On 2014-01-07 14:36:58 +0000, Joseph S. Myers wrote: > (As far as I know, the state of the art on exhaustive searches for > worst cases for correct rounding - as needed to implement correctly > rounded transcendental functions with bounded resource use - does > not make such searches feasible for IEEE binary128, which is a clear > reason not to require such functions to be provided.)
Well, an implementation can still provide very accurate versions (say, with a guaranteed 512 bits accuracy), and the functions will be correctly rounded with a very high probability. In practice, the proof of correct rounding can be obtained only with an exhaustive search (well there is some hope to obtain a proof if the maximum precision of the implementation is around several thousands bits). The exhaustive search also allows one to optimize code even more. On 2014-01-07 14:55:31 +0000, Andrew Haley wrote: > On 01/07/2014 02:48 PM, Joseph S. Myers wrote: > > On Tue, 7 Jan 2014, Joseph S. Myers wrote: > > > >> The IEEE 754 operations are corrected rounded. However, the C bindings > > > > (Except that the IEEE 754 reduction operations - subclause 9.4 - return > > "an implementation-defined approximation". But 9.2 is "Recommended > > correctly rounded functions", e.g. exp and sin, for which the strictly > > corresponding C functions are crexp and crsin.) > > Has anyone found a way to do it? Even crlibm only provides routines > that are probably correctly rounded. Although I'll grant you that the > probability of incorrect rounding is very low. For some of them, this is proved. Here's a summary of the current status: http://tamadiwiki.ens-lyon.fr/tamadiwiki/images/c/c1/Lefevre2013.pdf -- Vincent Lefèvre <vinc...@vinc17.net> - Web: <http://www.vinc17.net/> 100% accessible validated (X)HTML - Blog: <http://www.vinc17.net/blog/> Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)