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.
KeywordsExpert System Procedure Call Automatic Theorem Prove Abstract Data Type Remote Procedure Call
- [Huet & Oppen 80]Huet, G. and Oppen, D.C. Equations and Rewrite Rules: A Survey. Technical Report CSL-111. SRI international. January. 1980.Google Scholar