Skip to main content
SpringerLink
Log in

Simplification orders for term graph rewriting

  • Contributed Papers
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1997 (MFCS 1997)

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

Abstract

Term graph rewriting differs from term rewriting in that common subexpressions can be shared, improving the efficiency of rewriting in space and time. Moreover, computations by term graph rewriting terminate more often than computations by term rewriting. In this paper, simplification orders on term graphs are introduced as a means for proving termination of term graph rewriting. Simplification orders are based on an extension of the homeomorphic embedding relation from trees to term graphs. By generalizing Kruskal's Tree Theorem to term graphs, it is shown that simplification orders are well-founded. Then a recursive path order on term graphs is defined by analogy with the well-known order on terms, and is shown to be a simplification order. Examples of termination proofs with the recursive path order are given for rewrite systems that are non-terminating under term rewriting.

On leave from Universität Bremen, Germany. Author's research is partially supported by the HCM Network EXPRESS, the ESPRIT Working Group APPLIGRAPH, and the TMR Network GETGRATS.

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. Zena M. Ariola and Jan Willem Klop. Equational term graph rewriting. Fundamenta Informaticae, 26:207–240, 1996.

    Google Scholar 

  2. Andrea Corradini and Francesca Rossi. Hyperedge replacement jungle rewriting for term rewriting systems and logic programming. Theoretical Computer Science, 109:7–48, 1993.

    Article  Google Scholar 

  3. Nachum Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17:279–301, 1982.

    Article  Google Scholar 

  4. Nachum Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69–116, 1987.

    Google Scholar 

  5. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6. Elsevier, 1990.

    Google Scholar 

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

    Article  Google Scholar 

  7. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(2):326–336, 1952.

    Google Scholar 

  8. Berthold Hoffmann and Detlef Plump. Implementing term rewriting by jungle evaluation. RAIRO Theoretical Informatics and Applications, 25(5):445–472, 1991.

    Google Scholar 

  9. Richard Kennaway, Jan Willem Klop, Ronan Sleep, and Fer-Jan de Vries. On the adequacy of term graph rewriting for simulating term rewriting. ACM Transactions on Programming Languages and Systems, 16(3):493–523, 1994.

    Article  Google Scholar 

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

    Google Scholar 

  11. Joseph B. Kruskal. Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210–225, 1960.

    Google Scholar 

  12. Aart Middeldorp and Hans Zantema. Simple termination revisited. In Proc. 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 451–465. Springer-Verlag, 1994.

    Google Scholar 

  13. C. St. J. A. Nash-Williams. On well-quasi-ordering finite trees. Proceedings of the Cambridge Philosophical Society, 59:833–835, 1963.

    Google Scholar 

  14. David A. Plaisted. Equational reasoning and term rewriting systems. In Dov M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, pages 273–364. Clarendon Press, 1993.

    Google Scholar 

  15. Detlef Plump. Collapsed tree rewriting: Completeness, confluence, and modularity. In Proc. Conditional Term Rewriting Systems, volume 656 of Lecture Notes in Computer Science, pages 97–112. Springer-Verlag, 1993.

    Google Scholar 

  16. Detlef Plump. Evaluation of functional expressions by hypergraph rewriting. Dissertation, Universität Bremen, Fachbereich Mathematik und Informatik, 1993.

    Google Scholar 

  17. Ronan Sleep, Rinus Plasmeijer, and Marko van Eekelen, editors. Term Graph Rewriting: Theory and Practice. John Wiley, 1993.

    Google Scholar 

  18. Joachim Steinbach. Simplification orderings — history of results. Fundamenta Informaticae, 24:47–87, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, Kruislaan 413, 1098, SJ Amsterdam, The Netherlands

    Detlef Plump

Authors
  1. Detlef Plump
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Igor Prívara Peter Ružička

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Plump, D. (1997). Simplification orders for term graph rewriting. In: Prívara, I., Ružička, P. (eds) Mathematical Foundations of Computer Science 1997. MFCS 1997. Lecture Notes in Computer Science, vol 1295. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0029989

Download citation

  • DOI: https://doi.org/10.1007/BFb0029989

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63437-9

  • Online ISBN: 978-3-540-69547-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation