An abstract normalisation result with applications to non-sequential calculi

EDUARDO BONELLI; DELIA KESNER; CARLOS LOMBARDI; ALEJANDRO RÍOS

THEORETICAL COMPUTER SCIENCE

ELSEVIER SCIENCE BV

Lugar: Amsterdam; Año: 2015

0304-3975

We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focussing on the notion of emph{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 emph{needed} redex. We first prove a normalisation theorem for abstract rewrite systems or ARS, a general rewriting framework encompassing many rewriting systems developed by P-A.Melli`es~cite{thesis-mellies}. The theorem states that multistep strategies reducing so called emph{necessary} and emph{non-gripping} sets of redexes at a time are normalising in any ARS. Gripping refers to an abstract property reflecting the behavior of higher-order substitution. We then apply this result to the particular case of heppc, a calculus of patterns and to the lambda-calculus with parallel-or.