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?and minimal?algebraA,Ahas complexity?11if, and only if,Ahas a recursive second-order equational specification with constructors and hidden sorts and operators under higher-order initial semantics.