Artículo
On abstract normalisation beyond neededness
Fecha de publicación:
04/2017
Editorial:
Elsevier Science
Revista:
Theoretical Computer Science
ISSN:
0304-3975
Idioma:
Inglés
Tipo de recurso:
Artículo publicado
Clasificación temática:
Resumen
We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focusing on the notion of necessary sets, those which contain at least one redex that cannot be avoided in order to reach a normal form. This is particularly appealing in the setting of non-sequential rewrite systems, in which terms that are not in normal form may not have any needed redex. We first prove a normalisation theorem for abstract rewrite systems (ARS), a general rewriting framework encompassing many rewriting systems developed by P-A. Melliès [20]. The theorem states that multistep strategies reducing so called necessary and never-gripping sets of redexes at a time are normalising in any ARS. Gripping refers to an abstract property reflecting the behaviour of higher-order substitution. We then apply this result to the particular case of PPC, a calculus of patterns and to the lambda-calculus with parallel-or.
Palabras clave:
NEEDEDNESS
,
NORMALISATION
,
PATTERN CALCULI
,
REWRITING
,
SEQUENTIALITY
Archivos asociados
Licencia
Identificadores
Colecciones
Articulos(SEDE CENTRAL)
Articulos de SEDE CENTRAL
Articulos de SEDE CENTRAL
Citación
Bonelli, Eduardo Augusto; Kesner, Delia; Lombardi, Carlos; Rios, Alejandro Norberto; On abstract normalisation beyond neededness; Elsevier Science; Theoretical Computer Science; 672; 4-2017; 36-63
Compartir
Altmétricas