INFINITE, CANONICAL STRING REWRITING-SYSTEMS GENERATED BY COMPLETION

Most versions of the Knuth-Bendix completion 'procedure' are designed to compute when possible a canonical rewriting system. We show that even for string rewriting systems (SRSs) canonical systems may be generated by completion which are not recursively enumerable. This may happen also if the SRS has decidable word problem. We analyze how this phenomenon depends on the ordering used for completion. It turns out that in general if a SRS is completed with respect to a length-lexicographic ordering divergence sequences encoding the input/output behaviour of any primitive recursive function as well as any recursively enumerable set and some non recursively enumerable sets may be generated. But, if a SRS with decidable word problem is completed with such an ordering, then the generated canonical system will be recursive.