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.
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.
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.
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
FranÇois Bellegarde and Pierre Lescanne. Termination by completion. Applicable Algebra in Engineering, Communication and Computing, 1990.
Michel Bidoit. Une méthode de présentation de types abstraits: Applications. PhD thesis, Université de Paris-Sud, Orsay, France, June 1981. Rapport 3045.
J. M. Cadiou. Recursive Definitions of Partial Functions and their Computations. PhD thesis, Stanford University, Stanford, CA, March 1972.
Alonzo Church. The Calculi of Lambda Conversion, volume 6 of Ann. Mathematics Studies. Princeton University Press, Princeton, NJ, 1941.
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.
Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, March 1982.
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.
Nachum Dershowitz. Hierarchical termination. Unpublished report, Leibnitz Center for Research in Computer Science, Hebrew University, Jerusalem, Israel, December 1992.
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.
Nachum Dershowitz and Charles Hoot. Natural termination. Theoretical Computer Science, 142(2):179–207, May 1995.
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.
Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, August 1979.
K. Drosten. Termersetzungssysteme. PhD thesis, Universitat Passau, Berlin, Germany, 1989. Informatik Fachberichte 210, Springer-Verlag.
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.
Alfons Geser. Termination Relative. PhD thesis, Universität Passau, Passau, West Germany, 1989.
Oliver Geupel. Overlap closures and termination of term rewriting systems. Report MIP-8922, Universität Passau, Passau, West Germany, July 1989.
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.
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.
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.
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.
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).
M. R. K. Krishna Rao. Modular proofs for completeness of hierarchical systems. Unpublished report, December 1992.
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.
Masahito Kurihara and Ikuo Kaji. Modular term rewriting systems and the termination. Information Processing Letters, 34:1–4, February 1990.
Masahito Kurihara and Azuma Ohuchi. Modularity of simple termination of term rewriting systems. Journal of Information Processing Society, 34:632–642, 1990.
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.
Aart Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Vrije Universiteit, Amsterdam, The Netherlands, 1990.
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.
Michael J. O'Donnell. Computing in systems described by equations, volume 58 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1977.
Enno Ohlebusch. On the modularity of termination of term rewriting systems. Report 11, Abteilung Informationstechnik, Universität Bielefeld, Bielefeld, Germany, 1993.
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.
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.
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.
Michael Rusinowitch. On termination of the direct sum of term-rewriting systems. Information Processing Letters, 26:65–70, 1987.
Yoshihito Toyama. Counterexamples to termination for the direct sum for the direct sum of term rewriting systems. Information Processing Letters, 25:141–143, 1987.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights 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