Axiomatic rewriting theory II: the -calculus enjoys finite normalisation cones
P-A Mellies · Journal of Logic and Computation · 2000
Every needed strategy is normalizing in the λ-calculus. Here, we extend the result to the λσ-calculus, a λ-calculus with explicit substitutions. The extension requires considering rewriting systems with critical pairs, confluent or non-confluent, 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 λ-calculus, and we show that it is finite in the λσ-calculus.