Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Generalizing Newman’s Lemma for Left-Linear Rewrite Systems

  • Conference paper
Term Rewriting and Applications (RTA 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4098))

Included in the following conference series:

Abstract

Confluence criteria for non-terminating rewrite systems are known to be rare and notoriously difficult to obtain. Here we prove a new result in this direction. Our main result is a generalized version of Newman’s Lemma for left-linear term rewriting systems that does not need a full termination assumption. We discuss its relationships to previous confluence criteria, its restrictions, examples of application as well as open problems. The whole approach is developed in the (more general) framework of context-sensitive rewriting which thus turns out to be useful also for ordinary (context-free) rewriting.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baader, F., Nipkow, T.: Term rewriting and All That. Cambridge Univ. Press, Cambridge (1998)

    Google Scholar 

  2. Bezem, M., Klop, J.W., de Vrijer, R. (eds.): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science 55. Cambridge Univ. Press, Cambridge (2003)

    Google Scholar 

  3. Borralleras, C., Lucas, S., Rubio, A.: Recursive path orderings can be context-sensitive. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 314–331. Springer, Heidelberg (2002)

    Google Scholar 

  4. Dershowitz, N., Kaplan, S., Plaisted, D.A.: Rewrite, rewrite, rewrite, rewrite, rewrite,.. Theoretical Computer Science 83(1), 71–96 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  5. Giesl, J., Middeldorp, A.: Transformation techniques for context-sensitive rewrite systems. Journal of Functional Programming 14(4), 379–427 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  6. Godoy, G., Tiwari, A.: Confluence of Shallow Right-Linear Rewrite Systems. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 541–556. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Godoy, G., Tiwari, A., Verma, R.M.: On the confluence of linear shallow term rewrite systems. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 85–96. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Gramlich, B.: Confluence without termination via parallel critical pairs. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 211–225. Springer, Heidelberg (1996)

    Google Scholar 

  9. Gramlich, B., Lucas, S.: Modular termination of context-sensitive rewriting. In: Kirchner, C. (ed.) Proc. 4th PPDP, Pittsburgh, PA, USA, pp. 50–61. ACM Press, New York (2002)

    Google Scholar 

  10. Hindley, J.R.: An abstract Church–Rosser theorem, part ii: Applications. Journal of Symbolic Logic 39, 1–21 (1974)

    Article  MATH  MathSciNet  Google Scholar 

  11. Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM 27(4), 797–821 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  12. Kennaway, R., Klop, J.W., Sleep, R., de Vries, F.-J.: Transfinite reductions in orthogonal term rewriting systems. Information and Computation 119(1), 18–38 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  13. Klop, J.W.: Term rewriting systems. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, ch. 1, vol. 1, pp. 2–117. Clarendon Press, Oxford (1992)

    Google Scholar 

  14. Klop, J.W., Middeldorp, A., Toyama, Y., de Vrijer, R.: Modularity of confluence: A simplified proof. Information Processing Letters 49, 101–109 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  15. Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming 1998(1), 1–61 (1998)

    Google Scholar 

  16. Lucas, S.: Transfinite rewriting semantics for term rewriting systems. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 216–230. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Lucas, S.: Context-sensitive rewriting strategies. Information and Computation 178(1), 294–343 (2002)

    MATH  MathSciNet  Google Scholar 

  18. Lucas, S.: Polynomials over the reals in proofs of termination: From theory to practice. RAIRO Theoretical Informatics and Applications 39(3), 547–586 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  19. Newman, M.H.A.: On theories with a combinatorial definition of equivalence. Annals of Mathematics 43(2), 223–242 (1942)

    Article  MathSciNet  Google Scholar 

  20. Ohlebusch, E.: Modular properties of composable term rewriting systems. Journal of Symbolic Computation 20(1), 1–42 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  21. Okui, S.: Simultaneous critical pairs and Church-Rosser property. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 2–16. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  22. van Oostrom, V.: Confluence by decreasing diagrams. Theoretical Computer Science 126(2), 259–280 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  23. van Oostrom, V.: Developing developments. Theoretical Computer Science 175(1), 159–181 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  24. Oyamaguchi, M., Ohta, Y.: A new parallel closed condition for Church–Rosser of left-linear term rewriting systems. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 187–201. Springer, Heidelberg (1997)

    Google Scholar 

  25. Raoult, J.C., Vuillemin, J.: Operational and semantic equivalence between recursive programs. Journal of the ACM 27(4), 772–796 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  26. Rosen, B.K.: Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM 20, 160–187 (1973)

    Article  MATH  Google Scholar 

  27. Toyama, Y.: On the Church–Rosser property of term rewriting systems. ECL Technical Report 17672, NTT (in Japanese) (December 1981)

    Google Scholar 

  28. Toyama, Y.: On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM 34(1), 128–143 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  29. Toyama, Y., Oyamaguchi, M.: Church–Rosser property and unique normal form property of non-duplicating term rewriting systems. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 316–331. Springer, Heidelberg (1995)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9 – E185/2, A-1040, Wien, Austria

    Bernhard Gramlich

  2. DSIC, Universidad Politécnica de Valencia, Camino de Vera s/n, 46022, Valencia, Spain

    Salvador Lucas

Authors
  1. Bernhard Gramlich
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Salvador Lucas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Carnegie Mellon University,  

    Frank Pfenning

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gramlich, B., Lucas, S. (2006). Generalizing Newman’s Lemma for Left-Linear Rewrite Systems. In: Pfenning, F. (eds) Term Rewriting and Applications. RTA 2006. Lecture Notes in Computer Science, vol 4098. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11805618_6

Download citation

  • DOI: https://doi.org/10.1007/11805618_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-36834-2

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation