Perpetuality and Uniform Normalization
in Orthogonal Rewrite Systems

We study perpetuality of reduction steps, as well as perpetuality of redexes, in orthogonal rewrite systems.

A perpetual step is a reduction step which retains the possibility of infinite reductions. A perpetual redex is a redex which, when put into an arbitrary context, yields a perpetual step. We generalize and refine existing criteria for the perpetuality of reduction steps and redexes in orthogonal Term Rewriting Systems and the lambda-calculus due to Bergstra and Klop, and others.

We first introduce Context-sensitive Conditional Expression Reduction Systems (CCERSs) and define a concept of orthogonality (which implies confluence) for them. In particular, several important lambda-calculi and their extensions and restrictions can naturally be embedded into orthogonal CCERSs. We then define a perpetual reduction strategy which enables one to construct minimal (w.r.t.\ Lévy's permutation ordering on reductions) infinite reductions in orthogonal fully-extended CCERSs.

Using the properties of the minimal perpetual strategy, we prove

• perpetuality of any reduction step that does not erase potentially infinite arguments, which are arguments that may become, via substitution, infinite after a number of outside steps, and
• perpetuality (in every context) of any safe redex, which is a redex whose substitution instances may discard infinite arguments only when the corresponding contracta remain infinite.

We prove both these perpetuality criteria for orthogonal fully-extended CCERSs and then specialize and apply them to restricted lambda-calculi, demonstrating their usefulness. In particular, we prove the equivalence of weak and strong normalization (which equivalence is here called uniform normalization) for various restricted lambda-calculi, most of which cannot be derived from previously known perpetuality criteria.