Summary: We prove a version of the Standardization Theorem and the Discrete Normalization Theorem in stable Deterministic Residual Structures, Abstract Reduction Systems with axiomatized notions of residual, which model orthogonal rewrite systems. The latter theorem gives a strategy for construction of reductions Lévy-equivalent (or permutation-equivalent) to a given, finite or infinite, regular (or semi-linear) reduction, based on the neededness concept of Huet and Lévy. This and other results of this paper add to the understanding of Lévy-equivalence of reductions, and consequently, Lévy’s reduction space. We demonstrate how elements of this space can be used to give denotational semantics to known functional languages in an abstract manner.
For the entire collection see [Zbl 0856.68011].