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

Guardado en:
Detalles Bibliográficos
Autores principales: Bonelli, E., Kesner, D., Rios, A.
Formato: JOUR
Materias:
Alpha-conversion
De Bruijn indices
Higher-order rewriting
Logic programming
Syntactics
Notation
Metadata
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_0955792X_v15_n6_p855_Bonelli
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_0955792X_v15_n6_p855_Bonelli
record_format dspace
spelling todo:paper_0955792X_v15_n6_p855_Bonelli2023-10-03T15:51:48Z De Bruijn indices for metaterms Bonelli, E. Kesner, D. Rios, A. 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. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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
Bonelli, E.
Kesner, D.
Rios, A.
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.
format JOUR
author Bonelli, E.
Kesner, D.
Rios, A.
author_facet Bonelli, E.
Kesner, D.
Rios, A.
author_sort Bonelli, E.
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
url http://hdl.handle.net/20.500.12110/paper_0955792X_v15_n6_p855_Bonelli
work_keys_str_mv AT bonellie debruijnindicesformetaterms
AT kesnerd debruijnindicesformetaterms
AT riosa debruijnindicesformetaterms
_version_ 1782028723944423424

Ejemplares similares