Algorithmes certifiés de factorisation de polynômes

Sujet:

Le groupe CROAP s'intéresse au développement d'une librairie de calcul formel certifiée et efficace. La méthode utilisée consiste à développer l'algorithme en même temps que sa preuve de correction. Pour cela on utilise un assistant de preuve Coq (ref [2]) qui nous permet de définir les structures mathématiques usuelles (groupes, anneaux, polynômes) pour ensuite pouvoir raisonner et calculer avec. Les algorithmes définis à l'interieur de l'assistant de preuve Coq peuvent ensuite être compilés efficacement grâce au mécanisme de l'extraction.

Le travail de ce stage s'intègre dans cet effort en s'attaquant aux algorithmes de factorisation des polynômes. Le candidat devra développer à l'intérieur de Coq assez de mathématique pour pouvoir exprimer les algorithmes de factorisation que l'on peut trouver par exemple dans [1]. Tous ces algorithmes utilisent une représentation sous forme de facteurs des polynomes. Définir cette représentation et prouver un ensemble de propriétés (comme l'unicité) sur cette représentation constituront donc la première étape du stage. Dans une deuxième phase et si le temps le permet, on s'interessera à un algorithme particulier de factorisation celui de Cantor-Zassenhaus.