Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations
Abstract
We describe two approaches for the computation of mathematical constant approximations inside interactive theorem provers. These two approaches share the same basis of fixed point computation and differ only in the way the proofs of correctness of the approximations are described. The first approach performs interval computations, while the second approach relies on bounding errors, for example with the help of derivatives. As an illustration, we show how to describe good approximations of the logarithm function and we compute π to a precision of a million decimals inside the proof system, with a guarantee that all digits up to the millionth decimal are correct. All these experiments are performed with the Coq system, but most of the steps should apply to any interactive theorem prover.
Fichier principal
main (1).pdf (264.32 Ko)
Télécharger le fichier
agm.v (4.1 Ko)
Télécharger le fichier
computing.v (239 B)
Télécharger le fichier
coq_files.zip (41.35 Ko)
Télécharger le fichier
ln_2_10.v (6.1 Ko)
Télécharger le fichier
log2.v (47.92 Ko)
Télécharger le fichier
README (1.52 Ko)
Télécharger le fichier
rounding_big.v (2.16 Ko)
Télécharger le fichier
rounding_correct.v (129.87 Ko)
Télécharger le fichier
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Origin : Files produced by the author(s)
Loading...