Vol. 15 No. 6, © The Author, 2005. Published by Oxford University Press. All rights reserved.
Original Articles |
de Bruijn Indices for Metaterms
1 CONICET and LIFIA, Facultad de Informática, Universidad Nacional de La Plata, Argentina. Email: eduardo{at}sol.info.unlp.edu.ar, 2 PPS, CNRS and Université Paris 7, France. Email: kesner{at}pps.jussieu.fr, 3 Departamento de Computación, Universidad de Buenos Aires, Argentina. Email: rios{at}dc.uba.ar
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.
Keywords: Higher-order rewriting, de Bruijn indices, alpha-conversion
Received May 2002.