knuth-bendix completion algorithm

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. The word problem is, in general, undecidable, hence the algorithm cannot always terminate successfully. If it does not succeed, it will either run forever, or fail when it encounters an unorientable equation (i.e. an equation that it cannot turn into a rewrite rule). The enhanced completion without failure will not fail on unorientable equations and provides a semi-decision procedure for the word problem.

Description of the algorithm

Suppose we are given a presentation

\langle X \mid R \rangle

, where

X

is a set of generators and

R

is a set of relations giving the rewriting system. Suppose further that we have a well-ordering

<

words generated by

X

. For each relation

P_i = Q_i

R

, suppose

Q_i < P_i

. Thus we begin with the set of reductions

P_i \rightarrow Q_i

. First, if any relation

P_i = Q_i

can be reduced, replace

P_i

and

Q_i

with the reductions. Next, we add more reductions (that is, rewriting rules) to eliminate possible exceptions of confluence. Suppose that

P_i

and

P_j

, where

i \neq j

, overlap. That is, either the prefix of

P_i

equals the suffix of

P_j

, or vice versa. In the former case, we can write

P_i = BC, P_j = AB

; in the latter case,

P_i = AB, P_j = BC

. Reduce the word

ABC

using

P_i

first, then using

P_j

first. Call the results

r_1, r_2

, respectively. If

r_1 \neq r_2

, then we have an instance where confluence could fail. Hence, add the reduction

\max r_1, r_2 \rightarrow \min r_1, r_2

R

. After adding a rule to

R

, remove any rules in

R

that might have reducible left sides. Repeat the procedure until all overlapping left sides have been checked.

Example

Consider the presentation

\{ x, y \mid x^3 = y^3 = (xy)^3 = 1 \}

. We use the lexicographic ordering. In fact, this is an infinite group. Nevertheless, the Knuth-Bendix algorithm is able to solve the word problem. Our beginning three reductions are therefore (1)

x^3 \rightarrow 1

, (2)

y^3 \rightarrow 1

, and (3)

(xy)^3 \rightarrow 1

. First, we see an overlap of

x

in (1) and (3). Consider the word

x^3yxyxy

. Reducing using (1), we get

yxyxy

. Reducing using (3), we get

x^2

. Hence, we get

yxyxy = x^2

, giving the reduction rule (4)

yxyxy \rightarrow x^2

. Similarly, using the overlap of

y

in (2) and (3), we get the reduction (5)

xyxyx \rightarrow y^2

. Both of these rules obsolete (3), so we remove it. Next, consider the overlap of

x

of (1) and (5). Considering

x^3yxyx

we get the rule

yxyx = x^2y^2

, so we get the rule (6)

yxyx \rightarrow x^2y^2

. This obsoletes rule (4) and (5), so we remove them. Considering

xyxyx^3

, we get

xyxy = y^2x^2

, so we get the rule (7)

y^2x^2 \rightarrow xyxy

. Now, we are left with the rewriting system

(1) $x^3 \rightarrow 1$
(2) $y^3 \rightarrow 1$
(6) $yxyx \rightarrow x^2y^2$
(7) $y^2 x^2 \rightarrow xyxy$

Checking the overlaps of these rules, we find no potential failures of confluence. Therefore, we have a confluent rewriting system, and the algorithm terminates successfully.

<< Previous

Word Browser

Next >>

good manufacturing practice
self sufficient homes
replay attack
tacna
jg leathers
active wiretapping
bengt linder
barleysnail
llanvapley
onitsha
koprivshtitsa

david grubbs
passive wiretapping
pucallpa, peru
guy klucevsec
tony cedras
dandong
carmichael
bank of crete
anders bircow
rivas
the darling buds of may

pts dos
thomas fitzgerald
distant early warning line
guy vanderhaeghe
rafael carrera
masked shrike
sinuiju
autorooter
voltage controlled filter
paschen's law
uss sacagawea (yt 326)

kingdom of benin
list of classical architecture terms
st. joseph river
kandahar, saskatchewan
len dawson
uss mercy (ah 4)
uss savannah (cl 42)
eikon basilike
lydia lopokova
uss mercy (ah 8)
event related potential