de Bruijn indices for metaterms
Material type:
ArticleDescription: 1 archivo (417,3 kB)Subject(s): Online resources: Summary: 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.
| Item type | Home library | Collection | Call number | URL | Status | Date due | Barcode | |
|---|---|---|---|---|---|---|---|---|
Capítulo de libro
|
Biblioteca de la Facultad de Informática | Biblioteca digital | A0284 (Browse shelf(Opens below)) | Link to resource | No corresponde |
Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática - UNLP (Colección BIPA/Biblioteca)
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.
Journal of Logic and Computation, 15(6), pp. 855-899