Deuxième réunion

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