Term Rewrite Rules for Finite Fields

Stanley Burris^{∗} and John Lawrence^{†}

Abstract Let F_{1}, …, F_{k} be finite fields with distinct characteristics. We give a finite set of equations which axiomatize the equational theory of F_{1}, …, F_{k} and then use these axioms to find a finite AC-term rewrite system which is complete for this theory. In particular this gives finite complete AC-term rewrite systems for many instances of x^{m} ≈ x rings. However there are m for which no such term rewrite system exists — the smallest is m = 22.

A popular test problem for automated theorem proving has been the derivation of xy ≈ yx from ring axioms plus x^{m} ≈ x (m > 1). At present this has been achieved for m = 2, 3, 4, 6 using versions of the Knuth-Bendix algorithm. Zhang [6] has given a polynomial gcd algorithm which can be used to prove commutativity for about three-fourths of the even exponents m (by reducing such cases to x^{2} ≈ x or x^{4} ≈ x).

A related problem is to find a complete set of AC-term rewrite rules for x^{m} ≈ x rings. This has been solved for m = 2 by Hsiang [2] and for m = 3 by Stickel [5]. As a corollary to our theorem we find such rewrite rules for many m ≥ 2 (about 94% of the m below 100,000). Our result also covers Nipkow’s [4] AC-term rewrite rules for rings satisfying x^{p} ≈ x and p ≈ 0, where p is a prime.

1 From Equations to Rewrite Rules.

Throughout this section let F_{1}, …, F_{k} be a fixed list of finite fields with distinct characteristics p_{1}, …, p_{k}. The set of equations true of the fields F_{i} (1 ≤ i ≤ k) is the equational theory of F_{1}, …, F_{k}. Assume the respective sizes of these fields are q_{1} > ⋯ > q_{k}, let c = p_{1} ⋯ p_{k}, and let n be such that n − 1 is the least common multiple of q_{1} − 1, …, q_{k} − 1.

∗Research supported by a grant from NSERC

†Research supported by a grant from NSERC

LEMMA 1.1 The equational theory of F_{1}, …, F_{k} is axiomatized by the axioms for rings plus

\{ \begin{matrix}x^{n} ≈ x \\ c ≈ 0 \\ \frac{c}{p_{i}} x^{q_{i}} ≈ \frac{c}{p_{i}} x (1 ≤ i ≤ k). \end{matrix}  (1)

Proof. Clearly these equations are satisfied by F_{1}, …, F_{k} as F_{i} satisfies p_{i} ≈ 0 and x^{q_{i}} ≈ x (1 ≤ i ≤ k). Now if F is a finite field satisfying these equations then the characteristic of F divides c since c ≈ 0 holds, so the

characteristic is some p_{i} (1 ≤ i ≤ k). Next, F satisfies \frac{c}{p_{i}} x^{q_{i}} ≈ \frac{c}{p_{i}} x im-

plies F satisfies x^{q_{i}} ≈ x, so F embeds in F_{i}. Thus we have proved that the fields satisfying (1) are the subfields of F_{1}, …, F_{k}. By a result of Jacobson [3] we know that a ring equation follows from (1) iff it holds on the finite fields satisfying (1). Consequently we have found axioms for the equational theory of F_{1}, …, F_{k}.

In the following when we refer to polynomial we mean an element of Z[X], where X is an infinite set of commuting variables. Since we are working in the language +, ·, −, 0, 1 of rings, we really mean that for n > 0 the constant monomial n is an abbreviation for 1 + ⋯ + 1, and the expression nA means A+⋯+A (in both cases the number of summands is n). Given a monomial M = x_{1}^{s_{1}} ⋯ x_{l}^{s_{l}} we define vdeg(M) to be the maximum of s_{1}, …, s_{l}. If P is a polynomial define vdeg(P) to be the largest vdeg(M) for M a monomial in P.

LEMMA 1.2 If F is a finite field of characteristic p and size q, and if A and B are two polynomials such that vdeg(A) and vdeg(B) are less than q, then A ≈ B holds on F iff the corresponding coefficients are congruent modulo p.

Proof. Since F satisfies p ≈ 0, the direction (⇐) is clear. The direction (⇒) is a straight forward induction on the number of variables appearing in the equation. For one variable the result follows from the fact that x^{q} − x is the minimal polynomial of F. Now for the induction step suppose that the claim is true for any polynomials A and B with fewer than n variables. Let A(x_{1}, …, x_{n}) and B(x_{1}, …, x_{n}) be equal on F, and suppose both have vdeg less than q. The corresponding coefficients are congruent modulo p iff the coefficients of A − B (considered as a polynomial) are congruent to 0 modulo p. Writing A − B in the form

∑_{i=0}^{q−1} C_{i}(x_{1}, …, x_{n−1})x_{n}^{i}  (2)

we see that it suffices to show that each of the polynomials C_{i}(x_{1}, …, x_{n−1}) vanishes on F — for then by induction all the coefficients of each C_{i} will be congruent to 0 modulo p, and hence the same is true of the coefficients of A − B. We proceed by assuming some C_{i} does not vanish on F. Then one can choose elements a⃗ from F such that not all C_{i} vanish at a⃗. Substituting this into (2) gives the one-variable polynomial

∑_{i=0}^{q−1} C_{i}(a_{1}, …, a_{n−1})x_{n}^{i}

with coefficients in F, and not all coefficients are 0. As this is a non-zero polynomial of degree at most q − 1 it follows that it can have at most q − 1 roots in F, and consequently cannot vanish on F. With this contradiction we have proved the lemma.

Now we turn to the rewrite rules. Define

a_{1} = 1, a_{i} = p_{1} ⋯ p_{i−1} (2 ≤ i ≤ k).

Since the g.c.d. of \frac{c}{p_{1}} , …, \frac{c}{p_{k}} is 1, we can find integers n_{i} such that

∑_{i=1}^{k} n_{i} \frac{c}{p_{i}} = 1. Now define a_{ij} and b_{ij} (1 ≤ j ≤ i ≤ k) by

a_{ij} = [a_{j}n_{i} \frac{c}{p_{i}} ]_{c}

(where [ ]_{c} means to reduce modulo c to a non-negative value less than c),

b_{ij} = q_{j} − q_{i} + 1.

THEOREM 1.3 The following AC-term rewrite rules are complete for the equational theory of F_{1}, …, F_{k}:

R0: x + 0 ⟶ x
R1: x · 1 ⟶ x  R2: x · 0 ⟶ 0
R3: x + (−x) ⟶ 0 R4: x · (y + z) ⟶ x · y + x · z
R5: −1 ⟶ c − 1 R6: −x ⟶ (c − 1)x
R7: c ⟶ 0  R8 cx ⟶ 0
S_{j} : a_{j}x^{q_{j}} ⟶ ∑_{i=j}^{k} a_{ij}x^{b_{ij}} (1 ≤ j ≤ k)
T_{j} : a_{j}x^{q_{j}}v ⟶ ∑_{i=j}^{k} a_{ij}x^{b_{ij}}v (1 ≤ j ≤ k),

For those j such that q_{i} − 1|q_{j} − 1 for i ≥ j we can replace S_{j} and T_{j} by the following particularly simple rewrite rules:

\begin{matrix}S′_{j} : & a_{j}x^{q_{j}} ⟶ a_{j}x \\ T′_{j} : & a_{j}x^{q_{j}}v ⟶ a_{j}xv. \end{matrix}

This always applies to j = k.

Proof. Let F = {F_{1}, …, F_{k}}. From

1 = ∑_{i=1}^{k} n_{i} \frac{c}{p_{i}}

follows

a_{j} = ∑_{i=1}^{k} a_{j}n_{i} \frac{c}{p_{i}} ,

and thus

a_{j} ≡ ∑_{i=j}^{k} a_{j}n_{i} \frac{c}{p_{i}} (mod c).

This leads to

F ⊧ a_{j}x^{q_{j}} ≈ ∑_{i=j}^{k} a_{j}n_{i} \frac{c}{p_{i}} x^{q_{j}}.

Now from

F_{i} ⊧ x^{q_{i}} ≈ x, F_{i′} ⊧ \frac{c}{p_{i}} ≈ 0 (i′ ≠ i)

we have

F ⊧ \frac{c}{p_{i}} x^{q_{i}} ≈ \frac{c}{p_{i}} x,

and thus

F ⊧ \frac{c}{p_{i}} x^{q_{j}} ≈ \frac{c}{p_{i}} x^{b_{ij}} (1 ≤ j ≤ i ≤ k).

Consequently

a_{j}x^{q_{j}} ≈ ∑_{i=j}^{k} a_{j}n_{i} \frac{c}{p_{i}} x^{b_{ij}}

holds in F; and hence so does the equation

a_{j}x^{q_{j}} ≈ ∑_{i=j}^{k} a_{ij}x^{b_{ij}}.

Thus the proposed rewrite rules correspond to valid equations in F_{1}, …, F_{k}. Now observe that the rules in S_{j} and T_{j} are degree decreasing. Consequently the proposed set of rewrite rules is terminating, and any term t(x_{1}, …, x_{n}) can be reduced to a normal form

A_{1}(x_{1}, …, x_{n}) + ⋯ + A_{k}(x_{1}, …, x_{n})

where each A_{i} is a polynomial; and furthermore if A_{i} ≠ 0

i. the monomials M in A_{i} satisfy

q_{i+1} ≤ vdeg(M) < q_{i} (1 ≤ i ≤ k − 1)
0 ≤ vdeg(M) < q_{k} if i = k;

ii. the coefficients d in A_{i} satisfy

1 ≤ d < a_{i+1} = p_{1} ⋯ p_{i} (1 ≤ i ≤ k − 1)
1 ≤ d < c = p_{1} ⋯ p_{k} (i = k).

It only remains to show that two AC-distinct normal forms are not equivalent on F_{1}, …, F_{k}. So suppose ∑ A_{i} and ∑ B_{i} are two normal forms with ∑ A_{i} ≈ ∑ B_{i} true of F_{1}, …, F_{k}. Clearly the vdeg’s of ∑ A_{i} and ∑ B_{i} are less than q_{1}. As the coefficients in A_{1} and B_{1} are non-negative and less than p_{1} it follows from Lemma 1.2, using F_{1}, that A_{1} and B_{1} are AC-equivalent. Thus ∑_{i≥2} A_{i} ≈ ∑_{i≥2} B_{i} holds on F_{1}, …, F_{k}. As the coefficients in A_{2} and B_{2} are non-negative and less than p_{1} · p_{2} it follows from Lemma 1.2, using F_{1} and F_{2}, that A_{2} and B_{2} are AC-equivalent. Continuing we obtain ∑ A_{i} and ∑ B_{i} are AC-equivalent.

To see that one can use the simple forms S′_{j} and T′_{j} when q_{i−1}|q_{j−1} for i ≥ j, we only need to observe that a_{j}x^{q_{j}} ≈ a_{j}x holds on the fields F_{1}, …, F_{j−1} because their characteristics divide a_{j}, and on the fields F_{j}, …, F_{k} because they satisfy x^{q_{j}} ≈ x (since q_{i−1}|q_{j−1} implies x^{q_{i}} − x|x^{q_{j}} − x in Z[x]).

Thus we have not only found a finite and complete AC-term rewriting system for the equational theory of F_{1}, …, F_{k}, but we have also given an explicit description of the normal forms.

2 Examples.

1. Rings satisfying x^{p} ≈ x and p ≈ 0, where p is a prime.

By Lemma 1.2 these equations, along with defining equations for rings, axiomatize the equational theory of GF(p). Thus k = 1, p_{1} = p, q_{1} = p, c = p, a_{1} = 1. Hence the AC-term rewrite rules are R0–R4 plus

\begin{matrix}−1 ⟶ p − 1 & −x ⟶ (p − 1)x \\ p ⟶ 0 & px ⟶ 0 \\ x^{p} ⟶ x & x^{p}v ⟶ xv. \end{matrix}

The equational theory of x^{m} ≈ x rings, for m > 1, is given by the equational theory of the finite fields F satisfying x^{m} ≈ x, i.e., by those finite fields such that |F| − 1 divides m − 1, where |F| is the cardinality of F. (As noted by Zhang [6], if m is even only one characteristic appears, namely 2; so for even m we need the fields GF(2^{k}) such that 2^{k} − 1 divides m − 1). Our rewrite rules will thus apply to those m such that for each characteristic p of a field satisfying x^{m} ≈ x there is a largest field (under embedding) of characteristic p which satisfies x^{m} ≈ x. It turns out that for approximately 94% of the m < 100, 000 we have this situation. The only exceptions for m < 1, 000 are :

22 43 85 94 105 106 148 169 187 209 211 218 232 274 280 295 313 316 337 358 373 382 400 417 421 435 463 466 484 521 526 547 559 589 610 625 631 652 673 715 736 745 763 778 799 833 838 841 862 869 890 904 925 931 937 946 967 969 988

These are the numbers m below 1,000 for which there exists a prime p and two positive integers a and b such that both p^{a} − 1 and p^{b} − 1 divide m − 1, but p^{lcm(a,b)} − 1 does not divide m − 1. Now we give a table describing the maximal fields satisfying x^{m} ≈ x for 2 ≤ m ≤ 10, and a set of rewrite rules for each case (note that with one exception we can use the rules S′_{j}, T′_{j}).

\begin{matrix}m & q_{i} & p_{i} & c & a_{i} \\ 2 & 2 & 2 & 2 & 1 \\ 3 & 3,2 & 3,2 & 6 & 1,3 \\ 4 & 4 & 2 & 2 & 1 \\ 5 & 5,3,2 & 5,3,2 & 30 & 1,5,15 \\ 6 & 2 & 2 & 2 & 1 \\ 7 & 7,4,3 & 7,2,3 & 42 & 1,7,14 \\ 8 & 8 & 2 & 2 & 1 \\ 9 & 9,5,2 & 3,5,2 & 30 & 1,3,15 \\ 10 & 4 & 2 & 2 & 1 \end{matrix}

The rules R0–R4 are to be added to each of the following:

\underline{m = 2, 6} (Boolean rings)

\begin{matrix}−1 ⟶ 1 & −x ⟶ x \\ 2 ⟶ 0 & 2x ⟶ 0 \\ x^{2} ⟶ x & x^{2}v ⟶ xv. \end{matrix}

\underline{m = 3}

\begin{matrix}−1 ⟶ 5 & −x ⟶ 5x \\ 6 ⟶ 0 & 6x ⟶ 0 \\ x^{3} ⟶ x & x^{3}v ⟶ xv \\ 3x^{2} ⟶ 3x & 3x^{2}v ⟶ 3xv. \end{matrix}

\underline{m = 4, 10}

\begin{matrix}−1 ⟶ 1 & −x ⟶ x \\ 2 ⟶ 0 & 2x ⟶ 0 \\ x^{4} ⟶ x & x^{4}v ⟶ xv. \end{matrix}

\underline{m = 5}

\begin{matrix}−1 ⟶ 29 & −x ⟶ 29x \\ 30 ⟶ 0 & 30x ⟶ 0 \\ x^{5} ⟶ x & x^{5}v ⟶ xv \\ 5x^{3} ⟶ 5x & 5x^{3}v ⟶ 5xv \\ 15x^{2} ⟶ 15x & 15x^{2}v ⟶ 15xv. \end{matrix}

\underline{m = 7} We have k = 3, p_{1} = 7, p_{2} = 2, p_{3} = 3, q_{1} = 7, q_{2} = 4, q_{3} = 3 (so we can use S′_{1}, T′_{1}, S_{2}, T_{2}, S′_{3}, T′_{3}), c = 42, n_{1} = −1, n_{2} = 1, n_{3} = −1, a_{1} = 1, a_{2} = 7, a_{3} = 14, a_{22} = 21, a_{32} = 28, b_{22} = 1, b_{32} = 2.

\begin{matrix}−1 ⟶ 41 & −x ⟶ 41x \\ 42 ⟶ 0 & 42x ⟶ 0 \\ x^{7} ⟶ x & x^{7}v ⟶ xv \\ 7x^{4} ⟶ 28x^{2} + 21x & 7x^{4}v ⟶ (28x^{2} + 21x)v \\ 14x^{3} ⟶ 14x & 14x^{3}v ⟶ 14xv. \end{matrix}

\underline{m = 8}

\begin{matrix}−1 ⟶ 1 & −x ⟶ x \\ 2 ⟶ 0 & 2x ⟶ 0 \\ x^{8} ⟶ x & x^{8}v ⟶ xv. \end{matrix}

\underline{m = 9}

\begin{matrix}−1 ⟶ 29 & −x ⟶ 29x \\ 30 ⟶ 0 & 30x ⟶ 0 \\ x^{9} ⟶ x & x^{9}v ⟶ xv \\ 3x^{5} ⟶ 3x & 3x^{5}v ⟶ 3xv \\ 15x^{2} ⟶ 15x & 15x^{2}v ⟶ 15xv. \end{matrix}

We note that the only m in the examples above for which the q_{i} − 1 are not linearly ordered by divisibility is m = 7; hence the need for S_{2}, T_{2}. For the other m above we use the simple rewrite rules S′_{j} and T′_{j}.

3 Concluding Remarks.

We thought we could use the methods of this paper on any finite collection of finite fields. However the obvious attempt to generalize Lemma 1.2 fails. One can see the problem quite clearly if one considers the two fields GF(4) and GF(8) (this is precisely the set of maximal fields satisfying x^{22} ≈ x). The minimum polynomial for these two fields is the least common multiple of x^{4} + x and x^{8} + x in GF(2)[x], i.e., x^{10} + x^{9} + x^{8} + x^{3} + x^{2} + x. The single AC-rewrite rule

x^{10} ⟶ x^{9} + x^{8} + x^{3} + x^{2} + x

(along with R0–R4) suffices to reduce every polynomial in one variable to a polynomial of degree less than 10, and hence to the desired normal form as the minimum polynomial has degree 10. Now applying this rule to two variable polynomials would give 2^{10^{2}} distinct normal forms. However the free algebra in the variety generated by these two fields has size 2^{76}, and thus we need more AC-term rewrite rules. As there are no degree reducing one variable AC-term rewrite rules which apply to polynomials of degree less than 10 we are forced to look for two variable AC-term rewrite rules. From the fact that (x^{8} + x)(y^{4} + y) vanishes on both fields we obtain the rule

x^{8}y^{4} ⟶ x^{8}y + xy^{4} + xy

which reduces the number of normal forms to 2^{80}. Having approached this close to the desired result, we now claim that there is no set of AC-term rewrite rules for x^{22} ≈ x. Our justification hinges on the consideration of what the normal form q(x, y) of the polynomial p(x, y) defined to be x^{8}y^{2} + x^{8}y + x^{2}y could be. Since p(x, y) ≈ p(y, x) is a consequence of x^{22} ≈ x and since p(x, y) is not AC-equivalent to p(y, x) it follows that p(x, y) cannot be in normal form. Suppose q(x, y) is the normal form of p(x, y) using some AC-term rewrite rules. Then the (monomial) degree of q(x, y) is no more than 10, the degree of p(x, y). Since p(x, y) ≈ q(x, y) must be a consequence of x^{22} ≈ x, some calculations show that either p(x, y) or p(y, x) must be a part of q(x, y); but this would not be possible with a terminating set of AC-term rewrite rules.

Generalizing this we suspect that one cannot find AC-term rewrite rules for x^{n} ≈ x if there is a characteristic p such that there is no maximum field of characteristic p satisfying x^{n} ≈ x.

References

1. Arens, R.F., and Kaplansky, I., Topological representations of algebras. Trans. Amer. Math. Soc. 63 (1948), 457–481.

2. Hsiang, J. Topics in automated theorem proving and program generation. PhD Thesis, Report R-82-1113. Dept of Computer Science, University of Illinois, Urbana, IL., 1982.

3. Jacobson, N., Structure theory for algebraic algebras of bounded degree. Ann. of Math. 46 (1945), 695–707.

4. Nipkow, T., Unification in primal algebras, their powers and their varieties. J. Assoc. Comp. Mach. 37 (1990), 742–776.

5. Stickel, M.E. A case study of theorem proving by the Knuth-Bendix method: discovering that x^{3} ≈ x implies ring commutativity. 7^{th} International Conf. on Automated Deduction, Napa, California. Lecture Notes in Computer Science 170 (1984), 248–258.

6. Zhang, H. Automated proof of ring commutativity problems by algebraic methods. J. Symbolic Computation 9 (1990), 423–427.

Department of Pure Mathematics University of Waterloo Waterloo, Ontario, Canada N2L 3G1

(e-mail: snburris@thoralf.waterloo.edu) (e-mail: snburris@thoralf.uwaterloo.ca)