De Bruijn indices for metaterms
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 s...
Publicado: |
2005
|
---|---|
Materias: | |
Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v15_n6_p855_Bonelli http://hdl.handle.net/20.500.12110/paper_0955792X_v15_n6_p855_Bonelli |
Aporte de: |
id |
paper:paper_0955792X_v15_n6_p855_Bonelli |
---|---|
record_format |
dspace |
spelling |
paper:paper_0955792X_v15_n6_p855_Bonelli2023-06-08T15:55:54Z De Bruijn indices for metaterms Alpha-conversion De Bruijn indices Higher-order rewriting Logic programming Syntactics Alpha-conversion De Bruijn indices Higher-order rewriting Notation Metadata 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. 2005 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v15_n6_p855_Bonelli http://hdl.handle.net/20.500.12110/paper_0955792X_v15_n6_p855_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 |
Alpha-conversion De Bruijn indices Higher-order rewriting Logic programming Syntactics Alpha-conversion De Bruijn indices Higher-order rewriting Notation Metadata |
spellingShingle |
Alpha-conversion De Bruijn indices Higher-order rewriting Logic programming Syntactics Alpha-conversion De Bruijn indices Higher-order rewriting Notation Metadata De Bruijn indices for metaterms |
topic_facet |
Alpha-conversion De Bruijn indices Higher-order rewriting Logic programming Syntactics Alpha-conversion De Bruijn indices Higher-order rewriting Notation Metadata |
description |
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. |
title |
De Bruijn indices for metaterms |
title_short |
De Bruijn indices for metaterms |
title_full |
De Bruijn indices for metaterms |
title_fullStr |
De Bruijn indices for metaterms |
title_full_unstemmed |
De Bruijn indices for metaterms |
title_sort |
de bruijn indices for metaterms |
publishDate |
2005 |
url |
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v15_n6_p855_Bonelli http://hdl.handle.net/20.500.12110/paper_0955792X_v15_n6_p855_Bonelli |
_version_ |
1768545102009991168 |