Abstract
A linear term rewriting system \(\mathcal{R}\)is growing when, for every rule l→r ∈ \(\mathcal{R}\), each variable which is shared by l and r occurs at depth one in l. We show that the set of ground terms having a normal form w.r.t. a growing rewrite system is recognized by a finite tree automaton. This implies in particular that reachability and sequentiality of growing rewrite systems are decidable. Moreover, the word problem is decidable for related equational theories. We prove that our conditions are actually necessary: relaxing them yields undecidability of reachability.
Concerning sequentiality, the result may be restated in terms of approximations of term rewriting systems. An approximation of a system \(\mathcal{R}\)is a renaming of the variables in the right hand sides which yields a growing rewrite system. This gives the decidability of a new sufficient condition for sequentiality of left-linear rewrite systems, which encompasses known decidable properties such as strong, NV and NVNF sequentiality.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
H. Comon. Sequentially, second-order monadic logic and tree automata. In Tenth Annual IEEE Symposium on Logic in Computer Science, San Diego, CA, June 1995. IEEE Comp. Soc. Press.
H. Comon, M. Haberstrau, and J.-P. Jouannaud. Decidable properties of shallow equational theories. In Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science. IEEE Comp. Soc. Press, 1992.
M. Dauchet. Simulation of a turing machine by a left-linear rewrite rule. In Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, LNCS 355, 1989.
M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In Proc. 5th IEEE Symp. Logic in Computer Science, Philadelphia, 1990.
M. Dauchet, S. Tison, T. Heuillard, and P. Lescanne. Decidability of the confluence of ground term rewriting systems. Technical Report IT-102, LIFL, Université de Lille, May 1987. Actes de logic in Computer Science Second Annual Conference New-York Juin 87.
N. Dershowitz. Termination of linear rewriting systems. In Proceedings of the Eihgth Int. Colloquium on Automata, Languages and Programming, pages 448–458, Acre, Israel, 1981.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.
J. Gallier and R. Book. Reductions in tree replacement systems. Theorical Computer Science, 37:123–150, 1985.
M. Gécseg and M. Steinby. Tree Automata. Akademia Kiadó, Budapest, 1984.
G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM, 27(4):797–821, Oct. 1980.
G. Huet. Formal structures for computation and deduction. In: Working material for the International Summer School on Logic of Programming and Calculi of Discrete Design, Marktoberdorf, May 1986.
G. Huet and D. S. Lankford. On the uniform halting problem for term rewriting systems. Research Report 283, INRIA, Mar. 1978.
G. Huet and J.-J. Lévy. Computations in orthogonal term rewriting systems. In G. Plotkin and J.-L. Lassez, editors, Computational Logic: essays in Honour of Alan Robinson. MIT Press, 1990.
G. Huet and J.-J. Lévy. Call by need computations in non-ambiguous linear term rewriting systems. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991.
J. W. Klop and A. Middeldorp. Sequentiality in orthogonal term rewriting systems. Journal of Symbolic Computation, 12:161–195, 1991.
T. Nagaya, M. Sakai, and Y. Toyama. NVNF-sequentiality of left-linear term rewriting systems. In Proc. Japanese Workhop on Term Rewriting, Kyoto, July 1995.
M. Oyamaguchi. The reachability problem for quasi-ground term rewriting systems. J. Inf. Process., pages 232–236, 1986.
M. Oyamaguchi. On the word problem for right-ground term rewriting systems. Trans. IEICE Japan, E73:718–723, 1990.
M. Oyamaguchi. NV-sequentiality: a decidable condition for call-by-need computations in term rewriting systems. SIAM J. Comput., 22(1):114–135, 1993.
E. L. Post. Recursive unsolvability of a problem of Thue. Journal of Symbolic Logic, 13:1–11, 1947.
W. Sadfi. Contribution à l'étude de la séquentialité forte des définitions de fonctions par règles. Thèse de doctorat, Université Paris-Sud, Orsay, France, Dec. 1993.
A. Togashi and S. Noguchi. Some decision problems and their time complexity for term rewriting systems. Trans. IECE Japan, J66(D):1177–1184, 1983.
Y. Toyama. Strong sequentially of left linear overlapping term rewriting systems. In Proc. 7th IEEE Symp. on Logic in Computer Science, Santa Cruz, CA, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jacquemard, F. (1996). Decidable approximations of term rewriting systems. In: Ganzinger, H. (eds) Rewriting Techniques and Applications. RTA 1996. Lecture Notes in Computer Science, vol 1103. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61464-8_65
Download citation
DOI: https://doi.org/10.1007/3-540-61464-8_65
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61464-7
Online ISBN: 978-3-540-68596-8
eBook Packages: Springer Book Archive