Abstract
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.
| Original language | English |
|---|---|
| Pages (from-to) | 855-899 |
| Number of pages | 45 |
| Journal | Journal of Logic and Computation |
| Volume | 15 |
| Issue number | 6 |
| DOIs | |
| State | Published - Dec 2005 |
Keywords
- Alpha-conversion
- De Bruijn indices
- Higher-order rewriting
Fingerprint
Dive into the research topics of 'De Bruijn indices for metaterms'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver