Thèmes de recherche

Notre programme de recherche s'organise autour de trois thèmes :

• le premier thème se concentre sur l'environnement de travail du chercheur, de l'ingénieur ou de l'étudiant qui développe des algorithmes certifiés et les démonstrations mathématiques nécessaires à la certification,

• le deuxième thème se concentre sur la formalisation de théories mathématiques pour décrire les objets de base de la connaissance mathématique,

• le troisième thème s'intéresse aux outils permettant de faciliter les démonstrations mathématiques et la production d'implantations efficaces à partir des descriptions formelles des algorithmes et des démonstrations de leur correction.

Ces thèmes contribuent les uns aux autres de manière circulaire : l'environnement de travail du chercheur repose sur les outils de démonstration qui doivent être efficaces et sûrs. Le développement de ces outils de démonstration passe par la description certifiée d'algorithmes, qui repose elle-même sur une formalisation des outils mathématiques de base. Enfin, la formalisation des outils mathématiques de base est possible grâce à l'utilisation d'un environnement de travail pratique et efficace.

Environnements de preuves

Le but de ce thème est d'étudier les outils mécaniques de recherche et de vérification de preuves pour faciliter leur utilisation par des ingénieurs et des mathématiciens dans la production de logiciels et de théories mathématiques formelles.

Deux objectifs complémentaires apparaissent. Le premier est d'améliorer les moyens d'interaction entre l'ordinateur et l'utilisateur, afin de rendre les outils accessibles à des ingénieurs peu intéressés par la théorie de la preuve et à des mathématiciens peu intéressés par la programmation et les contraintes formelles. Le second objectif est de faciliter la maintenance de grands développements de mathématiques formelles, afin de faciliter leur réutilisation et leur adaptation à des contextes variés.

Ainsi, nous voulons augmenter la pénétration des méthodes formelles dans le développement des logiciels à la fois en facilitant leur usage par des débutants et en augmentant la productivité des utilisateurs confirmés.

Moyens d'interaction

En abordant le domaine des interfaces utilisateurs pour systèmes de preuve avec les outils initialement développés pour les environnements de programmation [45], le projet CROAP a permis une évolution rapide de ce domaine. Avec des concepts comme la preuve par sélection (proof-by-pointing [11]), il a acquis une grande notoriété.

La notion de preuve par sélection montre qu'une interaction riche entre l'utilisateur et la machine exige le développement de véritables compilateurs dont les données d'entrées forment une description symbolique des actions de l'utilisateur et dont les sorties sont des commandes exprimées dans le langage de bas niveau du système de preuve. De tels compilateurs méritent une description formelle précise et une réflexion sur les optimisations qui peuvent être appliquées sur le code engendré [13,7].

Les outils d'interactions doivent bien sûr s'adapter aux domaines mathématiques rencontrés. L'expérience a montré que l'outil de preuve par sélection devenait inefficace lorsque l'on aborde les raisonnements algébriques. Nous avons mis à jour d'autres possibilités d'interaction efficace, fondées non seulement sur l'interprétation de positions désignées par l'utilisateur mais aussi sur l'interprétation de ses mouvements [6,9] et nous avons montré comment on pouvait rendre de tels outils facilement extensibles par l'utilisateur, pour s'adapter à des domaines mathématiques variés. Un défi important pour ce domaine de travail est de comprendre si les deux modèles d'interaction peuvent être joints de façon naturelle, de manière à fournir une interface utilisateur avec un apprentissage court mais un apport réel pour les débutants et les utilisateurs experts.

L'interprétation des actions de l'utilisateur avec la souris prend en charge les problèmes de communication de l'utilisateur vers la machine. Il est aussi important de maîtriser la communication de la machine vers l'utilisateur. Nous nous appuyons sur les recherches effectuées ces dernières années dans l'équipe CROAP sur l'outil d'affichage bi-dimensionnel, incrémental, et multi-thread Figue et son extension Aïoli pour la manipulation d'objets arborescents. Nous voulons compléter cette investigation pour mieux comprendre comment cet outil interagit avec les outils de visualisation existants ou en cours de développement pour le Web.

Maintenance des développements formels

Dans notre stratégie, il est nécessaire de prendre en compte non seulement les travaux nécessaires à la production de nouveaux logiciels certifiés et de nouveaux développements de mathématiques formelles mais également l'évolution sur le long terme de ces logiciels et développements. Par rapport à un développement mathématique traditionnel, un développement formel est plus sensible à des changements de l'environnement de travail : ce développement est construit sur une version précise de formalisation d'une théorie mathématique, utilisant les règles de raisonnement permises par un système formel précis. Notre travail sur la maintenance des développements formels vise à diminuer la fragilité des développements en facilitant leur adaptation d'un contexte à l'autre.

Pour améliorer l'utilisation des méthodes formelles dans l'industrie du logiciel, il faut résoudre les problèmes de maintenance qu'elles posent. En effet, lorsque les techniques formelles seront plus répandues, les développements verront leur taille augmenter et les préoccupations des développeurs (ingénieurs ou mathématiciens) évolueront d'un cadre logique vers un cadre logistique. Les grands développements formels seront comme de grandes librairies de calcul : ils devront être organisés comme tels, et les outils pour assurer leur cohérence restent à développer.

Pour apporter des réponses satisfaisantes dans ce domaine, nous pouvons organiser nos investigations autour des objectifs secondaires suivants :

• Disposer de structures pour organiser les développements formels à un niveau d'abstraction plus élevé que les simples théorèmes. Ces travaux sont déjà abordés par l'étude des modules effectués dans l'équipe Coq. Cet objectif implique un besoin de comprendre les outils qui peuvent faciliter la maintenance de grands développements à partir de données organisées en modules.
• Étudier spécifiquement les opérations nécessaires pour adapter des développements existants à des domaines d'applications légèrement différents. Ces travaux passent par une étude des dépendances entre objets mathématiques et la propagation de modifications le long des chaînes de dépendance.
• Apporter un support pour les activités en amont et en aval d'un développement formel : en amont, description formelle ou informelle de modèles abstraits, raffinement de ces modèles, mise en correspondance et réutilisation des preuves; en aval, ré-ingéniérie de développements formels, documentation a posteriori, éventuellement par extraction systématique d'informations des développements formels (voir par exemple les travaux de Gilles Kahn, Laurent Théry et Yann Coscoy dans ce domaine [20]), aide à l'isolation de concepts apparus pendant le travail de formalisation, mécanisation des opérations systématiques.

Nous disposons déjà de plusieurs grands développements en Coq, l'algorithme de Buchberger certifié [44], l'algorithme de factorisation des polynômes [30], l'algorithme de Stålmark pour la satisfiabilité des formules logiques du premier ordre [29], un compilateur [8], et une formalisation de l'algèbre élémentaire [39]. Nous serons à même de mesurer la validité de notre approche en évaluant la façon dont ces développements vieillissent et s'adaptent aux versions successives de Coq. Pour pousser nos investigations dans des conditions plus sélectives, nous pourrons également étudier la façon dont ces développements s'adaptent à d'autres outils de formalisation comme le système NuPrl de Cornell University.

Formalisation de théories mathématiques

Le but de ce thème est d'étudier comment des théories mathématiques où interviennent de nombreux types d'objets peuvent être représentées dans le calcul des constructions inductives, de façon à être aussi lisibles et utilisables que possible par quelqu'un qui en a une connaissance scolaire ou académique.

Ce thème est très lié aux deux autres, en ce sens qu'il doit fournir des fondements sémantiques aux objets des environnements de preuves, et des bibliothèques d'objets, lemmes et théorèmes de base pour alléger le travail de preuve des algorithmes mathématiques, dont la preuve nécessite souvent de connaître et de manipuler de larges pans des mathématiques classiques.

L'exemple qu'on a commencé à étudier est l'algèbre commutative : on s'est inspiré pour cela des formalisations en Coq de la théorie des ensembles ⁴ et de la théorie des catégories⁵. Par la suite viendront la géométrie algébrique ⁶, les théories des groupes et des corps finis, et la géométrie des polytopes (2D et 3D).

Le CCI est assez puissant pour formaliser des mathématiques complexes : structures algébriques avec leurs dépendances et leurs opérations (comme le système de calcul formel Axiom l'a fait), mais aussi, et surtout puisqu'on veut faire des démonstrations, toutes leurs propriétés logiques, ce qui reste très marginal dans les systèmes de calcul scientifique. Le CCI permet aussi d'écrire des algorithmes, sous forme de programmes fonctionnels récursifs, avec des structures de données riches. Enfin, avec l'isomorphisme de Curry-Howard, le CCI est un langage de manipulation des preuves mathématiques. Mais ce langage est difficile d'accès, un peu comme un assembleur, bien que sa concision et sa puissance le rendent très élégant pour l'initié.

Le système Coq, l'interface CtCoq offrent des outils qui permettent souvent une formalisation satisfaisante : les ``record'', les coercions, le pretty-printer PPML, la syntaxe extensible de Coq par exemple. Mais de nombreux problèmes restent à résoudre : héritage multiple, complexité de l'empilement des coercions et du typage entre structures algébriques, manipulation difficile des types dépendants dans les preuves et les constructions d'objets, absence de sous-typage et de quotient dans le CCI.

On a pu à ce jour formaliser l'algèbre commutative et la théorie des catégories de base sans trop de problèmes [1]. Il est néanmoins certain que de nouveaux outils ont à être développés et intégrés à Coq et CtCoq à l'avenir (tactiques dédiées, macros de génération de code Coq, algorithmes de réflexion, par exemple).

Plus fondamentalement, on étudie comment les types inductifs particuliers qu'on utilise pour représenter les structures mathématiques (record, ou $\Sigma$-types) peuvent être abstraits dans Coq lui-même pour permettre de calculer et raisonner sur eux à un niveau plus général (utiliser la notion de télescopes [16] et les opérations de coercions associées, par exemple).

Implémentations certifiées d'algorithmes de calcul scientifique

Pour obtenir des programmes certifiés, nous proposons une approche inverse de celle généralement utilisée : plutôt que de chercher à prouver des propriétés d'un programme existant (en formalisant sa sémantique), nous proposons de produire des programmes dont la correction découle de celle de leur processus de création.

Par exemple, pour obtenir un programme de calcul de bases de Gröbner, on commence par écrire l'algorithme de Buchberger dans le CCI, puis on prouve en Coq qu'il calcule bien une base de Gröbner, enfin on utilise le processus d'extraction automatique de Coq pour produire un programme Ocaml, dont on sait qu'il calcule la même chose, puisque ceci est garanti par les propriétés du CCI et de son affaiblissement dans la théorie des types ML [44]. Le programme extrait est efficace, comme on pouvait le prévoir, et comme le montre l'expérience.

Cette approche a plusieurs avantages : on travaille à un haut niveau d'abstraction, en restant indépendant du langage d'implantation final (mais plus ce langage sera fonctionnel, plus l'implantation sera efficace). On peut aussi se concentrer sur les caractéristiques propres à l'algorithme qu'on étudie, en faisant abstraction du reste (gestion de la mémoire, choix d'implantation des données). Le niveau de certification peut être ainsi variable, et paramétrable (par exemple pour le calcul de bases de Gröbner, on peut supposer qu'une implantation de l'arithmétique des polynômes est donnée).

Mais elle pose aussi quelques problèmes qui, sans être bloquants, s'avèrent difficiles à résoudre. Par exemple il est très difficile actuellement de faire des preuves sur des algorithmes récursifs dont la terminaison découle d'un ordre bien fondé ⁷. Il est aussi délicat de travailler dans un style impératif, ou avec des opérations qui font des effets de bord (opérations en place sur les données par exemple).

Nous avons acquis une expérience originale dans ce domaine de la certification d'algorithmes mathématiques, où les expériences que nous avons menées ont toutes été concluantes : arithmétique des entiers longs, arithmétique des polynômes (multiplication de Karatzuba)[37], algorithme de Buchberger [40], factorisation de polynômes [30], satisfiabilité de formules booléennes [29].

L'efficacité des implantations obtenues est très bonne, puisqu'elle est au niveau de certains logiciels parmi les plus utilisés (Maple, Mupad, Pari).

Parmi les problèmes qui restent à résoudre, nous comptons traiter celui de l'extraction vers d'autres langages que Ocaml (quelques expériences avec C et Java sont encourageantes, et extraire vers Maple devrait être similaire), ainsi que celui de l'extraction de tout le CCI. En effet, actuellement, seule une partie du CCI (les sortes Set et Prop) s'extrait correctement en Ocaml. Nous avons une première implantation de cette extraction totale (incluant les univers de la sorte Type), vers Ocaml non typé, que nous comptons étendre et fonder théoriquement.

Notre but dans ce thème est triple : développer des outils nouveaux (extraction, récursion bien fondée), les valider sur des algorithmes fondamentaux du calcul scientifique, dont on testera les implantations sur des applications significatives.

Ce thème est lui aussi dépendant des deux autres, puisqu'il fournira la matière de leur développement, et devra bénéficier de leur avancement.