Skip to main content
SpringerLink
Log in

Hierarchical termination

  • Conference paper
  • First Online:
Conditional and Typed Rewriting Systems (CTRS 1994)

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

Included in the following conference series:

Abstract

From a practical perspective, it is important for programs to have modular correctness properties. Some (largely syntactic) sufficient conditions are given here for the union of terminating rewrite systems to be terminating, particularly in the hierarchical case, when one of the systems makes no reference to functions defined by the other.

This research was supported in part by the U. S. National Science Foundation under Grants CCR-90-07195 and CCR-90-24271, by a Lady Davis fellowship at the Hebrew University of Jerusalem, Israel, and by a Meyerhoff Visiting Professorship at the Weizmann Institute of Science, Rehovot, Israel.

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. Jürgen Avenhaus and Klaus Madlener. Term rewriting and equational reasoning. In R. B. Banerji, editor, Formal Techniques in Artificial Intelligence: A Sourcebook, pages 1–41. Elsevier, Amsterdam, 1990.

    Google Scholar 

  2. Leo Bachmair and Nachum Dershowitz. Commutation, transformation, and termination. In J. H. Siekmann, editor, Proceedings of the Eighth International Conference on Automated Deduction (Oxford, England), volume 230 of Lecture Notes in Computer Science, pages 5–20, Berlin, July 1986. Springer-Verlag.

    Google Scholar 

  3. FranÇois Bellegarde and Pierre Lescanne. Termination by completion. Applicable Algebra in Engineering, Communication and Computing, 1990.

    Google Scholar 

  4. Michel Bidoit. Une méthode de présentation de types abstraits: Applications. PhD thesis, Université de Paris-Sud, Orsay, France, June 1981. Rapport 3045.

    Google Scholar 

  5. J. M. Cadiou. Recursive Definitions of Partial Functions and their Computations. PhD thesis, Stanford University, Stanford, CA, March 1972.

    Google Scholar 

  6. Alonzo Church. The Calculi of Lambda Conversion, volume 6 of Ann. Mathematics Studies. Princeton University Press, Princeton, NJ, 1941.

    Google Scholar 

  7. Nachum Dershowitz. Termination of linear rewriting systems. In Proceedings of the Eighth International Colloquium on Automata, Languages and Programming (Acre, Israel), volume 115 of Lecture Notes in Computer Science, pages 448–458, Berlin, July 1981. European Association of Theoretical Computer Science, Springer-Verlag.

    Google Scholar 

  8. Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, March 1982.

    Article  Google Scholar 

  9. Nachum Dershowitz. Termination of rewriting. J. Symbolic Computation, 3(1&2):69–115, February/April 1987. Corrigendum: 4, 3 (December 1987), 409–410; reprinted in Rewriting Techniques and Applications, J.-P. Jouannaud, ed., pp. 69–115, Academic Press, 1987.

    Google Scholar 

  10. Nachum Dershowitz. Hierarchical termination. Unpublished report, Leibnitz Center for Research in Computer Science, Hebrew University, Jerusalem, Israel, December 1992.

    Google Scholar 

  11. Nachum Dershowitz. 33 examples of termination. In H. Comon and J.-P. Jouannaud, editors, French Spring School of Theoretical Computer Science Advanced Course on Term Rewriting (Font Romeux, France, May 1993), volume 909 of Lecture Notes in Computer Science, pages 16–26, Berlin, 1995. Springer-Verlag.

    Google Scholar 

  12. Nachum Dershowitz and Charles Hoot. Natural termination. Theoretical Computer Science, 142(2):179–207, May 1995.

    Article  Google Scholar 

  13. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–320. North-Holland, Amsterdam, 1990.

    Google Scholar 

  14. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, August 1979.

    Article  Google Scholar 

  15. K. Drosten. Termersetzungssysteme. PhD thesis, Universitat Passau, Berlin, Germany, 1989. Informatik Fachberichte 210, Springer-Verlag.

    Google Scholar 

  16. Maribel Fernandez and Jean-Pierre Jouannaud. Modular termination of term rewriting systems revisited. In Proceedings of the Eleventh Workshop on Specification of Abstract Data Types (Santa Margherita de Ligura, Italy), Lecture Notes in Computer Science, Berlin, 1995. Springer-Verlag.

    Google Scholar 

  17. Alfons Geser. Termination Relative. PhD thesis, Universität Passau, Passau, West Germany, 1989.

    Google Scholar 

  18. Oliver Geupel. Overlap closures and termination of term rewriting systems. Report MIP-8922, Universität Passau, Passau, West Germany, July 1989.

    Google Scholar 

  19. Bernhard Gramlich. Generalized sufficient conditions for modular termination of rewriting. Applicable Algebra in Engineering, Communication and Computing, 5:131–158, 1994. A preliminary version appeared in the Proceedings of the Third Internationnal Conference on Algebraic and Logic Programming, Lecture Notes in Computer Science 632, Springer-Verlag, Berlin, pp. 53–68, 1992.

    Google Scholar 

  20. Bernhard Gramlich. Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae, September 1995. Preliminary versions appeared as “Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems” in Proceedings of the Conference on Logic Programming and Automated Reasoning (St. Petersburg, Russia), A. Voronkov, ed., Lecture Notes in Artificial Intelligence 624, Springer-Verlag, Berlin, pp. 285–296 and as SEKI-Report SR-93-09, Fachbereich Informatik, Universität Kaiserslautern, Kaiserslautern, Germany, 1993.

    Google Scholar 

  21. Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. of the Association for Computing Machinery, 27(4):797–821, October 1980.

    Google Scholar 

  22. Jan Willem Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–117. Oxford University Press, Oxford, 1992.

    Google Scholar 

  23. Donald E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, U. K., 1970. Reprinted in Automation of Reasoning 2, Springer-Verlag, Berlin, pp. 342–376 (1983).

    Google Scholar 

  24. M. R. K. Krishna Rao. Modular proofs for completeness of hierarchical systems. Unpublished report, December 1992.

    Google Scholar 

  25. M. R. K. Krishna Rao. Completeness of hierarchical combinatins of term rewriting systems. In Proceedings of the Thirteenth Conference on Foundations of Software Technology and Theoretical Computer Science (Bombay, India), volume 761 of Lecture Notes in Computer Science, pages 125–138, Berlin, 1993. Springer-Verlag.

    Google Scholar 

  26. Masahito Kurihara and Ikuo Kaji. Modular term rewriting systems and the termination. Information Processing Letters, 34:1–4, February 1990.

    Article  MathSciNet  Google Scholar 

  27. Masahito Kurihara and Azuma Ohuchi. Modularity of simple termination of term rewriting systems. Journal of Information Processing Society, 34:632–642, 1990.

    Google Scholar 

  28. Aart Middeldorp. A sufficient condition for the termination of the direct sum of term rewriting systems. In Proceedings of the Fourth Symposium on Logic in Computer Science, pages 396–401, Pacific Grove, CA, 1989. IEEE.

    Google Scholar 

  29. Aart Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Vrije Universiteit, Amsterdam, The Netherlands, 1990.

    Google Scholar 

  30. Aart Middeldorp and Yoshihito Toyama. Completeness of combinations of constructor systems. In R. Book, editor, Proceedings of the Fourth International Conference on Rewriting Techniques and Applications (Como, Italy), volume 488 of Lecture Notes in Computer Science, pages 174–187, Berlin, April 1991. Springer-Verlag.

    Google Scholar 

  31. Michael J. O'Donnell. Computing in systems described by equations, volume 58 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1977.

    Google Scholar 

  32. Enno Ohlebusch. On the modularity of termination of term rewriting systems. Report 11, Abteilung Informationstechnik, Universität Bielefeld, Bielefeld, Germany, 1993.

    Google Scholar 

  33. Alberto Pettorossi. Comparing and putting together recursive path orderings, simplification orderings and non-ascending property for termination proofs of term rewriting systems. In Proceedings of the Eighth EATCS International Colloquium on Automata, Languages and Programming (Acre, Israel), volume 115 of Lecture Notes in Computer Science, pages 432–447, Berlin, July 1981. Springer-Verlag.

    Google Scholar 

  34. David A. Plaisted. Equational reasoning and term rewriting systems. In D. Gabbay, C. Hogger, J. A. Robinson, and J. Siekmann, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, chapter 5, pages 273–364. Oxford University Press, Oxford, 1993.

    Google Scholar 

  35. Jean-Claude Raoult and Jean Vuillemin. Operational and semantic equivalence between recursive programs. J. of the Association for Computing Machinery, 27(4):772–796, October 1980.

    Google Scholar 

  36. Michael Rusinowitch. On termination of the direct sum of term-rewriting systems. Information Processing Letters, 26:65–70, 1987.

    Article  Google Scholar 

  37. Yoshihito Toyama. Counterexamples to termination for the direct sum for the direct sum of term rewriting systems. Information Processing Letters, 25:141–143, 1987.

    Article  Google Scholar 

  38. Yoshihito Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. J. of the Association for Computing Machinery, 34(1):128–143, January 1987.

    Google Scholar 

  39. Yoshihito Toyama, Jan Willem Klop, and Hendrik Pieter Barendregt. Termination for the direct sum of left-linear term rewriting systems. In Nachum Dershowitz, editor, Proceedings of the Third International Conference on Rewriting Techniques and Applications (Chapel Hill, NC), volume 355 of Lecture Notes in Computer Science, pages 477–491, Berlin, April 1989. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Illinois at Urbana-Champaign, 1304 West Springfield Avenue, 61801, Urbana, IL, USA

    Nachum Dershowitz

Authors
  1. Nachum Dershowitz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Nachum Dershowitz Naomi Lindenstrauss

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dershowitz, N. (1995). Hierarchical termination. In: Dershowitz, N., Lindenstrauss, N. (eds) Conditional and Typed Rewriting Systems. CTRS 1994. Lecture Notes in Computer Science, vol 968. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60381-6_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-60381-6_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60381-8

  • Online ISBN: 978-3-540-45513-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation