Journal of Logic and Computation, Volume 10, Issue 3, pp. 323-348: Abstract.
Stable results and relative normalization
J Glauert1, R Kennaway1 and Z Khasidashvili2
1School of Information Systems, UEA, Norwich NR4 7TJ, UK, E-mail: J.Glauert, R.Kennaway@uea.ac.uk, 2Department of Mathematics and Computer Science, Bar-Ilan University, Ramat-Gan 52900, Israel, E-mail: Khasidz@cs.biu.ac.il
In orthogonal expression reduction systems, a common generalization of term rewriting and [lgr]-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.
Keywords: rewrite systems, normalizing strategy, needed reduction, stable sets of results, minimal and optimal normalization, high-order rewriting