Abstract data type as an algebra

Remarks

Initial models exist, and any two of them are isomorphic, so the abstract data type is one isomorphism class of algebras; this is the initial algebra semantics of the specification. An initial model has two features. Every element is the value of a ground term ("no junk"), and two ground terms are equal in it only if $E$ proves them equal ("no confusion").

Example: sorts $\mathrm{nat}$ and $\mathrm{bool}$; constants $\mathrm{true}, \mathrm{false} \colon \mathrm{bool}$ and $0 \colon \mathrm{nat}$; operations $s \colon \mathrm{nat} \to \mathrm{nat}$ and $\mathrm{iszero} \colon \mathrm{nat} \to \mathrm{bool}$; equations $\mathrm{iszero}(0) = \mathrm{true}$ and $\mathrm{iszero}(s(x)) = \mathrm{false}$. The model with carriers $\N$ and $\set{\mathrm{true}, \mathrm{false}}$ is initial. Each element is the value of a ground term, and two ground terms with the same value are equal by the equations.

Non-example: the model with one element in each sort satisfies $E$ but is not initial. A homomorphism from it to the model above would send its single Boolean element to both $\mathrm{true}$ and $\mathrm{false}$, which is impossible.