×
Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes

Termination proofs for string rewriting systems via inverse match-bounds. (English) Zbl 1105.68054

J. Autom. Reasoning 34, No. 4, 365-385 (2005).
Summary: Annotating a letter by a number, one can record information about its history during a rewrite derivation. In each rewrite step, numbers in the reduct are updated depending on the redex numbering. A string rewriting system is called match-bounded if there is a global upper bound to these numbers. Match-boundedness is known to be a strong sufficient criterion for both termination and preservation of regular languages. We show that the string rewriting systems whose inverse (left and right hand sides exchanged) is match-bounded, also have exceptional properties, but slightly different ones. Inverse match-bounded systems need not terminate; they effectively preserve context-free languages; their sets of normalizable strings and their sets of immortal strings are effectively regular. These languages can be used to decide the normalization, the uniform normalization, the termination and the uniform termination problem for inverse match-bounded systems. We also prove that the termination problem is decidable in linear time, and that a certain strong reachability problem is decidable, thereby solving two open problems of McNaughton’s. Like match-bounds, inverse match-bounds entail linear derivational complexity on the set of terminating strings.

Cited in 6 Documents

MSC:

68Q42 Grammars and rewriting systems
68Q45 Formal languages and automata

Software:

Matchbox
Cite Review PDF
Full Text: DOI Link

References:

[1] Berstel, J.: Transductions and Context-Free Languages, Teubner, Stuttgart, 1979. · Zbl 0424.68040
[2] Book, R. V. and Otto, F.: String-Rewriting Systems, Texts Monogr. Comput. Sci. Springer-Verlag, New York, 1993. · Zbl 0832.68061
[3] Coquand, T. and Persson, H.: A proof-theoretical investigation of Zantema’s problem, in M. Nielsen and W. Thomas (eds.), Proc. 11th Annual Conf. of the EACSL CSL-97, Lecture Notes in Comput. Sci., Vol. 1414, Springer-Verlag, 1998, pp. 177–188. · Zbl 0910.03033
[4] Dershowitz, N.: Termination of rewriting, J. Symb. Comput. 3(1–2) (1987), 69–115. · Zbl 0637.68035 · doi:10.1016/S0747-7171(87)80022-6
[5] Dershowitz, N. and Hoot, C.: Topics in termination, in C. Kirchner (ed.), Proc. 5th Int. Conf. Rewriting Techniques and Applications RTA-93, Lecture Notes in Comput. Sci., Vol. 690, Springer-Verlag, 1993, pp. 198–212.
[6] Geser, A.: Note on normalizing, non-terminating one-rule string rewriting systems, Theoret. Comput. Sci. 243 (2000), 489–498. · Zbl 0944.68085 · doi:10.1016/S0304-3975(00)00167-5
[7] Geser, A.: Termination of string rewriting rules that have one pair of overlaps, in R. Nieuwenhuis (ed.), Proc. 14th Int. Conf. Rewriting Techniques and Applications RTA-03, Lecture Notes in Comput. Sci, Vol. 2706, Springer-Verlag, pp. 410–423. · Zbl 1038.68065
[8] Geser, A., Hofbauer, D. and Waldmann, J.: Match-bounded string rewriting systems, in B. Rovan and P. Vojtas (eds.), Proc. 28th Int. Symp. Mathematical Foundations of Computer Science MFCS-03, Lecture Notes in Comput. Sci., Vol. 2747, Springer-Verlag, 2003, pp. 449–459. · Zbl 1124.68378
[9] Geser, A., Hofbauer, D. and Waldmann, J.: Match-bounded string rewriting systems, Appl. Algebra Eng. Commun. Comput. 15(3–4) (2004), 149–171. · Zbl 1101.68048 · doi:10.1007/s00200-004-0162-8
[10] Geser, A., Hofbauer, D., Waldmann, J. and Zantema, H.: Finding finite automata that certify termination of string rewriting systems, Int. J. Found. Comput. Sci. 16(3) (2005), 471–486. · Zbl 1097.68052 · doi:10.1142/S0129054105003108
[11] Ginsburg, S. and Greibach, S. A.: Mappings which preserve context sensitive languages, Inf. Control 9(6) (1966), 563–582. · Zbl 0145.00803 · doi:10.1016/S0019-9958(66)80016-5
[12] Hibbard, T. N.: Context-limited grammars, J. ACM 21(3) (1974), 446–453. · Zbl 0291.68026 · doi:10.1145/321832.321842
[13] Hofbauer, D. and Waldmann, J.: Deleting string rewriting systems preserve regularity, Theoret. Comput. Sci. 327 (2004), 301–317. · Zbl 1071.68034 · doi:10.1016/j.tcs.2004.04.009
[14] Kobayashi, Y., Katsura, M. and Shikishima-Tsuji, K.: Termination and derivational complexity of confluent one-rule string-rewriting systems, Theory Comput. Sci. 262(1–2) (2001), 583–632. · Zbl 0992.68120 · doi:10.1016/S0304-3975(00)00367-4
[15] Kurth, W.: Termination und Konfluenz von Semi-Thue-Systemen mit nur einer Regel. Dissertation, Technische Universität Clausthal, Germany, 1990. · Zbl 0719.03019
[16] McNaughton, R.: Semi-Thue systems with an inhibitor, J. Autom. Reason. 26 (2001), 409–431. · Zbl 0981.68073 · doi:10.1023/A:1010759024900
[17] Moore, C. and Eppstein, D.: One-dimensional peg solitaire, and duotaire, in R. J. Nowakowski (ed.), More Games of No Chance, MSRI Publications 42, Cambridge Univ. Press, 2002, pp. 341–350. · Zbl 1062.91527
[18] Ravikumar, B.: Peg-solitaire, string rewriting systems and finite automata, in H.-W. Leong, H. Imai and S. Jain (eds.), Proc. 8th Int. Symp. Algorithms and Computation ISAAC-97, Lecture Notes in Comput. Sci., Vol. 1350, Springer-Verlag, 1997, pp. 233–242.
[19] Sénizergues, G.: On the termination problem for one-rule semi-Thue systems, in H. Ganzinger (ed.), Proc. 7th Int. Conf. Rewriting Techniques and Applications RTA-96, Lecture Notes in Comput. Sci., Vol. 1103, Springer-Verlag, 1996, pp. 302–316.
[20] Tahhan Bittar, E.: Complexité linéaire du problème de Zantema, C. R. Acad. Sci. Paris Sér. I Inform. Théor. 323 (1996), 1201–1206. · Zbl 0864.68055
[21] Waldmann, J.: Matchbox: A tool for match-bounded string rewriting, in V. van Oostrom (ed.), Proc. 15th Int. Conf. Rewriting Techniques and Applications RTA-04, Lecture Notes in Comp. Sci. Vol. 3091, Springer-Verlag, 2004, pp. 85–94.
[22] Yu, S.: Regular languages, in G. Rozenberg and A. Salomaa (eds.), Handbook of Formal Languages, Vol. 1, Springer-Verlag, 1998, pp. 41–110.
[23] Zantema, H.: Termination, in Terese, Term Rewriting Systems, Cambridge Univ. Press, 2003, pp. 181–259.
[24] Zantema, H. and Geser, A.: A complete characterization of termination of 0 p 1 q 1 r 0 s , Appl. Algebra Eng. Commun. Comput. 11(1) (2000), 1–25. · Zbl 0962.68086 · doi:10.1007/s002009900019
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.