Spécifications, contraintes et preuves

Présentation

Dans cet axe, nous nous intéressons à la formalisation de la géométrie pour démontrer des théorèmes, construire des figures ou, plus généralement, des scènes géométriques, et certifier des algorithmes en géométrie.

Contexte et objectifs

Plus précisément, nous visons la définition formelle d'univers géométriques, la preuve de propriétés, la production automatique d'objets géométriques définis par une spécification exprimée dans et univers géométrique et la dérivation d'algorithmes géométriques certifiés corrects. Nous nous penchons sur des méthodes informatiques permettant d'assister les preuves, de garantir la correction et la faisabilité et, dans la mesure du possible, d'assurer automatiquement certaines tâches notamment à travers l'étude de tactiques Coq ou, dans un autre registre, la résolution de contraintes géométriques. Les retombées attendues concernent des domaines tels que la modélisation géométrique, l'algorithmique géométrique, la géométrie pure, l'enseignement des mathématiques et la planification assistée d'opérations chirurgicales percutanées ou assimilées.

Participants permanents

• Deux professeurs : Jean-François Dufourd et Pascal Schreck
• Quatre maîtres de conférences : Caroline Essert, Nicolas Magaud, Pascal Mathis, Julien Narboux

Autres participants

Chercheur associé : Gabriel Braun (MC) associé en 2009

Post-doctorants : Christophe Brun (ATER), Simon E.B. Thierry (ATER)

Doctorants : Rémi Imbach

Anciens doctorants : Claire Baegert, Christophe Brun, Simon E. B. Thierry.

Bilan

La fusion des opérations 2 et 3 dans l'ancienne terminologie LSIITesque, est une manière d'officialiser la réunion de 2 opérations, réunion qui était familièrement baptisée opération 23. Cette réorganisation a pour résultat l'axe "Spécifications, contraintes et preuves" qui continue sous une autre appellation un thème de recherche original en France et qui nous tient particulièrement à cœur. Il concerne la certification logicielle dans le domaine de la géométrie. Ce thème englobe naturellement le domaine de la formalisation et de la preuve en géométrie, mais aussi la spécification de types abstraits et d'algorithmes certifiés concernant la géométrie.

Cela s'est traduit lors de ces dernières années par des activités de recherche dans quatre directions légèrement différentes mais participant du même esprit :

• Formalisation de la géométrie et preuves de théorèmes géométriques (N. Magaud, J. Narboux et P. Schreck) ;

• Spécification et preuves d'algorithmes géométriques en utilisant des cartes combinatoires (C. Brun, J.-F. Dufourd et N. Magaud) ;

• Spécification de figures et résolution de contraintes géométriques (P. Mathis, P. Schreck et S. Thierry) ;

• Formalisation et planification d'opérations percutanées dans le cas de l'ablation de tumeurs hépatiques et d'intervention radiologiques (C. Baegert, C. Essert et P. Schreck) ;

Preuves de théorèmes

géométrie d'incidence et combinatoire

Hartong-Reeb

???

Spécification, preuves d'algorithmes et implantation

Cette recherche reconsidère la modélisation et l'algorithmique géométriques à travers des spécifications formelles et des preuves assistées par ordinateur. Elle s'appuie d'une part sur la modélisation géométrique à base topologique des subdivisions d'espaces par des hypercartes combinatoires, et d'autre part sur le Calcul des constructions inductives et le système Coq. Par le volet topologie combinatoire, ce thème est étroitement lié à l'Axe 1 de l'équipe IGG.

Après tout un travail avec des spécifications algébriques, nous avons, depuis la fin des années 90, formalisé les hypercartes et leurs dérivés (cartes et cartes généralisées) et construit une bilbliothèque Coq sur ces structures. Des preuves formelles ont été produites pour de grands résultats de topologie combinatoire : théorème de classification des surfaces, théorème du genre, formule d'Euler-Poincaré, théorème de Jordan discret.

Durant le présent contrat quadriennal, notamment dans le projet ANR Galapagos (2008-2011), nous avons étudié plusieurs problèmes liés à l'algorithmique géométrique. Ainsi, nous avons proposé un algorithme fonctionnel de segmentation d'images 2D faisant un pattern-matching sur la structure inductive des cartes combinatoires décrivant les images. Nous en avons prouvé la correction en Coq et avons pu en dériver un programme impératif (en C) efficace, qui a été expérimenté sur des images couleur en vraie grandeur. (Travail de J.-F. Dufourd).

Nous avons travaillé sur les algorithmes de construction d'enveloppe convexe. Deux versions en ont été étudiées et prouvées correctes en Coq. La première, qui travaille par induction structurelle, repose sur des idées semblables à la segmentation évoquée précédemment. La seconde, qui repose sur une induction noethérienne, simule un algorithme traditionnel de construction incrémentale. Des programmes en ont été automatiquement extraits en Ocaml, et, de la seconde version a été dérivé un programme en C++, qui a été intégré à la plateforme CGoGn d'IGG. (Travail de thèse de C. Brun, encadré par J.-F. Dufourd et N. Magaud).

Un gros travail a été effectué sur la formalisation des subdivisions de surfaces, avec les opérations merge et split pour fusionner et éclater des cellules d'hypercartes. Il a été particularisé aux triangulations avec la définition de l'opération classique de swap d'arêtes. Ceci nous a conduit à la première formalisation et preuve assistée en Coq d'un algorithme de construction d'une triangulation de Delaunay. Celle-ci travaille par une suite de swaps jusqu'à ce que toutes les arêtes soient valides par rapport à un critère de cercle de Delaunay. (Travail de J.-F. Dufourd et Y. Bertot, directeur de l'équipe Marelle de l'INRIA-Sophia).

Spécification et résolution de contraintes

décomposition multi-groupes

Re-paramétrisation de systèmes

systèmes articulés

Utilisation de la géométrie

Formalisation et planification d'opérations percutanées

Ablation de tumeurs hépatique

Stimulation cérébrale profonde

...

Perspectives

Spécification, preuves d'algorithmes et implantation :

Le travail sur la formalisation des structures combinatoires topologiques sera consolidé et amplifié. La bibliothèque d'hypercartes sera révisée et étendue en dimension n pour décrire et manipuler des subdivisions d'espace nD. Des liens seront établis avec les algorithmes de calcul des groupes d'homologie des variétés de dimension n.

L'expérimentation en preuves d'algorithmes géométriques sera poursuivie. L'accent sera mis sur les algorithmes de triangulation de Delaunay et de Voronoï en dimension 3, qui sont toujours des challenges, notamment en présence de contraintes. La question des approximations numériques sera également abordée. Jusqu'ici, elle a été évacuée de nos travaux au profit de calculs exacts dans les réels. Cette position devra être révisée, en examinant différentes hypothèses de travail : calcul exacts sur des rationnels, calculs approchés par intervalles, géométrie discrète, etc.

Enfin, le raffinement de nos structures abstraites d'hypercartes en structures concrètes en mémoire, notamment avec des pointeurs, devra être étudié. Le passage de nos algorithmes abstraits en programmes impératifs concrets avec pointeurs sera étudié, avec la preuve de conservation de la correction. Un travail préliminaire sur les structures linéaires et cycliques a déjà permis d'obtenir des résultats prometteurs.