[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Redex capturing in term graph rewriting (concise version)

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

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

Included in the following conference series:

Abstract

Term graphs are a natural generalization of terms in which structure sharing is allowed. Structure sharing makes term graph rewriting a time- and space-efficient method for implementing term rewrite systems. Certain structure sharing schemes can lead to a situation in which a term graph component is rewritten to another component that contains the original. This phenomenon, called redex capturing, introduces cycles into the term graph which is being rewritten—even when the graph and the rule themselves do not contain cycles. In some applications, redex capturing is undesirable, such as in contexts where garbage collectors require that graphs be acyclic. In other applications, for example in the use of the fixed-point combinator Y, redex capturing acts as a rewriting optimization. We show, using results about infinite rewritings of trees, that term graph rewriting with arbitrary structure sharing (including redex capturing) is sound for left-linear term rewrite systems.

The full version of this paper will appear in the International Journal of Foundations of Computer Science [7].

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.

Similar content being viewed by others

References

  1. H. P. Barendregt, M. C. J. D. van Elekelen, J. R. W. Glauert, J. R. Kennaway, M. J. Plasmeijer, and M. R. Sleep, “Term graph rewriting”, in PARLE — Parallel Architectures and Languages Europe, Springer Lecture Notes in Computer Science 259, (Springer-Verlag, Berlin, 1987), pp. 141–158.

    Google Scholar 

  2. M. Bickford, C. Mills, and E. A. Schneider, Clio: An applicative language-based verification system, Tech. Rep. 15-7, Odyssey Research Associates, Ithaca, NY, June 1989.

    Google Scholar 

  3. N. Dershowitz and S. Kaplan, “Rewrite, rewrite, rewrite, rewrite, rewrite, ...”, in Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989, pp. 250–259.

    Google Scholar 

  4. N. Dershowitz, S. Kaplan, and D. A. Plaisted, “Rewrite, rewrite, rewrite, rewrite, rewrite, ...”, to appear.

    Google Scholar 

  5. N. Dershowitz, S. Kaplan, and D. A. Plaisted, “Infinite normal forms”, in Proceedings of the 16th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 372, (Springer-Verlag, Berlin, 1989), pp. 249–262.

    Google Scholar 

  6. W. M. Farmer, J. D. Ramsdell, and R. J. Watro, “A correctness proof for combinator reduction with cycles”, ACM Trans. Prog. Lang. Syst. 12 (1990) 123–134.

    Google Scholar 

  7. W. M. Farmer, J. D. Ramsdell, and R. J. Watro, “Redex capturing in term graph rewriting”, Tech. Rep. M89-36, The MITRE Corporation, 1989; a revised version to appear in the International Journal of Foundations of Computer Science.

    Google Scholar 

  8. R. Kennaway, “On ‘On graph rewritings'”, Theoret. Comp. Sci. 52 (1987) 37–58.

    Google Scholar 

  9. J. R. Kennaway, J. W. Klop, M. R. Sleep, F. J. de Vries, “Transfinite reductions in orthogonal term rewriting systems,” to appear, Center for Mathematics and Computer Science (CWI) Report CS-R9042, Amsterdam, The Netherlands; a shortened version appears in this volume.

    Google Scholar 

  10. S. L. Peyton Jones, The Implementation of Functional Programming Languages, (Prentice Hall, New York, 1987).

    Google Scholar 

  11. J. C. Raoult, “On graph rewritings”, Theoret. Comp. Sci. 32 (1984) 1–24.

    Google Scholar 

  12. J. Staples, “Computation on graph-like expressions”, Theoret. Comp. Sci. 10 (1980) 171–185.

    Google Scholar 

  13. D. A. Turner, “A new implementation technique for applicative languages”, Soft. Pract. Exper. 9 (1979) 31–49.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The MITRE Corporation, Burlington Road, A156, 01730, Bedford, MA, USA

    William M. Farmer & Ronald J. Watro

Authors
  1. William M. Farmer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ronald J. Watro
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ronald V. Book

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Farmer, W.M., Watro, R.J. (1991). Redex capturing in term graph rewriting (concise version). In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_82

Download citation

  • DOI: https://doi.org/10.1007/3-540-53904-2_82

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-46383-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation