On abstract normalisation beyond neededness

Eduardo Bonelli, Delia Kesner, Carlos Lombardi, Alejandro Ríos

Research output: Contribution to journalArticlepeer-review

2 Scopus citations

Abstract

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.

Original languageEnglish
Pages (from-to)36-63
Number of pages28
JournalTheoretical Computer Science
Volume672
DOIs
StatePublished - 11 Apr 2017

Keywords

  • Neededness
  • Normalisation
  • Pattern calculi
  • Rewriting
  • Sequentiality

Fingerprint

Dive into the research topics of 'On abstract normalisation beyond neededness'. Together they form a unique fingerprint.

Cite this