WHICH DATA-TYPES HAVE OMEGA-COMPLETE INITIAL ALGEBRA SPECIFICATIONS

An algebraic specification is called omega-complete or inductively complete if all (open as well as closed) equations valid in its initial model are equationally derivable from it, i.e., if the equational theory of the initial model is identical to the equational theory of the specification. As the latter is recursively enumerable, the initial model of an omega-complete algebraic specification is a data type with a recursively enumerable equational theory. We show that if hidden sorts and functions are allowed in the specification, the converse is also true: every data type with a recursively enumerable equational theory has an omega-complete initial algebra specification with hidden sorts and functions. We also show that in the case of finite data types the hidden sorts can be dispensed with.