A de bruijn notation for higher-order rewriting
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 highe...
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | SER |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_03029743_v1833_n_p62_Bonelli |
| Aporte de: |
| id |
todo:paper_03029743_v1833_n_p62_Bonelli |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_03029743_v1833_n_p62_Bonelli2023-10-03T15:18:52Z A de bruijn notation for higher-order rewriting Bonelli, E. Kesner, D. Ríos, A. Bachmair L. Artificial intelligence Computers De Bruijn De-Bruijn indices Higher-order rewrite system Higher-order rewriting Meta-terms Program translators 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. © Springer-Verlag Berlin Heidelberg 2000. Fil:Bonelli, E. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v1833_n_p62_Bonelli |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Artificial intelligence Computers De Bruijn De-Bruijn indices Higher-order rewrite system Higher-order rewriting Meta-terms Program translators |
| spellingShingle |
Artificial intelligence Computers De Bruijn De-Bruijn indices Higher-order rewrite system Higher-order rewriting Meta-terms Program translators Bonelli, E. Kesner, D. Ríos, A. Bachmair L. A de bruijn notation for higher-order rewriting |
| topic_facet |
Artificial intelligence Computers De Bruijn De-Bruijn indices Higher-order rewrite system Higher-order rewriting Meta-terms Program translators |
| description |
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. © Springer-Verlag Berlin Heidelberg 2000. |
| format |
SER |
| author |
Bonelli, E. Kesner, D. Ríos, A. Bachmair L. |
| author_facet |
Bonelli, E. Kesner, D. Ríos, A. Bachmair L. |
| author_sort |
Bonelli, E. |
| title |
A de bruijn notation for higher-order rewriting |
| title_short |
A de bruijn notation for higher-order rewriting |
| title_full |
A de bruijn notation for higher-order rewriting |
| title_fullStr |
A de bruijn notation for higher-order rewriting |
| title_full_unstemmed |
A de bruijn notation for higher-order rewriting |
| title_sort |
de bruijn notation for higher-order rewriting |
| url |
http://hdl.handle.net/20.500.12110/paper_03029743_v1833_n_p62_Bonelli |
| work_keys_str_mv |
AT bonellie adebruijnnotationforhigherorderrewriting AT kesnerd adebruijnnotationforhigherorderrewriting AT riosa adebruijnnotationforhigherorderrewriting AT bachmairl adebruijnnotationforhigherorderrewriting AT bonellie debruijnnotationforhigherorderrewriting AT kesnerd debruijnnotationforhigherorderrewriting AT riosa debruijnnotationforhigherorderrewriting AT bachmairl debruijnnotationforhigherorderrewriting |
| _version_ |
1807316772504731648 |