The term algebra quotiented by the equations into equivalence classes is
called the Initial algebra. It can readily be seen that this algebra is
isomorphic to |Num| and also to 
, which are therefore also
initial algebras; the choice of labels for the classes is immaterial.
The isomorphism from the partitioned term algebra to |Num| can be
thought of as an evaluation function; each equivalence class is given
a value in the set of Natural numbers. There is no junk in the
initial model, (`spare' elements in the carrier which are not the
value of any class of terms), and no confusion (about the correct
value for a particular class). The initial algebra is unique up to
isomorphism.
We might ask how the initial model stands in relation to the other possible models of the theory; in fact, the class of initial algebras of a given theory possesses a unique property vis-à-vis other models. We can state this property as follows:
If |I| is an initial model ofThe uniqueness property of the homomorphism amounts to the `no junk, no confusion' condition described above; the presence of either of these in the model would mean that there were other possible homomorphisms.and |M| is any other model then there exists a unique homomorphism h from |I| to |M|:
When abstract data types are specified algebraically, the initial model is often taken as the meaning of the specification. Being unique up to isomorphism, it has the desirable property of being independent of any particular representation. It is also the case that the initial algebra always exists and can be constructed from the term algebra, partitioned or quotiented by the equations. (If the set E of equations is empty then the term algebra itself is initial). It is important to be aware that distinct terms are regarded here as distinguishable until equations have been used to prove that they can be grouped into equivalence classes. This assumption -- that elements are distinguishable until they are proved to be equivalent -- characterises initial algebra semantics.