MPFR : vers un calcul flottant correct ?

Qui n'a jamais vu s'afficher sur sa calculatrice 2,9999 ou 3,0001 ? Voici un des avatars du calcul avec des nombres à virgule flottante, plus couramment appelés nombres flottants. De tels résultats peuvent cependant s'expliquer. En effet, le résultat d'un calcul flottant, par exemple 1.0/3.0, n'est pas toujours représentable exactement ; il faut choisir entre 0,33333 et 0,33334. C'est ce qu'on appelle un arrondi . Plus gênant est le fait que le même calcul donne 0,33333 sur une machine et 0,33334 sur une autre. Imaginons les dérives que cela peut engendrer pour des calculs d'intérêt portant sur des milliards d'euros ! C'est le problème de la portabilité .

En double précision , la norme IEEE 754 régit la façon dont les calculs flottants sont effectués sur le processeur, en particulier l'arrondi. La conséquence majeure est que les programmes utilisant l'arithmétique flottante du processeur sont globalement plus précis et plus portables, et des algorithmes basés sur cette norme peuvent être écrits et prouvés facilement.

En précision arbitraire , il n'existe pour l'instant aucune norme. Depuis 1999, plusieurs chercheurs du Loria ont entrepris de développer une bibliothèque , nommée MPFR, de calcul flottant en précision arbitraire.

Quelques valeurs : à gauche, celles publiées dans le « Handbook of Mathematical Functions » et à droite, celles calculées avec MPFR. Par exemple, en 4e ligne, la valeur de 101/5 sur 22 chiffres vaut 1.584893192461113485202, ce qui arrondi au plus proche donne 1.5848931924611134852 comme indiqué par MPFR, et non 1.5848931924611134853.

Cette bibliothèque, diffusée sous forme de logiciel libre, sous la licence LGPL , reprend la philosophie de la norme IEEE 754, notamment la notion d'arrondi. Les calculs effectués via MPFR donnent ainsi un même résultat, quel que soit l'environnement (processeur, compilateur ou système d'exploitation).

Concilier exactitude et efficacité

Il faut souligner que lorsqu'on dispose d'une spécification formelle comme dans MPFR, il n'y a qu'un seul résultat correct pour un calcul donné. En effet, à toute entrée (fonction, nombre flottant, précision, arrondi) correspond une et une seule sortie correcte (et non pas à plus ou moins 1 ou 2 chiffres comme le font la plupart des logiciels). Cela rend plus difficile l'obtention de ce résultat, mais cela facilite la recherche de « bugs », et surtout cela permet d'avoir des fondations solides pour construire d'autres logiciels.

Une bibliothèque telle que MPFR a de nombreuses applications. On peut s'en servir pour vérifier les résultats obtenus en double précision (voir le fameux « bug du Pentium » ). MPFR permet aussi d'effectuer avec une plus grande précision certains calculs critiques : cela permet d'estimer la stabilité numérique d'un algorithme, ou d'évaluer l'erreur d'arrondi d'un calcul en double précision. Enfin, MPFR permet aussi de calculer avec arrondi correct les fonctions mathématiques qui ne sont pas standardisées par la norme IEEE 754, telles que le sinus, l'exponentielle ou le logarithme. C'est pour cette dernière application que MPFR est depuis peu utilisée dans le compilateur GNU GFORTRAN .

Cette applet a été écrite avec GMP et MPFR par Tomonori Kouya
avec le soutien du Research Institute of Systems Planning Inc.

La principale motivation pour développer MPFR était de montrer qu'il est possible de calculer sur des flottants en précision arbitraire avec une spécification formelle, comme c'est déjà le cas en double précision grâce à la norme IEEE 754, sans perte notable d'efficacité par rapport à d'autres outils sans spécification formelle. Il semble que ce pari soit réussi. Il reste cependant beaucoup à faire, notamment à convaincre les développeurs (et surtout les utilisateurs !) d'outils de calcul flottant en précision arbitraire de l'intérêt d'une spécification formelle.