Sujet de stage informatique niveau maîtrise:
Factorisation de polynômes à coefficients dans un corps fini.
Stage attribué:
François Maurel (Ens)
Sujet:
Le but du stage est de programmer l'algorithme de Cantor-Zassenhaus dans le
système Coq, et de prouver sa correction. Cet algorithme, simple et efficace,
permet de factoriser un polynôme à coefficients dans un corps fini. Il a
trois étapes indépendantes:
L'étape 3 est probabiliste, et peut échouer indéfiniment, mais
l'algorithme a la propriété de terminer avec une probabilité 1.
Les trois étapes utilisent comme opération de base le calcul du pgcd de
polynômes.
La preuve consiste à démontrer que le résultat de
l'algorithme, quand il existe, est bien la factorisation du polynômes de
départ en facteurs irréductibles; elle utilise des théorèmes élémentaires sur
les corps finis.
Ce stage commencera par un apprentissage de Coq, qui est un assistant à la
preuve mathématique, dans lequel on peut à la fois écrire des algorithmes
(dans un style fonctionnele proche de Caml), et prouver des propriétés
logiques.
Les résultats élémentaires de la théorie des corps finis pourront dans un
premier temps etre posés comme axiomes, de manière à se concentrer sur la
preuve de l'algorithme lui-meme.
Ce stage s'inscrit dans un domaine de recherche récent en plein
développement: la réalisation d'implantations certifiées d'algorithmes de
calcul formel. Plusieurs expériences ont déjà été menées dans le projet
CROAP (algorithmes de Karatsuba, de Buchberger, d'Euclide) qui ont montré
l'efficacité des implantations obtenues (bien meilleures que les systèmes de
calcul formel classiques).
Si le temps le permet, on pourra compléter ce travail par des tests
comparatifs avec d'autres implémentations, la preuve des théorèmes qu'on aura
posés comme axiomes, ou la preuve de complexité de cet algorithme.
Bibliographie:
P. Flajolet, X. Gourdon, D. Panario, The complete analysis of a polynomial factorization algorithm over finite
fields, rapport de recherche INRIA n. 3370, mars 98.
G. Huet, G. Kahn, C. Paulin-Mohring, The
Coq Proof Assistant : A Tutorial : Version 6.1, Rapport Technique INRIA
0204, août 1997
Encadrement:
Loic Pottier,
Laurent Théry
Contact:
Tel: 04 92 38 78 19 ou 04 92 38 78 16
E-mail : Loic.Pottier@sophia.inria.fr
, Laurent.Thery@sophia.inria.fr
Laboratoire d'accueil:
Projet CROAP, INRIA Sophia Antipolis
Laurent Théry
Retour à
la page du projet
Retour aux
autres stages proposés dans le projet