de Bruijn Indices for Metaterms
Eduardo Bonelli, Delia Kesner, Alejandro Ríos · Journal of Logic and Computation · 2005
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.