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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press (1998)
I. Durand and A. Middeldorp: Decidable Call by Need Computations in Term Rewriting (Extended Abstract). Proc. 14th CADE, LNAI 1249 (1997) 4–18 198
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
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
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
R. Mayr and T. Nipkow: Higher-order Rewrite Systems and their Confluence. Theoretical Computer Science 192 (1998) 3–29 198
A. Middeldorp: Call by Need Computations to Root-Stable Form. Proc. 24th POPL (1997) 94–105 198, 205, 206, 207
D. Miller: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. Journal of Symbolic Logic 14 (1991) 497–536 200
T. Nipkow: Higher-Order Critical Pairs. Proc. 6th IEEE Symp. Logic in Computer Science (1991) 342–349 198, 201
T. Nipkow: Orthogonal Higher-Order Rewrite Systems are Confluent. Proc. Int. Conf. Typed Lambda Calculi and Applications, LNCS 664 (1993) 306–317 198
V. van Oostrom: Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, (1994) 198
C. Talcott: A Theory of Binding Structures and Applications to Rewriting. Theoretical Computer Science 112 (1993) 99–143
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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