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.
Accepté le :
DOI : 10.1051/ita/2015008
Mots clés : String rewriting, termination, gradedness
@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
and , 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
and , 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
, Finiteness results on rewriting systems. RAIRO Inform. Théor. 15 (1981) 373–391. | DOI | Numdam | MR | Zbl
, and , 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
, Termination of string rewriting proved automatically, J. Automat. Reason. 34 (2005) 105–139. | DOI | MR | Zbl
and , A complete characterization of termination . Lect. Notes Comput. Sci. 914 (1995) 41–55. | MR | Zbl
Cité par Sources :
