Reduction

Definition

In an abstract reduction system, a reduction is a step $a\to b$ from one object to another according to the chosen reduction relation.

In a term rewriting system, reductions are generated by applying a rewrite rule to a matching subterm.

Reduction Sequences

Repeated reductions form a reduction sequence. One usually writes:

• $a\to b$ for one step
• $a{\to }^{\ast }b$ for zero or more steps
• $a{\to }^{+}b$ for one or more steps

The reflexive-transitive closure ${\to }^{\ast }$ is often the main relation used when stating properties such as confluence or the existence of normal forms.

Related Concepts

Abstract Reduction System
Reduction Rule
Normal Form
Confluence
Strong Normalization

References

baader1998-term-rewriting