Abstract
Limitations, such as right-linearity, on the form of rules in a term-rewriting system are shown to restrict the class of derivations that must be considered when determining whether or not the system terminates for all inputs. These restricted derivations, termed "chains", are obtained by attempting to apply rules to the final terms of derivations that issue from the left-hand side of rules. Similar limitations are shown to guarantee that combining two terminating systems yields a terminating system.
Research supported in part by the National Science Foundation under Grant MCS 79-04897.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Dershowitz, N. [1979], A note on simplification orderings, Information Processing Letters, vol. 9, no. 5, pp. 212–215.
Dershowitz, N. and Manna, Z. [Aug. 1979], Proving termination with multiset orderings, CACM, vol. 22, no. 8, pp. 465–476.
Huet, G. [Oct. 1980], Confluent reductions: Abstract properties and applications to term rewriting systems, J. ACM, vol. 27, no. 4, pp. 797–821.
Huet, G. and Lankford, D.S. [Mar. 1978], On the uniform halting problem for term rewriting systems, Rapport laboria 283, INRIA, Le Chesnay, France.
Huet, G. and Levy, J.-J. [Aug. 1979], Call by need computations in non-ambiguous linear term rewriting systems, Rapport laboria 359, INRIA, Le Chesnay, France; to appear.
Huet, G. and Oppen, D.C. [1980], Equations and rewrite rules: A survey, in "Formal Languages: Perspectives and Open Problems" (R. Book, ed.), Academic Press, New York.
Knuth, D.E. and Bendix, P.B. [1969], Simple word problems in universal algebras, in "Computational Problems in Universal Algebras" (J. Leech, ed.), Pergamon Press, Oxford, pp. 263–297.
O'Donnell, M. [1977], Computing in systems described by equations, Lecture Notes in Computer Science, vol. 58, Springer Verlag, Berlin.
Rosen, B.K. [1973], Tree-manipulation systems and Church-Rosser theorems, J. ACM, vol. 20, pp. 160–187.
Slagle, J.R. [Oct. 1974], Automated theorem-proving for theories with simplifiers, commutativity, and associativity, J. ACM, vol. 21, no. 4, pp. 622–642.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1981 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dershowitz, N. (1981). Termination of linear rewriting systems. In: Even, S., Kariv, O. (eds) Automata, Languages and Programming. ICALP 1981. Lecture Notes in Computer Science, vol 115. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10843-2_36
Download citation
DOI: https://doi.org/10.1007/3-540-10843-2_36
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-10843-6
Online ISBN: 978-3-540-38745-9
eBook Packages: Springer Book Archive