Journées Nationales de Calcul Formel (JNCF) 2011
CIRM, Luminy
14 – 18 novembre 2011

JNCF 2011 — Journées Nationales de Calcul Formel
14 – 18 novembre 2011

Cours

Quatre cours de trois heures sont prévus. Le reste du temps sera consacré à des exposés d'une vingtaine de minutes portant sur des travaux de recherche récents, principalement proposés par des doctorants et post-doctorants.

Théorie algébrique des nombres et calcul formel, par Karim Belabas, Université Bordeaux 1.

La théorie algébrique des nombres est née du désir de résoudre certaines équations diophantiennes en nombres entiers (typiquement, l'équation de Fermat). Elle introduit et étudie des structures algébriques associées aux extensions algébriques de ou de , en y retrouvant la trace des propriétés des entiers ordinaires, par exemple la factorisation unique en produit de nombres premiers, sous une forme affaiblie. Je motiverai l'introduction des objets correspondants (anneaux d'entiers, groupes de classes, unités, groupes de Galois, fonctions ), et expliquerai comment les calculer en temps raisonnable. On citera des applications à la résolution algorithmique d'équations diophantiennes concrètes (équations aux normes, équations de Thue).

Le télescopage créatif pour l'intégration et la sommation paramétrées, par Frédéric Chyzak, INRIA Rocquencourt.

La théorie des fonctions spéciales, celle des polynômes orthogonaux, ainsi que la combinatoire amènent à de nombreux problèmes d'intégrales et de sommes paramétrées, simples ou multiples, faisant intervenir des fonctions de plusieurs variables, continues ou discrètes. Diverses natures de questions interviennent, selon qu'il s'agit de trouver une expression explicite pour une intégrale ou une somme, ou de valider une identité, et selon que le problème à résoudre est exprimé comme une convolution, une extraction de coefficients, ou encore qu'il s'agit d'une intégrale plus générale.

L'approche algorithmique la plus fructueuse pour traiter ces intégrales et sommes est celle du «  télescopage créatif  », développée et popularisée depuis les travaux de Zeilberger au début des années 90. Le point de vue gagnant est l'abandon des formes explicites comme structure de donnée, au profit d'une représentation des fonctions à manipuler comme solution d'équations ou de systèmes linéaires, différentiels ou de récurrence. La méthode réalise, sur cette représentation implicite, un calcul qui généralise la dérivation sous le signe «  intégrale », et dont la terminaison est justifiée dans les bons cas par une théorie de dimension empruntée à la théorie des D-modules.

Depuis son introduction et son algorithmisation par Zeilberger pour les sommes hypergéométriques de la combinatoire, la méthode a été étendue dans diverses directions : le cas des sommes hypergéométriques correspondant à des récurrences d'ordre 1 a d'abord été transposé au cadre des équations différentielles d'ordre 1 pour les intégrales hyperexponentielles ; l'ensemble de cette algorithmique a été étendu aux solutions de systèmes linéaires d'ordre supérieur, pour la sommation et l'intégration de fonctions intégrales de fonctions spéciales «  D-finies  » et de polynômes orthogonaux ; les mêmes idées ont été appliquées à des fonctions dépendant d'un nombre infini de variables, pour l'étude de certaines extractions de coefficients de fonctions symétriques de la combinatoire ; enfin, la limitation au cas D-fini, correspondant à une dimension nulle d'un certain idéal non commutatif, a été partiellement levée dans un certain nombre de cas, de sorte à élargir la classe des fonctions spéciales admettant un traitement par télescopage créatif.

Du point de vue algorithmique, le point de départ de la méthode de Zeilberger peut s'interpréter comme une forme d'élimination polynomiale non commutative, entre les représentations polynomiales d'opérateurs linéaires différentiels et de récurrence. La théorie des bases de Gröbner s'étend à ce cadre et a fourni les premiers algorithmes. Une approche plus efficace s'appuie sur la résolution d'équations auxiliaires en leurs solutions fractions rationnelles. Néanmoins, ces deux solutions souffrent de ce qu'ils conservent dans leur sortie une forme de trace du calcul qui, si elle peut servir de certificat au résultat final, est bien souvent inutile dans les applications. C'est pourquoi il est apparu important de tenter de s'affranchir de ces certificats. Dans certains cas, la recherche heuristique d'une équation différentielle vérifiée par un développement en série adéquat à grand ordre peut être validé a posteriori, et fournir une équation sur l'intégrale. Dans le cas de fractions rationnelles bivariées, une approche mêlant l'algorithme de Zeilberger et la réduction de Hermite permet de représenter les certificats dans une taille acceptable.

Dans ce mini-cours, nous nous proposons de traiter des divers cadres d'applications et approches algorithmiques du télescopage créatif, jusqu'à aborder quelques questions de complexité.

Calcul analytique, par Joris van der Hoeven, CNRS & École polytechnique.

À l'heure actuelle, le calcul formel permet surtout la manipulation exacte d'objets de natures algébrique ou symbolique. Le calcul analytique se propose de généraliser cette démarche de calcul exact à l'analyse. Par rapport au calcul numérique classique, il faut donc être en mesure de certifier les calculs en s'appuyant sur une technologie systématique pour encadrer les erreurs de calcul. Un système de calcul analytique se compose de quatre couches de natures assez différentes.

Dans notre cours, nous aborderons en détail ces différents thèmes du calcul analytique, ainsi que quelques autres aspects, comme des techniques d'implantation, ou la démarche « expérimentation, hypothèse, vérification ». On fournira aussi quelques applications comme l'intégration certifiée de systèmes dynamiques ou la résolution de systèmes algébriques par des méthodes d'homotopie certifiées.

Preuves formelles automatiques en géométrie, par Loïc Pottier, INRIA Sophia Antipolis Méditerranée

De nombreux théorèmes de géométrie élémentaire (Desargues, Pappus, Feuerbach, etc) peuvent être démontrés automatiquement. Il existe différentes méthodes efficaces, dont la plus connue est dans doute celle de Wu, mais qui se prêtent plus ou moins à la formalisation. Nous étudierons une méthode qui consiste à utiliser un calcul incomplet de bases de Gröbner pour produire un certificat de petite taille (un programme sans boucle, ou straightline program), permettant de démontrer ensuite une égalité polynomiale de type Nullstellensatz: si sont des polynômes exprimant les hypothèses du théorème, et sa conclusion, alors on peut écrire . Le calcul du certificat représentant peut être fait dans n'importe langage (par exemple ocaml ou F7), alors que la preuve du Nullstellensatz est produite par réflexion dans le système d'assistance à la preuve Coq. On montrera sur des exemples dans le système Coq les différentes étapes et principes employés.


© Grégoire Lecerf, 2011.