Knuth-Bendix completion algorithm Guide, Meaning , Facts, Information and Description
The Knuth-Bendix completion algorithm is an algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it has effectively solved the word problem for the specified algebra. Hence, it can also be used to solve the coset enumeration problem. Note that since the word problem is, in general, undecidable, the algorithm is not guaranteed to succeed. Its original version may fail in certain situations , the enhanced completion without failure may fail to terminate instead.
Suppose we are given a presentation , where is a set of generatorss and is a set of relations giving the rewriting system. Suppose further that we have a well-ordering words generated by . For each relation in , suppose . Thus we begin with the set of reductions .
First, if any relation can be reduced, replace and with the reductions.
Next, we add more reductions (that is, rewriting rules) to eliminate possible exceptions of confluence. Suppose that and , where , overlap. That is, either the prefix of equals the suffix of , or vice versa. In the former case, we can write ; in the latter case, .
Reduce the word using first, then using first. Call the results , respectively. If , then we have an instance where confluence could fail. Hence, add the reduction to .
After adding a rule to , remove any rules in that might have reducible left sides.
Repeat the procedure until all overlapping left sides have been checked.Description of the algorithm
