Equality-Test and If-Then-Else Algebras: Axiomatization and Specification
Don Pigozzi · SIAM Journal on Computing · 1991
An equality-test algebra has a two-element Boolean sort and an equality-test operation $eq_s $ for each non-Boolean sort s, where $eq_s (x,y)$ equals TRUE if $x = y$ and FALSE otherwise. An if-then-else algebra is an equality-test algebra with the if-then-else operations $[\_,\_,\_]_s $ adjoined: $[b,x,y]_s $ equals x if $b = \text{TRUE}$ and y if $b = \text{FALSE}$. A finite set of axioms for the conditional-equational (i.e., quasi-equational) theory of equality-test algebras is given. A finite axiomatization of the equational theory of if-then-else algebras is also given, and it is shown that this also serves as a basis for the conditional-equational theory of if-then-else algebras. Finite bases for the equational theories of several classes of algebras closely related to if-then-else algebras were previously known. The power of conditional and equational specifications of equality-test and if-then-else data types are investigated, and the following results, among others, are obtained. (i) Every equality-test data type that can be specified in either the initial or final algebra sense by a finite set of universal first-order sentences can be completely specified (i.e., in both the initial and final algebra senses simultaneously) by a finite set of conditional equations. (ii) The same as (i) but with “equality-test” and “conditional equations” replaced, respectively, by “if-then-else” and “equations.” (iii) An arbitrary data type that can be specified in the initial algebra sense by a finite set of universal sentences can be specified in the same sense by a finite set of conditional equations with the equality-test operations as hidden operations. (iv) The same as (iii) but with “conditional equations” replaced by “equations,” and the if-then-else operations adjoined as additional hidden operations; this holds however only under the additional hypothesis that the original specification is complete.