CRM CAMP in Nonlinear Analysis

Computer-Assisted Mathematical Proofs in Nonlinear Analysis

January 19, 2021 from 10:00 to 11:00 (Montreal/EST time) Zoom meeting

Correct rounding for transcendental functions

Seminar presented by Nicolas Brisebarre (CNRS, ENS Lyon, France)

On a computer, real numbers are usually represented by a finite set of numbers called floating-point numbers. When one performs an operation on these numbers, such as an evaluation by a function, one returns a floating-point number, hopefully close to the mathematical result of the operation. Ideally, the returned result should be the exact rounding of this mathematical value. If we’re only allowed a unique and fast evaluation (a constraint often met in practice), one knows how to guarantee such a quality of results for arithmetical operations like +,−,x,/ and square root but, as of today, it is still an issue when it comes to evaluate an elementary function such as cos, exp, cube root for instance. This problem, called Table Maker’s Dilemma, is actually a diophantine approximation problem. It was tackled, over the last fifteen years, by V. Lefèvre, J.M. Muller, D. Stehlé, A. Tisserand and P. Zimmermann (LIP, ÉNS Lyon and LORIA, Nancy), using tools from algorithmic number theory. Their work made it possible to partially solve this question but it remains an open problem. In this talk, I will present a joint work with Guillaume Hanrot (ÉNS Lyon, LIP, AriC) that improve on a part of the existing results.