Deuxième réunion
Arithmétique des Ordinateurs Certifiée
Lundi 26 et Mardi 27 Juin, Nancy
Participants
- Yves Bertot
- Marc Daumas
- Guillaume Hanrot
- Emmanuel Jeandel
- Philippe Langlois
- Vincent Lefèvre
- Loïc Pottier
- Laurence Rideau
- Laurent Théry
- Paul Zimmerman
Programme
Lundi 26
- 09h30 Discussion technique
- 12h30 Repas
- 14h30 M. Daumas: Ce que Donald Knuth racontait déjà en 1969
- 15h00 L. Théry: Formalisation de la norme IEEE754 dans Coq
- 16h30 E. Jeandel: Garantir l'arrondi exact des fonctions hypergéométriques
Mardi 27
- 09h30 Ph. Langlois: Nombres s'écrivant comme la différence de 2 flottants
- 10h30 P. Zimmermann: Expérimentation avec MPFR et MPSolve
- 11h00 L. Pottier: Implantation de l'algorithme de Fourier-Motzkin en Coq
- 12h00 Repas
- 14h30 Discussion
- 16h30 Fin de la réunion
Compte-rendu
Les exposés:
Ce que Donald Knuth racontait déjà en 1969
Marc Daumas nous a présenté la preuve que Donald Knuth donne
dans son `Art of Programming` sur l'addition avec calcul d'erreur.
Cette preuve commence par la démonstration de certaines propriétés
de l'addition avec arrondi et se termine sur la preuve de correction
d'un algorithme de l'addition avec calcul d'erreur. Cet algorithme
est une des bases du calcul sur les expansions flottantes.
Formalisation de la norme IEEE754 dans Coq
Laurent Théry a présenté l'état de sa formalisation de la norme IEEE754.
Pour l'instant seuls les objets de base (flottants, flottants bornés,
normalisés, dénormalisés) ont été définis. Les opérations de base
(l'addition la soustraction et la multiplication) ont été définies.
Des propriétés comme celle de Sterbenz sur l'addition ont été prouvées.
La prochaine étape de cette formalisation sera la description des différents
types d'arrondis. Les transparents de l'exposé sont disponibles
ici
Garantir l'arrondi exact des fonctions hypergéométriques
Emmanuel Jeandel a présenté l'application de la méthode du "binary
splitting" pour l'implantation de fonctions hypergéométriques
dans MPFR. Un exemple de cette méthode est pour le calcul de la
factorielle. Si on pose F(i,j)=i!/j! on a n! = F(n,1)= F(n,n/2)F(n/2,1).
Ceci permet de séparer le calcul initial en deux sous-calculs et
ainsi de suite récursivement. Les premiers tests sur cette implantation
sont encourageants.
Nombres s'écrivant comme la différence de 2 flottants
Philippe Langlois nous a présenté ses premiers résultats
sur une caractérisation des nombres s'écrivant comme la
différence de deux flottants. Il s'intéresse au problème
d'existence et d'unicité. L'ensemble de ses cas se basant
sur des propriétés élémentaires des flottants. Sa preuve
semble un bon candidat à la formalisation sur machine.
Expérimentation avec MPFR et MPSolve
Paul Zimmermann nous a présenté un ensemble de tests d'utilisation
de sa bibliothèque MPFR.
Il a pris une application MPSolve en remplaçant MPF par la nouvelle
librairie MPFR. Les tests montrent que si MPF n'est pas portable
, MPFR donne les même résultats sur différentes architectures.
L'ensemble de ces tests est disponible ici.
Implantation de l'algorithme de Fourier-Motzkin en Coq
Loïc Pottier nous a présenté une procédure de décision pour
les systèmes linéaires d'équations et d'inéquations sur
les réels.
Cette procédure est séparée en deux parties. Une première partie
correspond à l'algorithme de Fourier-Motzkin. Elle
décide si le système est satisfiable ou non mais
retourne aussi une trace des calculs effectués. La
deuxième partie utilise cette trace pour construire un
terme de preuve qui est validé par le système Coq.
Les discussions:
Le calcul de la racine carrée à la Karatsuba
Paul Zimmermann nous a détaillé la preuve de correction
de son algorithme de calcul de la racine carrée.
L'organisation du workshop
Deux dates possibles du workshop ont été arrêtées: 23,24 Octobre ou
15,16 Novembre. Le workshop se déroulera à Lyon . Les possibles invités
sont: Harrison, Shewschuk, Sofroniou et Cuyt. On a aussi proposé de
donner des tutoriaux lors du workshop. Laurent Théry fera un appel à
abstract dès que les dates et les invités seront fixés.
Le recrutement du post-doctorant
Laurent Théry est chargé de faire la fiche de recrutement
du post-doc. On espère que la diffusion de cette annonce
en parallèle avec les recherches des membres d'AOC nous permettra
de trouver un bon candidat.
Prochaine réunion AOC
Elle aura lieu lors de la tenue du workshop.
[Page d'accueil]
Laurent Théry