Mardi 06 Novembre 2007, 14h, Salle S16
-
Orateur/Speaker :
Yves Bertot, Inria, Sophia
-
Titre/Title :
Formalisation d'algorithmes de géométrie: le cas des enveloppes convexes,
CC-systèmes et contournement des problèmes de dégénérescence
-
Résumé/Abstract :
Nous avons étudié dans quelle mesure un outil de preuve en logique
d'ordre supérieure
pouvait être utilisé pour mettre au point un algorithme de géométrie, en
nous concentrant
sur le système de preuve Coq et les algorithmes d'enveloppe convexe en
dimension 2.
Pour séparer les problèmes logiques des problèmes numériques, nous avons
suivi l'approche
proposée par Knuth dans "Axioms and Hulls" pour décrire les propriétés
du prédicat d'orientation
et nous avons décrit plusieurs algorithmes dans ce cadre.
Ensuite, nous avons abordé le problème de la dégénerescence: les axiomes
de Knuth supposent
que trois points ne sont jamais alignés. Plusieurs approches ont été
étudiées:
* ajouter les cas de figures possibles correspondant aux alignements
dans les axiomes, on
passe d'un système à 5 axiomes à un système à 19 axiomes
* affiner le prédicat d'orientation par une méthode de permutation, de
façon à donner aux points
alignés une orientation qui reste cohérente avec les axiomes de Knuth.
Du point de vue de la formalisation d'algorithmes, ces deux solutions
présente l'inconvénient de
déplacer la cible de formalisation : avec de nouveaux prédicats
d'orientation, on définit de nouvelles
notions d'enveloppe convexe. Un dernier point que nous avons étudié est
la description d'une
spécification de la notion d'enveloppe convexe qui soit indépendante de
la notion d'orientation.
Si le temps le permet, tous ces points seront abordés durant l'exposé.