A de bruijn notation for higher-order rewriting

Eduardo Bonelli, Delia Kesner, Alejandro Ríos

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

10 Scopus citations

Abstract

We propose a formalism for higher-order rewriting in de Bruijn notation. This notation not only is used for terms (as usually done in the literature) but also for metaterms, which are the syntactical objects used to express general higher-order rewrite systems. We give formal translations from higher-order rewriting with names to higher-order rewriting with de Bruijn indices, and vice-versa. These translations can be viewed as an interface in programming languages based on higher-order rewrite systems, and they are also used to show some properties, namely, that both formalisms are operationally equivalent, and that confluence is preserved when translating one formalism into the other.

Original languageEnglish
Title of host publicationRewriting Techniques and Applications - 11th International Conference, RTA 2000, Proceedings
EditorsLeo Bachmair
Pages62-79
Number of pages18
ISBN (Electronic)354067778X, 9783540677789
DOIs
StatePublished - 2000
Event11th International Conference on Rewriting Techniques and Applications, RTA 2000 - Norwich, United Kingdom
Duration: 10 Jul 200012 Jul 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1833
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th International Conference on Rewriting Techniques and Applications, RTA 2000
Country/TerritoryUnited Kingdom
CityNorwich
Period10/07/0012/07/00

Fingerprint

Dive into the research topics of 'A de bruijn notation for higher-order rewriting'. Together they form a unique fingerprint.

Cite this