Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 1-4/2018

20.12.2017

Distant Decimals of \(\pi \): Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation

verfasst von: Yves Bertot, Laurence Rideau, Laurent Théry

Erschienen in: Journal of Automated Reasoning | Ausgabe 1-4/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We describe how to compute very far decimals of \(\pi \) 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 \(\pi \) 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.
Vorheriger Artikel The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar
Nächster Artikel A Verified ODE Solver and the Lorenz Attractor

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
The name can be decomposed in is R for Riemann, Int for Integral, and gen for generalized.
 
2
It turns out that the theorem derivable_pt_lim_CVU was already introduced by a previous study on the implementation of \(\pi \) in the Coq standard library of real numbers [6].
 
3
In retrospect, it might have been useful to add hypotheses that returned values by all functions were positive, as long as the inputs were.
 
Literatur
1.
Almkvist, G., Berndt, B.: Gauss, Landen, Ramanujan, the Arithmetic–Geometric Mean, Ellipses, \(\pi \), and the Ladies Diary (1988), pp. 125–150. Springer, Berlin (2016)
2.
Anonymous: Première composition de mathématiques”, concours externe de recrutement de professeurs certifiés, section mathématiques (1995)
3.
Armand, M., Grégoire, B., Spiwack, A., Théry, L.: Extending Coq with imperative features and its application to SAT verification. In: Interactive Theorem Proving, First International Conference, ITP 2010, volume 6172 of LNCS. Springer, pp. 83–98 (2010)
4.
Bailey, D.: Borwein, Peter, Plouffe, Simon: on the rapid computation of various polylogarithmic constants. Math. Comput. 66(218), 903–913 (1997)CrossRef
5.
Bertot, Y.: Fixed precision patterns for the formal verification of mathematical constant approximations. In: Proceedings of the 2015 Conference on Certified Programs and Proofs. ACM, pp. 147–155 (2015)
6.
Bertot, Y., Allais, G.: Views of Pi: definition and computation. J. Formaliz. Reason. 7(1), 105–129 (2014)MathSciNet
7.
8.
9.
Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Proceedings of the 2006 International Conference on Types for Proofs and Programs, volume 4502 of LNCS. Springer, pp. 48–62 (2007)
10.
Boespflug, M., Dénès, M., Grégoire, B.: Full reduction at full throttle. In Certified Programs and Proofs: First International Conference, volume 7086 of LNCS. Springer, pp. 362–377 (2011)
11.
Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015)MathSciNetCrossRefMATH
12.
Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: IEEE Symposium on Computer Arithmetic. IEEE Computer Society, pp. 243–252 (2011)
13.
Borwein, J.M., Borwein, P.B.: Pi and the AGM: A Study in the Analytic Number Theory and Computational Complexity. Wiley, New York (1987)MATH
14.
15.
Cartan, H.: Théorie des filtres. Comptes Rendus de l’Académie des Sciences 205, 595–598 (1937)MATH
16.
Cohen, C., Dénès, M., Mörtberg, A.: Refinements for free! In: Certified Programs and Proofs: Third International Conference, volume 8307 of LNCS. Springer, pp. 147–162 (2013)
17.
Cruz-Filipe, L.: Constructive Real Analysis: A Type-Theoretical Formalization and Applications. PhD Thesis, University of Nijmegen, April (2004)
18.
Dénès, M., Mörtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Interactive Theorem Proving—Third International Conference, ITP 2012, volume 7406 of LNCS. Springer, pp. 83–98 (2012)
19.
20.
Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, volume 7792 of LNCS. Springer, pp. 125–128 (2013)
21.
Fousse, L., Hanrot, G., Lefèvre, V., Pélissier, P., Zimmermann, P.: MPFR: a multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33(2), 13 (2007)MathSciNetCrossRefMATH
22.
23.
24.
Grégoire, B., Théry, L.: A purely functional library for modular arithmetic and its application to certifying large prime numbers. In: Automated Reasoning: Third International Joint Conference, IJCAR 2006, volume 4130 of LNCS. Springer, pp. 423–437 (2006)
25.
26.
Harrison, J.: Formalizing basic complex analysis. In: From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar and Rhetoric. University of Białystok, pp. 151–165. http://​mizar.​org/​trybulec65/​ (2007)
27.
28.
Harrison, J.: Theorem Proving with the Real Numbers, 1st edn. Springer, Berlin (2011)MATH
29.
Hölzl, J.: Proving inequalities over reals with computation in Isabelle/HOL. In: Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS’09), Munich, pp. 38–45 (2009)
30.
Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Interactive Theorem Proving (ITP 2013), volume 7998 of LNCS. Springer, pp. 279–294 (2013)
31.
King, L.V.: On the Direct Numerical Calculation of Elliptic Functions and Integrals. Cambridge University Press, Cambridge (1924)MATH
32.
Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Log. Methods Comput. Sci. 9(1), 1–27 (2013)MathSciNetCrossRefMATH
33.
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef
34.
Martin-Dorel, É., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reason. 57(3), 187–217 (2016)MathSciNetCrossRefMATH
35.
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)CrossRefMATH
36.
O’Connor, R.: Certified exact transcendental real number computation in Coq. In: Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, volume 5170 of LNCS. Springer, pp. 246–261 (2008)
37.
Salamin, E.: Computation of \(\pi \) using arithmetic-geometric mean. Math. Comput. 33(135), 565–570 (1976)MathSciNetMATH
38.
39.
Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: NASA Formal Methods: 5th International Symposium, NFM 2013, volume 7871 of LNCS. Springer, pp. 383–397 (2013)
Metadaten
Titel
Distant Decimals of : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation
verfasst von
Yves Bertot
Laurence Rideau
Laurent Théry
Publikationsdatum
20.12.2017
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 1-4/2018
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-017-9444-2

Weitere Artikel der Ausgabe 1-4/2018

Journal of Automated Reasoning 1-4/2018 Zur Ausgabe

OriginalPaper

Hammer for Coq: Automation for Dependent Type Theory

OriginalPaper

A Verified ODE Solver and the Lorenz Attractor

OriginalPaper

Regular Language Representations in the Constructive Type Theory of Coq

EditorialNotes

Introduction to Milestones in Interactive Theorem Proving

OriginalPaper

Formally Verified Algorithms for Upper-Bounding State Space Diameters

OriginalPaper

Verified iptables Firewall Analysis and Verification

Premium Partner

    Bildnachweise