Skip to main content
SpringerLink
Log in

Weak orthogonality implies confluence: The higher-order case

  • Conference paper
  • First Online:
Logical Foundations of Computer Science (LFCS 1994)

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

Included in the following conference series:

Abstract

In this paper we prove confluence for weakly orthogonal Higher-Order Rewriting Systems. This generalises all the known ‘confluence by orthogonality’ results.

supported by NWO/SION project 612-316-606

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. Nachum Dershowitz, Jean-Pierre Jouannaud, and Jan Willem Klop. More problems in rewriting. Pp. 468–487 of LNCS 690, Proceedings of 5th RTA, 1993.

    Google Scholar 

  2. Georges Gonthier, Jean-Jacques Lévy, and Paul-André Melliès. An abstract standardisation theorem. Pp. 72–81, Proceedings of 7th LICS, 1992.

    Google Scholar 

  3. Gérard Huet and Jean-Jacques Lévy. Computations in orthogonal rewriting systems, I. Ch. 11 of Computational Logic: Essays in Honor of Alan Robinson, 1991.

    Google Scholar 

  4. J.W. Klop. Combinatory Reduction Systems. Mathematical Centre Tracts Nr. 127. Mathematisch Centrum, Amsterdam, 1980. PhD Thesis.

    Google Scholar 

  5. Tobias Nipkow. Higher-order critical pairs. Pp. 342–349 of Proceedings of 6th LICS, 1991.

    Google Scholar 

  6. Tobias Nipkow. Orthogonal higher-order rewrite systems are confluent. Pp. 306–317 of LNCS 664, Proceedings of TLCA'93, 1993.

    Google Scholar 

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

    Google Scholar 

  8. V. van Oostrom and F. van Raamsdonk. Comparing combinatory reduction systems and higher-order rewrite systems. Technical Report CS-R9361, CWI, 1993. To appear in LNCS, Proceedings of HOA'93.

    Google Scholar 

  9. D.A. Wolfram. The Clausal Theory of Types, volume 21 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, Vrije Universiteit, De Boelelaan 1081a, 1081, HV Amsterdam

    Vincent van Oostrom

  2. CWI, P.O. Box 94079, 1090, GB Amsterdam, The Netherlands

    Femke van Raamsdonk

Authors
  1. Vincent van Oostrom
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Femke van Raamsdonk
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Anil Nerode Yu. V. Matiyasevich

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van Oostrom, V., van Raamsdonk, F. (1994). Weak orthogonality implies confluence: The higher-order case. In: Nerode, A., Matiyasevich, Y.V. (eds) Logical Foundations of Computer Science. LFCS 1994. Lecture Notes in Computer Science, vol 813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58140-5_35

Download citation

  • DOI: https://doi.org/10.1007/3-540-58140-5_35

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58140-6

  • Online ISBN: 978-3-540-48442-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation