De Bruijn indices for metaterms

Eduardo Bonelli, Delia Kesner, Alejandro Rios

Research output: Contribution to journalArticlepeer-review

3 Scopus citations

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 languageEnglish
Pages (from-to)855-899
Number of pages45
JournalJournal of Logic and Computation
Volume15
Issue number6
DOIs
StatePublished - 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