Abstract
We propose a formalism for higher-order rewriting in de Bruijn notation. This notation not only is used for terms (as usually done in the literature) but also for metaterms, which are the syntactical objects used to express general higher-order rewrite systems. We give formal translations from higher-order rewriting with names to higher-order rewriting with de Bruijn indices, and vice-versa. These translations can be viewed as an interface in programming languages based on higher-order rewrite systems, and they are also used to show some properties, namely, that both formalisms are operationally equivalent, and that confluence is preserved when translating one formalism into the other.
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
Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics, Revised edn. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1984)
Bloo, R.: Preservation of Termination for Explicit Substitution. PhD thesis, Eindhoven University (1997)
Bloo, R., Rose, K.: Combinatory reduction systems with explicit substitution that preserve strong normalisation. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 169–183. Springer, Heidelberg (1996)
Bonelli, E., Kesner, D., Ríos, A.: A de Bruijn notation for higher-order rewriting (2000), Available as ftp://ftp.lri.fr/LRI/articles/kesner/dBhor.ps.gz
Curien, P.-L.: Categorical combinators, sequential algorithms and functional programming, 2nd edn. Progress in Theoretical Computer Science. Birkhaüser, Basel (1993)
Curien, P.-L., Hardin, T., Lévy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM 43(2), 362–397 (1996)
de Bruijn, N.: Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indag. Mat. 5(35), 381–392 (1972)
Dowek, G.: La part du calcul. Univesité de Paris VII, Thèse d’Habilitation à diriger des recherches (1999)
Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. In: LICS (1995)
Hindley, R., Seldin, J.P.: Introduction to Combinators and λ-calculus. London Mathematical Society (1980)
Kamareddine, F., Ríos, A.: Bridging de bruijn indices and variable names in explicit substitutions calculi. Logic Journal of the Interest Group of Pure and Applied Logic (IGPL) 6(6), 843–874 (1998)
Khasidashvili, Z.: Expression reduction systems. In: Proceedings of I. Vekua Institute of Applied Mathematics, Tbilisi, vol. 36 (1990)
Khasidashvili, Z., van Oostrom, V.: Context-sensitive Conditional Expression Reduction Systems. In: Proceedings of the Joint COMPUGRAPH/ SEMAGRAPH Workshop on Graph Rewriting and Computation (SEGRAGRA 1995), ENTCS, Volterra, vol. 2 (1995)
Klop, J.W.: Combinatory Reduction Systems. Mathematical Centre Tracts, vol. 127. CWI, Amsterdam (1980), PhD Thesis
Nipkow, T.: Higher order critical pairs. In: LICS, pp. 342–349 (1991)
Pagano, B.: Des Calculs de Susbtitution Explicite et leur application à la compilation des langages fonctionnels. PhD thesis, Université Paris VI (1998)
Pollack, R.: Closure under alpha-conversion. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, Springer, Heidelberg (1994)
Rehof, J., Sørensen, M.H.: The λ Δ calculus. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 516–542. Springer, Heidelberg (1994)
Rose, K.: Explicit cyclic substitutions. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 36–50. Springer, Heidelberg (1993)
van Oostrom, V., van Raamsdonk, F.: Weak orthogonality implies confluence: the higher-order case. In: Matiyasevich, Y.V., Nerode, A. (eds.) LFCS 1994. LNCS, vol. 813, pp. 379–392. Springer, Heidelberg (1994)
van Raamsdonk, F.: Confluence and Normalization for higher-Order Rewriting. PhD thesis, Amsterdam University, The Netherlands (1996)
Wolfram, D.: The Clausal Theory of Types. Cambridge Tracts in Theoretical Computer Science, vol. 21. Cambridge University Press, Cambridge (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonelli, E., Kesner, D., Ríos, A. (2000). A de Bruijn Notation for Higher-Order Rewriting. In: Bachmair, L. (eds) Rewriting Techniques and Applications. RTA 2000. Lecture Notes in Computer Science, vol 1833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721975_5
Download citation
DOI: https://doi.org/10.1007/10721975_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67778-9
Online ISBN: 978-3-540-44980-5
eBook Packages: Springer Book Archive