Axiomatic Rewriting Theory II: the λσ-calculus Enjoys Finite Normalisation Cones

摘要

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 Levy 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.