Journées Nationales de Calcul Formel 2018
CIRM, Luminy, 22–26 janvier 2018
Journées Nationales de Calcul Formel — 22–26 janvier 2018
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.
Calcul tensoriel formel sur les variétés différentielles
par Éric Gourgoulhon (CNRS, LUTH, Observatoire de Paris)Le calcul tensoriel sur les variétés différentielles comprend l'arithmétique des champs tensoriels, le produit tensoriel, les contractions, la symétrisation et l'antisymétrisation, la dérivée de Lie le long d'un champ vectoriel, le transport par une application différentiable (pullback et pushforward), mais aussi les opérations intrinsèques aux formes différentielles (produit intérieur, produit extérieur et dérivée extérieure). On ajoutera également toutes les opérations sur les variétés pseudo-riemanniennes (variétés dotées d'un tenseur métrique) : connexion de Levi-Civita, courbure, géodésiques, isomorphismes musicaux et dualité de Hodge.
Dans ce cours, nous introduirons tout d'abord la problématique du calcul tensoriel formel, en distinguant le calcul dit “abstrait” du calcul explicite. C'est ce dernier qui nous intéresse ici. Il se ramène in fine au calcul symbolique sur les composantes des champs tensoriels dans un champ de repères, ces composantes étant exprimées en termes des coordonnées d'une carte donnée.
Nous discuterons alors d'une méthode de calcul tensoriel générale, valable sur l'intégralité d'une variété donnée, sans que l'utilisateur ait à préciser dans quels champs de repères et avec quelles cartes doit s'effectuer le calcul. Cela suppose que la variété soit couverte par un atlas minimal, défini carte par carte par l'utilisateur, et soit décomposée en parties parallélisables, i.e. en ouverts couverts par un champ de repères. Ces contraintes étant satisfaites, un nombre arbitraire de cartes et de champs de repères peuvent être introduits, pourvu qu'ils soient accompagnés des fonctions de transition correspondantes.
Nous décrirons l'implémentation concrète de cette méthode dans SageMath ; elle utilise fortement la structure de dictionnaire du langage Python, ainsi que le schéma parent/élément de SageMath et le modèle de coercition associé. La méthode est indépendante du moteur de calcul formel utilisé pour l'expression symbolique des composantes tensorielles dans une carte. Nous présenterons la mise en œuvre via deux moteurs de calcul formel différents : Pynac/Maxima (le défaut dans SageMath) et SymPy. Différents champs d'application seront discutés, notamment la relativité générale et ses extensions.
notes | support | site web | vidéo
Calcul formel et preuves formelles
par Assia Mahboubi (Inria Saclay -- Île-de-France)Les assistants de preuve sont des logiciels qui permettent de représenter et de manipuler les énoncés mathématiques et leurs preuves. Énoncés et preuves sont ainsi décrits par l'utilisateur dans le formalisme logique sous-jacent à l'outil, de sorte que la vérification des démonstrations peut être rendue entièrement mécanique. L'assistant de preuve fournit des outils pour combler (dans une certaine mesure) le fossé qui sépare ce langage formel de bas niveau, où tout doit être explicite, et la pratique usuelle de la langue mathématique, avec ses appareils de conventions, de notations et d'implicite.
Par ailleurs, la plupart des assistants de preuve peuvent aussi être utilisés pour produire des programmes dits certifiés. Ces programmes font l'objet d'un théorème, lui-même formellement vérifié, qui décrit et garantit les propriétés mathématiques des résultats produits. En particulier, ces outils ont été utilisés pour la vérification de preuves mathématiques reposant crucialement sur une puissance de calcul surhumaine comme celles du théorème des quatre couleurs, de la conjecture de Kepler, ou encore l'étude numérique de l'attracteur de Lorentz.
Ce cours se propose de présenter de manière non technique l'activité de formalisation de résultats mathématiques à l'aide d'un assistant de preuve. En particulier, il tentera de donner un aperçu des possibilités offertes par ces logiciels pour garantir formellement les propriétés que l'on attend des résultats d'un algorithme du calcul formel, et de son implémentation.
Méthodes formelles pour les équations aux dérivées partielles
par Daniel Robertz (Plymouth University)Given a system of linear or nonlinear partial differential equations, various tasks like finding all power series solutions, finding all compatibility conditions, or deciding whether another given equation is a consequence of the system, require formal manipulation of the system.
This course will give an introduction to methods of symbolic computation, notably Janet bases and Thomas decomposition, which perform the above tasks and which are fundamental for a further algebraic study of differential equations.
Janet bases provide normal forms for systems of linear partial differential equations which allow to solve the above (and other) tasks.
The Thomas decomposition method splits a system of polynomially nonlinear partial differential equations into finitely many so-called simple differential systems whose solution sets form a partition of the original solution set. The power series solutions of each simple system can be determined in a straightforward way.
On the other hand, certain sets of analytic functions admit an implicit description in terms of partial differential equations and inequations. Strategies for solving related differential elimination problems and applications to symbolic solving of differential equations are presented as well.
Maple implementations of the discussed algorithms are freely available.
Sur le calcul formel et numérique des singularités
par Jean-Claude Yakoubsohn (Institut de Mathématiques de Toulouse, Université Paul Sabatier)Les modélisations de la « nature » regorgent de problèmes dont la résolution est difficile du fait de la présence de singularités. Or le calcul des singularités est toujours un challenge en ce début d'année 2016. Après un exposé liminaire sur les mathématiques des singularités, je propose de donner une synthèse sur les différentes méthodes de calcul des solutions singulières en développant deux points de vue
- Celui de la géométrie algébrique qui est basé sur l'algèbre locale, la dualité et les matrices de Macaulay.
- Celui de l'analyse qui repose sur le théorème de Rouché, la détermination de rang numérique et la convergence « rapide ».
Enfin je donnerai une liste de problèmes ouverts.