these
114 pages
Français
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
114 pages
Français
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Description

´UNIVERSITE PARIS. DIDEROT (Paris 7)´ECOLE DOCTORALE : Sciences math´ematiques de Paris CentreDOCTORATInformatiqueˆBENOIT RAZETMACHINESD’EILENBERGEFFECTIVESTh`ese dirig´ee par G´erard HUETSoutenue le 26 novembre 2009JURYMM. Jean-Marc Champarnaud RapporteurJean-Christophe Filliˆatre RapporteurChristine Paulin-Mohring RappG´erard Berry ExaminateurRoberto Di Cosmo ExamiAarne Ranta ExaminateurG´erard Huet Directeur de th`eseTable des mati`eresIntroduction 7I Langages R´eguliers, Automates Finis et Axiomatisations 131 Th´eories des langages r´eguliers et des automates finis . . . . . . . . . . . . . . . . 131.1 Semigroupe, mono¨ıde libre, mot, langage. . . . . . . . . . . . . . . . . . . 131.2 Expressions r´eguli`eres et langages r´eguliers . . . . . . . . . . . . . . . . . 141.3 Automates finis et langages reconnaissables . . . . . . . . . . . . . . . . . 151.4 Th´eor`eme de Kleene . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162 Quelques axiomatisations des alg`ebres de Kleene . . . . . . . . . . . . . . . . . . 172.1 Axiomatisation des alg`ebres de Kleene par Kozen . . . . . . . . . . . . . . 182.2 des alg`ebres d’actions de Pratt . . . . . . . . . . . . . . . 222.3 Exemples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 252.4 Compl´ements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 283 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30II ...

Sujets

Informations

Publié par
Nombre de lectures 70
Langue Français

Extrait

´UNIVERSITE PARIS. DIDEROT (Paris 7)
´ECOLE DOCTORALE : Sciences math´ematiques de Paris Centre
DOCTORAT
Informatique
ˆBENOIT RAZET
MACHINESD’EILENBERGEFFECTIVES
Th`ese dirig´ee par G´erard HUET
Soutenue le 26 novembre 2009
JURY
MM. Jean-Marc Champarnaud Rapporteur
Jean-Christophe Filliˆatre Rapporteur
Christine Paulin-Mohring Rapp
G´erard Berry Examinateur
Roberto Di Cosmo Exami
Aarne Ranta Examinateur
G´erard Huet Directeur de th`eseTable des mati`eres
Introduction 7
I Langages R´eguliers, Automates Finis et Axiomatisations 13
1 Th´eories des langages r´eguliers et des automates finis . . . . . . . . . . . . . . . . 13
1.1 Semigroupe, mono¨ıde libre, mot, langage. . . . . . . . . . . . . . . . . . . 13
1.2 Expressions r´eguli`eres et langages r´eguliers . . . . . . . . . . . . . . . . . 14
1.3 Automates finis et langages reconnaissables . . . . . . . . . . . . . . . . . 15
1.4 Th´eor`eme de Kleene . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2 Quelques axiomatisations des alg`ebres de Kleene . . . . . . . . . . . . . . . . . . 17
2.1 Axiomatisation des alg`ebres de Kleene par Kozen . . . . . . . . . . . . . . 18
2.2 des alg`ebres d’actions de Pratt . . . . . . . . . . . . . . . 22
2.3 Exemples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.4 Compl´ements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
II Simulation des Machines d’Eilenberg 33
1 Machines relationnelles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2 Programmation fonctionnelle en ML . . . . . . . . . . . . . . . . . . . . . . . . . 35
3 Relations calculables et flux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4 Machines d’Eilenberg . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.1 D´efinition du noyau . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.2 Modularit´e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.3 Interfaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.4 G´en´eralit´e du mod`ele . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
5 Machines d’Eilenberg finies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
5.1 D´efinitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
5.2 Automates finis et transducteurs . . . . . . . . . . . . . . . . . . . . . . . 47
5.3 Un moteur r´eactif de simulation . . . . . . . . . . . . . . . . . . . . . . . 48
5.4 Formalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
5.5 F du moteur r´eactif en Coq . . . . . . . . . . . . . . . . . . . 54
5.6 Moteur r´eactif optimis´e . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
5.7 Exemple : un automate a` pile pour la grammaire du λ-calcul . . . . . . . 57
5.8 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
6 Machines d’Eilenberg effectives dans un cadre g´en´eral de calculabilit´e. . . . . . . 60
6.1 Moteur r´eactif avec strat´egies . . . . . . . . . . . . . . . . . . . . . . . . . 60
6.2 semi-r´eactif avec strat´egies . . . . . . . . . . . . . . . . . . . . . . 66
7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69`4 TABLE DES MATIERES
IIIAlgorithmes Fonctionnels de Synth`ese d’Automates 71
1 Structures primitives et algorithme de Thompson . . . . . . . . . . . . . . . . . . 71
1.1 Expressions r´eguli`eres . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
1.2 Automates finis non-d´eterministes . . . . . . . . . . . . . . . . . . . . . . 72
1.3 Algorithme de Thompson . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
2 R´eduire les expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
2.1 Expressions r´eguli`eres d´ecor´ees . . . . . . . . . . . . . . . . . . . . . . . . 74
2.2 Associativit´e de la concat´enation . . . . . . . . . . . . . . . . . . . . . . . 76
2.3 -r´eduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
2.4 Forme normale d’´etoile . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
2.5 Expression r´eguli`ere normalis´ee . . . . . . . . . . . . . . . . . . . . . . . . 80
3 D´eriver les expressions r´eguli`eres . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
3.1 D´eriv´ees de Brzozowski et m´ethode g´en´erale . . . . . . . . . . . . . . . . . 80
3.2 D´eriv´ees d’expressions r´eguli`eres lin´eaires . . . . . . . . . . . . . . . . . . 82
3.3 D´eriv´ees partielles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
3.4 D´eriv´ees canoniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
4 Synth`ese de l’automate de positions . . . . . . . . . . . . . . . . . . . . . . . . . 88
5 Synth`ese de l de continuations . . . . . . . . . . . . . . . . . . . . . . . 90
6 Synth`ese de l’automate d’´equations . . . . . . . . . . . . . . . . . . . . . . . . . . 95
7 Performances des algorithmes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
7.1 Temps de calcul des algorithmes . . . . . . . . . . . . . . . . . . . . . . . 99
7.2 Nombre de transitions-´etats de l’automate . . . . . . . . . . . . . . . . . . 100
7.3 Nombre d’´etats de l’automate . . . . . . . . . . . . . . . . . . . . . . . . . 100
7.4 Valider l’impl´ementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
8 Remarques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
9 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
Conclusion 105R´esum´e
La th´eorie des automates est apparue pour r´esoudre des probl`emes aussi bien pratiques que
th´eoriques, et ceci d`es le d´ebut de l’informatique. D´esormais, les automates font partie des no-
tions fondamentales de l’informatique, et se retrouvent dans la plupart des logiciels. En 1974,
Samuel Eilenberg proposa un mod`ele de calcul qui unifie la plupart des automates (transduc-
teurs, automates a` pile et machines de Turing) et qui a une propri´et´e de modularit´e int´eressante
auvud’applicationsreposantsurdiff´erentescouchesd’automates;commecelapeutˆetrelecasen
linguistique computationnelle. Nous proposons d’´etudier les techniques permettant d’avoir des
machines d’Eilenberg effectives. Cette ´etude commence par la mod´elisation de relations calcu-
lables`abasedeflux,puiscontinueavecl’´etudedelasimulationdesmachinesd’Eilenbergd´efinies
avec ces relations. Le simulateur est un programme fonctionnel ´enum´erant progressivement les
solutions, en explorant un espace de recherche selon diff´erentes strat´egies. Nous introduisons,
en particulier, la notion de machine d’Eilenberg finie pour laquelle nous fournissons une preuve
formelledecorrectiondelasimulation.Lesrelationssontunepremi`erecomposantedesmachines
d’Eilenberg,ladeuxi`emecomposante´etantsoncontrˆole,quiestd´efiniparunautomatefini.Dans
ce contexte, on peut utiliser une expression r´eguli`ere comme syntaxe pour d´ecrire la composante
decontrˆoled’unemachined’Eilenberg.R´ecemment,unensembledetravauxexploitantlanotion
de d´eriv´ees de Brzozowski, a ´et´e la source d’algorithmes efficaces de synth`ese d’automates non-
d´eterministes a` partir d’expressions r´eguli`eres. Nous faisons l’´etat de l’art de ces algorithmes,
tout en donnant une impl´ementation efficace en OCaml permettant de les comparer les uns aux
autres.Introduction
Lespremiersordinateurssontapparusauvingti`emesi`ecle.Cesontdesmachinesd’unegrande
complexit´e et pour lesquelles il est utile d’avoir des mod`eles plus simples et plus intuitifs qui
rendent compte de leur capacit´e. Parmi les pionniers de l’informatique on peut mentionner Alan
Turing qui a propos´e un mod`ele math´ematique assez simple rendant compte de ces machines
complexes, on parle d´esormais des machines de Turing et c’est le mod`ele de r´ef´erence. Voyons
les diff´erentes notions qui sont mises en jeu dans une machine de Turing. Une machine de Tu-
ring est une machine a` calculer, elle prend donc une donn´ee en entr´ee et produit un r´esultat
de sortie. Elle se compose d’un programme et d’une m´emoire. Le programme sert a` d´ecrire les
s´equences d’actions qui peuvent op´erer sur la m´emoire. Le protocole pour ex´ecuter un calcul est
le suivant : il faut pr´eparer la m´emoire de mani`ere `a ce qu’elle contienne la donn´ee d’entr´ee,
puis on lance l’ex´ecution de la machine qui modifie la m´emoire, et enfin si la machine s’arrˆete
alors on r´ecup`ere en m´emoire le r´esultat de sortie. La m´emoire est mod´elis´ee par un ruban (de
longueur non born´ee) sur lequel est ´ecrit une suite de valeurs binaires (0 ou 1) qu’on appelle
des bits. Toute i

  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents