Proof of Canonical Property for Stack

In order to show that the above collection of reduced forms constitutes a set of canonical forms, we must demonstrate that any stack expression is equivalent to one of the above forms. In other words, we have to prove firstly that

Theorem :     any well-formed stack expression s $\in$stack is equivalent to one of the forms

(a) init

(b) ${\tt push(s',e)}$ where ${\tt s'}$ is a reduced expression and e $\in$ nat

Base Case : From our stated theorem, the base case s = init, corresponding to an expression of length 1, is true. (For this example, init is the only nullary constructor).

Hypothesis : Suppose that any given stack expression s of length n is equivalent to ${\tt push(s',e)}$ or init where ${\tt s'}$ is itself a reduced expression (of length (n - 1)). What we must do now is show that the above theorem also holds for all stack expressions obtained from s of length (n+1), that is for the terms push(s,${\tt e_n}$) and pop(s), ( ${\tt e_n \in nat}$).

Inductive Step : Given that s $\in$ stack (of length n) is a reduced expression.

(1) Consider the application of push to s. Then push ${\tt (s,e_n)}$ = push(push ${\tt (s',e),e_n)}$ and since ${\tt s'}$ is a reduced expression, push ${\tt (s,e_n)}$ is immediately of the form (b).

(2) Consider now the expression pop(s), defined for all non-empty stack values s. We can use the axioms of Stack to reduce pop(s). In particular, pop(s) = ${\tt pop(push(s',e))}$ = ${\tt s'}$ by axiom (3) of Fig. 9.7. But from our hypothesis, ${\tt s'}$ is a reduced expression (of length n - 1) so the fact that s is a reduced expression implies that pop(s) is also a reduced expression.

Hence, by induction on the length of the sequence of operation applications, we have proved that all stack expressions can be expressed in terms of just the atomic constructors init and push. What we have shown is that since the stack expression init of length 1 is a reduced expression, so is any term of length 2 obtained by applying a legal constructor operation to init. Hence, ${\tt t_2}$ = push(init, ${\tt e_1)}$ is a also a reduced expression. (Remember pop is only defined for non-empty stack values).

Continuing the inductive proof, since all stack expressions of length 2 are reduced expressions, so are all stack expressions of length 3 derived from applying legal constructor operations to ${\tt t_2}$. Hence the two terms ${\tt push(t_2, e_2)}$and ${\tt pop(t_2)}$ are also reduced expressions. Starting from these reduced expressions, any stack expression of length 4 derived from the terms of length 3 by applying the constructors push and pop will also be reduced expressions and so the inductive proof goes on.

To prove that the set of reduced expressions is a canonical set of terms, we must now show that every well-formed stack expression s is equivalent to one and only one of these reduced terms. We have already shown that every well-formed expression s is equivalent to a reduced expression. Furthermore, it cannot be shown using the axioms of Stack, that any one member of the set of reduced expressions is equivalent to another. The only way such a result could be derived was if an axiom were included which related two of the reduced expressions directly, that is an axiom whose outermost left-most operation were an atomic constructor - which is not the case here. Hence each member of the set of reduced expressions is in a different equivalence class.

We have therefore proved that every term is equivalent to a reduced term and that each reduced term is in a different equivalence class. Hence, by definition, the collection of reduced terms constitutes a set of canonical forms.