Algebraic specification with built-in domain constructions

A way of integrating predefined data type constructions into the framework of algebraic specifications is proposed in such a way that some standard results such as existence of initial and terminal algebras for hierarchical specifications are preserved. A general technique is presented which includes as special cases higher-order function spaces, cartesian products and standard power-set constructions. The central idea is to employ the generation principle also for the built-in constructions; this means that e.g. in the higher-order case not all functions use considered but only those that can be denoted by terms. This leads to a particularly simple theory by which the extended specifications can be related to the usual first-order ones.