THEME 1 OPERATION3

Opération 3 : Spécifications et preuves en géométrie

Responsable : Jean-François Dufourd, PR CE2

Participants : Nicolas Magaud, MC, nommé au 1-09-2005, Julien Narboux, MC, nommé au 1-09-2007

Doctorants : Christophe Brun.

Non permanents : Christophe Dehlinger (Docteur, ATER 2003-2004), Sabine Carouge (DEA 2004), Aurélie Vielcastel (Allocataire-monitrice, 2004-2005, abandon), Christophe Brun (M2R 2007)

Présentation générale

Dans l'opération 3, nous visons la définition formelle d'univers d'objets géométriques et d'opérations, la preuve de propriétés de ces objets et la dérivation d'algorithmes géométriques certifiés corrects. Nous envisageons de plus en plus ces activités comme devant être assistées par ordinateur pour en assurer la faisabilité pratique, et en garantir la rigueur et la qualité. Les retombées sont en modélisation géométrique, en algorithmique géométrique, en géométrie pure et en enseignement des mathématiques. Nous avons voulu séparer de ces activités l'opération 2 Résolution de contraintes géométriques, qui utilise des techniques spécifiques, pour mieux faire ressortir les deux thématiques. Cependant, elles gardent des liens très forts, notamment dans la manière symbolique d'aborder les problèmes, et des projets communs se dessineront à nouveau.

Historique

On trouve l'origine de ces préoccupations dans les années 90-97 avec la promotion des spécifications algébriques et de la réécriture dans les modèles topologiques et géométriques de cartes combinatoires et leurs extensions. Ces travaux ont permis de développer de manière rationnelle plusieurs logiciels, comme un modeleur interactif volumique à base topologique, appelé Topofil (thèse de Yves Bertrand), un prototype fonctionnel en Ocaml pour définir et manipuler des courbes, surfaces et volumes (thèse de Laurent Fuchs), et une bibliothèque d'opérations ensemblistes, ou "booléennes", sur des subdivisions du plan et de l'espace, avec comme opération de base le raffinement de subdivisions (thèse de David Cazier, 1997).

Plus tard, dans les années 98-04, nous avons voulu que ces spécifications servent d'axiomatique pour des preuves de propriétés d'objets topologiques. Nous souhaitions également que ces preuves soient, sinon automatiques, au moins assistées et vérifiées par ordinateur. Les logiciels de spécification algébriques tels que OBJ3 (ou Maude, CaféOBJ, Larch) que nous utilisions n'offrant guère d'outils d'assistance, nous avons cherché des systèmes mieux adaptés. Nous nous sommes alors tout naturellement tournés vers le système Coq de l'INRIA. Il nous a permis de reprendre et adapter nos anciennes spécifications et d'aller bien au-delà en direction des preuves.

Nous avons d'abord formalisé de manière constructive en Coq les cartes combinatoires comme un type inductif avec invariant, puis donné et démontré une condition suffisante de préservation de la planarité lors d'une construction. Nous avons enfin énoncé et prouvé une forme simple du théorème de Jordan discret (thèse de François Puitg, 2000).

Contributions récentes

Classification des surfaces combinatoires

Voulant montrer le caractère effectif de nos propositions et leur généralité, nous nous sommes attaqués aux surfaces combinatoires et à un grand théorème de topologie (thèse de Christophe Dehlinger, 2003). Il s'agit du théorème de classification des surfaces ouvertes par des triplets d'entiers caractéristiques (p,q,r), où p, q et r dénombrent respectivement les anneaux (ou oreilles droites), les torsions (ou bandes de Moebius, ou oreilles torses) et les tunnels (ou ponts). Dans les preuves classiques (Griffiths, Fomenko), la preuve est décomposée en deux parties. La première consiste à simplifier le maillage en un plan de construction normalisé de mêmes caractéristiques : c'est le sous-théorème de normalisation. La seconde consiste à échanger, quand q >= 3, 2 oreilles torses contre 1 pont : c'est le sous-théorème d'échange (trading theorem). Ainsi, le théorème de classification en entier affirme que toute surface ouverte peut être rangée dans une seule classe topologique correspondant à un triplet (p,q,r), avec q <= 2, où les surfaces sont homéomorphes. Ce travail a été l'occasion de fournir une spécification inductive des cartes généralisées. Le sous-théorème d'échange a été prouvé à l'aide de Coq par une technique d'induction structurelle sur les cartes généralisées. Ce travail a été publié dans deux papiers joints de la revue Theoretical Computer Science [2-DD04, 2-DD04]. Le sous-théorème de normalisation l'a ensuite été par une induction noethérienne faisant intervenir une distance assez complexe entre deux cartes.

Théorème du genre et formule d'Euler

Nous nous sommes ensuite attachés à simplifier et généraliser ces spécifications en considérant des hypercartes combinatoires (au sens de Cori). Nous avons développé à partir de zéro (from scratch) une bibliothèque de spécification sur les hypercartes, en partant d'un type inductif de cartes libres, que nous avons contraint progressivement par des invariants jusqu'à obtenir un type d'hypercartes satisfaisant sur lequel nous avons défini des opérations et prouvé des propriétés intéressantes pour la modélisation géométrique. Ainsi, nous défini avons pu énoncer et prouver le théorème du genre affirmant que le genre g = c – K/2 d'une hypercarte est toujours en entier naturel, où c est le nombre de composantes connexes, et K la caractéristique d'Euler, définie par K = v – e + f, où v, e et f dénombrent les sommets, arêtes et faces de l'hypercarte. Un corollaire est alors la formule d'Euler-Poincaré v – e + f = 2c pour les hypercartes planaires, c'est-à-dire de genre nul. La correspondance hypercartes-surfaces closes orientables permet de transposer ces résultats aux surfaces elles-mêmes. Ces résultats ont pu être prouvés en Coq essentiellement par une technique d'induction structurelle (Jean-François Dufourd, 2006). Ce travail, qui est en cours de publication, a été partiellement présenté à la conférence ACM SAC'07 [4-DUF07]. C'est, semble-t-il, la première fois qu'une preuve de la formule d'Euler est formalisée, si l'on se réfère à la liste des théorèmes classiques (top 100) maintenue par Freek Weidijk (http://www.cs.ru.nl/~freek/100/).

Hypercartes et critère de planarité

Récemment, ce travail a été repris de manière à simplifier et élargir nos propositions. La révision porte notamment sur une définition allégée du type des hypercartes et une définition générique grâce à la notion de signature et de module paramétré de Coq, des parcours d'orbites (sommets, arêtes, faces) avec détermination d'une période. Il en est résulté la possibilité de prouver la symétrie du parcours d'orbites, ce qui n'avait jamais pu être obtenu auparavant, ainsi qu'un critère de planarité constructif complet, c'est-à-dire une condition nécessaire et suffisante de maintien de la planarité lors de la construction d'une hypercarte. Ces résultats (Jean-François Dufourd, 2006) n’ont pas encore été publiés. Ils seront à comparer avec le travail de formalisation des hypercartes effectué par G. Gonthier et al. pour leur formidable preuve en Coq du théorème des 4 couleurs mise en exergue au moment de la création du laboratoire commun INRIA-Microsoft (Gonthier et al., 2005). Nos propositions sont différentes, et nous avons la faiblesse de penser qu'elles sont plus simples.

Hypercartes et certification de la segmentation d'images

Par ailleurs, nous avons voulu faire une première incursion dans le domaine de la conception et de la certification d'algorithmes. Nous avons choisi comme benchmark un classique de l'imagerie : la segmentation d'images colorées 2D par fusion de cellules. Notre subdivision en cellules (pixels au départ) est modélisée par une hypercarte (ou une carte comme cas particulier) colorée. Elle est segmentée en deux phases par un algorithme fonctionnel décrit en Coq par une récursion structurelle sur l'hypercarte. La correction totale, terminaison et correction partielle, par rapport à certains critères a pu être prouvée. Nous avons ensuite dérivé un programme impératif optimal faisant la segmentation sur une hypercarte représentée comme une liste chaînée de brins, comme cela est la règle dans les modeleurs que nous avions conçus. Ce travail était à l'origine le sujet de thèse d'Aurélie Vielcastel. Il a été mené par Jean-François Dufourd après l'abandon de celle-ci pour convenances personnelles. Il a été récemment présenté aux Journées de l'AFIG 06 (4-DUF06), aux JFLA 07 [5-DUF07], et publié dans la revue Pattern Recognition [2-DUF07].

Structures de données et algorithmique géométrique

Nous avons également commencé à explorer un premier problème d'algorithmique géométrique où interviennent des notions de cartes combinatoires et de plongement. Il s'agit de la construction de l'enveloppe convexe de points du plan. Selon le même principe que ci-dessus, nous avons conçu un algorithme fonctionnel en Coq travaillant par induction structurelle sur nos contours et s'inspirant de l'algorithme incrémental classique. Très rapidement, un prototype en OCaml a pu en être extrait et testé à l'aide d'une interface graphique ad hoc. La preuve de correction de cet algorithme, basé sur une classification fine des brins et de leurs propriétés, est en bonne voie (Christophe Brun, Nicolas Magaud, Jean-François Dufourd). Ce travail a été présenté en juin 2007 aux Journées de Géométrie et Informatique (Nice-Sophia, ERCIM, juin 2007) du nouveau GDR IM. Parallèlement, nous travaillons sur une représentation alternative des cartes en Coq. Une structure chaînée, contenant pour chaque brin ses successeurs et prédécesseurs aux deux dimensions ainsi que son plongement, présente en effet l'avantage d'être proche des implantations usuelles des cartes dans les langages impératifs. Nous avons repris la théorie des cartes initialement développée dans Coq et travaillons à l'adaptation des définitions et des démonstrations à la nouvelle structure de données considérée. Ce travail, commencé par Christophe Brun et Nicolas Magaud au cours de l'été 2006, se poursuit actuellement.