On abstract normalisation beyond neededness

Citation data:

Theoretical Computer Science, ISSN: 0304-3975, Vol: 672, Page: 36-63

Publication Year:
2017
Usage 16
Abstract Views 16
Social Media 3
Tweets 3
DOI:
10.1016/j.tcs.2017.01.025
Author(s):
Eduardo Bonelli; Delia Kesner; Carlos Lombardi; Alejandro Ríos
Publisher(s):
Elsevier BV
Tags:
Mathematics; Computer Science
Most Recent Tweet View All Tweets
article 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.