Skip to main content
SpringerLink
Log in

Transforming termination by self-labelling

  • Session 5B
  • Conference paper
  • First Online:
Automated Deduction — Cade-13 (CADE 1996)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1104))

Included in the following conference series:

Abstract

We introduce a new technique for proving termination of term rewriting systems. The technique, a specialization of Zantema's semantic labelling technique, is especially useful for establishing the correctness of transformation methods that attempt to prove termination by transforming term rewriting systems into systems whose termination is easier to prove. We apply the technique to modularity, distribution elimination, and currying, resulting in new results, shorter correctness proofs, and a positive solution to an open problem.

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. F. Bellegarde and P. Lescanne, Termination by Completion, Applicable Algebra in Engineering, Communication and Computing 1 (1990) 79–96.

    Google Scholar 

  2. L. Bachmair and N. Dershowitz, Commutation, Transformation, and Termination, Proceedings of the 8th Conference on Automated Deduction, Oxford, Lecture Notes in Computer Science 230 (1986) 5–20.

    Google Scholar 

  3. N. Dershowitz, Orderings for Term-Rewriting Systems, Theoretical Computer Science 17 (1982) 279–301.

    Article  Google Scholar 

  4. N. Dershowitz, Termination of Rewriting, Journal of Symbolic Computation 3 (1) (1987) 69–116.

    Google Scholar 

  5. N. Dershowitz, Hierarchical Termination, Proceedings of the 4th International Workshop on Conditional (and Typed) Rewriting Systems, Jerusalem, Lecture Notes in Computer Science 968 (1995) 89–105.

    Google Scholar 

  6. N. Dershowitz and J.-P. Jouannaud, Rewrite Systems, in: Handbook of Theoretical Computer Science, Vol. B (ed. J. van Leeuwen), North-Holland (1990) 243–320.

    Google Scholar 

  7. M.C.F. Ferreira, Termination of Rewriting: Well-foundedness, Totality and Transformations, Ph.D. thesis, University of Utrecht, 1995.

    Google Scholar 

  8. M.C.F. Ferreira and H. Zantema, Dummy Elimination: Making Termination Easier, Proceedings of the 10th International Conference on Fundamentals of Computation Theory, Dresden, Lecture Notes in Computer Science 965 (1995) 243–252.

    Google Scholar 

  9. S. Kamin and J.J. Lévy, Two Generalizations of the Recursive Path Ordering, unpublished manuscript, University of Illinois, 1980.

    Google Scholar 

  10. J.R. Kennaway, J.W. Klop, R. Sleep, and F.-J. de Vries, On Comparing Curried and Uncurried Rewrite Systems, report CS-R9350, CWI, Amsterdam, 1993. To appear in the Journal of Symbolic Computation.

    Google Scholar 

  11. J.W. Klop, Term Rewriting Systems, in: Handbook of Logic in Computer Science, Vol. II (eds. S. Abramsky, D. Gabbay and T. Maibaum), Oxford University Press (1992) 1–116.

    Google Scholar 

  12. M.R.K. Krishna Rao, Modular Proofs for Completeness of Hierarchical Term Rewriting Systems, Theoretical Computer Science 151 (1995) 487–512.

    Article  Google Scholar 

  13. M.R.K. Krishna Rao, Simple Termination of Hierarchical Combinations of Term Rewriting Systems, Proceedings of the 2nd International Symposium on Theoretical Aspects of Computer Software, Sendai, Lecture Notes in Computer Science 789 (1994) 203–223.

    Google Scholar 

  14. A. Middeldorp, A Sufficient Condition for the Termination of the Direct Sum of Term Rewriting Systems, Proceedings of the 4th IEEE Symposium on Logic in Computer Science, Pacific Grove (1989) 396–401.

    Google Scholar 

  15. E. Ohlebusch, Modular Properties of Composable Term Rewriting Systems, Ph.D. thesis, Universität Bielefeld, 1994.

    Google Scholar 

  16. Y. Toyama, On the Church-Rosser Property for the Direct Sum of Term Rewriting Systems, Journal of the ACM 34 (1) (1987) 128–143.

    Article  Google Scholar 

  17. Y. Toyama, Counterexamples to Termination for the Direct Sum of Term Rewriting Systems, Information Processing Letters 25 (1987) 141–143.

    Article  Google Scholar 

  18. H. Zantema, Termination of Term Rewriting by Semantic Labelling, Fundamenta Informaticae 24 (1995) 89–105.

    Google Scholar 

  19. H. Zantema, Termination of Term Rewriting: Interpretation and Type Elimination, Journal of Symbolic Computation 17 (1994) 23–50.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Information Sciences and Electronics, University of Tsukuba, 305, Tsukuba, Japan

    Aart Middeldorp & Hitoshi Ohsaki

  2. Department of Computer Science, Utrecht University, P.O. Box 80.089, 3508, TB Utrecht, The Netherlands

    Hans Zantema

Authors
  1. Aart Middeldorp
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hitoshi Ohsaki
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hans Zantema
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

M. A. McRobbie J. K. Slaney

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Middeldorp, A., Ohsaki, H., Zantema, H. (1996). Transforming termination by self-labelling. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_101

Download citation

  • DOI: https://doi.org/10.1007/3-540-61511-3_101

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-68687-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation