In rewriting, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an evaluation strategy.
Definitions Formally, for an abstract rewriting system ( A , → ) {\displaystyle (A,\to )} , a reduction strategy → S {\displaystyle \to _{S}} is a binary relation on A {\displaystyle A} with → S ⊆ → + {\displaystyle \to _{S}\subseteq {\overset {+}{\to }}} , where → + {\displaystyle {\overset {+}{\to }}} is the transitive closure of → {\displaystyle \to } (but not the reflexive closure). In addition the normal forms of the strategy must be the same as the normal forms of the original rewriting system, i.e. for all a {\displaystyle a} , there exists a b {\displaystyle b} with a → b {\displaystyle a\to b} iff ∃ b ′ . a → S b ′ {\displaystyle \exists b'.a\to _{S}b'} . A one step reduction strategy is one where → S ⊆→ {\displaystyle \to _{S}\subseteq \to } . Otherwise it is a many step strategy. A deterministic strategy is one where → S {\displaystyle \to _{S}} is a partial function, i.e. for each a ∈ A {\displaystyle a\in A} there is at most one b {\displaystyle b} such that a → S b {\displaystyle a\to _{S}b} . Otherwise it is a nondeterministic strategy.
Term rewriting In a term rewriting system a rewriting strategy specifies, out of all the reducible subterms (redexes), which one should be reduced (contracted) within a term. One-step strategies for term rewriting include:
leftmost-innermost: in each step the leftmost of the innermost redexes is contracted, where an innermost redex is a redex not containing any redexes leftmost-outermost: in each step the leftmost of the outermost redexes is contracted, where an outermost redex is a redex not contained in any redexes rightmost-innermost, rightmost-outermost: similarly Many-step strategies include:
parallel-innermost: reduces all innermost redexes simultaneously. This is well-defined because the redexes are pairwise disjoint. parallel-outermost: similarly Gross-Knuth reduction, also called full substitution or Kleene reduction: all redexes in the term are simultaneously reduced Parallel outermost and Gross-Knuth reduction are hypernormalizing for all almost-orthogonal term rewriting systems, meaning that these strategies will eventually reach a normal form if it exists, even when performing (finitely many) arbitrary reductions between successive applications of the strategy. Stratego is a domain-specific language designed specifically for programming term rewriting strategies.
Lambda calculus
In the context of the lambda calculus, normal-order reduction refers to leftmost-outermost reduction in the sense given above. Normal-order reduction is normalizing, in the sense that if a term has a normal form, then normal‐order reduction will eventually reach it, hence the name normal. This is known as the standardization theorem. Leftmost reduction is sometimes used to refer to normal order reduction, as with a pre-order traversal the notions coincide, and similarly the leftmost-outermost redex is the redex with leftmost starting character when the lambda term is considered as a string of characters. When "leftmost" is defined using an in-order traversal the notions are distinct. For example, in the term ( λ x . x Ω ) ( λ y . I ) {\displaystyle (\lambda x.x\Omega )(\lambda y.I)} with Ω , I {\displaystyle \Omega ,I} defined here, the leftmost redex of the in-order traversal is Ω {\displaystyle \Omega } while the leftmost-outermost redex is the entire expression. Applicative order reduction refers to leftmost-innermost reduction. In contrast to normal order, applicative order reduction may not terminate, even when the term has a normal form. For example, using applicative order reduction, the following sequence of reductions is possible:
… excerpt ends here. Continue reading the full article.
