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 II or a set of terms, S so that each existing notion of neededness can be given by specifying II or S. We imposed natural conditions on S, called stability, that are sufficient and necessary for each term not in S-normal form (i.e., not in 8) to have at least one S-needed redex, and repeated contraction of S-needed redexes in a term t to lead to an 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.
CITATION STYLE
Glauert, J., & Khasidashvili, Z. (1995). Relative normalization in orthogonal expression reduction systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 968, pp. 144–165). Springer Verlag. https://doi.org/10.1007/3-540-60381-6_9
Mendeley helps you to discover research relevant for your work.