Christophe Raffalli's home page

Thèmes de recherche

Géometrie

J'ai aussi commencé à travailler un peu en géométrie algébrique:

Dans [Raf22] nous avons trouvé avec Frédéric Mangolte la preuve d'un petit lemme amusant dont il avait besoin pour clore la preuve d'un de ses théorèmes: trouver une condition suffisante pour qu'il existe toujours un hyper-plan s'appuyant sur n ensembles convexe de $ℝ^{n}$ .

J'ai aussi réalisé GlSurf, un logiciel permettant de trianguler, visualiser et animer des surfaces implicites. Ce travail (utilisant un algorithme du type "marching cubes" nouveau) est relaté dans [Raf03a].

En ce moment, je prolonge ce travail en un algorithme exacte de résolution des systèmes algébriques réels, si le système est lisse (sans point critique). L'algorithme est implémenté et donne déjà des résultats intéressants dans certains cas. Dans [Raf23], on trouvera une preuve pour la codimension 1 et une conjecture pour le cas général.

Systèmes de type pour les langages de programmation

Dans [Raf99a] et [Raf98b] J'étudie le système F-eta (une extension du système F de Girard), qui est indécidable mais qui néanmoins peut être utilisé pour implanter un vrai langage de programmation. Il y a deux approches possibles:

Dans [Raf98b], j'utilise un algorithme incomplet qui termine toujours et ne "backtrack" jamais. Cela permet d'afficher des messages d'erreurs clairs et l'on peut toujours ajouter assez d'information de type pour que le typage d'un programme correct puisse être vérifé.
Dans [Raf99a] Je décrit un algorithme complet et optimisé. Cette algorithme marche bien (et vite) pour de petits programmes polymorphes. Mais, pour des programmes plus longs, il est trop lent et en plus comme l'algorithme "backtrack", il semble difficile de fabriquer des messages d'erreurs utiles. Il faudrait un debugger interactif de typage.

Mes recherches portent essentiellement sur des applications de la théorie de la démonstration. Elles se décomposent en quatre sous-thèmes:

Extraction de programmes à partir de preuves

L'isomorphisme de Curry-Howard permet d'extraire des programmes à partir de preuves classiques. Toutefois, étant donné un programme, il n'est pas toujours facile de trouver une preuve dont on peut l'extraire. Dans [Raf03b] et [Raf02b], j'introduis Système ST, un système complet pour la programmation purement fonctionnel (le lambda-calcul pur) : tout programme peut être extrait d'une preuve. La thèse de Frédéric Ruyer que je dirige en ce moment à pour objectif d'explorer les applications pratiques de Système ST.

Dans le même cadre, j'étudie aussi le contenu algorithmique des preuves classiques (utilisant le raisonnement par l'absurde). Il est maintenant clair que la logique classique correspond aux opérateurs de contrôle tels que le Call-CC de Felleisen. Toutefois, toute preuve classique ne donne pas un vrai programme (par exemple les preuves d'existence d'objets non calculables comme le plus petit entier dans un ensemble d'entiers). De plus, même lorsqu'une preuve classique donne un algorithme, on ne comprend pas toujours comment il marche. Dans [Raf02c], je montre comment d'une preuve de " $\forall x, \exists y, S (x, y)$ " on peut extraire un programme calculant $y$ à partir de $x$ si $S$ est décidable. J'explique de plus comment marche le programme : en bref, c'est une interaction entre la preuve de l'énoncé précédent et la preuve de décidabilité de $S$ . cette interaction teste une succession de valeurs possibles pour $y$ en finissant par s'arrêter sur un résultat correct.

Contenu algorithmique des preuves mathématiques

On peut aussi étudier la relation dans l'autre sens: quels programmes correspondent à une preuve mathématique donnée. Ou bien, quelles propriétés partagent tous les programmes extraits de preuves d'un même théorème.

Dans [Raf98a], Je donne une généralisation du théorème de Krivine sur les opérateurs de mises en mémoire (pas seulement pour les types "pour-tout" positif. Dans cet article je donne le contenu algorithmique de tous les programmes extraits d'une preuve d'un théorème de la forme $D^{*} \to \neg \neg D$ où $D^{*}$ est la traduction de Gödel de $D$ .

Dans [Raf98c], je démontre que toutes les preuves du théorème de complétude pour la logique minimale traduise une représentation des lambda-termes utilisant la syntaxe d'ordre supérieur en une représentation d'un terme de même type, utilisant des indices de Debruijn. De plus, je démontre qu'il existe une preuve ne changeant pas le terme. Ceci semble impossible (ce n'est pas démontré) pour la logique classique (traité par Krivine) ou pour la logique intuitioniste complète (avec disjonction ou existentiel). Cela donne un argument concret pour dire qu'une sémantique est triviale quand le théorème de complétude correspond à un calcul trivial

Implementation d'un assistant de preuve

Depuis ma thèse, je travaille sur PhoX. Il s'agit d'un logiciel permettant de réaliser des preuves mathématiques vérifiées par un ordinateur. L'objectif est de rendre cette réalisation la plus simple possible. La version actuelle a été utilisée (par René David et moi) plusieurs années avec des étudiant de DEUG et licence de math, de DEA de logique, de maîtrise d'informatique (pour prouver des programmes). Nous avons pu constater que le logiciel est de plus en plus facile à prendre en main (nous progressons). Ces expériences sont décrites dans [Raf02a] et [Raf01c]