Théorie des Automates Finis en Coq
Une preuve constructive du théorème de Kleene
Résumé :
Nous décrivons dans cet article un développement dans le système Coq
d'une partie de la Théorie des Automates Finis. Le principal
résultat est le théorème de Kleene, qui établit que les expressions
rationnelles et les automates finis définissent la même classe de langages.
A partir d'une preuve constructive de ce résultat, on obtient automatiquement
un programme fonctionnel qui compile une expression rationnelle en un
automate fini, ce qui constitue la partie critique de l'implémentation
des programmes du style grep. Ce programme fonctionnel est obtenu
par la méthode automatique d'extraction qui supprime les parties
logiques de la preuve pour ne conserver que son contenu informatif.
Avec en tête l'idée du programme ML que l'on aurait écrit directement,
on écrit la spécification et on mène les preuves de manière à
obtenir le programme voulu, qui est par conséquent efficace.
Un rapport de recherche est disponible.
Le récupérer.
BibTeX.
Sources du développement
Le développement en Coq sera bientôt disponible à partir de cette page.
Contenu calculatoire de la preuve
De la preuve constructive de ce théorème, on obtient automatiquement
un programme Caml certifié (c'est-à-dire réalisant la spécification).
Pour plus de détails sur le procédé d'extraction dans le système Coq,
vous pouvez consulter la documentation
(disponible en FTP avec le système) : Execution of extracted programs in Caml and Gofer.
Voici le programme que l'on obtient :
Le programme Caml extrait de la preuve
Test du programme extrait
Pour tester le programme extrait, on commence par définir
quelques pretty-printers pour certains types, afin de rendre le
résultat plus lisible (fichier test.ml).
Voici le résultat obtenu pour les expressions rationnelles
suivantes :
Jean-Christophe Filliâtre
(formatté avec yamlpp).