A completeness theorem for the expressive power of higher-order algebraic specifications

We consider the expressive power of a general form of higher-order algebraic specification which allows constructors and hidden sorts and operations. We prove a completeness theorem which exactly characterises the expressiveness of such specifications with respect to the analytical hierarchy. In particular we show that for any countable signature Sigma and minimal Sigma algebra A, A has complexity Pi(1)(1) if, and only if, A has a recursive second-order equational specification with constructors and hidden sorts and operators under higher-order initial semantics. (C) 1997 Academic Press.