Sufficient-completeness, ground-reducibility and their complexity (Q2641108)

The complexity of checking term rewriting systems for sufficient completeness is considered. Given an equational theory, its function symbols are supposed to be divided into two classes: constructors and non-constructors. Constructors are operations used to construct the values of a data type, and non-constructors are the remaining operations which are defined on ground terms. An equational theory is sufficiently complete iff for every ground term (term without any variables), there is an equivalent ground term built up using only constructors. A number of results about the complexity of this property is analyzed for different classes of term rewriting systems.