Abstract
A prefix property is the property that, given a reduction, the ancestor of a prefix of the target is a prefix of the source. In this paper we prove a prefix property for the class of Higher-Order Rewriting Systems with patterns (HRSs), by reducing it to a similar prefix property of a λ-calculus with explicit substitutions. This prefix property is then used to prove that Higher-order Rewriting Systems enjoy Finite Family Developments. This property states, that reductions in which the creation depth of the redexes is bounded are finite, and is a useful tool to prove various properties of HRSs.
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.
References
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1-2), 133–178 (2000)
Bethke, I., Klop, J.W., de Vrijer, R.: Descendants and origins in term rewriting. Information and Computation 159(1-2), 59–124 (2000)
Bloo, R.: Preservation of Termination for Explicit Substitution. PhD thesis, Technische Universiteit Eindhoven (1997)
Sander Bruggink, H.J.: A proof of finite family developments for higher-order rewriting using a prefix property. LGPS 245, Zeno Inst. of Phil.(2006) (preprint)
Dowek, G., Hardin, T., Kirchner, C.: Higher order unification via explicit substitutions. Information and Computation 157(1-2), 184–233 (2000)
Hyland, J.M.E.: A syntactic characterization of the equality in some models of the λ-calculus. Journal of the London Mathematical Society 12(2), 361–370 (1976)
Klop, J.W.: Combinatory Reduction Systems. PhD thesis, Utrecht Univ.(1980)
Lévy, J.-J.: Réductions correctes et optimales dans le λ-calcus. PhD thesis, Université Paris VII (1978)
Maranget, L.: Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems. In: POPL (1991)
Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science 192, 3–29 (1998)
Miller, D.: A logic programming language with lambda abstraction, function variables and simple unification. Journal of Logic and Computation 1(4) (1991)
Nipkow, T.: Higher-order critical pairs. In: LICS (1991)
Terese: Term Rewriting Systems. Number 55 in CTTCS. CUP (2003)
van Daalen, D.T.: The language theory of Automath. PhD thesis, Technische Universiteit Eindhoven (1980)
van Oostrom, V.: Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit Amsterdam (1994)
van Oostrom, V.: Finite family developments. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232. Springer, Heidelberg (1997)
van Oostrom, V., de Vrijer, R.: Four equivalent equivalences of reductions. ENTCS 70(6) (2002)
Wadsworth, C.P.: The relation between computational and denotational properties for Scott’s D ∞ -models of the λ-calculus. SIAM Journal on Computing 5 (1976)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bruggink, H.J.S. (2006). A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property. In: Pfenning, F. (eds) Term Rewriting and Applications. RTA 2006. Lecture Notes in Computer Science, vol 4098. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11805618_28
Download citation
DOI: https://doi.org/10.1007/11805618_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-36834-2
Online ISBN: 978-3-540-36835-9
eBook Packages: Computer ScienceComputer Science (R0)