Journal of Logic and Computation, Volume 10, Issue 3, pp. 461487: Abstract.
Axiomatic rewriting theory II: the [lgr][sgr]calculus enjoys finite normalisation conesPA Melliès Preuves, Programmes, Systèmes, CNRS EPJ2025, Université Paris 7, Paris, France, Email: mellies@pps.jussieu.fr
Every needed strategy is normalizing in the [lgr]calculus. Here, we extend the result to the [lgr][sgr]calculus, a [lgr]calculus with explicit substitutions. The extension requires considering rewriting systems with critical pairs, confluent or nonconfluent, and developing for them a satisfactory theory of needed normalization. Our idea is to count for every term M the number of its normalizing paths, up to Lévy permutation equivalence. We deduce from standardization that every needed strategy normalizes when this number is finite. The number is zero or one in the [lgr]calculus, and we show that it is finite in the [lgr][sgr]calculus. Keywords: rewriting theory, lambda calculus, explicit substitutions, strategies, critical pairs, normalization
