Reducing the gradedness problem of string rewriting systems to a termination problem
Stein, Itamar1
1 Department of Mathematics, Bar Ilan University, 52900 Ramat Gan, Israel
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 49 (2015) no. 3, pp. 233-254.

A finite string rewriting system (SRS) is called graded if every word over its alphabet is equivalent to only a finite number of other words. We consider the problem of deciding whether a given finite SRS is graded. We show that, in general, this problem is not decidable. Moreover we show that for many SRSs (including all one-rule SRSs), one can convert the SRS to another SRS such that the original one is graded if and only if the converted one is terminating. Since there are computer programs that can decide for many cases whether a given SRS is terminating or not, this can give us a method to prove automatically if a given SRS is graded or not.

Reçu le :
Accepté le :
DOI : 10.1051/ita/2015008
Classification : 68Q42
Mots-clés : String rewriting, termination, gradedness
Stein, Itamar 1

1 Department of Mathematics, Bar Ilan University, 52900 Ramat Gan, Israel 
@article{ITA_2015__49_3_233_0,
     author = {Stein, Itamar},
     title = {Reducing the gradedness problem of string rewriting systems to a termination problem},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {233--254},
     publisher = {EDP-Sciences},
     volume = {49},
     number = {3},
     year = {2015},
     doi = {10.1051/ita/2015008},
     mrnumber = {3434600},
     zbl = {1347.68201},
     language = {en},
     url = {http://www.numdam.org/articles/10.1051/ita/2015008/}
}
TY  - JOUR
AU  - Stein, Itamar
TI  - Reducing the gradedness problem of string rewriting systems to a termination problem
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2015
SP  - 233
EP  - 254
VL  - 49
IS  - 3
PB  - EDP-Sciences
UR  - http://www.numdam.org/articles/10.1051/ita/2015008/
DO  - 10.1051/ita/2015008
LA  - en
ID  - ITA_2015__49_3_233_0
ER  - 
%0 Journal Article
%A Stein, Itamar
%T Reducing the gradedness problem of string rewriting systems to a termination problem
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2015
%P 233-254
%V 49
%N 3
%I EDP-Sciences
%U http://www.numdam.org/articles/10.1051/ita/2015008/
%R 10.1051/ita/2015008
%G en
%F ITA_2015__49_3_233_0
Stein, Itamar. Reducing the gradedness problem of string rewriting systems to a termination problem. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 49 (2015) no. 3, pp. 233-254. doi : 10.1051/ita/2015008. http://www.numdam.org/articles/10.1051/ita/2015008/

S.I. Adjan, Defining Relations and Algorithmic Problems for Groups and Semigroups. Proc. of the Steklov Institute of Mathematics, No. 85 (1966). Translated from the Russian by M. Greendlinger. American Mathematical Society, Providence, R.I. (1966). | MR | Zbl

S.I. Adjan and G.U. Oganesjan, On the word and divisibility problems in semigroups with a single defining relation. Izvestiya: Mathematics 12 (1978) 207–212. | DOI | Zbl

F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press, Cambridge (1998). | MR | Zbl

R.V. Book and F. Otto, String-rewriting systems. Texts and Monogr. Comput. Sci. Springer-Verlag, New York (1993). | MR | Zbl

J. Giesl, P. Schneider-Kamp and R. Thiemann, AProVE 1.2: automatic termination proofs in the dependency pair framework. In Proc. of Automated reasoning. Vol. 4130 of Lect. Notes Comput. Sci. Springer, Berlin (2006) 281–286. | MR

M. Katsura and Y. Kobayashi, Undecidable properties of monoids with word problem solvable in linear time, Theoret. Comput. Sci. 290 (2003) 1301–1316. | DOI | MR | Zbl

S.W. Margolis, J. Meakin and Z. Šuniḱ, Distortion functions and the membership problem for submonoids of groups and monoids. In Geometric methods in group theory. Vol. 372 of Contemp. Math. Amer. Math. Soc. Providence, RI (2005) 109–129. | MR | Zbl

J.-C. Raoult, Finiteness results on rewriting systems. RAIRO Inform. Théor. 15 (1981) 373–391. | DOI | Numdam | MR | Zbl

K. Shikishima-Tsuji, M. Katsura and Y. Kobayashi, On termination of confluent one-rule string-rewriting systems. Inform. Process. Lett. 61 (1997) 91–96. | DOI | MR | Zbl

C. Wrathall, Confluence of one-rule Thue systems. In Word equations and related topics (Tübingen, 1990). Vol. 572 of Lect. Notes Comput. Sci. Springer, Berlin (1992) 237–246. | MR

H. Zantema, Termination of string rewriting proved automatically, J. Automat. Reason. 34 (2005) 105–139. | DOI | MR | Zbl

H. Zantema and A. Geser, A complete characterization of termination 0 p 1 q →1 r 0 s . Lect. Notes Comput. Sci. 914 (1995) 41–55. | MR | Zbl

Cité par Sources :