Skip to main content
SpringerLink
Log in

Normalization by leftmost innermost rewriting

  • Applications to Logic Programming, Normalization Strategies and Unification
  • Conference paper
  • First Online:
Conditional Term Rewriting Systems (CTRS 1992)

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

Included in the following conference series:

Abstract

We define a transformation of rewrite systems that allows one to compute the normal form of a term in the source system by leftmost innermost rewriting of a corresponding term in the target system. This transformation is the foundation of an implementation technique used in an application of rewriting to software development. We also show in an example how our transformation accommodates lazy, non-deterministic computations in an eager, deterministic programming language.

Supported by the National Science Foundation grant CCR-8908565.

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. S. Antoy and R. Hamlet. Automatically checking an implementation against its formal specification. In R. Selby, editor, Irvine Software Symposium, pages 29–48, Irvine, CA, March 1992.

    Google Scholar 

  2. Sergio Antoy. Definitional trees. In ALP'92, Volterra, Italy, September 1992. (to appear).

    Google Scholar 

  3. Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In PLILP'91, pages 1–13, Passau, Germany, August 1991. Lect. Notes in Comp. Sci., Vol. 528.

    Google Scholar 

  4. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pages 243–320. North Holland, Amsterdam, 1990.

    Google Scholar 

  5. Alfons Geser, Heinrich Hussmann, and Andreas Mück. A compiler for a class of conditional term rewriting systems. In S. Kaplan and J.-P. Jouannaud, editors, CTRS'87, pages 84–90, Orsay, France, July 1987. LNCS 308.

    Google Scholar 

  6. J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In R. T. Yeh, editor, Current Trends in Programming Methodology, volume 4, pages 80–149. Prentice-Hall, Englewood Cliff, NJ, 1978.

    Google Scholar 

  7. Joseph A. Goguen and Timothy Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI International, Menlo Park, CA, 1988.

    Google Scholar 

  8. J. V. Guttag. Abstract data types and the development of data structures. Comm. of the ACM, 20:396–404, 1977.

    Google Scholar 

  9. Ellis Horowitz. Fundamentals of Programming Languages. Computer Science Press, Rockville, MD, second edition, 1984.

    Google Scholar 

  10. Gérard Huet and Jean-Marie Hullot. Proofs by induction in equational theories with constructors. JCSS, 25:239–266, 1982.

    Google Scholar 

  11. Gérard Huet and Jean-Jacques Lévy. Call by need computations in non-ambiguous linear term rewriting systems. Technical Report 359, INRIA, Le Chesnay, France, 1979.

    Google Scholar 

  12. Stéphane Kaplan. A compiler for conditional term rewriting systems. In P. Lescanne, editor, RTA'87, pages 25–41, Bordeaux, France, May 1987. LNCS 256.

    Google Scholar 

  13. J. R. Kennaway. The specificity rule for lazy pattern-matching in ambiguous term rewrite systems. In Third European Symp. on Programming, pages 256–270, 1990. LNCS 432.

    Google Scholar 

  14. H. Klaeren and K. Indermark. Efficient implementation of an algebraic specification language. In M. Wirsing and J. A. Bergstra, editors, Algeraic Methods: Theory, Tools and Applications, pages 69–90, Passau, Germany, June 1987. LNCS 394.

    Google Scholar 

  15. Jan Willem Klop. Term rewriting systems. Technical Report CS-R9073, Stichting Mathematisch Centrum, Amsterdam, The Netherlands, 1990.

    Google Scholar 

  16. J. C. Knight and N. G. Leveson. An experimental evaluation of the assumption of independence in multi-version programming. IEEE Trans. on Soft. Eng., 12:96–109, 1986.

    Google Scholar 

  17. Michael J. O'Donnell. Computing in systems described by equations. Springer-Verlag, 1977. Lect. Notes in Comp. Sci., Vol. 58.

    Google Scholar 

  18. R. C. Sekar and I. V. Ramakrishnan. Programming in equational logic: Beyond strong sequentiality. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 230–241, Philadelphia, PA, June 1990.

    Google Scholar 

  19. B. Stroustrup. The C++ Programming Language. Addison-Wesley, Reading, MA, 1986.

    Google Scholar 

  20. Yonggong Yan. Building definitional trees. Master's project, Portland Stale University, Portland, OR, March 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Portland State University, 97207-0751, Portland, Oregon

    Sergio Antoy

Authors
  1. Sergio Antoy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michaël Rusinowitch Jean-Luc Rémy

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Antoy, S. (1993). Normalization by leftmost innermost rewriting. In: Rusinowitch, M., Rémy, JL. (eds) Conditional Term Rewriting Systems. CTRS 1992. Lecture Notes in Computer Science, vol 656. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56393-8_36

Download citation

  • DOI: https://doi.org/10.1007/3-540-56393-8_36

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-47549-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation