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

This paper is dedicated to a significant section of universal algebra. This section is related to a research of the expressive power of a general form of higher-order algebraic specification which allows constructors and hidden sorts and operations. It is possible to summarize the situation for first-order algebraic specifications as follows: (i) recursive or recursively enumerable sets of first-order equations, together with first-order initial semantics, can specify precisely the countable minimal algebras of complexity \(\Sigma^0_1\); (ii) recursive or recursively enumerable sets of first-order equations, together with first-order final semantics, can specify precisely the countable minimal algebras of complexity \(\Pi^0_1\). The results of this paper deal with higher-order equational specifications which allow a subsignature of constructors, as well as hidden sorts and operations. Since any partial recursive function is recursively first-order axiomatizable and the quantifier functional is finitely second-order axiomatizable we obtain the main result of this paper. Completeness Theorem. For any countable \(S\)-sorted signature \(\Sigma\) and any minimal algebra \(A\), \(A\) has complexity \(\Pi^1_1\) if and only if, there exists a recursive second-order equational specification Spec with constructors and hidden sorts and operations such that Spec specifies \(A\) under higher-order initial semantics. This theorem precisely characterizes the expressive power of a very general form of higher-order algebraic specification. Its proof also gives deeper insight into the role of the quantifier functional and, thus, into the relationship between constructive and nonconstructive higher-order specifications. This theme forms one of the cornerstones of the theory of higher-order algebraic specification and is taken up by the author in Higher-order equational logic for specification, simulation and testing [Proc. Second Int. Workshop on Higher-order Algebra, Logic and Term rewriting, HOA '95 (1995)].