Stage de Luminy 2002

Luc Albert et Jean Jacques Técourt : bases de Gröbner, cas dégénérés

La géométrie algébrique a considérablement évolué dans la seconde moitié du siècle dernier. En 1960, Buchberger découvre des algorithmes pour la manipulation des systèmes d'équations polynômiales ; dans les années 1970, Wu met au point des techniques de démonstration automatique de théorèmes de géométrie euclidienne ; enfin, ces dernières années, le développement des systèmes de calcul formel allié à la démocratisation des ordinateurs personnels permet à tout un chacun de tester ces techniques. Nous présentons les bases de Groebner et les liens entre variétés et ideaux en géométrie algébrique sur différents corps. On illustre à l'aide d'exemples les différentes méthodes, leurs possibilités et leurs limitations à l'aide des logiciels Maple et CoCoA. On insiste sur la détermination automatique des cas dégénérés, au sens de Kapur.

Denis Cazor : automatisation d'un "kholloscope"

Le texte de l'exposé et et le programme de colloscope sont disponibles ici (archive compressée, 591ko)

Laurent Cheno : développement sous Mac OS X

Nous commençons par une brève présentation de Objective-C, l'extension objet de C par la GNU-fondation, qui est le langage de choix dans la programmation sous MacOS X. On décrit la création de classes, de catégories et de protocoles, et on détaille les questions liées à l'allocation et la désallocation. Dans une deuxième partie, on met en oeuvre les outils développeur de MacOS X, pour montrer comment mettre sur pied une interface Cocoa, en créant une application simple, utilisant zones de saisie, boutons et zone de dessin.

Les transparents et programmes accompagnant cet exposé sont disponibles ici (archive compressée, 1.6Mo)

Gilles Dowek : Qu'est-ce qu'une démonstration constructive

Le but de cet exposé est de montrer, à partir d'un certain nombre d'exemples, que certaines démonstrations mathématiques sont constructives (c'est-à-dire qu'elles contiennent un algorithme) et d'autres non. On cherchera à montrer que les démonstrations non constructives peuvent être caractérisées par le fait que qu'elles utilisent l'une des règles de raisonnement, appelée le "tiers exclu", qui permet de démontrer la proposition (A ou non A) sans démontrer A ni (non A). On comparera plusieurs définitions du pgcd et plusieurs démonstrations du théorème de Bezout. On cherchera enfin à comparer plusieurs démonstrations du théorème des valeurs intermédiaires et à mettre en évidence leur rapport avec l'algorithme de recherche de zéros de fonctions par dichotomie.

Daniel Goffinet : factorisation d'automates

Je présente une bonne partie du contenu de "An introduction to Automata Theory " de M.W.Shields : on peut déterminer si un automate est ou non équivalent au produit cartésien de deux autres automates en étudiant l'ensemble des partitions de l'ensemble des états qui sont compatibles avec notre automate.

Détails en Postscript dans le fichier joint (archive compressée, 2Mo).

Yves Lemaire : fonctions pour MLgraph

Fichier mlg.zip (archive compressée, 154Ko)

Bruno Petazzoni : arbres de recherche optimaux et problèmes apparentés

L'exposé comporte trois parties indépendantes.

La première partie présente la notion de tri par renversement (sorting by reversal). Cette notion est illustrée par le casse-tête Top-Spin, puis par le problème de la pile de crêpes; celui-ci fournit l'occasion de parler du graphe de Cayley associé à une partie $S$ d'un groupe $G$. Cette partie se termine par une brève discussion du calcul du nombre minimal de renversements permettant de passer d'une permutation à une autre: en génétique moléculaire, cette quantité permet d'estimer la plus ou moins grande proximité de deux espèces.

La deuxième partie présente les arbres binaires de recherche optimaux; on montre que l'algorithme glouton ne s'applique pas, puis on expose la méthode de calcul d'un tel arbre par programmation dynamique. On voit ensuite le lien avec la recherche d'une triangulation optimale d'un polygone convexe. Le cas particulier de l'optimisation du calcul d'un produit matriciel conclut cette partie.

Enfin, la troisième partie présente deux programmes écrits en Maple, et fabriquant des feuilles d'exercices de mathématiques personnalisés.

...et si vous avez le temps, jetez un oeil sur http://www.bruno.maitresdumonde.com

Antoine Petit : Automates sur les mots infinis

Nous introduisons plusieurs modes d'acceptation de chemins infinis par un automate fini : Büchi, Muller et Rabin. Nous commençons par étudier les automates de Büchi et nous montrons que les automates déterministes reconnaissent une sous-classe stricte. Nous proposons une caractérisation des langages acceptés par des automates de Büchi déterministes. Nous étudions ensuite les automates déterministes de Muller et caractérisons ceux équivalents à des automates de Büchi. Enfin, nous énonçons le théorème de Mac Naughton affirmant que tout automate de Büchi est équivalent à un automate de Rabin et nous donnons les grandes lignes de la construction de Safra.

Référence: http://www.liafa.jussieu.fr/~jep/Resumes/InfiniteWords.html

Michel Quercia : réseaux et bases réduites

On introduit la notion de réseau (sous-groupe discret engendrant un espace vectoriel euclidien) et on présente les principaux problèmes algorithmiques liés aux réseaux : shortest vector, closest point. On définit alors les notions de base réduite d'un réseau au sens de Hermite et au sens de Lovascz et on montre que la connaissance d'une base réduite permet de résoudre les problèmes SV et CP en temps constant (compté en nombre d'opérations) lorsque la dimension du réseau est fixée (algorithme de Babaï). On présente ensuite deux algorithmes de calcul d'une base réduite : l'algorithme de Gauss qui fournit une base de Hermite pour un réseau bidimensionnel et l'algorithme LLL qui fournit une base de Lovascz pour un réseau de dimension quelconque. Enfin on présente deux applications du calcul d'une base réduite : la recherche d'approximations simultannées de plusieurs réels par des rationnels ayant même dénominateur, et la recherche de relations de dépendance linéaire à coefficients entiers entre nombres connus par des approximations arbitrairement précises.

Le texte complet de cet exposé et les programmes de démonstration l'accompagnant sont disponibles ici (archive compressée, 22Ko).

Christophe Raffalli : utilisation du prouveur PhoX à des fins pédagogiques

Je commencerai par une présentation de l'assistant de preuve PhoX, qui ne nécessite aucun préalable, puisque le prouveur est utilisable et utilisé par des étudiants de DEUG première année. Ensuite, je présenterai les systèmes logiques qui sont à la base de ce prouveur et de la plupart des prouveurs: la déduction naturelle et la logique d'ordre supérieure (HOL). J'expliquerai aussi comment on implante de tels systèmes.

Pour plus de renseignements sur le système: http://www.lama.univ-savoie.fr/~raffalli/phox.html