Abstract
We define a strong and versatile termination order for term rewriting systems, called theImproved General Path Order, which simplifies and strengthens Dershowitz/Hoot's General Path Order. We demonstrate the power of the Improved General Path Order by proofs of termination of non-trivial examples, among them a medium-scale term rewriting system that models a lift control.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Arts, T., Zantema, H.: Termination of logic programs via labelled term rewriting systems. Technical Report UU-CS-1994-20, Universiteit Utrecht, The Netherlands, 1994
Avenhaus, J., Madlener, K.: Term rewriting and equational reasoning. In: Banerji, R. B. (ed) Formal Techniques in Artificial Intelligence: A Source-Book. Elsevier Science Publishers, North-Holland, 1990
Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Ait-Kaci, H., Nivat, M. (eds) Resolution of Equations in Algebraic Structures 2: Rewriting Techniques, pages 1–30. Academic Press, 1989
Bellegarde, F., Lescanne, P.: Termination by completion. AAECC 1, 79–96 (1990)
Broy, M.: An example for the design of distributed systems in a formal setting: The lift problem. Technical Report MIP-8804, Universität Passau, Germany, 1988
Dauchet, M.: Simulation of Turing machines by a regular rule. Theoret. Comput. Sci.,103, 409–420 (1992)
Dershowitz, N.: A note on simplification orderings. Inform. Process. Lett.9, 212–215, 1979
Dershowitz, N.: Orderings for term rewriting systems. Theoret. Comput. Sci.17(3), 279–301 (March 1982)
Dershowitz, N.: Termination of rewriting. J. Symb. Comput.3(1–2), 69–115, Feb./April 1987. Corrigendum: 4 (3), 409–410, Dec. 1987
Dershowitz, N., Hoot, C.: Topics in termination. In: Kirchner, C. (ed), 5th Int. Conf. Rewriting Techniques and Applications, pp. 198–212. LNCS vol. 690, Berlin, Heidelberg, New York: Springer 1993
Dershowitz, N., Hoot, C.: Natural termination. Theoret. Comput. Sci.142 (2), 179–207, 1995
Dershowitz, N., Jouannaud, J.-P.: Notations for rewriting. Bulletin of the EATCS,43, 162–172, (1991)
Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, volume B (Formal Models and Semantics), pp. 243–320. Elsevier — The MIT Press, 1991
Dershowitz, N., Jouannaud, J.-P., Klop, J. W.: Problems in rewriting III. In: Hsiang, J. (ed), 6th Int. Conf. Rewriting Techniques and Applications, pp. 457–471. LNCS vol. 914, Berlin, Heidelberg, New York: Springer 1995
Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM,22(8), 465–476 (1979)
Dershowitz, N., Okada, M., Sivakumar, G.: Canonical conditional rewrite systems. In 9th Int. Conf. Automated Deduction, pp 538–549. LNCS vol. 310, Berlin, Heidelberg, New York: Springer 1988
Fraus, U.: Verifying the specification of a technical software system by induction. Research report FORWISS, Universität Passau, Germany, 1992
Fraus, U., Inductive theorem proving for algebraic specifications-TIP system user's manual. Technical Report MIP-9401, Universität Passau, Germany, Feb. 1994
Geser, A.: On a monotonie semantic path ordering. Technical Report 92-13, Ulmer Informatik-Berichte, Universität Ulm, Germany, 1992
Geser, A.: An improved general path order. Technical Report MIP-9407, Universität Passau, Germany, June 1994
Hofstadter, D. R.: Gödel, Escher, Bach: An eternal golden braid. Basic Books, New York, 1979
Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. J Assoc. Comput. Mach.27, 797–821 (1980)
Huet, G., Lankford, D.: On the uniform halting problem for term rewriting systems. Technical Report 283, INRIA, Rocquencourt, FR, Mar. 1978
Huet, G., Oppen, D. C: Equations and rewrite rules — a survey. In: Book, R. (ed) Formal Languages: Perspectives and Open Problems, pp 349–405. Academic Press, 1980
Jouannaud, J.-P., Lescanne, P., Reinig, F.: Recursive decomposition ordering. In: Bjørner, D. (ed), Formal description of programming concepts 2, pp 331–348. North-Holland, 1982
Kamin, S., Lévy, J.-J.: Attempts for generalizing the recursive path orderings. Manuscript; copy available at Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign, Feb. 1980
Kapur, D., Narendran, P., Sivakumar, G.: A path ordering for proving termination of term rewriting system. In: 10th Colloquium on Trees in Algebra and Programming, pp 173–185. LNCS vol. 185, Berlin, Heidelberg, New York: Springer 1985
Klop, J. W.: Term rewrite systems. In: Abramsky, S., Gabbay, D. M., Maibaum, T. (eds), Handbook of Logic in Computer Science, volume II, pp 1–116. Clarendon Press, Oxford, UK, 1992
Knuth, D. E., Bendix, P. B.: Simple word problems in universal algebras. In: Leech, J. (ed), Computational Problems in Abstract Algebra, pp 263–297. Pergamon Press, 1970
Lankford, D. S.: On proving term rewriting systems are noetherian. Technical Report MTP-3, Louisiana Technical University, Math. Dept., Ruston, LA, 1979
Lescanne, P.: Uniform termination of term rewriting systems: Recursive decomposition ordering with status. In: Courcelle, B. (ed), 6th Colloquium on Trees in Algebra and Programming, pp 181–194, Bordeaux, France, Mar. 1984
Lescanne, P.: On the recursive decomposition ordering with lexicographic status and other related orderings. J. Automated Reasoning,6, 39–49 (1990)
Plaisted, D. A.: Term rewriting systems: In: Gabbay, D. M., Hogger, C. J., Robinson, J. A.(eds), Handbook of Logic in Artificial Intelligence and Logic Programming, volume 4, Chap. 2. Clarendon Press, Oxford, UK, 1993
Rusinowitch, M.: Path of subterms ordering and recursive decomposition ordering revisited. J. Symb. Comput,3(1–2), 117–131 (1987)
Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Inform. Process. Lett.25, 141–143 (1987)
Wirth, C.-P., Grämlich, B.: A constructor-based inductive validity in positive/negative-conditional equational specifications. J. Symb. Comput.11, 1994
Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae24, 89–105 (1995)
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Geser, A. An Improved General Path Order. AAECC 7, 469–511 (1996). https://doi.org/10.1007/BF01293264
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF01293264