Stable results and relative normalization
John Glauert · Journal of Logic and Computation · 2000
In orthogonal expression reduction systems, a common generalization of term rewriting and λ-calculus, we extend the concepts of normalization and needed reduction by considering, instead of the set of normal forms, a set S of 'results'. When S satisfies some simple axioms which we call stability, we prove the corresponding generalizations of some fundamental theorems: the existence of needed redexes, that needed reduction is normalizing, the existence of minimal normalizing reductions, and the optimality theorem.