Rewrite Rules

Abstract

Rewrite rules are sets of ordered pairs of expressions (lhs,rhs) usually depicted as (lns ⇒ rhs). There is usually a similarity relation between the “lhs” and the “rhs” such as equality, inequality or double implication. Rewrite rules, as the pairs are called, together with the rewriting rule of inference allow one expression to be “rewritten” into another. A subexpression of the initial expression is matched with the “lhs” of the rewrite rule yielding a substitution. The resulting expression is the expression obtained by replacing the distinguished subexpression with the “rhs” of the rewrite rule after applying the substitution.