LIP6 2003/009
- Habilitation à Diriger des Recherches
Programmer le Calcul Formel, de L'Algorithmique à la Sémantique - R. Rioboo
- 118 pages - 18/12/2002- document en - http://www.lip6.fr/lip6/reports/2003/lip6.2003.009.pdf - 903 Ko
- Contact : Renaud.Rioboo (at) nulllip6.fr
- Ancien Thème : CALFOR
- Mots clés : Calcul Formel, FoC, nombres reels,
- Directeur de la publication : David.Massot (at) nulllip6.fr
Mes travaux de recherche ce sont toujours centres sur le Calcul Formel. C'est à dire la manipulation automatique de formules mathématiques. Pour pouvoir décrire des algorithmes sur les formules, on est amené à utiliser des arithmétiques <<exactes>>. Les <<nombres>> avec lesquels on travaille n'ont plus une taille fixe.
La première partie traite des nombres algébriques réels qui sont l'analogue des nombres réels usuels pour le calcul formel. Ils sont du point de vue du calcul avec des racines de polynômes ce que sont les nombres réels du point de vue des limites de suites. On sait que l'arithmétique exacte sur ces nombres algébriques réels est décidable depuis longtemps. Toutefois aucune des techniques utilisées dans les grands logiciels de calcul formel ne permet de faire de <<gros calculs>> avec ces nombres.
La raison principale de cette limitation vient de ce qu'on ne peut pas décrire facilement les représentations alternatives que je propose dans ces systèmes. Aujourd'hui, seul le langage Axiom permet d'exprimer des
algorithmes efficaces pour manipuler des nombres algébriques réels.
Implémenter des algorithmes compliqués pose au programmeur la question de correction. On veut des manipulations exactes et on doit donc démontrer les méthodes que l'on utilise. Il nous faut pour cela maîtriser complètement la sémantique du langage que l'on utilise. On peut ainsi faire une <<bonne assimilation>> entre les mathématiques que l'on démontre et l'implantation des algorithmes dans un langage de programmation.
La seconde partie présente les bases du projet FoC (http://www-calfor.lip6.fr/foc/) qui se propose d'étudier des outils pour la programmation certifiée d'algorithmes de Calcul Formel. Le langage de programmation offre au programmeur un cadre unifié dans lequel il peut à la fois énoncer ses algorithmes et leurs spécifications.
La première partie traite des nombres algébriques réels qui sont l'analogue des nombres réels usuels pour le calcul formel. Ils sont du point de vue du calcul avec des racines de polynômes ce que sont les nombres réels du point de vue des limites de suites. On sait que l'arithmétique exacte sur ces nombres algébriques réels est décidable depuis longtemps. Toutefois aucune des techniques utilisées dans les grands logiciels de calcul formel ne permet de faire de <<gros calculs>> avec ces nombres.
La raison principale de cette limitation vient de ce qu'on ne peut pas décrire facilement les représentations alternatives que je propose dans ces systèmes. Aujourd'hui, seul le langage Axiom permet d'exprimer des
algorithmes efficaces pour manipuler des nombres algébriques réels.
Implémenter des algorithmes compliqués pose au programmeur la question de correction. On veut des manipulations exactes et on doit donc démontrer les méthodes que l'on utilise. Il nous faut pour cela maîtriser complètement la sémantique du langage que l'on utilise. On peut ainsi faire une <<bonne assimilation>> entre les mathématiques que l'on démontre et l'implantation des algorithmes dans un langage de programmation.
La seconde partie présente les bases du projet FoC (http://www-calfor.lip6.fr/foc/) qui se propose d'étudier des outils pour la programmation certifiée d'algorithmes de Calcul Formel. Le langage de programmation offre au programmeur un cadre unifié dans lequel il peut à la fois énoncer ses algorithmes et leurs spécifications.