Complexity of Normal Form Properties and Reductions for Term Rewriting Problems

• Autorzy: Verma R.
• Języki publikacji: EN

Abstrakty

EN

We present several new and some significantly improved polynomial-time reductions between basic decision problems of term rewriting systems. We prove two theorems that imply tighter upper bounds for deciding the uniqueness of normal forms (UN^=) and unique normalization (UN^&rar;) properties under certain conditions. From these theorems we derive a new and simpler polynomial-time algorithm for the UN^= property of ground rewrite systems, and explicit upper bounds for both UN^= and UN! properties of left-linear right-ground systems. We also show that both properties are undecidable for right-ground systems. It was already known that these properties are undecidable for linear systems. Hence, in a sense the decidability results are "close" to optimal.

Słowa kluczowe

EN

term rewriting systems; decision problem; reduction; confluence; existence of normal form; uniqueness of normal forms; reachability; joinability; unique normalization

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 92, nr 1-2
• Strony: 145--168
• Opis fizyczny: Bibliogr.23 poz.

Twórcy

autor

Verma R.

• Comp. Sci. Dept. –-501 PGH, 4800 Calhoun Road, University of Houston, Houston, TX 77204-3010, USA,

Bibliografia

• [1] Book, R.: Thue Systems as Rewriting Systems, Lecture Notes in Computer Science, 202, 1985, 63-94.
• [2] Comon, H.: Sequentiality,Monadic Second-Order Logic and Tree Automata, Information and Computation, 157, 2000, 25-51.
• [3] Comon, H., Dauchet, M., Gilleron, R., et al.: Tree Automata Techniques and Applications, Available at http://www.grappa.univ-lille3.fr/tata/tata.pdf, 1999.
• [4] Comon, H., Godoy, G., Nieuwenhuis, R.: Confluence of ground rewrite systems is in P, Proc. IEEE Symp. On Foundations of Computer Science, 2001.
• [5] Dauchet, M., Heuillard, T., Lescanne, P., Tison, S.: Decidability of the Confluence of Finite Ground Term Rewrite Systems, Information and Computation, 88, 1990, 187-201, Also in Proc. IEEE Symp. on LICS 1987.
• [6] Dauchet, M., Tison, S.: The Theory of Ground Rewrite Systems is Decidable, Proc. IEEE Conf. on Logic in Computer Science, 1990.
• [7] Dershowitz, N., Plaisted, D.: Rewriting, in: Handbook of Automated Reasoning (J. A. Robinson, A. Voronkov, Eds.), vol. 1, chapter 9, Elsevier Science, 2001, 535-610.
• [8] Downey, P., Sethi, R., Tarjan, R.: Variations on the Common Subexpression Problem, Journal of the ACM, 27(4), 1980, 758-771.
• [9] Geser, A., Middeldorp, A., Ohlebusch, E., Zantema, H.: Relative undecidability in term rewriting: II. The confluence hierarchy, Information and Computation, 178(1), October 2002, 132-148.
• [10] Geser, A., Zantema, H.: Non-looping string rewriting., Rairo-Theoretical Informatics and Applications, 33(3), 1999, 279-302.
• [11] Godoy, G., Tiwari, A., Verma, R.: On the Confluence of Linear Shallow Rewrite Systems, Proceedings of the Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, 2003.
• [12] Godoy, G., Tiwari, A., Verma, R.: Characterizing Confluence by Rewrite Closure and Right Ground Term Rewrite Systems, Applicable Algebra in Engineering, Communication and Computing, 15(1), 2004, 13-36.
• [13] Hirokawa, N., Middeldorp, A.: Dependency Pairs Revisited, Proc. Conf. on Rewriting Techniques & Applications, 2004.
• [14] Huet, G., Oppen, D.: Equations and Rewrite Rules: A Survey, in: Formal Language Theory: Perspectives and Open Problems (R. Book, Ed.), Academic Press, 1980. R. Verma / Complexity of Normal Form Properties and Reductions for Rewriting
• [15] Jacquemard, F.: Decidable Approximations of Term Rewriting Systems, Proc. Conf. on Rewriting Techniques & Applications, 1996.
• [16] Kozen, D.: Complexity of Finitely Presented Algebras, Proc. Ninth ACM Symposium on Theory of Computing, 1977.
• [17] Nelson, G., Oppen, D.: Fast Decision Algorithms Based on Congruence Closure, Journal of the ACM, 27, 1980, 356-364, Also in the 18th IEEE FOCS, 1977.
• [18] Oyamaguchi, M.: On the Word problem for Right-Ground Term Rewriting Systems, Transactions of the IEICE, E 73(5), 1990, 718-723.
• [19] Plaisted, D.: Polynomial Time Termination and Constraint Satisfaction Tests, Proc. Conf. on Rewriting Techniques & Applications, 1993.
• [20] Shostak, R.: An Algorithm for Reasoning About Equality, Communications of the ACM, 21(7), 1978, 583-585.
• [21] Verma, R.: Algorithms and Reductions for Rewriting Problems. II, Information Processing Letters, 84(4), 2002, 227-233.
• [22] Verma, R., Hayrapetyan, A.: A New Decidability Technique for ground term rewriting systems with applications, ACM Transactions on Computational Logic, 6(1), 2005, 102-123.
• [23] Verma, R., Rusinowitch, M., Lugiez, D.: Algorithms and Reductions for Rewriting Problems, Fundamenta Informaticae, 46(3), 2001, 257-276, Also in Proc. of Int'l Conf. on Rewriting Techniques and Applications 1998.