CR-03 : Preuve et arithmétique virgule flottante

Programme de l’UE

L’arithmétique virgule flottante, grâce à son efficacité (grande « dynamique » et opérateurs très rapides) s’est imposée en calcul scientifique. Aucun des problèmes numériques de très grande taille qui se posent quotidiennement aux ingénieurs (mécanique des fluides, calculs de structures, etc.) ne serait résoluble en temps raisonnable autrement qu’en arithmétique virgule flottante. Pourtant son caractère approché peut parfois poser problème (des erreurs d’arrondis peuvent s’accumuler). Egalement, une programmation erronée ou naïve peut rendre le comportement des programmes imprévisibles. Enfin, les utilisateurs ignorent trop souvent que depuis quelques années le comportement des opérations virgule flottante est complètement spécifié (norme IEEE 754), et qu’on peut élaborer des preuves qui utilisent ces spécifications. Ce dernier point est très important lorsque l’arithmétique virgule flottante est utilisée dans un contexte où une erreur pourrait avoir des conséquences graves (transport aérien, contrôle de processus physico/chimiques dangereux, etc.)

L’objet de ce cours est d’abord de présenter aux étudiants des propriétés « fines » de l’arithmétique virgule flottante: grâce aux spécifications de la norme IEEE 754, on peut construire et prouver des algorithmes qui permettent de faire des calculs « exacts » (ou très précis) avec cette arithmétique « approchée » (calculs exacts de sommes, de produits scalaires, mise au point d’algorithmes de division, de calcul des fonctions « transcendantes »). On se focalisera ensuite sur la possibilité d’élaborer des preuves formelles des algorithmes virgule flottante, en illustrant ce point par la formalisation dans l’assistant de preuve Coq de l’arithmétique virgule flottante.

Modalités d’examen. L’évaluation se fera par une analyse d’articles présentée par un rapport écrit et une soutenance orale, lors de laquelle des questions portant sur le cours pourront être posées.

Prérequis: un minimum de notions de logique et d’algorithmique. Les débutants complets en Coq sont les bienvenus, le cours s’adaptera à eux.

Bibliographie pour le cours

Calendrier prévisionnel

11/09, 18/09, 19/09, 25/09, 2/10, 3/10, 9/10, 16/10, 17/10, 24/10, 6/11, 7/11 [de 8h à 10h].

Intervenants

  • Jean-Michel Muller, DR CNRS (responsable)
  • Damien Pous, CR CNRS
  • Laurent Théry, CR INRIA

CB-03 : Arithmétique des ordinateurs

Programme de l’UE

L’arithmétique des ordinateurs s’intéresse à la fois à la conception d’opérateurs arithmétiques, et à leur utilisation fine pour réaliser des fonctions plus complexes.

Ce cours présente un panorama des représentations utilisées en machine pour manipuler les nombres entiers, les réels et les polynômes, ainsi que l’algorithmique associée à chaque représentation pour réaliser les opérations de base (addition, multiplication, division, racine carrée… ) et calculer des fonctions « élémentaires » (logarithme, exponentielle, fonctions trigonométriques, etc.).

On s’intéressera d’abord à la manipulation de nombres en « précision fixée » (entiers, virgule flottante, norme IEEE 754) ainsi qu’à diverses techniques permettant d’augmenter ou de garantir la précision des calculs: on montrera ainsi qu’une arithmétique « approchée » comme la virgule flottante permet de faire des calculs exacts.

On étudiera ensuite la complexité et l’algorithmique des opérations de base sur les polynômes (multiplication, division, évaluation, interpolation), en arithmétique exacte.

Enfin, nous aborderons la question du calcul sur les polynômes en arithmétique approchée. Cela permettra d’une part de présenter les notions fondamentales de conditionnement d’un problème et de stabilité d’un algorithme et, d’autre part, de comprendre pourquoi l’évaluation polynomiale est de plus en plus souvent au coeur des implantations (logicielles ou matérielles) d’opérateurs arithmétiques de base comme la division ou la racine carrée.

Intervenants

  • Jean Michel Muller, DR CNRS (http://perso.ens-lyon.fr/jean-michel.muller/)
  • Claude Pierre Jeannerod, CR INRIA (http://perso.ens-lyon.fr/claude-pierre.jeannerod/)

Quelques ouvrages de référence

  • Ercegovac et Lang, Digital Arithmetic, The Morgan Kaufmann Series in Computer Architecture and Design, 2004
  • D.E. Knuth, The Art of Computer Programming, Volume 2, Addison Wesley 1997
  • Muller, Arithmétique des Ordinateurs, Masson, 1989 (texte intégral accessible à http://prunel.ccsd.cnrs.fr/ensl-00086707)
  • J. von zur Gathen et J. Gerhard, Modern Computer Algebra, Cambridge 2003.
  • Muller, Elementary functions, algorithms and implementation, 2ème édition, Birkhauser, 2006
  • P. Burgisser, M. Clausen, et M.A. Shokrollahi, Algebraic Complexity Theory, Springer 1997.
  • Higham, Accuracy and Stability of Numerical Algorithms, SIAM, Seconde édition, Août 2002
  • Muller, Brisebarre, de Dinechin, Jeannerod, Lefèvre, Melquiond, Revol, Stehlé et Torrès, Handbook of Floating-Point Arithmetic, Birkhauser, 2010