Term Rewriting for Stack

These ideas are explored further with the help of some examples for the stack. With reference to the specification Stack of Fig. 8.2 consider the term

t = push(pop(push(init,3)), 1)

which has the subterm u = pop(push(init,3)).

The first thing to note for this example is that there are no axioms which have push as the left-most operation on the left-hand side of an axiom. Therefore, for the first reduction, looking down the list of axioms, we look for any axioms that have pop as the first operation on their left-hand side. The first such axiom, pop(init) = stack-error cannot be used since init is not a variable, but the second axiom pop(push(s,n)) = s can be applied, with the left-hand side L as pop(push(s,n)), and the right-hand side R as s. The appropriate unifier is

s      $\leftarrow$     init         ;         n      $\leftarrow$     3

or equivalently replace s by init and n by 3.

The subterm u of t is now replaced by the right-hand side of the rewrite rule R, with all variables in the substitutions replaced by their corresponding terms. Hence the subterm u of t rewrites to the value init and the term t becomes

t = push(init,1)

This term, which corresponds to a stack containing the single value 1, is now in reduced form since there are no axioms which have push as the outermost operation on the left-hand side of a rule. In general, however, the process will continue until no further reductions are possible.