Rigorous global search using taylor models
Martin Berz, Kyoko Makino · 2009
A Taylor model of a smooth function f over a sufficiently small domain D is a pair (P,I) where P is the Taylor polynomial of f at a point d in D, and I is an interval such that f differs from P by not more than I over D. As such, they represent a hybrid between numerical techniques for the interval and the coefficients of P and algebraic techniques for the manipulation of polynomials. A calculus including addition, multiplication and differentiation/integration is developed to compute Taylor models for code lists, resulting in a method to compute rigorous enclosures of arbitrary computer functions in terms of Taylor models. The methods combine the advantages of numeric methods, namely finite size of representation, speed, and no limitations on the objects on which operations can be carried out with those of symbolic methods, namely the ability to treat functions instead of points and making rigorous statements.