Participants : Yves Bertot, Yann Coscoy, Stéphane Lavirotte, Pascal Lequang, Francis Montagnac, Olivier Pons, Loïc Pottier, Laurence Rideau, Laurent Théry.
Depuis sa conception initiale, l'environnement de preuve CtCoq est bâti sur le système Centaur, dont les qualités ont permis des développements efficaces et novateurs. Néanmoins, le travail sur des formules mathématiques a montré les limites des capacités d'affichage de Centaur et a poussé Laurent Théry et Bruno Conductier à développer un outil d'affichage beaucoup plus performant en Java, appelé Figue8. Cet outil arrive maintenant à maturité et nous voulons reprendre l'architecture de CtCoq pour la détacher de Centaur et l'adapter à ce module d'affichage afin de pouvoir continuer nos expériences sur une base moins ancienne et plus facile à distribuer.
Ce travail est l'occasion d'une réflexion sur plusieurs aspects de l'environnement de preuve pour y améliorer plusieurs aspects de l'interface.
Participant : Yves Bertot.
Des expériences récentes ont montré que l'on pouvait étendre l'utilisation de la souris pour augmenter la variété des figures de raisonnement mathématiques que l'on pouvait exprimer à l'aide de la souris. Ces expériences n'ont laissé qu'entrevoir les nouvelles possibilités qu'il reste à explorer entièrement.
Parmi les points que nous voulons étudier, citons particulièrement le traitement des relations d'égalité. En effet, le système Coq permet de gérer deux sortes de relations d'égalité : l'égalité primitive pour laquelle le système fournit une procédure de réécriture et des notions d'égalités définies, pour lesquelles les propriétés de réflexivité, symétrie, transitivité, et congruence par rapport à certains opérateurs doivent être exprimées par des opérateurs et pour lesquelles le système Coq ne fournit aucun support particulier. L'objectif que nous espérons atteindre dans ce domaine est un traitement uniforme pour les deux formes d'égalités.
Participants : Yves Bertot, Pascal Lequang, Francis Montagnac, Laurence Rideau, Laurent Théry.
Intégrer nos outils d'interface sur le Web nous permettra de bénéficier des développements effectués dans les navigateurs et d'atteindre une population plus large d'utilisateurs potentiels d'outils mathématiques sur ordinateur. Nous comptons explorer deux approches : d'une part les outils que nous développons sont écrits en Java, ce qui permet une intégration aisée dans les navigateurs Web les plus répandus. Il est alors possible d'envisager que les utilisateurs téléchargent nos modules comme de simples applets; d'autre part, les navigateurs Web sont déjà construits pour manipuler des données structurées et il devrait être possible d'utiliser directement ces primitives de manipulation pour gérer l'ensemble des données nécessaire au développement des démonstrations.
Participants : Stéphane Lavirotte, Loïc Pottier.
La thèse de Stéphane Lavirotte (dirigée par Loïc Pottier) porte sur la reconnaissance de formules mathématiques. On suppose donnés les caractères de la formule, leur position et leur taille. Il s'agit de reconstruire la structure d'une formule pour obtenir sa représentation arborescente. L'approche que nous avons choisie est en deux étapes. La première consiste à construire un graphe dont les noeuds sont les symboles de la formule, et dont les arcs représentent les proximités géométriques entre les symboles [28]. La deuxième étape se fonde sur le développement d'une catégorie de grammaires de graphes avec contextes, dont on a montré que l'on pouvait résoudre formellement les ambiguïtés [27]. Les règles de grammaire sont utilisées une à une pour transformer un sous-graphe en un noeud qui contiendra alors la sous-formule reconnue.
Sur ce sujet de la reconnaissance de formules mathématiques, nous avons des contacts avec les équipes de recherche du domaine [38].
Il nous reste à améliorer la construction du graphe, sur lequel opère la grammaire, qui ne doit être ni trop riche (trop d'ambiguïtés), ni trop pauvre. Il faut aussi concevoir des grammaires capables de traiter des exemples complexes comme les matrices, les diagrammes commutatifs, en non pas seulement des structures essentiellement linéaires et arborescentes comme les polynômes, fractions et intégrales. Des problèmes algorithmiques se posent aussi, qu'on doit résoudre pour pouvoir traiter par exemple le contenu entier d'une page de livre mathématique.
Une connexion du prototype de Stéphane Lavirotte avec un logiciel de reconnaissance d'écriture manuscrite à partir d'une tablette graphique[26] a été faite, et testée avec succès sur des formules simples. Nous prévoyons d'avoir pour juin 1999 un prototype plus complet, qui puisse être intégré à un environnement comme CtCoq, ou Maple. Le portage en Java sous forme d'une applet est aussi prévu.
Participants : Yann Coscoy, Laurent Théry.
Le travail de thèse de Yann Coscoy a montré la faisabilité de la production automatique d'un document en langue naturelle à partir d'un développement en Coq. Il montre aussi que dans une certaine mesure le langage naturel pouvait servir comme langage d'entrée pour la construction de preuve. On se propose d'approfondir ce travail. L'utilisation du langage naturel dans l'interface nous semble un facteur important dans la diminution du temps d'apprentissage d'un démonstrateur.
Participants : Yves Bertot, Laurent Chicli, Frédérique Guilhot, André Hirschowitz, Loïc Pottier, Laurence Rideau.
Faire des preuves simples et compréhensibles d'algorithmes mathématiques suppose de parler ce langage mathématique dans les preuves. Il faut donc rendre disponibles des théories de base comme l'algèbre, l'analyse et l'arithmétique9.
On peut réaliser une preuve précise (sur le papier et sûrement en Coq) de l'algorithme cryptographique RSA sans parler de groupes finis, d'idéaux et de corps finis. Mais les choses sont bien plus rapides et claires en utilisant des résultats de ces théories.
Il en va de même avec des algorithmes de géométrie algébrique comme celui de Buchberger : 30% de la preuve formelle en Coq réalisée par Laurent Théry concernent l'arithmétique des polynômes à plusieurs indéterminées. Avec une librairie algébrique étoffée et bien conçue, cette preuve aurait été considérablement simplifiée. En effet, la preuve de Laurent Théry est modulaire : la partie arithmétique est clairement séparée du reste, qui concerne l'algorithme de Buchberger. 10
Ce travail de formalisation de mathématiques en théorie des types est en cours dans d'autres équipes de recherche, à commencer par Coq.
Le projet Coq a traité différents domaines comme les nombres réels, les anneaux commutatifs, les catégories. Les contributions apportées par les utilisateurs de Coq concernent l'arithmétique, la théorie des ensembles, les groupes, la géométrie, etc [19]. Elles sont plus ou moins développées, compatibles entre elles, conçues pour être réutilisables facilement.
Nous essayons de les réutiliser dans nos développements : directement par exemple pour les catégories, l'arithmétique des entiers, ou en les adaptant, notamment pour la théorie des ensembles finis. Lorsque ce n'est pas possible, par exemple quand les choix qui ont été faits sont incompatibles avec les nôtres, nous essayons de garder possible leur intégration dans nos contributions (théorie des anneaux, des groupes par exemple).
Participants : Laurent Chicli, André Hirschowitz, Loïc Pottier.
Une bonne partie de l'algèbre de base est aujourd'hui disponible et en développement dans notre équipe[39]. C'est d'ailleurs sur cette base que commence la thèse de Laurent Chicli dont le but est de réaliser une formalisation de la géométrie algébrique, pour prouver la méthode d'Horace pour l'interpolation de polynômes à plusieurs variables.
Un premier but précis de cette formalisation concerne un énoncé connu sous le nom de "lemme d'Horace". Cet énoncé présente deux caractéristiques qui nous intéressent. D'une part il concerne des objets très abstraits : variétés projectives, faisceaux inversibles, sous-schémas non-réduits, points génériques divers. Et d'autre part il a un contenu algorithmique, plus précisément il justifie un algorithme qui a déjà été implémenté 11. Ce sujet comporte trois parties :
- un travail de formalisation complète des notions de géométrie algébrique nécessaires à la formulation du lemme d'Horace.
- l'implantation d'un algorithme (beaucoup plus général que celui implémenté par Mignon) reposant sur ce lemme, avec les structures de données adaptées.
- la démonstration que cet algorithme est correct, au sens où ses entrées et ses résultats vérifient le théorème voulu.
Participants : Loïc Pottier, Laurence Rideau.
Un autre domaine qui nous intéresse est la théorie des groupes finis 12 et en particulier les théorèmes de Sylow et les groupes de permutations, avec une application au Rubik's cube : prouver qu'une configuration donnée est valide (i.e. un petit farceur n'a pas fait sauter un élément pour le remettre à l'envers) et extraire de cette preuve une solution : suite de mouvements qui ramènent le cube à son état initial. Il va de soi que les preuves issues de cet exercice devront être réutilisables et sont elles mêmes plus importantes que la résolution du Rubik's cube.
L'arithmétique des corps finis est un troisième domaine que nous abordons, à la suite du stage de François Maurel [30], dans le but de traiter des algorithmes de codage et de cryptographie. C'est un domaine qui semble beaucoup plus délicat à traiter que celui de l'algèbre équationnelle. La notion d'ensembles finis y est centrale et il faut soigneusement la formaliser sous peine de rapidement tomber dans des preuves herculéennes.
Participants : Frédérique Guilhot.
Participants : Yves Bertot, Loïc Pottier.
Enfin, la géométrie 2D et 3D est un domaine très intéressant, où nous avons fait quelques expériences (Yves Bertot, Gilles Kahn), et où l'algorithmique est très développée. Nous proposons un sujet de stage sur la preuve d'un algorithme de calcul d'enveloppe convexe [3].
Participants : Antonia Balaa, Yves Bertot, Loïc Pottier, Laurent Théry.
Participants : Loïc Pottier, Laurent Théry.
Les algorithmes que nous comptons prouver, tout en restant en cohérence avec le thème précédent (formalisation de théories mathématiques), seront soit des algorithmes fondamentaux du calcul formel (polynômes, fractions rationnelles et matrices), soit des algorithmes numériques dont une implantation certifiée peut avoir un intérêt clair (calculs sur les réels, les complexes, développements limités avec contrôle des erreurs), ou encore des algorithmes qui relèvent des mathématiques discrètes (géométrie algorithmique, codage et cryptographie, formules booléennes).
Notre choix d'un algorithme particulier est guidé par différents paramètres :
Participant : Loïc Pottier.
Démontrer formellement la correction d'un algorithme dont on sait par avance
qu'il est correct, sans pouvoir en tirer un programme qui l'implémente de
façon sûre est un peu frustrant. L'extraction en Ocaml fournie par le
système Coq est une originalité forte de ce système [35]. La relative
simplicité de cette extraction est d'ailleurs déconcertante; ce qui la rend
aussi crédible. Son efficacité est aussi impressionnante, comme on a pu le
vérifier.
Elle n'est toutefois pas étendue à tout le CCI : elle ne fonctionne que sur
les premiers niveaux de la hiérarchie des univers du CCI, qui sont trop
limités pour une formalisation agréable des mathématiques. Une autre
limitation est le typage de Ocaml : certains termes extractibles (dans
F
)
ne sont pas typables en Ocaml.
C'est pour résoudre ces problèmes que nous avons cherché depuis un an à
étendre l'extraction à tout le CCI. En collaboration avec le projet Coq (dans
l'action CFC), nous avons mis au point un processus d'extraction
qui semble théoriquement sûr et qui traite tout le CCI. Un premier
prototype écrit dans le langage d'implantation de Coq, Ocaml, a été
développé par Loïc Pottier, dont le langage cible est encore Ocaml, mais non
typé.
En fait il peut se transposer facilement à tout langage objet qui contient un
évaluateur de 
-calcul avec pattern-matching et récurseurs.
Sous réserve d'y implémenter cet évaluateur, on devrait pouvoir extraire les
termes Coq vers Java, C, ou Maple. Un sujet de stage sur ce thème (Java) est
d'ailleurs proposé.
Ce prototype d'extraction du CCI a été testé avec succès sur l'algorithme de Cantor-Zassenhaus (avec des temps supportant la comparaison avec Mupad), et sur l'algorithme de Buchberger (où on perd un facteur 2 avec l'extraction standard).
Nous comptons d'une part fonder théoriquement cette extraction, d'autre part l'améliorer (évaluation partielle, pré-compilation), et l'intégrer aux outils disponibles autour du système Coq.
Participant : Yves Bertot.
Les travaux effectués dans le projet CROAP ont montré que les spécifications de sémantique naturelle [25] se prêtaient bien à la vérification de correction de compilateurs [21] et que ces vérifications formelles pouvaient être contrôlées mécaniquement en utilisant le système Coq [41,42,10]. Par exemple, nous disposons maintenant de la preuve complète d'un compilateur pour un embryon de langage impératif [8]. Dans le cadre de l'action de développement Génie, nous sommes engagés dans une collaboration avec Joëlle Despeyroux du projet CERTILAB et l'équipe d'Emmanuel Ledinot de Dassault Aviation. L'expérience acquise dans la preuve de compilateur est fructueuse pour cette collaboration.
Les travaux que nous envisageons de faire à court terme sur ce sujet consistent en l'ajout progressif de fonctionnalités au langage et à son compilateur : manipulation de tableaux, appel de procédures, utilisation de types définis. Il s'agit ensuite d'étudier comment la preuve de correction du compilateur est modifiée à chaque étape et de construire les outils qui permettent d'automatiser cette modification. Nous croyons que ces travaux apporteront des connaissances utiles non seulement au thème particulier du développement de compilateurs certifiés, mais aussi plus généralement au thème important de la maintenance de développements formels en présence de modifications des spécifications.
A long terme, ce travail pourra aussi contribuer à la fabrication d'outils d'extraction plus fiables, en fournissant la possibilité de compiler les programmes extraits de façon totalement sûre.
Participants : Antonia Balaa, Yves Bertot.
Le style de programmation fonctionnelle pure en usage dans le système Coq repose sur la définition récursive de fonctions. Une étude fine de ces définitions montre qu'il existe en fait deux styles distincts de récursivité : la récursivité structurelle, dirigée par la structure des données manipulées, et la récursivité ``bien fondée'' qui repose sur l'existence d'un ``bon ordre'' pour contrôler les appels récursifs et éviter les boucles infinies.
La récursivité structurelle est admirablement bien traitée dans le système Coq, qui fournit des primitives naturelles de simplification pour ce modèle de calcul [34]. En revanche, la récursivité bien fondée se décrit en théorie des types grâce à une notion d'accessibilité [32] qui est complexe à manipuler en pratique. Au cours du stage de DEA d'Antonia Balaa, nous avons pu montrer sur quelques exemples que ces difficultés pouvaient être surmontées en suivant une méthode systématique fondée sur une analyse du code des fonctions récursives. Au cours de la thèse d'Antonia Balaa, nous comptons fournir des outils qui automatisent cette méthode et préciser les conditions dans lesquelles cette méthode s'applique. Ces travaux font l'objet de discussions fréquentes avec les membres du projet Coq.
Participant : Loïc Pottier.
La réflexion consiste à exprimer dans un langage des propriétés du langage lui-même. C'est possible avec le CCI, comme l'ont montré Bruno Barras et Benjamin Werner [4] , ainsi que Samuel Boutin [15], les premiers pour le typage de Coq, le second pour la décision d'égalité dans les anneaux commutatifs. Dans ce dernier cas, la réflexion permet de remplacer une preuve d'égalité, qui consiste en une suite de preuves d'égalités élémentaires, par un calcul de forme canonique (par la réduction de Coq) et une preuve d'égalité syntaxique. On remplace ainsi un coût en espace par un coût en temps, ce qui est très avantageux : une fois la réduction effectuée, il suffit de stoker une preuve de taille réduite. Cette technique peut s'appliquer à une large classe de problèmes, et pas seulement aux décisions de théories équationnelles avec forme canonique. Nous comptons utiliser et développer cette technique dans différents domaines :
types par des télescopes).
Participant : Laurent Théry.
Prouver formellement la complexité d'un algorithme : à notre connaissance, c'est un problème qui n'a pas été traité directement. Nous comptons l'aborder en étudiant les travaux qui peuvent s'y rapporter (par exemple, en juin 1999 a lieu un ``workshop'', lié à la conférence LICS, sur le sujet ``implicit computational complexity''), et en réfléchissant sur les deux voies suivantes :