Vendredi 25/06/2010, à partir de 11h, en salle Byron Blanc.
Orateur : Érik Martin-Dorel.
Titre : Formalisation du lemme de Hensel en Coq.
Résumé :
Le lemme de Hensel est un résultat d’arithmétique qui peut être vu comme l’analogue discret de la méthode de Newton-Raphson, au sens où les fonctions considérées sont des polynômes à coefficients entiers.Outre son intérêt propre pour déterminer les racines entières de polynômes sur Z, la technique de calcul proposée par ce lemme est, dans sa version bivariée, intensivement utilisé par l’algorithme SLZ (Stehlé/Lefèvre/Zimmermann) conçu pour résoudre de manière exacte ce qu’on appelle le Dilemme du fabricant de tables.
La formalisation puis la preuve de ce lemme dans un système formel tel que Coq est donc essentielle pour le processus de validation de ce type d’algorithme, dont la complexité intrinsèquement exponentielle donne des temps de calcul considérables. Nous présenterons ainsi les diverses étapes que nous avons rencontées lors de la formalisation du lemme de Hensel univarié en SSReflect, ainsi que les pistes envisagées pour la suite de cette formalisation.
