TY - JOUR
T1 - De Bruijn indices for metaterms
AU - Bonelli, Eduardo
AU - Kesner, Delia
AU - Rios, Alejandro
PY - 2005/12
Y1 - 2005/12
N2 - In this paper we encode higher-order rewriting with names into higher-order rewriting in de Bruijn notation. This notation not only is defined for terms (as usually done in the literature) but also for metaterms, which are the syntactical objects used to express the rewriting rules of higher-order systems. Several examples are discussed. Fundamental properties such as confluence and normalisation are shown to be preserved.
AB - In this paper we encode higher-order rewriting with names into higher-order rewriting in de Bruijn notation. This notation not only is defined for terms (as usually done in the literature) but also for metaterms, which are the syntactical objects used to express the rewriting rules of higher-order systems. Several examples are discussed. Fundamental properties such as confluence and normalisation are shown to be preserved.
KW - Alpha-conversion
KW - De Bruijn indices
KW - Higher-order rewriting
UR - http://www.scopus.com/inward/record.url?scp=29144449495&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=29144449495&partnerID=8YFLogxK
U2 - 10.1093/logcom/exi051
DO - 10.1093/logcom/exi051
M3 - Article
AN - SCOPUS:29144449495
SN - 0955-792X
VL - 15
SP - 855
EP - 899
JO - Journal of Logic and Computation
JF - Journal of Logic and Computation
IS - 6
ER -