Relative normalization in orthogonal expression reduction systems

Abstract

We study reductions in orthogonal (left-linear and non-ambiguous) Expression Reduction Systems, a formalism for Term Rewriting Systems with bound variables and substitutions. To generalise the normalization theory of Huet and Lévy, we introduce the notion of neededness with respect to a set of reductions π or a set of terms $\mathcal{S}$ so that each existing notion of neededness can be given by specifying π or $\mathcal{S}$. We imposed natural conditions on $\mathcal{S}$, called stability, that are sufficient and necessary for each term not in $\mathcal{S}$-normal form (i.e., not in $\mathcal{S}$) to have at least one $\mathcal{S}$-needed redex, and repeated contraction of $\mathcal{S}$-needed redexes in a term t to lead to an $\mathcal{S}$-normal form of t whenever there is one. Our relative neededness notion is based on tracing (open) components, which are occurrences of contexts not containing any bound variable, rather than tracing redexes or subterms.

This work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300.