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.