Valérie Ménissier-Morain

Arithmétique exacte: conception, algorithmique et performances d'une implémentation informatique en précision arbitraire

Résumé: Nous montrons dans cette thèse la nécessité d'avoir une arithmétique sûre, c'est-à-dire une arithmétique rationnelle exacte et une arithmétique réelle en précision arbitraire.

Nous décrivons tout d'abord l'implémentation en Caml d'une arithmétique rationnelle exacte et efficace. Nous discutons les problèmes de normalisation des nombres rationnels et de l'intégration à un langage fortement typé. Nous présentons quelques exemples d'utilisation spectaculaires ainsi qu'une comparaison avec les principaux langages dotés d'une arithmétique entière exacte.

Nous abordons ensuite l'arithmétique réelle en présentant une théorie axiomatique des nombres réels calculables. Dans ce cadre, nous donnons trois descriptions algorithmiques différentes d'arithmétique réelle. Nous représentons tout d'abord un nombre réel par une suite de nombres rationnels avec des dénominateurs de la forme d'une puissance de la base de travail et nous obtenons une description constructive complète et entièrement prouvée. La deuxième approche représente les nombres réels par la suite infinie des chiffres du développement de ce nombre dans une base de travail et nous donnons une description constructive et entièrement prouvée des opérations rationnelles sur cette représentation. La troisième représentation décrit les nombres réels par leur développement en fractions continues. Nous montrons deux algorithmes de transformation d'un type classique de fractions continues en un autre et nous décrivons les algorithmes pour les opérations usuelles. La première et la troisième représentations ont fait l'objet d'un prototype en Caml et nous comparons ces différentes représentations des nombres réels calculables.

Version PostScript de cette publication file

Référence BibTeX de cette publication

Page personnelle de Valérie Ménissier-Morain