Reduction strategy

Formally, for an abstract rewriting system ${\displaystyle (A,\to )}$, a reduction strategy ${\displaystyle \to _{S}}$ is a binary relation on ${\displaystyle A}$ with ${\displaystyle \to _{S}\subseteq {\overset {+}{\to }}}$ , where ${\displaystyle {\overset {+}{\to }}}$ is the transitive closure of ${\displaystyle \to }$ (but not the reflexive closure).[1] 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 ${\displaystyle a}$, there exists a ${\displaystyle b}$ with ${\displaystyle a\to b}$ iff ${\displaystyle \exists b'.a\to _{S}b'}$.[4]

A one step reduction strategy is one where ${\displaystyle \to _{S}\subseteq \to }$. Otherwise it is a many step strategy.[5]

A deterministic strategy is one where ${\displaystyle \to _{S}}$ is a partial function, i.e. for each ${\displaystyle a\in A}$ there is at most one ${\displaystyle b}$ such that ${\displaystyle a\to _{S}b}$. Otherwise it is a nondeterministic strategy.[5]

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:[5]

• leftmost-innermost: in each step the leftmost of the innermost redexes is contracted, where an innermost redex is a redex not containing any redexes[6]
• 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[6]
• rightmost-innermost, rightmost-outermost: similarly

Many-step strategies include:[5]

• parallel-innermost: reduces all innermost redexes simultaneously. This is well-defined because the redexes are pairwise disjoint.
• parallel-outermost: similarly
• Gross-Knuth reduction,[7] also called full substitution or Kleene reduction:[5] 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.[8]

Stratego is a domain-specific language designed specifically for programming term rewriting strategies.[9]

In the context of the lambda calculus, normal-order reduction refers to leftmost-outermost reduction in the sense given above.[10] 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.[11][12]

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.[13][14] When "leftmost" is defined using an in-order traversal the notions are distinct. For example, in the term ${\displaystyle (\lambda x.x\Omega )(\lambda y.I)}$ with ${\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.[15]

Applicative order reduction refers to leftmost-innermost reduction.[10] In contrast to normal order, applicative order reduction may not terminate, even when the term has a normal form.[10] For example, using applicative order reduction, the following sequence of reductions is possible:

$${\displaystyle {\begin{aligned}&(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\&\ldots \end{aligned}}}$$

But using normal-order reduction, the same starting point reduces quickly to normal form:

$${\displaystyle (\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))}$$

$${\displaystyle \rightarrow z}$$

Full β-reduction refers to the nondeterministic one-step strategy that allows reducing any redex at each step.[3] Takahashi's parallel β-reduction is the strategy that reduces all redexes in the term simultaneously.[16]

Optimal reduction

Optimal reduction is motivated by the existence of lambda terms where there does not exist a sequence of reductions which reduces them without duplicating work. For example, consider

((λg.(g(g(λx.x))))
 (λh.((λf.(f(f(λz.z))))
      (λw.(h(w(λy.y)))))))

It is composed of three nested terms, x=((λg. ... ) (λh.y)), y=((λf. ...) (λw.z) ), and z=λw.(h(w(λy.y))). There are only two possible β-reductions to be done here, on x and on y. Reducing the outer x term first results in the inner y term being duplicated, and each copy will have to be reduced, but reducing the inner y term first will duplicate its argument z, which will cause work to be duplicated when the values of h and w are made known.[lower-alpha 1]

Optimal reduction is not a reduction strategy for the lambda calculus in a narrow sense because performing β-reduction loses the information about the substituted redexes being shared. Instead it is defined for the labelled lambda calculus, an annotated lambda calculus which captures a precise notion of the work that should be shared.[21]^{: 113–114}

Labels consist of a countably infinite set of atomic labels, and concatenations ${\displaystyle ab}$, overlinings ${\displaystyle {\overline {a}}}$ and underlinings ${\displaystyle {\underline {a}}}$ of labels. A labelled term is a lambda calculus term where each subterm has a label. The standard initial labeling of a lambda term gives each subterm a unique atomic label.[21]^: 132 Labelled β-reduction is given by:[22]

$${\displaystyle ((\lambda x.M)^{\alpha }N)^{\beta }\to \beta {\overline {\alpha }}\cdot M[x\mapsto {\underline {\alpha }}\cdot N]}$$

where ${\displaystyle \cdot }$ concatenates labels, ${\displaystyle \beta \cdot T^{\alpha }=T^{\beta \alpha }}$, and substitution ${\displaystyle M[x\mapsto N]}$ is defined as follows (using the Barendregt convention):[22]

$${\displaystyle {\begin{aligned}x^{\alpha }[x\mapsto N]&=\alpha \cdot N&\quad (\lambda y.M)^{\alpha }[x\mapsto N]&=(\lambda y.M[x\mapsto N])^{\alpha }\\y^{\alpha }[x\mapsto N]&=y^{\alpha }&\quad (MN)^{\alpha }[x\mapsto P]&=(M[x\mapsto P]N[x\mapsto P])^{\alpha }\end{aligned}}}$$

The system can be proven to be confluent. Optimal reduction is then defined to be normal order or leftmost-outermost reduction using reduction by families, i.e. the parallel reduction of all redexes with the same function part label.[23] The strategy is optimal in the sense that it performs the optimal (minimal) number of family reduction steps.[24]

A practical algorithm for optimal reduction was first described in 1989,[25] more than a decade after optimal reduction was first defined in 1974.[26] The Bologna Optimal Higher-order Machine (BOHM) is a prototype implementation of an extension of the technique to interaction nets.[21]^: 362[27] Lambdascope is a more recent implementation of optimal reduction, also using interaction nets.[28][lower-alpha 2]

• Reduction system
• Reduction semantics
• Thunk

• Lambda calculus reduction workbench