Proof of the Sufficient Completeness of Stack

The claim that Stack is sufficiently complete can now be proved using the theorem just derived. The proof involves verifying that all possible outcomes of the accessor operations top and is-empty? applied to any stack value s are defined by the axioms.

>From the theorem just proved, we know that any stack value s is equivalent to a canonical form (that is s reduces either to init or to a composition of push operations). Hence if the axioms show how top and is-empty? act on init and on push(s,n) (where s $\in$ stack and n $\in$ nat), then the axiomatisation is sufficiently complete. Indeed this is precisely the systematic procedure we have been adopting so far to generate our axioms and its fundamental importance is now clear.

We now prove the corresponding result for the specification Set of Fig. 12.3.

Exercise 12.3

Show formally that remove is a non-atomic constructor operation for the specification Queue and that the collection of reduced expressions involving compositions of the atomic constructors new and add constitutes a set of canonical forms. Deduce that the axiomatisation is sufficiently complete. (If you find this difficult, see the discussion on the specification of a set data type which follows, where structural induction is used to prove corresponding results for that specification).