Skip to main content
SpringerLink
Log in

Termination

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1985)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 202))

Included in the following conference series:

Abstract

This survey describes methods for proving that systems of rewrite rules terminate. Illustrations of the use of path orderings and other simplification orderings in termination proofs are given. The effect of restrictions, such as linearity, on the form of rules is considered. In general, though, termination is an undecidable property of rewrite systems.

The preparation of this survey was supported in part by the National Science Foundation under Grant MCS 83-07755.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ait-Kaci, H. “An algorithm for finding a minimal recursive path ordering”, Report MS-CIS-83-7, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA, 1983.

    Google Scholar 

  2. Bachmair, L., and Dershowitz, N. “Commutation, transformation, and termination”. (1985) (submitted).

    Google Scholar 

  3. Bachmair, L., and Plaisted, D. A. “Associative path ordering”. Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France (May 1985).

    Google Scholar 

  4. Ben Cherifa, A. “Preuve de la terminaison finie d'un système de reécriture par l'ordre polynômial”, Unpublished manuscript, Centre de Recherche en Informatique de Nancy, Nancy, France, 1984.

    Google Scholar 

  5. Bergstra, J. A., and Tucker, J. V. “Equational specifications for computable data types: Six hidden functions suffice and other sufficiency bounds”, Preprint IW 128/80, Mathematisch Centrum, Amsterdam, The Netherlands, January 1980.

    Google Scholar 

  6. Bidoit, M. “Thesis”, Thèse.

    Google Scholar 

  7. [Bucher, et al.-84] Bucher, W., Ehrenfeucht, A., and Haussler, D. “On total regulators generated by derivation relations”, University of Denver, 1984.

    Google Scholar 

  8. Calladine, P. “Personal communication”, Laboratoire d'Informatique, Université de Poitiers, May 1985.

    Google Scholar 

  9. Choque, G. “Calcul d'un ensemble complet d'incrementations minimales pour l'ordre recursif de decomposition”, Technical report, Centre de Recherche en Informatique de Nancy, Nancy, France, 1983.

    Google Scholar 

  10. Cohen, P. J. “Decision procedures for real and p-adic fields”. Communications of Pure and Applied Mathematics, Vol. 22, No. 2 (1969), pp. 131–151.

    Google Scholar 

  11. Collins, G. “Quantifier elimination for real closed fields by cylindrical algebraic decomposition”. Proceedings Second GI Conference on Automata Theory and Formal Languages (1975), pp. 134–183.

    Google Scholar 

  12. Dauchet, M., and Tison, S. “Decidability of confluence for ground term rewriting systems”, Unpublished report, Université de Lille I, Lille, France, 1984.

    Google Scholar 

  13. [Dershowitz, et al.-83] Dershowitz, N., Hsiang, J., Josephson, N. A., and Plaisted, D. A. “Associative-commutative rewriting”. Proceedings of the Eighth International Joint Conference on Artificial Intelligence, Karlsruhe, West Germany (August 1983), pp. 940–944.

    Google Scholar 

  14. Dershowitz, N. “A note on simplification orderings”. Information Processing Letters, Vol. 9, No. 5 (November 1979), pp. 212–215.

    Google Scholar 

  15. Dershowitz, N. “On representing ordinals up to Λ0”, Unpublished note, Department Computer Science, University of Illinois, Urbana, IL, June 1980.

    Google Scholar 

  16. Dershowitz, N. “Termination of linear rewriting systems”. Proceedings of the Eighth EATCS International Colloquium on Automata, Languages and Programming, Vol. 115, Acre, Israel (July 1981), pp. 448–458.

    Google Scholar 

  17. Dershowitz, N. “Orderings for term-rewriting systems”. J. Theoretical Computer Science, Vol. 17, No. 3 (March 1982), pp. 279–301 (previous version appeared in Proceedings of the Symposium on Foundations of Computer Science, San Juan, PR, pp. 123–131 [October 1979]).

    Google Scholar 

  18. Dershowitz, N. “Well-founded orderings”, Technical Report ATR-83(8478)-3, Information Sciences Research Office, The Aerospace Corporation, El Segundo, CA, May 1983.

    Google Scholar 

  19. Dershowitz, N., and Manna, Z. “Proving termination with multiset orderings”. Communications of the ACM, Vol. 22, No. 8 (August 1979), pp. 465–476 (also in Proceedings of the International Colloquium on Automata. Languages and Programming, Graz, 188–202 [July 1979]).

    Google Scholar 

  20. Dershowitz, N., and Zaks, S. “Applied tree enumerations”. Proceedings of the Sixth Colloquium on Trees in Algebra and Programming, Vol. 112, Genoa, Italy (March 1981), pp. 180–193.

    Google Scholar 

  21. Detlefs, D., and Forgaard, R. “A procedure for automatically proving the termination of a set of rewrite rules”. Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France (May 1985).

    Google Scholar 

  22. [Ehrenfeucht, et al.-83] Ehrenfeucht, A., Haussler, D., and Rozenberg, G. “On regularity of context-free languages”. Theoretical Computer Science, Vol. 27 (1983), pp. 311–32.

    Google Scholar 

  23. Feferman, S. “Systems of predicative analysis II: Representation of ordinals”. J. Symbolic Logic, Vol. 33 (1968), pp. 193–220.

    Google Scholar 

  24. Filman, R. E. “personal communication”, 1978.

    Google Scholar 

  25. Forgaard, R. “A program for generating and analyzing term rewriting systems”, Master's thesis, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, September 1984.

    Google Scholar 

  26. Gardner, M. “Mathematical games: Tasks you cannot help finishing no matter how hard you try to block finishing them”. Scientific American, Vol. 24, No. 2 (August 1983), pp. 12–21.

    Google Scholar 

  27. Gentzen, G. “New version of the consistency proof for elementary number theory”. In: Collected Papers of Gerhard Gentzen, M. E. Szabo, ed (1938). North-Holland, 1969, pp. 252–286 (1938).

    Google Scholar 

  28. Gnaedig, I. “personal communication”, 1985.

    Google Scholar 

  29. Gorn, S. “Handling the growth by definition of mechanical languages”. Proceedings of the Spring Joint Computer Conference (Spring 1967), pp. 213–224.

    Google Scholar 

  30. Gorn, S. “On the conclusive validation of symbol manipulation processes (How do you know it has to work?)”. J. of the Franklin Institute, Vol. 296, No. 6 (December 1973), pp. 499–518.

    Google Scholar 

  31. [Guttag,etal.-83] Guttag, J. V., Kapur, D., and Musser, D. R. “On proving uniform termination and restricted termination of rewriting systems”. SIAM Computing, Vol. 12, No. 1 (February 1983), pp. 189–214.

    Google Scholar 

  32. Higman, G. “Ordering by divisibility in abstract algebras”. Proceedings of the London Mathematical Society (3), Vol. 2, No. 7 (September 1952), pp. 326–336.

    Google Scholar 

  33. Huet, G. “Confluent reductions: Abstract properties and applications to term rewriting systems”. J. of the Association for Computing Machinery, Vol. 27, No. 4 (1980), pp. 797–821 (previous version in Proceedings of the Symposium on Foundations of Computer Science, Providence, RI, pp. 30–45 [1977]).

    Google Scholar 

  34. Huet, G., and Lankford, D. S. “On the uniform halting problem for term rewriting systems”, Rapport Laboria 283, IRIA, March 1978.

    Google Scholar 

  35. Huet, G., and Levy, J. J. “Call by need computations in non-ambiguous linear term rewriting systems”, Rapport laboria 359, INRIA, Le Chesnay, France, August 1979.

    Google Scholar 

  36. Huet, G., and Oppen, D. C. “Equations and rewrite rules: A survey”. In: Formal Language Theory: Perspectives and Open Problems, R. Book, ed. Academic Press, New York, 1980, pp. 349–405.

    Google Scholar 

  37. Hullot, J. M. “Canonical forms and unification”. Proceedings of the Fifth Conference on Automated Deduction, Les Arcs, France (July 1980), pp. 318–334.

    Google Scholar 

  38. Iturriaga, R. “Contributions to mechanical mathematics”, Ph.D. Thesis, Carnegie-Mellon University, Pittsburgh, Pennsylvania, 1967.

    Google Scholar 

  39. [Jouannaud,etal.-82] Jouannaud, J. P., Lescanne, P., and Reinig, F. “Recursive decomposition ordering”. Proceedings of the Second IFIP Workshop on Formal Description of Programming Concepts, Garmisch-Partenkirchen, West Germany (June 1982), pp. 331–348.

    Google Scholar 

  40. Jouannaud, J. P., and Kirchner, H. “Construction d'un plus petit order de simplification”, Unpublished note, Centre de Recherche en Informatique de Nancy, Nancy, France, 1982.

    Google Scholar 

  41. Jouannaud, J. P., and Muñoz, M. “Termination of a set of rules modulo a set of equations”. Proceedings of the Seventh International Conference on Automated Deduction, Napa, CA (May 1984), pp. 175–193.

    Google Scholar 

  42. Kamin, S., and Levy, J. J. “Two generalizations of the recursive path ordering”, Unpublished note, Department of Computer Science, University of Illinois, Urbana, IL, February 1980.

    Google Scholar 

  43. [Kapur,etal.-85] Kapur, D., Narendran, P., and Sivakumar, G. “A path ordering for proving termination of term rewriting systems”. Proceedings of the Tenth Colloquium on Trees in Algebra and Programming (1985).

    Google Scholar 

  44. Kapur, D., and Sivakumar, G. “Experiments with and architecture of RRL, a rewrite rule laboratory”. Proceedings of an NSF Workshop on the Rewrite Rule Laboratory, Schenectady, NY (September 1983), pp. 33–56 (available as Report 84GEN008, General Electric Research and Development [April 1984]).

    Google Scholar 

  45. Kirby, L., and Paris, J. “Accessible independence results for Peano arithmetic”. Bulletin London Mathematical Society, Vol. 14 (1982), pp. 285–293.

    Google Scholar 

  46. Knuth, D. E. Fundamental algorithms. Addison-Wesley, Reading, MA, 1973 (second edition).

    Google Scholar 

  47. Knuth, D. E., and Bendix, P. B. “Simple word problems in universal algebras”. In: Computational Problems in Abstract Algebra, J. Leech, ed. Pergamon Press, 1970, pp. 263–297.

    Google Scholar 

  48. Krishnamoorthy, M. S., and Narendran, P. “A note on recursive path ordering”, Unpublished note, General Electric Corporate Research and Development, Schenectady, NY, 1984.

    Google Scholar 

  49. Kruskal, J. B. “Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture”. Transactions of the American Mathematical Society, Vol. 95 (May 1960), pp. 210–225.

    Google Scholar 

  50. Kruskal, J. B. “The theory of well-quasi-ordering: A frequently discovered concept”. J. Combinatorial Theory Ser. A, Vol. 13 (1972), pp. 297–305.

    Google Scholar 

  51. Lankford, D. S. “Canonical algebraic simplification in computational logic”, Memo ATP-25, Automatic Theorem Proving Project, University of Texas, Austin, TX, May 1975.

    Google Scholar 

  52. Lankford, D. S. “On proving term rewriting systems are Noetherian”, Memo MTP-3, Mathematics Department, Louisiana Tech. University, Ruston, LA, May 1979.

    Google Scholar 

  53. Lankford, D. S., and Musser, D. R. “A finite termination criterion”, Unpublished draft, 1981.

    Google Scholar 

  54. Laver, R. “Better-quasi-orderings and a class of trees”. Studies in Foundations and Combinatorics (1978), pp. 31–48.

    Google Scholar 

  55. Lescanne, P. “Two implementations of the recursive path ordering on monadic terms”. Proceedings of the Nineteenth Allerton Conference on Communication, Control, and Computing, Monticello, IL (September 1981), pp. 634–643.

    Google Scholar 

  56. Lescanne, P. “Computer experiments with the REVE term rewriting system generator”. Proceedings of the Tenth Symposium on Principles of Programming Languages, Austin, TX (January 1983), pp. 99–108.

    Google Scholar 

  57. Lescanne, P. “Some properties of decomposition ordering, A simplification ordering to prove termination of rewriting systems”. RAIRO Theoretical Informatics, Vol. 16, No. 4, pp. 331–347.

    Google Scholar 

  58. Lescanne, P. “Uniform termination of term-rewriting systems with status”. Proceedings of the Ninth Colloquium on Trees in Algebra and Programming, Bordeaux, France (March 1984).

    Google Scholar 

  59. Lescanne, P., and Jouannaud, J. P. “On multiset orderings”. Information Processing Lett., Vol. 15, No. 2 (September 1982), pp. 57–62.

    Google Scholar 

  60. Lescanne, P., and Steyaert, J. M. “On the study of data structures: Binary tournaments with repeated keys”. Proceedings of the Tenth EATCS International Colloquium on Automata, Languages and Programming, Barcelona, Spain (July 1983), pp. 466–475.

    Google Scholar 

  61. Levy, J. J. “Problem 80-5”. J. of Algorithms, Vol. 1, No. 1 (March 1980), pp. 108–109.

    Google Scholar 

  62. Lipton, R., and Snyder, L. “On the halting of tree replacement systems”. Proceedings of the Conference on Theoretical Computer Science, Waterloo, Canada (August 1977), pp. 43–46.

    Google Scholar 

  63. Manna, Z. “Termination of algorithms”, Ph.D. thesis, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, April 1969.

    Google Scholar 

  64. Manna, Z. Mathematical Theory of Computation. McGraw-Hill, New York, 1974.

    Google Scholar 

  65. Manna, Z., and Ness, S. “On the termination of Markov algorithms”. Proceedings of the Third Hawaii International Conference on System Science, Honolulu, HI (January 1970), pp. 789–792.

    Google Scholar 

  66. Metivier, Y. “About the rewriting systems produced by the Knuth-Bendix completion algorithm”. Information Processing Letters, Vol. 16 (January 1983), pp. 31–34.

    Google Scholar 

  67. Nash-Williams, C. S. J. A. “On well-quasi-ordering finite trees”. Proceedings of the Cambridge Philosophical Society, 59 (1963), pp. 833–835.

    Google Scholar 

  68. O'Donnell, M. J. “Computing in systems described by equations”. Lecture Notes in Computer Science, Vol. 58, Berlin (1977).

    Google Scholar 

  69. Paulson, L. C. “Constructing recursion operations in intuitionistic type theory”, Technical Report 57, Computer Laboratory, University of Cambridge, Cambridge, UK, October 1984.

    Google Scholar 

  70. Pettorossi, A. “A property which guarantees termination in weak combinatory logic and subtree replacement systems”, Report R.78-23, Instituto di Automatica, Università di Roma, Rome, Italy, November 1978.

    Google Scholar 

  71. Pettorossi, A. “Comparing and putting together recursive path orderings, simplification orderings and non-ascending property for termination proofs of term rewriting systems”. Proceedings of the Eighth International Colloquium on Automata, Languages and Programming, Acre, Israel (July 1981), pp. 432–447.

    Google Scholar 

  72. Plaisted, D. A. “Well-founded orderings for proving termination of systems of rewrite rules”, Report R78-932, Department of Computer Science, University of Illinois, Urbana, IL, July 1978.

    Google Scholar 

  73. Plaisted, D. A. “A recursively defined ordering for proving termination of term rewriting systems”, Report R-78-943, Department of Computer Science, University of Illinois, Urbana, IL, September 1978.

    Google Scholar 

  74. Plaisted, D. A. “personal communication”, 1979.

    Google Scholar 

  75. Plaisted, D. A. “An associative path ordering”. Proceedings of an NSF Workshop on the Rewrite Rule Laboratory, Schenectady, NY (September 1983), pp. 123–136 (available as Report 84GEN008, General Electric Research and Development [April 1984]).

    Google Scholar 

  76. Plaisted, D. A. “The undecidability of self embedding for term rewriting systems”. Information Processing Lett., Vol. 20, No. 2 (February 1985), pp. 61–64.

    Google Scholar 

  77. Porat, S., and Francez, N. “Fairness in term rewriting systems”. Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France (May 1985).

    Google Scholar 

  78. Puel, L. “personal communication”, May 1985.

    Google Scholar 

  79. Raoult, J. C., and Vuillemin, J. “Operational and semantic equivalence between recursive programs”. J. of the Association of Computing Machinery, Vol. 27, No. 4 (October 1980), pp. 772–796.

    Google Scholar 

  80. Rosen, B. “Tree-manipulating systems and Church-Rosser theorems”. J. of the Association for Computing Machinery, Vol. 20 (1973), pp. 160–187.

    Google Scholar 

  81. Rusinowitch, M. “Plaisted ordering and recursive decomposition ordering revisited”. Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France (May 1985).

    Google Scholar 

  82. Sakai, K. “An ordering method for term rewriting systems”. Proceedings of the First International Conference on Fifth Generation Computer Systems, Tokyo, Japan (November 1984).

    Google Scholar 

  83. Scherlis, W. L. “Expression procedures and program derivation”, Ph.D. Dissertation, Department Computer Science, Stanford University, Stanford, CA, August 1980.

    Google Scholar 

  84. Slagle, J. R. “Automated theorem-proving for theories with simplifiers, commutativity, and associativity”. J. of the Association for Computing Machinery, Vol. 21, No. 4 (1974), pp. 622–642.

    Google Scholar 

  85. Smullyan, R. M. “Trees and ball games”. Annals of the New York Academy of Science, Vol. 321 (1979), pp. 86–90.

    Google Scholar 

  86. Tarski, A. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, CA, 1951.

    Google Scholar 

  87. Veblen, O. “Continuous increasing functions of finite and transfinite ordinals”. Transactions of the American Mathematical Society, Vol. 9 (1908), pp. 280–292.

    Google Scholar 

  88. Weyhrauch, R. W. “Some notes on ordinals up to Γ0”, Informal note 13, Stanford University, Stanford, CA, March 1978.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Illinois at Urbana-Champaign, 61801, Urbana, Illinois, USA

    Nachum Dershowitz

Authors
  1. Nachum Dershowitz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jean-Pierre Jouannaud

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dershowitz, N. (1985). Termination. In: Jouannaud, JP. (eds) Rewriting Techniques and Applications. RTA 1985. Lecture Notes in Computer Science, vol 202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15976-2_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-15976-2_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-15976-6

  • Online ISBN: 978-3-540-39679-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation