On abstract normalisation beyond neededness

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

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Bonelli, E., Kesner, D., Lombardi, C., Ríos, A.
Formato:	JOUR
Materias:	Neededness Normalisation Pattern calculi Rewriting Sequentiality Biomineralization Differentiation (calculus) Calculations
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_03043975_v672_n_p36_Bonelli
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_03043975_v672_n_p36_Bonelli
record_format	dspace
spelling	todo:paper_03043975_v672_n_p36_Bonelli2023-10-03T15:20:30Z On abstract normalisation beyond neededness Bonelli, E. Kesner, D. Lombardi, C. Ríos, A. Neededness Normalisation Pattern calculi Rewriting Sequentiality Biomineralization Differentiation (calculus) Neededness Normalisation Pattern calculi Rewriting Sequentiality Calculations 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. © 2017 Elsevier B.V. Fil:Bonelli, E. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Lombardi, C. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03043975_v672_n_p36_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	Neededness Normalisation Pattern calculi Rewriting Sequentiality Biomineralization Differentiation (calculus) Neededness Normalisation Pattern calculi Rewriting Sequentiality Calculations
spellingShingle	Neededness Normalisation Pattern calculi Rewriting Sequentiality Biomineralization Differentiation (calculus) Neededness Normalisation Pattern calculi Rewriting Sequentiality Calculations Bonelli, E. Kesner, D. Lombardi, C. Ríos, A. On abstract normalisation beyond neededness
topic_facet	Neededness Normalisation Pattern calculi Rewriting Sequentiality Biomineralization Differentiation (calculus) Neededness Normalisation Pattern calculi Rewriting Sequentiality Calculations
description	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. © 2017 Elsevier B.V.
format	JOUR
author	Bonelli, E. Kesner, D. Lombardi, C. Ríos, A.
author_facet	Bonelli, E. Kesner, D. Lombardi, C. Ríos, A.
author_sort	Bonelli, E.
title	On abstract normalisation beyond neededness
title_short	On abstract normalisation beyond neededness
title_full	On abstract normalisation beyond neededness
title_fullStr	On abstract normalisation beyond neededness
title_full_unstemmed	On abstract normalisation beyond neededness
title_sort	on abstract normalisation beyond neededness
url	http://hdl.handle.net/20.500.12110/paper_03043975_v672_n_p36_Bonelli
work_keys_str_mv	AT bonellie onabstractnormalisationbeyondneededness AT kesnerd onabstractnormalisationbeyondneededness AT lombardic onabstractnormalisationbeyondneededness AT riosa onabstractnormalisationbeyondneededness
_version_	1807317564595896320

On abstract normalisation beyond neededness

Ejemplares similares