Axioms as Rewrite Rules

We know also that the axioms of an algebraic specification can be treated as a collection of rewrite rules in which we use a restrictive form of equational logic. It is important to understand the difference between axioms (in the strict equational sense) and rewrite rules. We can represent a typical rewrite rule by

$$L \rightarrow R$$

where L, R denote the left and right components of the rule.

The fundamental difference between an axiom and a rewrite rule is that while equality for axioms is symmetric, that is L = R implies R = L and R = L implies L = R, term re-writing schema treat axioms uni-directionally, for example as one way replacements from L to R say. Hence, when axioms are treated as rewrite rules, the operator `` $\rightarrow$ '' is transitive, but not symmetric or reflexive. A computation which uses rewrite rules will produce a sequence of expressions E₁, E₂, ..., E_i by repeatedly replacing instances of the left-hand side of rules within an expression by their corresponding right-hand sides. This process will continue until an expression is obtained which contains no instances of any left-hand rule, in which case the process terminates. The resulting expression is said to be in a normal or reduced form. One restriction for such rewriting systems is that any free variable which occurs in the right-hand side R must also occur in the left-hand side L.