Terminaison en temps moyen fini de systèmes de règles probabilistes

Je tiens remercier en premier lieu mon encadrant Olivier Bournez qui en plus de m'avoir propos ce sujet de thse, s'est toujours montr disponible pour me venir en aide et m'apporter ses conseils prcieux.Je remercie galement mon directeur de thse Claude Kirchner pour sa patience, ses grandes qualits pdagogiques ainsi que sa gentillesse.Je remercie chaleureusement les personnes qui ont accept d'tre membres de mon jury, en particulier Catuscia Palamidessi et Laurent Fribourg qui ont accept d'tre mes rapporteurs.Je ne remercierais jamais assez mes amis et collgues, Emmanuel, Germain, Antoine qui ont facilit mon arrive Nancy et qui m'ont appuy moralement et parfois matriellement durant toute la dure de ma thse.Je remercie galement tous le membres de l'quipe PROTHEO avec qui j'ai pass des moments forts agrables dans le cadre de la recherche et parfois en dehors.Merci mes parents ainsi et mes deux frres Sylvain et Ghislain pour leur appui moral.Je remercie aussi Grme pour m'avoir transmis la passion du cyclisme la montagne.Et merci encore tous mes amis que je n'ai pas cit ici, mais qui mriteraient de l'tre.i Pour donner une intuition de ce que nous voulons faire, considrons l'exemple reprsent par la figure 1.On va exprimer pour chaque mthode une manire d'exprimer la transition probabiliste reprsente par le graphique.Appelons le terme de gauche l 1 , puis les termes de droite, numrots de haut en bas, r 1 , r 2 et r 3 .Dans le premier cas de figure, on dfinit un systme de rcriture avec trois rglesDans le second cas, on reprsente cette transition grce ce que l'on dfinira Plan du documentCe document se dcompose en les trois parties suivantes, Rappels sur quelques notions de baseDans cette partie nous dcrirons de manire succincte les outils et les notions sur lesquelles reposent les travaux prsents dans ce document.Nous commencerons par introduire le formalisme de la rcriture en se basant sur la prsentation de [BN98], puis nous aborderons l'tude de la terminaison des systmes de rcriture.* x * y 2 y 1 y 2 Terminante si il n'existe pas de drivation infinie a 0 a 1 Normalisante si tout lment a une forme normale Convergente si est terminante et confluente 1.2 Le principe de l'induction bien fonde Dans cette partie on dcrit un principe fondamental, l'induction bien fonde, parfois appel rcurence Noethrienne.On va voir que cette proprit caractrise les relation terminantes.Le principe d'induction bien fonde (WFI pour Well Founded Induction) est en fait une gnralisation de l'induction sur (N, >) pour au cas des systmes de rduction terminants (A, ).Soit P une proprit sur A, nonons la proprit d'induction bien fonde l'aide d'une rgle d'infrence : x A.(y A. x + y P (y)) P (x) x A. P (x) Cette notion d'induction bien fonde est importante cause du thorme suivant : Thorme 1.2.1.La relation termine si et seulement si vrifie le principe d'induction bien fonde.La preuve de ce thorme se trouvent dans [BN98].Ce rsultat permet d'tudier des critres permettant de certifier la terminaison de certaines drivations.Parmi ceux-ci, on peut citer : Dfinition 1.2.1.Une relation est dite,

Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.