|
Polynomial
Interpolation
Title: |
Polynomial Interpolation |
Authors:
|
René Thiemann and
Akihisa Yamada (ayamada /at/ trs /dot/ cm /dot/ is /dot/ nagoya-u /dot/ ac /dot/ jp)
|
Submission date: |
2016-01-29 |
Abstract: |
We formalized three algorithms for polynomial interpolation over arbitrary
fields: Lagrange's explicit expression, the recursive algorithm of Neville
and Aitken, and the Newton interpolation in combination with an efficient
implementation of divided differences. Variants of these algorithms for
integer polynomials are also available, where sometimes the interpolation
can fail; e.g., there is no linear integer polynomial p such that
p(0) = 0 and p(2) = 1. Moreover, for the Newton interpolation
for integer polynomials, we proved that all intermediate results that are
computed during the algorithm must be integers. This admits an early
failure detection in the implementation. Finally, we proved the uniqueness
of polynomial interpolation.
The development also contains improved code equations to speed up the
division of integers in target languages. |
BibTeX: |
@article{Polynomial_Interpolation-AFP,
author = {René Thiemann and Akihisa Yamada},
title = {Polynomial Interpolation},
journal = {Archive of Formal Proofs},
month = jan,
year = 2016,
note = {\url{http://isa-afp.org/entries/Polynomial_Interpolation.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Sqrt_Babylonian |
Used by: |
Berlekamp_Zassenhaus, Deep_Learning, Polynomial_Factorization |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|