Proof of Canonical Property for Set

To prove that the set of terms

  {empty, add(empty, n1), add(add(empty, n1), n2) , ...

           add( ... add(add(empty, n1), n2) ... , np) , ... }

with the ordering n1 < n2 < ... < np constitutes a set of canonical terms we must first demonstrate that each such term belongs to a different equivalence class. This result follows immediately by observing first that no two terms of this set can be proved to be equivalent as a result of the axioms. We must next show that any reduced set expression s is equivalent to one of these canonical forms.

Given a general set expression s of the form

add( ... add(add(empty, v1), v2) ... , vp)

where v1, v2, ... , vp $\in$ nat are not necessarily ordered and may include duplicate values, then repeated application of axiom (5) of Fig. 12.3 will ``reduce'' the above expression to a canonical form in which the values v1, v2, ... are ordered with all duplicates removed. This result follows since the ELSE clause of axiom (5) can be applied to interchange two adjacent values, for example add(add( ... , vi), vj) is equivalent to add(add( ... , vj), vi) and repeating this process, the subterms can be arranged with the v1, v2 , ... , vp values arranged in ascending order. The procedure is nothing more than a bubble sort. (With a bubble sort, a sequence of values can be placed in ascending or descending order by systematically comparing adjacent pairs of values and interchanging their position if the two values are not in the required order. This procedure is repeated on each new sequence of values until every pair of adjacent values is in the correct order).

Identical values will be brought together which can then be removed using the THEN clause of axiom (5). This idea is explained further in the next section when we discuss the use of hidden operations.

We have shown that any reduced expression is equivalent to a term in our proposed set of canonical terms. However, to prove that our set of terms is indeed a canonical set, we must now show that any set term s can be reduced to one of the proposed canonical forms. Just as with the stack example, we prove this result using structural induction.

Theorem :     all well-formed set expressions s $\in$ set can be reduced to one of the forms

(a) empty

(b) add(add( ... add(add(empty, e1), e2) ... , ek), em)

where e1 < e2 < ... < ek < em.

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

Hypothesis :     Suppose that any given set expression s of length n can be reduced to

add(add( ... add(add(empty, e1), e2) ... , ek), em)

where e1 < e2 < ... < ek < em (and m = n - 1).

What we must do now is show that the above theorem also holds for all set expressions obtained from s of length (n+1), that is for the terms add(s, en) and delete(s, en), (en $\in$ nat