Canonical Term Algebra and Reduced Expressions

While the basic idea of generating all the terms of the term algebra and then placing each term in an appropriate equivalence class may seem attractive, the approach does not provide a practical method for deriving an initial algebra. However the use of canonical terms, also referred to as canonical forms provides us with a pragmatic solution to this problem. It is often possible to identify a subset of the terms such that each term in the subset is a member of a different equivalence class and every term of the term algebra is equivalent to exactly one member of this subset. The individual terms which comprise such a subset are called canonical terms and algebras whose carrier sets consist of such a collection of canonical terms are referred to as canonical term algebras. It is not hard to see that the resulting algebra whose carrier set consists of these canonical terms will be isomorphic to the quotient term algebra and hence will itself be initial.

Moreover, if an appropriate set of atomic constructors can be identified, it can be shown that each reduced expression (that is any ground term consisting of a composition of atomic constructors) is also a canonical term. This result is proved in chapter 12. Canonical terms can therefore be systematically generated using the atomic constructors and a canonical term algebra derived. Identification of a set of atomic constructors for an abstract data type therefore provides a valuable link between the (initial) canonical term algebra and our intuitive conception of the properties of that abstract data type.

In the case of the presentation of Fig. 10.3, the initial algebra ${\cal A}_{CanonicalNat}$of canonical terms can be derived using the corresponding atomic constructors zero and succ

$${\cal A}_{CanonicalNat} = [A_{CanonicalNat}, \{ {\tt zero}, \enskip {\tt succ}, \enskip {\tt add} \}]$$

where the carrier set of the algebra is

$$A_{CanonicalNat} = \{{\tt zero, \enskip succ(zero), \enskip succ(succ(zero)), \enskip \dots }\}$$

Note that each member of the carrier set of a canonical term algebra is an individual term drawn from the term algebra. Compare this with the quotient term algebra where the individual members of the carrier set are sets of values (equivalence classes).