Knuth-Bendix Completion Algorithm

The Knuth-Bendix completion algorithm attempts to transform a finite set of identities into a finitely terminating, confluent term rewriting system whose reductions preserve identity. This term rewriting system serves a decision procedure for validating identities.

As defined in universal algebra, identities are equalities of two terms: . Presumably, the values of the two terms are equal for all values of variables occurring in them. A reduction order is another input to the completion algorithm provided that every identity is viewed as two candidates for rewrite rules transforming the left-hand side into the right-hand side and vice versa.

The output term rewriting system is used to determine whether is an identity or not in the following manner. If two distinct terms and have the same normal form, then is an identity. Otherwise, is not an identity. Term rewriting systems that are both finitely terminating and confluent enjoy the property of having unique normal forms for all expressions. The problem of deciding whether is an identity is also known as the word problem.

Initially, this algorithm attempts to orient input identities according to the reduction order (if, then becomes a rule). Then, it completes this initial set of rules with derived ones. The algorithm iteratively detects critical pairs, obtains their normal forms, and adds a new rule for every pair of the normal forms in accordance with the reduction order.

This algorithm may

1. Terminate with success and yield a finitely terminating, confluent set of rules,

2. Terminate with failure, or

3. Loop without terminating.

Note that Buchberger's algorithm for constructing Gröbner bases is very similar to the Knuth-Bendix completion algorithm.

Wolfram Web Resources