Which data types have ω-complete initial algebra specifications?

An algebraic specification is called ω-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 ω-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 ω-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.

Authors

• J.A. Bergstra
• J. Heering

Keywords

No keywords are indexed for this paper.