The sufficient-completeness property of algebraic specifications is useful in providing guidelines for designing abstract data types and in proving inductive properties by the “induction-less induction” method. The sufficient-completeness check is also needed in Boyer and Moore’s computational logic. This property is undecidable in general; in fact, the authors show it to be undecidable even for linear rewriting systems with monadic function symbols and complete rewriting systems. The decidability of sufficient-completeness is known, however, for complete rewriting systems with constructor-preserving rules.

This paper discusses the complexity of sufficient-completeness checking for various subclasses of complete constructor-preserving rewriting systems. In particular, the authors establish the following results. Checking sufficient-completeness is co-NP-complete for rewriting systems with free constructors and for rewriting systems with unary and nullary constructors. For linear rewriting systems, checking sufficient-completeness is provably intractable. For constructor-preserving rewriting systems with associative functions, checking sufficient-completeness is, in general, undecidable. An exponential-time algorithm based on the test-set method is given for checking the sufficient-completeness of left-linear complete rewriting systems. These complexity results also hold for checking the ground-reducibility of constructor-preserving rewriting systems. These results are important and have ramifications for the efficiency and practicality of the methods proposed (based on ground-reducibility and test-sets) for induction-less induction.