Events

Bât. I, 1st floor
Microsoft Research - Inria Joint Centre
Parc Orsay UniversitéFormally Verified Polynomial Approximations of Real Functions
Ioana Pasca, ENS Lyon

The purpose of this work is to compute in a formally certified manner a polynomial that is an approximation of a given function at a given accuracy and on a given interval. We are in a particular setting, where we only treat functions in a single variable and where we need very accurate approximations. The challenge is to be efficient enough in order to compute thousands of polynomials for each base function and on each binade (interval between consecutive powers of 2).

We compute these approximation polynomials and the associated approximation error by using Taylor Models. A Taylor Model for a function on an interval is a pair formed from a polynomial and an interval corresponding to the error between the function and the polynomial on the interval. For the base functions we use Taylor polynomials and the Taylor-Lagrange reminder, while for composite functions we use a special arithmetic on Taylor Models to determine the approximation polynomial and error.

Some issues that will be discussed concern efficient computation of the coefficients of Taylor polynomials for base functions. This is based on the fact that most base functions are D-finite, which means their Taylor coefficients can be computed by recurrence relations. Another interesting issue is the use of interval arithmetic in our work, through the library Coq.Interval.

The presentation will also include some preliminary benchmarks as well as potential extensions of this work.