Sufficient-completeness,ground-reducibility and their complexity

Summary The sufficient-completeness property of equational algebraic specifications has been found useful in providing guidelines for designing abstract data type specifications as well as in proving inductive properties using the induction-less-induction method. The sufficient-completeness property is known to be undecidable in general. In an earlier paper, it was shown to be decidable for constructor-preserving, complete (canonical) term rewriting systems, even when there are relations among constructor symbols. In this paper, the complexity of the sufficient-completeness property is analyzed for different classes of term rewriting systems. A number of results about the complexity of the sufficient-completeness property for complete (canonical) term rewriting systems are proved: (i) The problem is co-NP-complete for term rewriting systems with free constructors (i.e., no relations among constructors are allowed), (ii) the problem remains co-NP-complete for term rewriting systems with unary and nullary constructors, even when there are relations among constructors, (iii) the problem is provably in almost exponential time for left-linear term rewriting systems with relations among constructors, and (iv) for left-linear complete constructor-preserving rewriting systems, the problem can be decided in steps exponential innlogn wheren is the size of the rewriting system. No better lower-bound for the complexity of the sufficient-completeness property for complete (canonical) term rewriting system with nonlinear left-hand sides is known. An algorithm for left-linear complete constructor-preserving rewriting systems is also discussed. Finally, the sufficient-completeness property is shown to be undecidable for non-linear complete term rewriting systems with associative functions. These complexity results also apply to the ground-reducibility property (also called inductive-reducibility) which is known to be directly related to the sufficient-completeness property.Some of the results in this paper were reported in a paper titled Complexity of Sufficient-Completeness presented at theSixth Conf. on Foundations of Software Technology and Theoretical Computer Science, New Delhi, India, Dec. 1986. The term quasi-reducibility is replaced in this paper by ground-reducibility as the latter seems to convey a lot more about the concept than the former.Partially supported by the National Science Foundation Grant nos. CCR-8408461 and CCR-8906678Partially supported by the National Science Foundation Grant nos. CCR-8408461 and CCR-9009414Partially supported by the National Science Foundation Grant no. DCR-8603184