 |
 |
|
|
| inria-00369511, version 1 |
 |
|
|
|
| Voir la fiche détaillée |  BibTeX EndNote TEI RefWorks |
|
|
|||||||
| Theorem Proving in Higher Order Logics 5674 (2009) 408-423 |
| Lien vers texte intégral chez l'éditeur |
|
| We are interested in the certification of Newton's method. We use a formalization of the convergence and stability of the method done with the axiomatic real numbers of Coq's Standard Library in order to validate the computation with Newton's method done with a library of exact real arithmetic based on co-inductive streams. The contribution of this work is twofold. Firstly, based on Newton's method, we design and prove correct an algorithm on streams for computing the root of a real function in a lazy manner. Secondly, we prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding turns out to be much more efficient. |
|
|
|
|
|
|
|
|
|
| 1 : | MARELLE (INRIA Sophia Antipolis) |
|
INRIA |
|
|
|
|
|
|
|
|
|
| Domaine | : | Informatique/Calcul formel |
| formal verification – Newton's method – exact real arithmetic – co-recursive algorithms |
| 10.1007/978-3-642-03359-9_28 |
|
| inria-00369511, version 1 | |
| http://hal.inria.fr/inria-00369511/fr/ | |
| oai:hal.inria.fr:inria-00369511_v1 | |
| Contributeur : Ioana Pasca | |
| Soumis le : Vendredi 20 Mars 2009, 10:39:05 | |
| Dernière modification le : Mardi 22 Septembre 2009, 14:08:15 | |
