A completeness theorem for the expressive power of higher-order algebraic specifications
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)].
- A recursive second order initial algebra specification of primitive recursion
- Algebraic specifications of computable and semicomputable data types
- Correctness of dataflow and systolic algorithms using algebras of streams
- scientific article; zbMATH DE number 3888893 (Why is no real title available?)
- scientific article; zbMATH DE number 3911679 (Why is no real title available?)
- scientific article; zbMATH DE number 3655328 (Why is no real title available?)
- scientific article; zbMATH DE number 3784848 (Why is no real title available?)
- scientific article; zbMATH DE number 3577197 (Why is no real title available?)
- scientific article; zbMATH DE number 217097 (Why is no real title available?)
- Initial and Final Algebra Semantics for Data Type Specifications: Two Characterization Theorems
- On the power of higher-order algebraic specification methods
- The completeness of the algebraic specification methods for computable data types
- Universal algebra in higher types
- Proof theory of higher-order equations: Conservativity, normal forms and term rewriting.
- On the power of higher-order algebraic specification methods
- Verifying an infinite systolic algorithm using third-order equational methods
- On algebraic specifications of computable algebras with the discriminator technique
- scientific article; zbMATH DE number 4078768 (Why is no real title available?)
- scientific article; zbMATH DE number 4078770 (Why is no real title available?)
- scientific article; zbMATH DE number 18648 (Why is no real title available?)
- Higher-order equational logic for specification, simulation and testing
- Higher-order algebra with transfinite types
This page was built for publication: A completeness theorem for the expressive power of higher-order algebraic specifications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1362341)
