Quotient Term Algebra

Under equational inference, with no axioms, each term of a theory presentation would denote a distinct value for any initial interpretation. The axioms identify those terms which are to have equivalent meanings in the intended semantic domain (model), that is those which are to denote the same value. Pairs of terms not equivalent under the axioms are treated as denoting distinct values. Identifying equivalent terms in the term algebra generates what is called the quotient term algebra or quotient term structure, and this aspect is worth developing in a little more detail.

The axioms of a specification define a collection of equality relations between the variable-free (ground) terms for each sort. These equality relations are equivalence relations in that they are reflexive, symmetric and transitive. For example, for the specification Stack of Fig. 8.2, the following ground terms are all equal

init,     pop(push(init,3)),      pop(pop(push(push(init,1),2)))

pop(push(init,top(push(init,1))))

and this property stems directly from the inference rules of equational logic. If we use the notation <t> to denote the set of all terms equivalent to a given term t, the above terms are members of the equivalence class $<{\tt init}>$ where we have selected the ``simplest'' term init (simplest in the sense of being the shortest string) to represent the class, although any member of the equivalence class could have been chosen.

For each sort, the axioms (equality relations) therefore partition the ground terms of the term algebra into a number of equivalence classes. If we imagine partitioning all the ground terms of the term algebra into the appropriate collection of equivalence classes, the resulting algebra whose carrier set(s) consist of this collection of equivalence classes is called the quotient term algebra. For the quotient term algebra, each member of the carrier(s) is an equivalence class of terms and we are at liberty to choose any member of an equivalence class to represent that class. An important property of the quotient term algebra is that this algebra is initial.

A distinct advantage of using term algebras is that term rewriting can be performed directly upon the theory presentation itself.