Skip to main content
SpringerLink
Log in

Transfinite reductions in orthogonal term rewriting systems

  • 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

Strongly convergent reduction is the fundamental notion of reduction in infinitary orthogonal term rewriting systems (OTRSs). For these we prove the Transfinite Parallel Moves Lemma and the Compressing Lemma. Strongness is necessary as shown by counterexamples. Normal forms, which we allow to be infinite, are unique, in contrast to ω-normal forms. Strongly converging fair reductions result in normal forms.

In general OTRSs the infinite Church-Rosser Property fails for strongly converging reductions. However for Böhm reduction (as in Lambda Calculus, subterms without head normal forms may be replaced by ⊥) the infinite Church-Rosser property does hold. The infinite Church-Rosser Property for non-unifiable OTRSs follows. The top-terminating OTRSs of Dershowitz c.s. are examples of non-unifiable OTRSs.

(Extended abstract)

All authors were partially sponsored by SEMAGRAPH, ESPRIT Basic Research Action 3074. The first author was also partially surported by a SERC Advanced Fellowship, and by SERC grant no. GR/F 91582.

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.

5. References

  1. A. ARNOLD and M. NIVAT, The metric space of infinite trees. Algebraic and topological properties, Fundamenta Informatica, 4 (1980) 445–76.

    Google Scholar 

  2. H.P. BARENDREGT, The Lambda Calculus, its Syntax and Semantics, 2nd ed., (North-Holland, 1984).

    Google Scholar 

  3. H.P. BARENDREGT, M.C.J.D. VAN EEKELEN, J.R.W. GLAUERT, J.R. KENNAWAY, M.J. PLASMEIJER, and M.R. SLEEP, Term graph rewriting, Proc. PARLE Conference vol II, LNCS vol. 259, pp. 141–158 (Springer-Verlag, 1987).

    Google Scholar 

  4. N. DERSHOWITZ and S. KAPLAN, Rewrite, rewrite, rewrite, rewrite, rewrite, Principles of programming languages, Austin, Texas, 1989, pp. 250–259.

    Google Scholar 

  5. N. DERSHOWITZ, S. KAPLAN and D.A. PLAISTED, Infinite Normal Forms (plus corrigendum), ICALP 1989, pp. 249–262.

    Google Scholar 

  6. N. DERSHOWITZ and J.P. JOUANNAUD, Rewrite Systems, to appear in Handbook of Theoretical Computer Science (ed. J. van Leeuwen) vol.B, chapter 15, North-Holland.

    Google Scholar 

  7. N. DERSHOWITZ, S. KAPLAN and D.A. PLAISTED, Rewrite, rewrite, rewrite, rewrite, rewrite to appear.

    Google Scholar 

  8. W.M. FARMER and R.J. WATRO, Redex capturing in term graph rewriting, in Computing with the Curry Chip (eds. W.M. Farmer, J.D. Ramsdell and R.J. Watro), Report M89-59, MITRE, 1989.

    Google Scholar 

  9. P. HUDAK et al, Report on the Functional Programming Language Haskell. Draft Proposed Standard, 1988.

    Google Scholar 

  10. G. HUET and J.-J. LÉVY, Call by need computations in non-ambiguous linear term rewriting systems, Report 359,INRIA, 1979.

    Google Scholar 

  11. J.L. KELLEY, General Topology, Graduate Texts in Mathematics 27, Springer-Verlag New York, 1955, Second Printing 1985.

    Google Scholar 

  12. J.R.KENNAWAY, J.W. KLOP, M.R. SLEEP and F.J. DE VRIES, Transfinite reductions in orthogonal term rewriting systems (Full paper), report CS-R9041, CWI, Amsterdam, 1990.

    Google Scholar 

  13. J.R. KENNAWAY, J.W. KLOP, M.R. SLEEP and F.J. DE VRIES, An infinitary Church-Rosser property for non-collapsing orthogonal term rewriting systems, report CS-R9043, CWI, Amsterdam, 1990.

    Google Scholar 

  14. J.W. KLOP, Combinatory reduction systems, Mathematical Centre Tracts no. 127, CWI, Amsterdam, 1980.

    Google Scholar 

  15. J.W. KLOP, Term rewriting systems, to appear in Handbook of Logic in Computer Science, Vol I (eds. S. Abramsky, D. Gabbay and T. Maibaum), Oxford University Press, 1991.

    Google Scholar 

  16. S.L. PEYTON JONES, The Implementation of Functional Programming Languages, (Prentice-Hall, 1987).

    Google Scholar 

  17. B.K. ROSEN, Tree manipulating systems and Church Rosser theorems, JACM 20 (1973) 160–187.

    Google Scholar 

  18. D.A. TURNER, Miranda: a non-strict functional language with polymorphic types, in J.-P. Jouannaud (ed.), Proc. ACM Conf. on Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science, vol. 201, Springer-Verlag, 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, Centre for Mathematics and Computer Science, Amsterdam

    J. W. Klop & F. J. de Vries

  2. School of Information Systems, University of East Anglia, Norwich

    J. R. Kennaway & M. R. Sleep

Authors
  1. J. R. Kennaway
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. J. W. Klop
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. M. R. Sleep
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. F. J. de Vries
    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

Kennaway, J.R., Klop, J.W., Sleep, M.R., de Vries, F.J. (1991). Transfinite reductions in orthogonal term rewriting systems. 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_81

Download citation

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

  • 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