TY - JOUR
T1 - On abstract normalisation beyond neededness
AU - Bonelli, Eduardo
AU - Kesner, Delia
AU - Lombardi, Carlos
AU - Ríos, Alejandro
N1 - Publisher Copyright:
© 2017 Elsevier B.V.
PY - 2017/4/11
Y1 - 2017/4/11
N2 - 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.
AB - 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.
KW - Neededness
KW - Normalisation
KW - Pattern calculi
KW - Rewriting
KW - Sequentiality
UR - http://www.scopus.com/inward/record.url?scp=85014329314&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85014329314&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2017.01.025
DO - 10.1016/j.tcs.2017.01.025
M3 - Article
AN - SCOPUS:85014329314
SN - 0304-3975
VL - 672
SP - 36
EP - 63
JO - Theoretical Computer Science
JF - Theoretical Computer Science
ER -