Verifying the Accuracy of Polynomial Approximations in HOL

John Harrison.

Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'97, Springer LNCS 1275, pp. 137-152..

Abstract:

Many modern algorithms for the transcendental functions rely on a large table of precomputed values together with a low-order polynomial to interpolate between them. In verifying such an algorithm, one is faced with the problem of bounding the error in this polynomial approximation, quite apart from the usual analysis of rounding or discretization errors. The most straightforward methods are based on numerical approximations, and are not prima facie reducible to a formal HOL proof. We discuss a technique for proving such results formally in HOL. This is achieved via the formalization of a number of results in polynomial theory, e.g. squarefree decomposition and Sturm's theorem, and the use of a computer algebra system to compute results that are then checked in HOL. We demonstrate our method by tackling an example from the literature.

DVI or PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-poly,
        crossref        = "hol97",
        author          = "John Harrison",
        title           = "Verifying the accuracy of polynomial approximations
                           in {HOL}",
        pages           = "137--152"}

@PROCEEDINGS{hol97,
        editor          = "Elsa L. Gunter and Amy Felty",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           10th International Conference, TPHOLs'97",
        series          = "Lecture Notes in Computer Science",
        volume          = 1275,
        address         = "Murray Hill, NJ",
        date            = "19--22 August 1997",
        year            = 1997,
        publisher       = "Springer-Verlag"}