Reduction Rule

Definition

A reduction rule is a schema that generates individual reduction steps. In a term rewriting system, a rule is typically written $l\to r$, indicating that an instance of the pattern $l$ may be replaced by the corresponding instance of $r$.

Usually one requires every variable occurring in $r$ to already occur in $l$, so that applying the rule does not introduce arbitrary new variables.

In Term Rewriting

Given a substitution $\sigma$ and a context $C[-]$, a rule $l\to r$ induces a step

$C[l\sigma ]\to C[r\sigma ].$

This is how a finite presentation of rules generates the global reduction relation on terms.

Related Concepts

Reduction
Abstract Reduction System
Term Rewriting System
Small-step operational semantics

References

baader1998-term-rewriting