Etude de la stratégie de réécriture de termes k-bornée

• Main Author: Sylvestre, Marc
• Other Authors: Bordeaux
• Language: fr
• Published: 2014
• Subjects: Réécriture de termes,; Stratégies; Préservation de la reconnaissabilité,; Terminaison; Term rewriting,; Strategies; Préservation of recognizability,; Termination
• Online Access: http://www.theses.fr/2014BORD0121/document

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. === 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.