A data structure is a heterogeneous algebra in which every element is denoted by a ground term, i.e., a term without variables. A data type is an isomorphism class of a data structure….Our main results on specification are the following. An equality-test algebra is a heterogeneous algebra with a two-element Boolean sort and an equality-test operation for each non-Boolean sort. The if-then-else algebras are obtained from the equality-test algebras by adjoining the if-then-else operation for each non-Boolean sort. We give a simple algorithm that converts any universal initial or final specification of an equality-test data type A into a conditional specification of A; moreover the new specification is complete in the sense that it is both initial and final. As a consequence every semicomputable or cosemicomputable equality-test data type is computable. If A is an arbitrary data type, essentially the same algorithm can be used to convert a universal initial specification of A into a conditional specification with the equality-tests as hidden operations. In this case the new specification will be complete only if the original one is complete. Thus an arbitrary data type is computable if and only if its equality-test enrichment is semicomputable or, equivalently, cosemicomputable….
Many of the above results can be improved in the presence of if-then-else operations….
The main feature of the paper, and the principal tool in obtaining the specification results mentioned above, is a detailed analysis of the structure of the algebras in the quasi variety and variety generated, respectively, by all equality-test and if-then-else algebras of a fixed but arbitrary finite signature….
In fact our two main structure theorems can beviewed as analogues of the Stone representation theorem of Boolean algebra….
With regard to equality-test algebras, the method of initial specification is no more powerful than complete (i.e., simultaneous initial and final) specification….
In [1] we extend the investigations of this paper to equality-test algebras in which the equality-tests may take values in a multiple-valued logic different from classical two-valued logic….
--From the Paper
This paper also investigates the power of conditional and equational specifications of arbitrary data types when the Boolean sort and the equality-tests and if-then-else operations are hidden. The hiding makes little difference in the equality-test case, but Pigozzi shows that arbitrary incomplete initial specifications cannot be converted to equational specifications by hidden operations.