Knuth–Bendix completion algorithm

Knuth–Bendix completion algorithm
Name	Knuth–Bendix completion algorithm
Class	Term rewriting
Data	Rewrite rules
Time	Not guaranteed to terminate
Space	Varies
Authors	Donald Knuth, Peter Bendix
Year	1970

Knuth–Bendix completion algorithm is a fundamental method in computer algebra and automated theorem proving for transforming a set of equational axioms into a confluent term rewriting system. Developed by Donald Knuth and Peter Bendix in 1970, it provides a semi-decision procedure for the word problem in universal algebra. The algorithm attempts to generate a complete set of rewrite rules from which the equivalence of any two terms can be decided by normalization.

Overview

The algorithm addresses a core problem in symbolic computation: determining if two expressions, defined by a set of algebraic identities, are provably equal. It operates on a finite set of equations and a chosen well-founded term ordering, such as the lexicographic path ordering. The goal is to produce a terminating and confluent (or complete) set of rewrite rules. This process is closely related to the concept of Gröbner bases in commutative algebra, but for general, non-commutative algebraic structures. The completion procedure is a critical component in systems like the Maude language and the Theorema project.

Algorithm description

The procedure begins with an initial set of oriented equations, treated as directed rewrite rules. The main loop involves two operations: critical pair generation and rule simplification. All possible superpositions of left-hand sides of rules are computed to find critical pairs. Each new critical pair is normalized using the current rule set; if the two normalized forms are not identical, a new rule is added, orienting them according to the chosen term ordering. Existing rules are also simplified by rewriting their right-hand sides with newer, more general rules. This process iterates until no new non-joinable critical pairs remain, indicating a complete system, or it may run indefinitely.

Termination and correctness

Termination of the Knuth–Bendix procedure is not guaranteed; it may fail by generating an infinite sequence of new rules or by encountering an equation that cannot be oriented by the given ordering. Successful termination produces a complete rewriting system, which solves the word problem for the presented algebra. Correctness relies on the properties of the term ordering ensuring termination and the completion process preserving the original equational theory. The theoretical foundation is deeply connected to the Newman's Lemma and the Knuth–Bendix theorem for abstract reduction systems.

Examples

A classic example is completing the axioms for groups. Starting with equations for associativity, identity, and inverses, the algorithm can derive a complete set of rules for free groups. Another well-known case is the completion for monoids or semigroups, often studied in conjunction with the Makanin's algorithm for solving equations. The algorithm can also be applied to finitely presented algebras in varieties like Boolean algebras or lattices, demonstrating its utility across different branches of universal algebra.

Extensions and variations

Many extensions have been developed to increase the algorithm's power and scope. The unification algorithm is integrated in versions for equational unification. Order-sorted and many-sorted generalizations handle typed algebraic specifications. The completion procedure has been adapted for associative-commutative (AC) operators, leading to AC-completion algorithms used in systems like REVE and SPIKE. Other variants include incremental completion, constraint-based completion, and integration with model checking techniques for infinite state systems.

Applications

The Knuth–Bendix algorithm is a cornerstone of automated reasoning. It is implemented in theorem provers such as OTTER, E, and Waldmeister. In functional programming, it underpins equational reasoning tools and Haskell's type class resolution. Within computer algebra systems like Mathematica and Maple, it aids in simplifying symbolic expressions. Further applications exist in protocol verification, rewrite-based programming languages like Elan, and the analysis of string rewriting systems and semi-Thue systems.

Category:Automated theorem proving Category:Algorithms Category:Term rewriting