Stage de Luminy 2002
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.
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
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