TY - GEN
T1 - A de bruijn notation for higher-order rewriting
AU - Bonelli, Eduardo
AU - Kesner, Delia
AU - Ríos, Alejandro
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2000.
PY - 2000
Y1 - 2000
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84937395954&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84937395954&partnerID=8YFLogxK
U2 - 10.1007/10721975_5
DO - 10.1007/10721975_5
M3 - Conference contribution
AN - SCOPUS:84937395954
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 62
EP - 79
BT - Rewriting Techniques and Applications - 11th International Conference, RTA 2000, Proceedings
A2 - Bachmair, Leo
T2 - 11th International Conference on Rewriting Techniques and Applications, RTA 2000
Y2 - 10 July 2000 through 12 July 2000
ER -