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...

Descripción completa

Detalles Bibliográficos
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