Design and Analysis of Algorithms

606 Design and Analysis of Algorithms

The fi rst thing to note in 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 fi rst reduction, looking down the list of

axioms, we look for any axioms that have pop as the fi rst operation on their left-hand side. The fi rst 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 unifi er is

s ← init; n ← 3 (21)

or equivalently replace s by init ...