Skip to main content
SpringerLink
Log in

Descendants and Head Normalization of Higher-Order Rewrite Systems

  • Conference paper
  • First Online:
Functional and Logic Programming (FLOPS 2002)

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

Included in the following conference series:

  • 258 Accesses

Abstract

This paper describes an extension of head-needed rewriting on term rewriting systems to higher-order rewrite systems. The main difficulty of this extension is caused by the β-reductions induced from the higher-order reductions. In order to overcome this difficulty, we define a new descendant of higher-order rewrite systems. This paper shows the new definition of descendant, its properties and head normalization of head-needed rewriting on orthogonal higher-order rewrite systems.

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

Access this chapter

Log in via an institution
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.

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press (1998)

    Google Scholar 

  2. I. Durand and A. Middeldorp: Decidable Call by Need Computations in Term Rewriting (Extended Abstract). Proc. 14th CADE, LNAI 1249 (1997) 4–18 198

    MathSciNet  Google Scholar 

  3. G. Huet and J.-J. Lévy: Computations in Orthogonal Rewriting Systems, I and II. Computational Logic, Essays in Honor of Alan Robinson, The MIT Press (1991) 396–443 198, 201, 206

    Google Scholar 

  4. M. Iwami and Y. Toyama: Simplification Ordering for Higher-order Rewrite systems. IPSJ Trans. on Programming 40 SIG 4 (PRO 3) (1999) 1–10 198

    Google Scholar 

  5. J.-P. Jouannaud and A. Rubio: Rewrite Orderings for Higher-order Terms in η-long β-normal Form and the Recursive Path Ordering. Theoretical Computer Science 208 (1998) 33–58 198, 200

    Article  MATH  MathSciNet  Google Scholar 

  6. R. Mayr and T. Nipkow: Higher-order Rewrite Systems and their Confluence. Theoretical Computer Science 192 (1998) 3–29 198

    Article  MATH  MathSciNet  Google Scholar 

  7. A. Middeldorp: Call by Need Computations to Root-Stable Form. Proc. 24th POPL (1997) 94–105 198, 205, 206, 207

    Google Scholar 

  8. D. Miller: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. Journal of Symbolic Logic 14 (1991) 497–536 200

    Google Scholar 

  9. T. Nipkow: Higher-Order Critical Pairs. Proc. 6th IEEE Symp. Logic in Computer Science (1991) 342–349 198, 201

    Google Scholar 

  10. T. Nipkow: Orthogonal Higher-Order Rewrite Systems are Confluent. Proc. Int. Conf. Typed Lambda Calculi and Applications, LNCS 664 (1993) 306–317 198

    Chapter  Google Scholar 

  11. V. van Oostrom: Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, (1994) 198

    Google Scholar 

  12. C. Talcott: A Theory of Binding Structures and Applications to Rewriting. Theoretical Computer Science 112 (1993) 99–143

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Information Science and Technology, Aichi Prefectural University, 1522-3 Ibaragabasama, Kumabari Nagakute-cho, Aichi, 480-1198, Japan

    Hideto Kasuya

  2. Department of Information Engineering, Nagoya University, Furo-cho, Chikusa-ku, Nagoya, 464-8603, Japan

    Masahiko Sakai & Kiyoshi Agusa

Authors
  1. Hideto Kasuya
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Masahiko Sakai
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kiyoshi Agusa
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Mathematical Informatics, University of Tokyo, Hongo 7-3-1, Bunkyo-Ku, Tokyo, 113-8656, Japan

    Zhenjiang Hu

  2. Department of Informatic Languages and Systems, Universidad Complutense de Madrid, Av. Complutense s/n, 28040, Madrid, Spain

    Mario Rodríguez-Artalejo

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kasuya, H., Sakai, M., Agusa, K. (2002). Descendants and Head Normalization of Higher-Order Rewrite Systems. In: Hu, Z., Rodríguez-Artalejo, M. (eds) Functional and Logic Programming. FLOPS 2002. Lecture Notes in Computer Science, vol 2441. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45788-7_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-45788-7_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44233-2

  • Online ISBN: 978-3-540-45788-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation