Résumé | Nous introduisons la notion de réécriture de termes k-bornée (bo(k), 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 bo(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 k-borné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.
|