Distant decimals of π: Formal proofs of some algorithms computing them and guarantees of exact computation

Yves Bertot 1 Laurence Rideau 1 Laurent Théry 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We describe how to compute very far decimals of π and how to provide formal guarantees that the decimals we compute are correct. In particular, we report on an experiment where 1 million decimals of π and the billionth hexadecimal (without the preceding ones) have been computed in a formally verified way. Three methods have been studied, the first one relying on a spigot formula to obtain at a reasonable cost only one distant digit (more precisely a hexadecimal digit, because the numeration basis is 16) and the other two relying on arithmetic-geometric means. All proofs and computations can be made inside the Coq system. We detail the new formalized material that was necessary for this achievement and the techniques employed to guarantee the accuracy of the computed digits, in spite of the necessity to work with fixed precision numerical computation.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2017
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01582524
Contributeur : Yves Bertot <>
Soumis le : mercredi 6 septembre 2017 - 10:25:07
Dernière modification le : jeudi 7 septembre 2017 - 01:10:32

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

  • HAL Id : hal-01582524, version 1
  • ARXIV : 1709.01743

Collections

Citation

Yves Bertot, Laurence Rideau, Laurent Théry. Distant decimals of π: Formal proofs of some algorithms computing them and guarantees of exact computation. Journal of Automated Reasoning, Springer Verlag, 2017. 〈hal-01582524〉

Partager

Métriques

Consultations de la notice

94

Téléchargements de fichiers

13