Etude de la stratégie de réécriture de termes k-bornée / Marc Sylvestre ; sous la direction de Irène Durand et de Géraud Senizergues

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Planification -- Informatique

Systèmes de réécriture (informatique)

Durand, Irène (1961-....) (Directeur de thèse / thesis advisor)

Senizergues, Géraud (1957-....) (Directeur de thèse / thesis advisor)

Retoré, Christian (1964-....) (Président du jury de soutenance / praeses)

Lugiez, Denis (19..-.... ; auteur en informatique) (Rapporteur de la thèse / thesis reporter)

Genet, Thomas (19..-....) (Rapporteur de la thèse / thesis reporter)

Kirchner, Hélène (1952-.... ; informaticienne) (Membre du jury / opponent)

Sakarovitch, Jacques (1947-....) (Membre du jury / opponent)

Université de Bordeaux (2014-....) (Organisme de soutenance / degree-grantor)

École doctorale Mathématiques et informatique (Talence, Gironde ; 1991-....) (Ecole doctorale associée à la thèse / doctoral school)

Université Bordeaux-I (1971-2013) (Autre partenaire associé à la thèse / thesis associated third party)

Laboratoire bordelais de recherche en informatique (Laboratoire associé à la thèse / thesis associated laboratory)

Résumé / Abstract : Nous introduisons la stratégie de réécriture de termes k-bornée (bo(k), pour k entier) pour les systèmes linéaires. Cette stratégie est associée à une classe de systèmes dits k-bornés LBO(k). Nous démontrons que les systèmes de la classe LBO (union des LBO(k) pour tous les k), inversent-préservent la reconnaissabilité. Nous montrons que les différents problèmes de terminaison et d'inverse-terminaison pour la stratégie bo(k) sont décidables et utilisons ce résultat pour démontrer la décidabilité de ces problèmes pour des sous-classes de LBO: les classes de systèmes linéaires fortement k-bornés: LFBO(k). La classe LFBO (union des LFBO(k)) inclut strictement de nombreuses classes de systèmes connues: les systèmes inverses basiques à gauche, linéaires growing, et linéaires inverses Finite-Path-Overlapping. Le problème de l'appartenance à LFBO(k) est décidable alors qu'il ne l'est pas pour LBO(0). Pour les mots, nous prouvons que la stratégie bo(k) préserve l'algébricité. Nous étendons la notion de réécriture k-bornée aux systèmes de réécriture de termes linéaires à gauche. Comme dans le cas linéaire, nous associons à cette stratégie la classe des systèmes linéaires à gauche k-bornés BO(k) qui étend la classe LBO(k). Nous démontrons que les systèmes de cette classe inverse-préservent la reconnaissabilité.Comme dans le cas linéaire, nous définissons ensuite la classe des systèmes fortement kbornés FBO(k), qui étend la classe LFBO(k). Nous montrons que le problème de l'appartenance à FBO(k) est décidable. La classe FBO contient strictement la classe des systèmes growing linéaires à gauche.

Résumé / Abstract : We introduce k-bounded term rewriting for linear systems (bo(k), for k integer). This strategy is associated with the class of k-bounded systems LBO(k). We show that the systems in the class LBO (union of the LBO(k) for all k), inverse-preserve recognizability. We show that the problems of termination and inverse-termination for the bo(k) strategy are decidable and use this result to show the decidability of these two problems for subclasses of LBO: the classes of linear systems strongly k-bounded: LFBO(k). The class LFBO (union of the LFBO(k)) includes strictly many known classes: the inverse left-basic systems, the linear growing systems, the linear inverse Finite-Path-Overlapping systems. Membership to LFBO(k) is decidable but this is not hte case for LBO(0). For words, we show that the bo(k) strategy preserves algebricity. We extend k-bounded rewriting to left-linear systems. As in the linear case, we associate a class of systems to the strategy: the class of left-linear kbounded systems BO(k) which extends LBO(k). We show that the systems in BO(k) inversepreserve recognizability. As in the linear case, we define the class of strongly k-bounded systems FBO(k), which extends LFBO(k). Membership to FBO(k) is proved decidable. The FBO class contains stricly the class of left-linear growing systems.