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: x=y. 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 t=v is an identity or not in the following manner. If two distinct terms t and v have the same normal form, then t=v is an identity. Otherwise, t=v 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 t=v is an identity is also known as the word problem.

Initially, this algorithm attempts to orient input identities according to the reduction order (ifs<t, then t->s 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.

See also

Buchberger's Algorithm, Confluent, Finitely Terminating, Gröbner Basis, Kruskal's Tree Theorem, Term Rewriting System

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha


Baader, F. and Nipkow, T. Term Rewriting and All That. Cambridge, England: Cambridge University Press, 1999.Knuth D. E. and Bendix P. B. "Simple Word Problems in Universal Algebra." In Computational Problems in Abstract Algebra (Proc. Conf., Oxford, 1967). Pergamon Press, pp. 263-297, 1970.Wolfram, S. A New Kind of Science. Champaign, IL: Wolfram Media, p. 1037, 2002.

Referenced on Wolfram|Alpha

Knuth-Bendix Completion Algorithm

Cite this as:

Sakharov, Alex. "Knuth-Bendix Completion Algorithm." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein.

Subject classifications