Canonical Forms for the Stack

>From the outset we have asserted that any stack value of sort stack can be ``constructed'' using just the atomic constructors init and push. In other words the set of reduced expressions

{init, push(init, e1), push(push(init, e1), e2), ...}

for all e1, e2, ...$\in$ nat constitutes a set of canonical forms. This assertion will now be proved using structural induction.

To start, we define more precisely what we mean by the length of a sequence of operation applications (for this example expressions whose result are of type stack). The length len of a stack expression is defined as the number of occurrences of the constructor names init, push and pop which appear as the left-most outermost part of a stack expression. In other words, the function len is defined recursively as

• len (init) = 1
• len (push(s,n)) = 1 + len (s)
• len (pop(s)) = 1 + len (s)

where s $\in$ stack and n $\in$ nat. Hence, for example

(a) len (init) = 1

(b) len (push(push(init,3),6)) = 3

(c) len (push(pop(push(init,2)),4)) = 4

(d) len (pop(pop(push(push(init,1),2)))) = 5

(e) len (push(init,top(push(init,1)))) = 2

Note that in the last example (e), the subterm top(push(init,1)), (which produces a value which belongs to nat), does not contribute to the length of the outer expression - we are concerned only with the length of expressions constructed from compositions of the constructor operations. (In other words, expressions returning values other than of sort stack must be evaluated before len).

We recall that a reduced stack expression is one which is either the empty stack, init or an expression of the form push(s,e) where e $\in$ nat and s is itself a reduced expression. (That is reduced expressions are terms involving only the atomic constructors of Stack). Hence, a general reduced expression of length n is given by

push( ... push(push(init,${\tt e_1}$),${\tt e_2}$) ... , ${\tt e_{n-1}}$)

where ${\tt e_i} \in {\tt nat}$, ( $1 \leq i \leq (n - 1)$).