Knuth-Bendix Completion on Non-Abelian Group Theory

Applying Knuth-Bendix Completion to the theory of non-abelian groups to come to a rewrite system that reflects decidability of the theory it implements, where semantic equality is equivalent to syntactic equality of normal forms.

Introduction

It turns out that the way we were thought group theory in the lower grades of high school was not optimal, at least not from a computational point of view. Simple statements in group theory could be rather tricky to prove, while some theories are decidable and consequently problems formulated in these theories can be solved mechanically.

In this post, we will use a procedure referred to as Knuth-Bendix completion to transform the traditional axioms for non-abelian group theory into a deterministic rewrite system with the same expressive power. The different steps of the procedure are enumerated exhaustively. Intermediate theories will introduce new axioms and make older ones obsolete.

Being exhaustive makes the post somewhat verbose. In fact, the text has largely been generated as a side effect of the automation of the Knuth-Bendix completion procedure. Skip the sections that feel like you get them. Use them for reference if you are interested in the detail.

The whole Knuth-Bendix completion procedure on non-abelian group theory is presented graphically using the graphviz dot language. Go for the graphics if you want to scan through quickly.

Non-Abelian Groups

A non-abelian group is defined as a collection of elements, a binary operation on these elements and four axioms: closure, identity, invertibility and associativity. We will consider the collection of all well-formed terms over an alphabet using a typical algebraic term syntax, meaning closure is implicit.

The theory of non-abelian groups can then be formulated using the axioms:

[1] a*1 = a
[2] a*i(a) = 1
[3] a*b*c = a*(b*c)

Here, the binary operation is represented by an asterisk (*), and any letter that is not used as a functor denotes a variable.

Briefly explained:

• Axiom [1] states that there is an element 1 which is the right-side identity for the operation.
• Axiom [2] states that the unary functor i denotes right-side inverse element of its argument.
• Axiom [3] expresses that the binary operation is associative. The operation is assumed to associate to the left, but that is mere notational convention.

A Simple Exercise

Semantic equality in non-abelian groups is decidable, meaning that there is an effective procedure to determine semantic equality within finite space and time. However, using the axioms provided above, decidability may not be apparent.

Let's illustrate the problem with a simple exercise, proving that the right-side inverse is also the left-side inverse, a property known to be valid for non-abelian groups. In other words, the exercise is to prove, for all a, the following equation:

i(a)*a = 1

Before reading on, we urge you to give it a try, to appreciate how tricky the exercise is, given the axioms provided above.

The proof is given using the following derivation:

i(a)*a
  [1]= i(a)*a*1
  [2]= i(a)*a*(i(a)*i(i(a)))
  [3]= i(a)*a*i(a)*i(i(a))
  [3]= i(a)*(a*i(a))*i(i(a))
  [2]= i(a)*1*i(i(a))
  [1]= i(a)*i(i(a))
  [2]= 1

As one can see, the proof requires making the term i(a)*a much more complex before reducing the complexity to obtain the desired result. Proving equality using the axioms above is semi-decidable. If you cannot find the proof, there is no way of knowing whether equality does not hold or whether you did not try hard enough.

Rewrite Systems

So far, we have been using the term theory as referring to a collection of axioms, and the term axiom as the equality of two terms, symmetric. In what follows, we will be using the term rewrite rule to refer to a directed axiom, which can be used only from left to right. We will refer to a collection of rewrite rules as a rewrite system.

A rewrite system may suffer the same problem regarding decidability as a theory does. However, under the right conditions a rewrite system may reflect the decidability of the theory it implements.

Rewriting a term using a rewrite system is referred to as reduction. If a term has a unique simplest, reduced form, this is called the normal form of the term. If all terms have a normal form, the rewrite system is called confluent.

This post is about transforming the theory of non-abelian groups described above to a rewrite system that implements the semantics of that theory and that is decidable.

Knuth-Bendix Completion

The Knuth-Bendix completion procedure starts off by restricting the use of the axioms to a single direction, from complex to simple. Typically, syntactic complexity is used as a metric.

Obviously, the rewrite system consisting of rewrite rules (directed axioms) does not implement the full semantics of the theory we started off with. One can prove equality for many more terms with the theory than with the rewrite system obtained out of it by directing axioms.

The Knuth-Bendix completion procedure will therefore try adding new axioms to the rewrite system in order to restore the expressive power. It will do so by looking for occurrences of the left-hand side of a rewrite rule in the left-hand side of another rewrite rule, using unification. When applying the substitution obtained by the unification to the left-hand side of the latter rewrite rule, we get a term that can be reduced (rewritten) in two distinct ways, once using each of the two rewrite rules involved.

If these reductions result in syntactically different terms, a so-called critical pair is found. A new rewrite rule is added to the rewrite system that consists of these terms, again directed from complex to simple. While adding new rewrite rules to the rewrite system, existing rewrite rules potentially can be reduced, and even become trivial.

If, by repeating this process of adding new rewrite rules and reducing existing ones, we eventually reach a fixed-point, where no more new rewrite rules can be added, the resulting rewrite system will have the same expressive power as the original theory consisting of non-directed axioms. We may also conclude that the theory is decidable, and the rewrite system provides a mechanism that realizes that decidability. Using the rewrite system, semantic equality of terms is equivalent to syntactic equality of the normal forms of these terms.

If on the other hand no such fixed-point is reached, no conclusion can be made on the decidability of the theory. In fact, Knuth-Bendix completion itself is semi-decidable.

From Theory to Rewrite System

The axioms part of the theory of non-abelian groups are directed to get a rewrite system with directed rewrite rules. The criterion used for directing an axiom is based on the syntactical complexity of the terms in the axiom, using the complexer term as the left-hand side and the simpler term as the right-hand side, such that rewrite rules always "simplify" a term.

The result is rewrite system 1:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)

Graphical Representation

Using the graphviz dot language, this rewrite system can be represented as:

In what follows, we will illustrate each iteration in the Knuth-Bendix procedure with such a graphical representation, illustrating new rewrite rules, reduced rewrite rules and rewrite rules that have become trivial. We will use graphical conventions as presented in this legend:

Iteration 1

The first iteration of the procedure can be represented graphically as:

Two new rewrite rules can be derived. The critical term for the derivation of each new rewrite rule is included in the box representing the new rewrite rule.

In what follows, we will document each of the critical terms found and how they can be used to derive a new rewrite rule.

Iteration 1 - Critical Pairs

Combining rewrite rules [1] and [3] the term a*1*b can be rewritten as in

a*1*b
  [1]-> a*b

or as in

a*1*b
  [3]-> a*(1*b)

Therefore, we create a new rewrite rule:

[4] a*(1*b) -> a*b

Combining rewrite rules [2] and [3] the term a*i(a)*b can be rewritten as in

a*i(a)*b
  [2]-> 1*b

or as in

a*i(a)*b
  [3]-> a*(i(a)*b)

Therefore, we create a new rewrite rule:

[5] a*(i(a)*b) -> 1*b

The result is rewrite system 1:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[4] a*(1*b) -> a*b
[5] a*(i(a)*b) -> 1*b

Iteration 1 - Simplification

The rewrite system cannot be simplified.

Iteration 2

The second iteration of the procedure can be represented graphically as:

Iteration 2 - Critical Pairs

Combining rewrite rules [2] and [4] the term a*(1*i(1)) can be rewritten as in

a*(1*i(1))
  [2]-> a*1
  [1]-> a

or as in

a*(1*i(1))
  [4]-> a*i(1)

Therefore, we create a new rewrite rule:

[6] a*i(1) -> a

Combining rewrite rules [2] and [5] the term a*(i(a)*i(i(a))) can be rewritten as in

a*(i(a)*i(i(a)))
  [2]-> a*1
  [1]-> a

or as in

a*(i(a)*i(i(a)))
  [5]-> 1*i(i(a))

Therefore, we create a new rewrite rule:

[7] 1*i(i(a)) -> a

Combining rewrite rules [5] and [4] the term a*(1*(i(1)*b)) can be rewritten as in

a*(1*(i(1)*b))
  [5]-> a*(1*b)
  [4]-> a*b

or as in

a*(1*(i(1)*b))
  [4]-> a*(i(1)*b)

Therefore, we create a new rewrite rule:

[8] a*(i(1)*b) -> a*b

The result is rewrite system 2:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[4] a*(1*b) -> a*b
[5] a*(i(a)*b) -> 1*b
[6] a*i(1) -> a
[7] 1*i(i(a)) -> a
[8] a*(i(1)*b) -> a*b

Iteration 2 - Simplification

The rewrite system cannot be simplified.

Iteration 3

The third iteration of the procedure can be represented graphically as:

During this iteration, four new rewrite rules [9], [10], [11] and [12] are added. The new rewrite rule [9] becomes trivial immediately using rewrite rule [12]. The existing rewrite rule [7] can be reduced using rewrite rule [12]. The new rewrite rule [11] can also be reduced using rewrite rule [7]. It remains marked green however, as it is a new rewrite rule.

Note that after reducing rewrite rule [7], it expresses the fact that the left identity element is also the right identity element, even in non-abelian groups, which is a nice intermediate result.

Iteration 3 - Critical Pairs

Combining rewrite rules [2] and [8] the term a*i(1)*i(i(1)) can be rewritten as in

a*(i(1)*i(i(1)))
  [2]-> a*1
  [1]-> a

or as in

a*(i(1)*i(i(1)))
  [8]-> a*i(i(1))

Therefore, we create a new rewrite rule:

[9] a*i(i(1)) -> a

Combining rewrite rules [5] and [8] the term a*i(1)*i(i(1))*b can be rewritten as in

a*(i(1)*(i(i(1))*b))
  [5]-> a*(1*b)
  [4]-> a*b

or as in

a*(i(1)*(i(i(1))*b))
  [8]-> a*(i(i(1))*b)

Therefore, we create a new rewrite rule:

[10] a*(i(i(1))*b) -> a*b

Combining rewrite rules [7] and [3] the term (1*i(i(a)))*b can be rewritten as in

1*i(i(a))*b
  [7]-> a*b

or as in

1*i(i(a))*b
  [3]-> 1*(i(i(a))*b)

Therefore, we create a new rewrite rule:

[11] 1*(i(i(a))*b) -> a*b

Combining rewrite rules [7] and [4] the term a*(1*i(i(b))) can be rewritten as in

a*(1*i(i(b)))
  [7]-> a*b

or as in

a*(1*i(i(b)))
  [4]-> a*i(i(b))

Therefore, we create a new rewrite rule:

[12] a*i(i(b)) -> a*b

The result is rewrite system 3:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[4] a*(1*b) -> a*b
[5] a*(i(a)*b) -> 1*b
[6] a*i(1) -> a
[7] 1*i(i(a)) -> a
[8] a*(i(1)*b) -> a*b
[9] a*i(i(1)) -> a
[10] a*(i(i(1))*b) -> a*b
[11] 1*(i(i(a))*b) -> a*b
[12] a*i(i(b)) -> a*b

Iteration 3 - Simplification

Looking at rewrite rule [7], the left-hand side can be rewritten as in

1*i(i(a))
  [12]-> 1*a

We therefore replace the rewrite rule by

[7] 1*a -> a

Looking at rewrite rule [9], the left-hand side can be rewritten as in

a*i(i(1))
  [12]-> a*1
  [1]-> a

The rewrite rule can therefore be removed.
Looking at rewrite rule [11], the left-hand side can be rewritten as in

1*(i(i(a))*b)
  [7]-> i(i(a))*b

We therefore replace the rewrite rule by

[11] i(i(a))*b -> a*b

The result is rewrite system 3bis:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[4] a*(1*b) -> a*b
[5] a*(i(a)*b) -> 1*b
[6] a*i(1) -> a
[7] 1*a -> a
[8] a*(i(1)*b) -> a*b
[10] a*(i(i(1))*b) -> a*b
[11] i(i(a))*b -> a*b
[12] a*i(i(b)) -> a*b

Iteration 4

The fourth iteration of the procedure can be represented graphically as:

During this iteration, three new rewrite rules [13], [14] and [15] are added. Rewrite rules [4], [10], [11], [12] and [13] become trivial. The existing rewrite rule [5] can be reduced using rewrite rule [7].

Note that rewrite rule [15] expresses the fact that the inverse of the inverse of an element is the element itself, which is a nice intermediate result.

Iteration 4 - Critical Pairs

Combining rewrite rules [2] and [5] the term a*(i(a)*i(i(a))) can be rewritten as in

a*(i(a)*i(i(a)))
  [2]-> a*1
  [1]-> a

or as in

a*(i(a)*i(i(a)))
  [5]-> 1*i(i(a))
  [7]-> i(i(a))

Therefore, we create a new rewrite rule:

[13] i(i(a)) -> a

Combining rewrite rules [11] and [5] the term i(a)*(i(i(a))*b) can be rewritten as in

i(a)*(i(i(a))*b)
  [11]-> i(a)*(a*b)

or as in

i(a)*(i(i(a))*b)
  [5]-> 1*b
  [7]-> b

Therefore, we create a new rewrite rule:

[14] i(b)*(b*a) -> a

Combining rewrite rules [12] and [5] the term a*(i(a)*i(i(b))) can be rewritten as in

a*(i(a)*i(i(b)))
  [12]-> a*(i(a)*b)
  [5]-> 1*b
  [7]-> b

or as in

a*(i(a)*i(i(b)))
  [5]-> 1*i(i(b))
  [7]-> i(i(b))

Therefore, we create a new rewrite rule:

[15] i(i(a)) -> a

The result is rewrite system 4:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[4] a*(1*b) -> a*b
[5] a*(i(a)*b) -> 1*b
[6] a*i(1) -> a
[7] 1*a -> a
[8] a*(i(1)*b) -> a*b
[10] a*(i(i(1))*b) -> a*b
[11] i(i(a))*b -> a*b
[12] a*i(i(b)) -> a*b
[13] i(i(a)) -> a
[14] i(b)*(b*a) -> a
[15] i(i(a)) -> a

Iteration 4 - Simplification

Looking at rewrite rule [4], the left-hand side can be rewritten as in

a*(1*b)
  [7]-> a*b

The rewrite rule can therefore be removed. Looking at rewrite rule [5], the right-hand side can be rewritten as in

1*b
  [7]-> b

We therefore replace the rewrite rule by

[5] a*(i(a)*b) -> b

Looking at rewrite rule [10], the left-hand side can be rewritten as in

a*(i(i(1))*b)
  [11]-> a*(1*b)
  [7]-> a*b

The rewrite rule can therefore be removed. Looking at rewrite rule [11], the left-hand side can be rewritten as in

i(i(a))*b
  [13]-> a*b

The rewrite rule can therefore be removed. Looking at rewrite rule [12], the left-hand side can be rewritten as in

a*i(i(b))
  [13]-> a*b

The rewrite rule can therefore be removed. Looking at rewrite rule [13], the left-hand side can be rewritten as in

i(i(a))
  [15]-> a

The rewrite rule can therefore be removed. The result is rewrite system 4bis:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[5] a*(i(a)*b) -> b
[6] a*i(1) -> a
[7] 1*a -> a
[8] a*(i(1)*b) -> a*b
[14] i(b)*(b*a) -> a
[15] i(i(a)) -> a

Iteration 5

The fifth iteration of the procedure can be represented graphically as:

During this iteration, eight new rewrite rules [16], [17], [18], [19], [20], [21], [22] and [23] are added. Rewrite rules [6], [8], [16], [19], [20], [21] and [22] become trivial.

Note that rewrite rule [18] states that the identity element is its own inverse. Also note that rewrite rule [23] expresses the fact that the right symmetric element is equally the left symmetric element, even in non-abelian groups. These are nice intermediate results.

Iteration 5 - Critical Pairs

Combining rewrite rules [1] and [14] the term i(a)*(a*1) can be rewritten as in

i(a)*(a*1)
  [1]-> i(a)*a

or as in

i(a)*(a*1)
  [14]-> 1

Therefore, we create a new rewrite rule:

[16] i(a)*a -> 1

Combining rewrite rules [3] and [14] the term i(a*b)*(a*b*c) can be rewritten as in

i(a*b)*(a*b*c)
  [3]-> i(a*b)*(a*(b*c))

or as in

i(a*b)*(a*b*c)
  [14]-> c

Therefore, we create a new rewrite rule:

[17] i(b*c)*(b*(c*a)) -> a

Combining rewrite rules [6] and [5] the term a*(i(a)*i(1)) can be rewritten as in

a*(i(a)*i(1))
  [6]-> a*i(a)
  [2]-> 1

or as in

a*(i(a)*i(1))
  [5]-> i(1)

Therefore, we create a new rewrite rule:

[18] i(1) -> 1

Combining rewrite rules [6] and [14] the term i(a)*(a*i(1)) can be rewritten as in

i(a)*(a*i(1))
  [6]-> i(a)*a

or as in

i(a)*(a*i(1))
  [14]-> i(1)

Therefore, we create a new rewrite rule:

[19] i(a)*a -> i(1)

Combining rewrite rules [7] and [14] the term i(1)*(1*a) can be rewritten as in

i(1)*(1*a)
  [7]-> i(1)*a

or as in

i(1)*(1*a)
  [14]-> a

Therefore, we create a new rewrite rule:

[20] i(1)*a -> a

Combining rewrite rules [8] and [5] the term a*(i(a)*(i(1)*b)) can be rewritten as in

a*(i(a)*(i(1)*b))
  [8]-> a*(i(a)*b)
  [5]-> b

or as in

a*(i(a)*(i(1)*b))
  [5]-> i(1)*b

Therefore, we create a new rewrite rule:

[21] i(1)*a -> a

Combining rewrite rules [8] and [14] the term i(a)*(a*(i(1)*b)) can be rewritten as in

i(a)*(a*(i(1)*b))
  [8]-> i(a)*(a*b)
  [14]-> b

or as in

i(a)*(a*(i(1)*b))
  [14]-> i(1)*b

Therefore, we create a new rewrite rule:

[22] i(1)*a -> a

Combining rewrite rules [15] and [2] the term i(a)*i(i(a)) can be rewritten as in

i(a)*i(i(a))
  [15]-> i(a)*a

or as in

i(a)*i(i(a))
  [2]-> 1

Therefore, we create a new rewrite rule:

[23] i(a)*a -> 1

The result is rewrite system 5:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[5] a*(i(a)*b) -> b
[6] a*i(1) -> a
[7] 1*a -> a
[8] a*(i(1)*b) -> a*b
[14] i(b)*(b*a) -> a
[15] i(i(a)) -> a
[16] i(a)*a -> 1
[17] i(b*c)*(b*(c*a)) -> a
[18] i(1) -> 1
[19] i(a)*a -> i(1)
[20] i(1)*a -> a
[21] i(1)*a -> a
[22] i(1)*a -> a
[23] i(a)*a -> 1

Iteration 5 - Simplification

Looking at rewrite rule [6], the left-hand side can be rewritten as in

a*i(1)
  [18]-> a*1
  [1]-> a

The rewrite rule can therefore be removed. Looking at rewrite rule [8], the left-hand side can be rewritten as in

a*(i(1)*b)
  [20]-> a*b

The rewrite rule can therefore be removed. Looking at rewrite rule [16], the left-hand side can be rewritten as in

i(a)*a
  [19]-> i(1)
  [18]-> 1

The rewrite rule can therefore be removed. Looking at rewrite rule [19], the left-hand side can be rewritten as in

i(a)*a
  [23]-> 1

while the right-hand side can be rewritten as in

i(1)
  [18]-> 1

The rewrite rule can therefore be removed. Looking at rewrite rule [20], the left-hand side can be rewritten as in

i(1)*a
  [21]-> a

The rewrite rule can therefore be removed. Looking at rewrite rule [21], the left-hand side can be rewritten as in

i(1)*a
  [22]-> a

The rewrite rule can therefore be removed. Looking at rewrite rule [22], the left-hand side can be rewritten as in

i(1)*a
  [18]-> 1*a
  [7]-> a

The rewrite rule can therefore be removed. The result is rewrite system 5bis:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[5] a*(i(a)*b) -> b
[7] 1*a -> a
[14] i(b)*(b*a) -> a
[15] i(i(a)) -> a
[17] i(b*c)*(b*(c*a)) -> a
[18] i(1) -> 1
[23] i(a)*a -> 1

Iteration 6

The sixth iteration of the procedure can be represented graphically as:

During this iteration, seven new rewrite rules [24], [25], [26], [27], [28], [29] and [30] are added. Rewrite rules [17], [25], [26], [28], [29] and [30] become trivial.

Iteration 6 - Critical Pairs

Combining rewrite rules [2] and [17] the term i(a*b)*(a*(b*i(b))) can be rewritten as in

i(a*b)*(a*(b*i(b)))
  [2]-> i(a*b)*(a*1)
  [1]-> i(a*b)*a

or as in

i(a*b)*(a*(b*i(b)))
  [17]-> i(b)

Therefore, we create a new rewrite rule:

[24] i(b*a)*b -> i(a)

Combining rewrite rules [3] and [17] the term i(a*b*c)*(a*b*(c*d)) can be rewritten as in

i(a*b*c)*(a*b*(c*d))
  [3]-> i(a*b*c)*(a*(b*(c*d)))
  [3]-> i(a*(b*c))*(a*(b*(c*d)))

or as in

i(a*b*c)*(a*b*(c*d))
  [17]-> d

Therefore, we create a new rewrite rule:

[25] i(b*(c*d))*(b*(c*(d*a))) -> a

Combining rewrite rules [3] and [17] the term i(a*(b*c))*(a*(b*c*d)) can be rewritten as in

i(a*(b*c))*(a*(b*c*d))
  [3]-> i(a*(b*c))*(a*(b*(c*d)))

or as in

i(a*(b*c))*(a*(b*c*d))
  [17]-> d

Therefore, we create a new rewrite rule:

[26] i(b*(c*d))*(b*(c*(d*a))) -> a

Combining rewrite rules [5] and [17] the term i(a*b)*(a*(b*(i(b)*c))) can be rewritten as in

i(a*b)*(a*(b*(i(b)*c)))
  [5]-> i(a*b)*(a*c)

or as in

i(a*b)*(a*(b*(i(b)*c)))
  [17]-> i(b)*c

Therefore, we create a new rewrite rule:

[27] i(c*a)*(c*b) -> i(a)*b

Combining rewrite rules [14] and [17] the term i(a*i(b))*(a*(i(b)*(b*c))) can be rewritten as in

i(a*i(b))*(a*(i(b)*(b*c)))
  [14]-> i(a*i(b))*(a*c)

or as in

i(a*i(b))*(a*(i(b)*(b*c)))
  [17]-> b*c

Therefore, we create a new rewrite rule:

[28] i(c*i(a))*(c*b) -> a*b

Combining rewrite rules [23] and [17] the term i(i(a*b)*a)*(i(a*b)*(a*b)) can be rewritten as in

i(i(a*b)*a)*(i(a*b)*(a*b))
  [23]-> i(i(a*b)*a)*1
  [1]-> i(i(a*b)*a)

or as in

i(i(a*b)*a)*(i(a*b)*(a*b))
  [17]-> b

Therefore, we create a new rewrite rule:

[29] i(i(b*a)*b) -> a

Combining rewrite rules [23] and [17] the term i(a*i(b))*(a*(i(b)*b)) can be rewritten as in

i(a*i(b))*(a*(i(b)*b))
  [23]-> i(a*i(b))*(a*1)
  [1]-> i(a*i(b))*a

or as in

i(a*i(b))*(a*(i(b)*b))
  [17]-> b

Therefore, we create a new rewrite rule:

[30] i(b*i(a))*b -> a

The result is rewrite system 6:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[5] a*(i(a)*b) -> b
[7] 1*a -> a
[14] i(b)*(b*a) -> a
[15] i(i(a)) -> a
[17] i(b*c)*(b*(c*a)) -> a
[18] i(1) -> 1
[23] i(a)*a -> 1
[24] i(b*a)*b -> i(a)
[25] i(b*(c*d))*(b*(c*(d*a))) -> a
[26] i(b*(c*d))*(b*(c*(d*a))) -> a
[27] i(c*a)*(c*b) -> i(a)*b
[28] i(c*i(a))*(c*b) -> a*b
[29] i(i(b*a)*b) -> a
[30] i(b*i(a))*b -> a

Iteration 6 - Simplification

Looking at rewrite rule [17], the left-hand side can be rewritten as in

i(b*c)*(b*(c*a))
  [27]-> i(c)*(c*a)
  [14]-> a

The rewrite rule can therefore be removed. Looking at rewrite rule [25], the left-hand side can be rewritten as in

i(b*(c*d))*(b*(c*(d*a)))
  [26]-> a

The rewrite rule can therefore be removed. Looking at rewrite rule [26], the left-hand side can be rewritten as in

i(b*(c*d))*(b*(c*(d*a)))
  [27]-> i(c*d)*(c*(d*a))
  [27]-> i(d)*(d*a)
  [14]-> a

The rewrite rule can therefore be removed. Looking at rewrite rule [28], the left-hand side can be rewritten as in

i(c*i(a))*(c*b)
  [27]-> i(i(a))*b
  [15]-> a*b

The rewrite rule can therefore be removed. Looking at rewrite rule [29], the left-hand side can be rewritten as in

i(i(b*a)*b)
  [24]-> i(i(a))
  [15]-> a

The rewrite rule can therefore be removed. Looking at rewrite rule [30], the left-hand side can be rewritten as in

i(b*i(a))*b
  [24]-> i(i(a))
  [15]-> a

The rewrite rule can therefore be removed. The result is rewrite system 6bis:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[5] a*(i(a)*b) -> b
[7] 1*a -> a
[14] i(b)*(b*a) -> a
[15] i(i(a)) -> a
[18] i(1) -> 1
[23] i(a)*a -> 1
[24] i(b*a)*b -> i(a)
[27] i(c*a)*(c*b) -> i(a)*b

Iteration 7

The seventh iteration of the procedure can be represented graphically as:

During this iteration, eight new rewrite rules [31], [32], [33], [34] and [35] are added. Rewrite rules [27], [32], [33], [34] and [35] become trivial.

Note that rewrite rule [31] states that the inverse of a product of two elements is the product of the inverted elements in inverted order, which is a nice intermediate result.

Iteration 7 - Critical Pairs

Combining rewrite rules [2] and [27] the term i(a*b)*(a*i(a)) can be rewritten as in

i(a*b)*(a*i(a))
  [2]-> i(a*b)*1
  [1]-> i(a*b)

or as in

i(a*b)*(a*i(a))
  [27]-> i(b)*i(a)

Therefore, we create a new rewrite rule:

[31] i(b*a) -> i(a)*i(b)

Combining rewrite rules [5] and [27] the term i(a*b)*(a*(i(a)*c)) can be rewritten as in

i(a*b)*(a*(i(a)*c))
  [5]-> i(a*b)*c

or as in

i(a*b)*(a*(i(a)*c))
  [27]-> i(b)*(i(a)*c)

Therefore, we create a new rewrite rule:

[32] i(b*a)*c -> i(a)*(i(b)*c)

Combining rewrite rules [14] and [27] the term i(i(a)*b)*(i(a)*(a*c)) can be rewritten as in

i(i(a)*b)*(i(a)*(a*c))
  [14]-> i(i(a)*b)*c

or as in

i(i(a)*b)*(i(a)(*a*c))
  [27]-> i(b)*(a*c)

Therefore, we create a new rewrite rule:

[33] i(i(b)*a)*c -> i(a)*(b*c)

Combining rewrite rules [23] and [27] the term i(i(a)*b)*(i(a)*a) can be rewritten as in

i(i(a)*b)*(i(a)*a)
  [23]-> i(i(a)*b)*1
  [1]-> i(i(a)*b)

or as in

i(i(a)*b)*(i(a)*a)
  [27]-> i(b)*a

Therefore, we create a new rewrite rule:

[34] i(i(b)*a) -> i(a)*b

Combining rewrite rules [24] and [27] the term i(i(a*b)*c)*(i(a*b)*a) can be rewritten as in

i(i(a*b)*c)*(i(a*b)*a)
  [24]-> i(i(a*b)*c)*i(b)

or as in

i(i(a*b)*c)*(i(a*b)*a)
  [27]-> i(c)*a

Therefore, we create a new rewrite rule:

[35] i(i(b*c)*a)*i(c) -> i(a)*b

The result is rewrite system 7:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[5] a*(i(a)*b) -> b
[7] 1*a -> a
[14] i(b)*(b*a) -> a
[15] i(i(a)) -> a
[18] i(1) -> 1
[23] i(a)*a -> 1
[24] i(b*a)*b -> i(a)
[27] i(c*a)*(c*b) -> i(a)*b
[31] i(b*a) -> i(a)*i(b)
[32] i(b*a)*c -> i(a)*(i(b)*c)
[33] i(i(b)*a)*c -> i(a)*(b*c)
[34] i(i(b)*a) -> i(a)*b
[35] i(i(b*c)*a)*i(c) -> i(a)*b

Iteration 7 - Simplification

Looking at rewrite rule [24], the left-hand side can be rewritten as in

i(b*a)*b
  [32]-> i(a)*(i(b)*b)
  [23]-> i(a)*1
  [1]-> i(a)

The rewrite rule can therefore be removed. Looking at rewrite rule [27], the left-hand side can be rewritten as in

i(c*a)*(c*b)
  [32]-> i(a)*(i(c)*(c*b))
  [14]-> i(a)*b

The rewrite rule can therefore be removed. Looking at rewrite rule [32], the left-hand side can be rewritten as in

i(b*a)*c
  [31]-> (i(a)*i(b))*c
  [3]-> i(a)*(i(b)*c)

The rewrite rule can therefore be removed. Looking at rewrite rule [33], the left-hand side can be rewritten as in

i(i(b)*a)*c
  [31]-> i(a)*i(i(b))*c
  [3]-> i(a)*(i(i(b))*c)
  [15]-> i(a)*(b*c)

The rewrite rule can therefore be removed. Looking at rewrite rule [34], the left-hand side can be rewritten as in

i(i(b)*a)
  [31]-> i(a)*i(i(b))
  [15]-> i(a)*b

The rewrite rule can therefore be removed. Looking at rewrite rule [35], the left-hand side can be rewritten as in

i(i(b*c)*a)*i(c)
  [31]-> i(a)*i(i(b*c))*i(c)
  [3]-> i(a)*(i(i(b*c))*i(c))
  [15]-> i(a)*(b*c*i(c))
  [3]-> i(a)*(b*(c*i(c)))
  [2]-> i(a)*(b*1)
  [1]-> i(a)*b

The rewrite rule can therefore be removed. The result is rewrite system 7bis:

[1] a*1 -> a
[2] a*i(a) -> 1
[3] a*b*c -> a*(b*c)
[5] a*(i(a)*b) -> b
[7] 1*a -> a
[14] i(b)*(b*a) -> a
[15] i(i(a)) -> a
[18] i(1) -> 1
[23] i(a)*a -> 1
[31] i(b*a) -> i(a)*i(b)

Completion

The resulting rewrite system 7bis cannot be extended anymore. We have therefore reached the fixed-point of the Knuth-Bendix completion algorithm.

The rewrite system can be represented graphically as:

This result constitutes the deterministic rewrite system that is semantically equivalent to the theory consisting of the three non-directed axioms we started off with. It provides a decidable computational framework for non-abelian groups, in the sense that, repeat, semantic equality of terms is equivalent to syntactic equality of normal forms.