Nothing Special   »   [go: up one dir, main page]

Skip to main content

Normalisation in Weakly Orthogonal Rewriting

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1999)

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

Included in the following conference series:

Abstract

A rewrite sequence is said to be outermost-fair if every outermost redex occurrence is eventually eliminated. Outermost-fair rewriting is known to be (head-)normalising for almost orthogonal rewrite systems. We study (head-)normalisation for the larger class of weakly orthogonal rewrite systems. (Infinitary) normalisation is established and a counterexample against head-normalisation is given.

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

Access this chapter

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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.

Similar content being viewed by others

References

  1. Sergio Antoy and Aart Middeldorp. A sequential reduction strategy. Theoretical Computer Science, 165(1):75–95, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  2. H.P. Barendregt. The Lambda Calculus, Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, revised edition, 1984.

    Google Scholar 

  3. Inge Bethke, Jan Willem Klop, and Roel de Vrijer. Descendants and origins in term rewriting. IR 458, Vrije Universiteit, Amsterdam, December 1998.

    Google Scholar 

  4. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, February 1998.

    Google Scholar 

  5. G. Boudol. Computational semantics of term rewriting systems. In M. Nivat and J.C. Reynolds, editors, Algebraic Methods in Semantics, pages 169–236. Cambridge University Press, 1985.

    Google Scholar 

  6. Alonzo Church. The Calculi of Lambda-Conversion. Princeton University Press, Princeton, New Jersey, 1941. Second Printing 1951.

    Google Scholar 

  7. Alonzo Church and J.B. Rosser. Some properties of conversion. Transactions of the American Mathematical Society, 39:472–482, January to June 1936.

    Article  MATH  MathSciNet  Google Scholar 

  8. John Glauert and Zurab Khasidashvili. Relative normalization in orthogonal expression reduction systems. In CTRS’94, volume 968 of Lecture Notes in Computer Science, pages 144–165. Springer, 1994.

    Google Scholar 

  9. Georges Gonthier, Jean-Jacques Lévy, and Paul-André Melliès. An abstract standardisation theorem. In Proceedings of the 7th IEEE Symposium on Logic in Computer Science, pages 72–81, 1992.

    Google Scholar 

  10. Bernhard Gramlich. Termination and Confluence Properties of Structured Rewrite Systems. PhD thesis, Universität Kaiserslautern, 19. Januar 1996.

    Google Scholar 

  11. G_erard Huet and Jean-Jacques Lévy. Computations in orthogonal rewriting systems, I. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  13. J.W. Klop. Combinatory Reduction Systems. PhD thesis, Rijksuniversiteit Utrecht, June 1980. Mathematical Centre Tracts 127.

    Google Scholar 

  14. Jean-Jacques Lévy. Réductions correctes et optimales dans le λ-calcul. Thèse de doctorat d’etat, Université Paris VII, 1978.

    Google Scholar 

  15. Paul-André Melliès. Axiomatic rewriting theory III, a factorisation theorem in rewriting theory. In CTCS’97, volume 1290 of Lecture Notes in Computer Science, pages 49–68. Springer, 1997.

    Google Scholar 

  16. Paul-André Melliès. Axiomatic rewriting theory IV, a stability theorem in rewriting theory. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science, pages 287–298, 1998.

    Google Scholar 

  17. Aart Middeldorp. Call by need computations to root-stable form. In Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, pages 94–105, 1997.

    Google Scholar 

  18. Tobias Nipkow. Higher-order critical pairs. In Proceedings of the 6th IEEE Symposium on Logic in Computer Science, pages 342–349, 1991.

    Google Scholar 

  19. M.J. O’Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer Verlag, 1977.

    MATH  Google Scholar 

  20. Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, March 1994.

    Google Scholar 

  21. Vincent van Oostrom. Finite family developments. In RTA’97, volume 1232 of Lecture Notes in Computer Science, pages 308–322. Springer, 1997.

    Google Scholar 

  22. Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall International, 1987.

    Google Scholar 

  23. Femke van Raamsdonk. Confluence and Normalisation for Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, May 1996.

    Google Scholar 

  24. Femke van Raamsdonk. Outermost-fair rewriting. In TLCA’97, volume 1210 of Lecture Notes in Computer Science, pages 284–299. Springer, 1997.

    Google Scholar 

  25. J.B. Rosser. A mathematical logic without variables I. Annals of Mathematics, 36:127–150, 1935.

    Article  MathSciNet  Google Scholar 

  26. R.C. Sekar and I.V. Ramakrishnan. Programming in equational logic: Beyond strong sequentiality. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science, pages 230–241, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van Oostrom, V. (1999). Normalisation in Weakly Orthogonal Rewriting. In: Narendran, P., Rusinowitch, M. (eds) Rewriting Techniques and Applications. RTA 1999. Lecture Notes in Computer Science, vol 1631. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48685-2_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-48685-2_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66201-3

  • Online ISBN: 978-3-540-48685-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics