An automated proof theory approach to computation with permutation groups

Arjeh M. Cohen Department of Mathematics Eindhoven University of Technology Netherlands

Scott H. Murray School of Mathematics and Statistics University of Sydney Australia

August 28, 2002

Abstract

This is an introduction to data structures for permutation groups with a proof theoretic flavour.

1 Introduction

In this paper, we introduce the reader to computational permutation group theory. We describe the basic concepts and first results in this area of mathematics, as well as the data structures required to do actual computations. We follow [1], but our aim is to apply the theory to the graph isomorphism problem.

In the spirit of the Calculemus Autumn School, our approach will be proof theoretic. Computer algebra has always had an emphasis on complexity of algorithms, so that bigger and bigger problems could be solved on a given machine. The internet will play an increasingly large role in the exchange of mathematics between people, and we believe this will require a different approach to computational mathematics. As the exchange of mathematics across the World Wide Web becomes easier than solving all problems locally, the management of mathematical queries becomes more prominent. The problem of verifying the correctness of computations is particularly acute when they are no longer done on local machines with software the user trusts.

In this paper, our queries are invocations of permutation group algorithms that have been developed over the years and are implemented as part of the GAP computer algebra package. The response to a query is the output of the algorithm, which may have been run on a remote computer which the user knows nothing about. The user has reason to doubt the validity of the response, and so will demand some kind of verification. Since our queries are mathematical in nature, this verification should take the form of (an encoding of) a proof.

A classical example is the factorization of a natural number. If a sequence p_{1}, p_{2}, …, p_{t} of numbers is returned as a response to the query “factor the natural number n,” it is easy for the user to verify whether n = p_{1} ⋯ p_{t}. In order to verify that each p_{i} is a prime number, it would be very useful to receive additional data, such as the primality witnesses for each p_{i}. This example has been worked out by Olga Caprotti, Martijn Oostdijk and the first author [2].

We treat computational permutation group theory in a similar manner. We give additional data that allows for a relatively easy check of the correctness of the answer. Of course this requirement may prevent us from using the most efficient possible algorithms and implementations. In general, we use functions in the computer algebra system GAP, which are close to the state of the art. However, on occasion we have been forced to implement simpler methods that allow us to provide the data for a straight forward verification of the result.

This paper will be concerned with providing human readable proofs that could be transformed to a computer checkable proof without too much effort. In this way, we contribute to the integration of computer algebra and proof verification, which is the research focus of the Calculemus project.

2 Membership: Prove that the permutation g belongs to the group G

In computational permutation group theory, a group G is specified by a set of generating permutations A. Suppose that

A = {a_{1}, a_{2}, …, a_{k}}

consists of permutations of the points {1, 2, …, n}, i.e. A is a subset of the symmetric group Sym_{n}. Hence, by the definition of a generating set, G is the unique smallest subgroup of Sym_{n} which contains A.

We define a word in A to be an expression of the form

a_{i_{1}}^{e_{1}}a_{i_{2}}^{e_{2}} ⋯ a_{i_{m}}^{e_{m}}

where the indices i_{j} are in the range 1, …, k and the exponents e_{j} are integers. It is now easily shown that the set of words in A form a subgroup of Sym_{n}, and it is obvious that there is no smaller subgroup containing A. Hence a permutation g ∈ Sym_{n} is an element of G if, and only if, it can be expressed as a word in A. (A note for those who know combinatorial group theory: since we make little use of words, we are not making the normal distinction between a word in the free group, and its evaluation in the symmetric group).

Writing an arbitrary permutation g as a word in A is a difficult computational problem, which is beyond the scope of this tutorial. Instead we just use the existing methods implemented in GAP without explaining how they work. See Section 8, for a technique to show that a permutation is not an element of G.

Example 2.1 The Mathieu group on 11 points, M_{11}, has generating set A = {a_{1}, a_{2}}, where:

a_{1} = (1, 10)(2, 8)(3, 11)(5, 7),
a_{2} = (1, 4, 7, 6)(2, 11, 10, 9).

Query input

• A permutation g.

• A list A of permutations generating G.

• We are given the fact that g ∈ ⟨A⟩.

GAP input

     G := Group(A);
     IsIn_Proof(g,G)

GAP output A word in A that is equal to g.

Query output By definition, G is generated by A and so G consists of those elements which can be expressed as a word in A. In particular g = IsIn Proof(g, G), and so belongs to G.

3 Subgroup: Prove that H is a subgroup of G

Suppose H is another permutation group with generating set B. From the definition of a generating set it follows that H is a subgroup of G if, and only if, every element of B is contained in G.

Query input

• A list A of permutations which generate G.

• A list B of permutations which generate H.

• We are given the fact that H is a subgroup of G.

GAP input

     G := Group(A);
     H := Group(B);
     IsSubgroup_Proof(H,G);

GAP output A list of words in A indexed by B.

Query output In order to show that H is a subgroup of G, it suffices to show that each element of the generating set B belongs to G. IsSubgroup Proof(H, G) presents, for each element b of B, how it can be expressed as a word in A. This establishes that each element of B belongs to G, and so H is a subgroup of G.

4 The orbit X = Gx with proof.

The concept of an orbit is used in the construction of sets of coset representatives for stabilisers. Let G be a permutation group on {1, …, n}. The orbit of x under the action of G is

xG = {xg : g ∈ G} .

Suppose G has generating set A = {a_{1}, a_{2}, …, a_{k}} and let X be an orbit of G. Then the orbit graph G has vertex set X, label set {1, 2, …, k} and labeled edges

y ⟶^{i} z where ya_{i} = z.

Example 4.1 Consider M_{11} = ⟨s_{1}, s_{2}⟩, where s_{1} and s_{2} are defined in Example 2.1. The action of {s_{1}, s_{2}} on the orbit X = {1, 2, …, 11} is shown in Figure 1, where the dotted lines are labeled by 1 and solid lines by 2.

[figure: 1; 10; 9; 2; 11; 3; 8; 4; 7; 6; 5]

Figure 1: Orbit graph of M_{11}

Algorithm 4.1 Calculate orbit

(∗ input: x ∈ Ω, generating set A = {a_{1}, a_{2}, …, a_{k}}.

output: X = xG. ∗) begin

let X = {x};
for y ∈ X, for a_{j} ∈ A do

let y = ya_{j}; if y ∉ X then

add y to X;

end if; end for; return X;

end

This algorithm terminates after it has applied every generator to every point in X.

Query Input

• A list A of permutations generating G.

• A point x.

GAP input

     G := Group(A);
     Orbit_Proof(G,x);

GAP output A set of points X and a list B of words in A indexed by X. The set X is just the orbit Gx. The word in A corresponding to y ∈ X maps x to y.

Query output In order to show that X is the G-orbit of x, we need to show two statements:

1. Each element of X is image of x under an element of G. These elements are produced by the table Orbit Proof(Group(A), x).

2. Each element of A leaves the set X invariant. This is a straightforward check that the cycles containing points of X do not contain any points not in X.

5 The Schreier tree for the orbit X = xG.

Stabiliser subgroups are of fundamental importance to both theoretical and computational permutation group theory. The stabiliser subgroup in G of x is

G_{x} = {g ∈ G : xg = x}.

It is not immediately clear how to compute with this subgroup, since the definition gives us a test for whether g is an element of G_{x}, but does not give us for example a generating set.

The following lemma gives us a one-to-one correspondence between the orbit of a point and the set of cosets of its stabiliser.

Lemma 5.1 (Orbit-stabiliser lemma) If y ∈ xG, then {g ∈ G : xg = y} is a coset of G_{x}. In particular, |xG| = |G : G_{x}|.

Proof: Choose h ∈ G such that xh = y; then

{g ∈ G : x^{g} = y} = {g ∈ G : xg = xh}
= {g ∈ G : xgh^{−1} = x}
= {g ∈ G : gh^{−1} ∈ G_{x}} = G_{x}h.

Hence there is a one-to-one correspondence between the orbit and the cosets, and the second result follows.

Suppose that for every element y of the orbit xG, we choose u_{y} ∈ G with the property that xu_{y} = y. Then it follows immediately from the orbit-stabiliser lemma that all such u_{y} form a set of coset representatives for G_{x} in G.

Figure 2: Schreier tree T for M_{11}

It would be inefficient to store all the elements u_{y}, so instead we construct of Schreier tree. That is, a subgraph T of the orbit graph G which contains, for every y ∈ X, a unique path in T from x to y.

Example 5.1 Consider M_{11} with the generating set of Example 2.1. Then G is the graph shown in Figure 1, where dotted lines are labeled by 1 and solid lines by 2. A Schreier tree T rooted at 1 is shown in Figure 2.

In practice, we store this tree in a linearised form, using two vectors v : X → {−m, …, −1, 0, 1, …, m} and ω : V → X ∪ {0} defined by:

v(z) = \{ \begin{matrix}l & if y ⟶^{l} z is in T \\ −l & if y ⟵^{l} z is in T \\ 0 & if z = x \end{matrix} ,

ω(z) = \{ \begin{matrix}y & if y ⟶^{l} z is in T \\ 0 & if y = x \end{matrix} .

We call v the Schreier vector and ω the backpointers. They can be computed by a modified version of the orbit algorithm.

Algorithm 5.1 Calculate orbit

(∗ input: x ∈ Ω, generating set A = {a_{1}, a_{2}, …, a_{k}}.

output: X = xG, Schreier vector v, vector of backward pointers ω. ∗) begin let X = {x}; let v (y) = ω (y) = 0 for all y; for x ∈ X, for a_{j} ∈ A do

let y = xa_{j}; if y ∉ X then

add y to X;
let v(y) = j, ω(y) = x;

end if; end for; return X, v, ω;

end

Example 5.2 The linearised version of the Schreier tree in Figure 2 is given in the following table

1 2 3 4 5 6 7 8 9 10 11
v 0 2 1 2 1 2 2 1 2 1 2
ω 0 9 11 1 7 7 4 2 10 1 2

Query Input

• A list A of permutations generating G.

• A point x.

GAP input

G := Group(A);
SchreierData(G,x);

GAP output A triple [X, v, ω] of integers sequences consisting of the orbit, the Schreier vector, and the backpointers.

Query output Consider the table SchreierData(G, x). It has three rows, the first of which represents the orbit X = Gx. In order to show that X is indeed the G-orbit containing x, see Section 4. To show that v is a Schreier vector and ω is backpointers, consider a column of the table, say x_{j}, v_{j}, ω_{j}. It suffices to show that x_{j}a_{v_{j}} = ω_{j} if v_{j} > 0 or that x_{j}x_{v_{j}}^{−1} = ω_{j} if v_{j} < 0. This is a (perhaps tedious but) trivial check.

6 The stabiliser G_{x}

Now that we have a set of coset representatives for G_{x}, we can use it to compute a generating set, with the following lemma.

Lemma 6.1 (Schreier’s lemma) Suppose G is a group with generating set A, and H is a subgroup of G. If U is a set of coset representatives for H in G, and the function t : G → U maps an element g of G to the representative of Hg, then a generating set for H is given by

{ua t(ua)^{−1} : u ∈ U, a ∈ A} .

Proof: Every element h of H can be written in the form b_{1}b_{2} ⋯ b_{l}, where each b_{i}, or its inverse, is in A. Let u_{i} = t(b_{1}b_{2} s b_{i}), for i = 0, 1, …, l. Then u_{0} = t(1) = 1 and u_{l} = t(h) = 1, so

h = u_{0}hu_{l}^{−1} = (u_{0}b_{1}u_{1}^{−1})(u_{1}b_{2}u_{2}^{−1}) ⋯ (u_{l−1}b_{l}u_{l}^{−1}).

Consider u_{i−1}b_{i}u_{i}, for i = 1, 2, …, l. Now u_{i} = t(b_{1}b_{2} s b_{i}) = t(u_{i−1}b_{i}), since Hb_{1}b_{2} ⋯ b_{i} = Hu_{i−1}b_{i}. Let u = u_{i−1} ∈ U and b = b_{i}; we can now write

u_{i−1}b_{i}u_{i}^{−1} = ub t(ub)^{−1}.

This has the desired form if b ∈ A; otherwise, b = a^{−1} for some a ∈ A and let v = t(ua^{−1}) ∈ U. Since Hva = Hua^{−1}a, we have t(va) = u, and so the inverse of ub t(ub)^{−1} can be written

t(ua^{−1}) au^{−1} = va t(va)^{−1},

which has the desired form. The result now follows.

Query Input

• A list A of permutations generating G.

• A point x.

GAP input

     G := Group(A);
     Stabiliser Proof(G,x);

GAP output • A triple [X, v, ω] of integers sequences consisting of the orbit, the

Schreier vector, and the backpointers.

• A sequence of triples (y, i, g) consisting of a point y ∈ X, an index i = 1, …, m, and the Schreier generator g = t(y)a_{i}t(t(y)a_{i})^{−1}.

Query output The proof that [X, v, ω] describes a Schreier tree is given in (Section 5). Checking the correctness of the Schreier generators is straightforward.

7 Stabilizer chain

Now that we have a stabiliser of a subgroup, we can repeat the process to form a chain of subgroups. A base for G is a finite sequence B = [x_{1}, …, x_{t}] of distinct points in Ω such that

G_{x_{1},x_{2},...,x_{k}} = 1.

Hence, the only element of G which fixes all of the points x_{1}, x_{2}, …, x_{k} is the identity. Clearly every permutation group has a base, but not all bases for a given group are of the same length. If we write G^{(i)} = G_{x_{1},x_{2},...,x_{i−1}}, then we have a chain of stabilisers

G = G^{(1)} ≥ G^{(2)} ≥ ⋯ ≥ G^{(k)} ≥ G^{(k+1)} = 1.

We often require that a base has the additional property that G^{(i)} ≠ G^{(i+1)}. A strong generating set for G with respect to B is a set S of group elements such that, for i = 1, 2, …, k,

G^{(i)} = ⟨S ∩ G^{(i)}⟩ .

Note that S ∩ G^{(i)} is just the set of elements in S which fix β_{1}, β_{2}, …, β_{i−1}.

A base can be constructed by starting with B = [x_{1}], and recursively choosing a letter x_{i} in a nontrivial G_{x_{1},...,x_{i−1}}-orbit and appending it to B. The construction is finished when G_{x_{1},...,x_{i}} = 1.

Example 7.1 The Mathieu group on 11 points, M_{11}, has a base [1, 2, 3, 4] and strong generating set {s_{1}, s_{2}, …, s_{7}}, where:

s_{1} = (1, 10)(2, 8)(3, 11)(5, 7),
s_{2} = (1, 4, 7, 6)(2, 11, 10, 9),
s_{3} = (2, 3)(4, 5)(6, 11)(8, 9),
s_{4} = (3, 5, 7, 9)(4, 8, 11, 6),
s_{5} = (4, 6)(5, 11)(7, 10)(8, 9),
s_{6} = (4, 10, 6, 7)(5, 9, 11, 8),
s_{7} = (4, 11, 6, 5)(7, 8, 10, 9).

Note that s_{1} and s_{2} suffice to generate M_{11}.

The Schreier trees and backpointers for this stabiliser chain are given in the following table

1 2 3 4 5 6 7 8 9 10 11
v_{1} 0 2 1 2 1 2 2 1 2 1 2
ω_{1} 0 9 11 1 7 7 4 2 10 1 2
v_{2} – 0 3 7 4 7 4 6 4 6 5
ω_{2} – 0 2 5 3 11 5 11 7 4 5
v_{3} – – 0 7 4 7 4 6 4 6 5
ω_{3} – – 0 5 3 11 5 11 7 4 5
v_{4} – – – 0 7 5 6 6 7 6 7
ω_{4} – – – 0 6 4 6 11 10 4 4

Query Input A list A of permutations generating G.

GAP input A group G with generating set A.

GAP input

     G := Group(A);
     StabiliserChain Proof(G,x);

GAP output A base B together with strong generators, and the corresponding Schreier trees and Schreier generators for each base point.

Query output This is simply the proof of Section 6 repeated inductively.

8 Nonmembership: Prove that the permutation g does not belong to G

We now have a chain of subgroups

G = G^{(1)} ≥ G^{(2)} ≥ ⋯ ≥ G^{(k)} ≥ G^{(k+1)} = 1.

and sets U^{(i)} consisting of coset representatives for G^{(i+1)} in G^{(i)}. An element g of G is contained in exactly one coset of G^{(2)} in G^{(1)}, so g = h_{2} · u_{1} for some unique h_{2} in G^{(2)} and u_{1} in U^{(1)}. By induction, we can show that

g = u_{k} · u_{k−1} · · · · · u_{1}

where each u_{i} ∈ U^{(i)} is uniquely determined by g. This process, called sifting an element, gives a canonical form for the elements of G and underpins most of the more advanced applications of stabiliser chains.

On the other hand, if g is not in G, then sifting fails because at some stage we get that x_{i}h_{i} is not in the orbit x_{i}G^{(i)}, and so h_{i} is not in G^{(i)}. This gives us our proof on nonmembership.

Query Input

• A list A of permutations generating G.

• A permutation g.

• The fact that g is not in G.

GAP input

     G := Group(A);
     IsNotIn_Proof ( g, G )

GAP output A base B together with generators for the stabiliser subgroups, and the corresponding Schreier trees and Schreier generators for each base point. A sequence of permutations [h_{1}, …, h_{j}] such that h_{i} = g; h_{i} = h_{i+1}u_{i} for u_{i} in the ith set of coset representatives; and x_{j}h_{j} is not in the ith orbit.

Query output A proof that the stabiliser chain is correct is given in Section 7. It is now easy to check that the permutations h_{i} have the properties claimed.

9 The order of G

The order of G follows directly from the stabilizer chain

|G| = |G_{x_{1}}| · |x_{1}G|
= |G_{x_{1}}| · |G_{x_{2}}| · |x_{2}G|
= ⋯
= ∏_{i=1}^{t} |x_{i}G_{{x_{1},...,x_{i−1}}}|

where B = [x_{1}, …, x_{t}] is a base. Example 9.1 From Example 7.1 it immediately follows that the Mathieu group on 11 points has order 11 · 10 · 9 · 8 = 7920. Query Input A list A of permutations generating G. GAP input

     G := Group(A);
     Order_Proof(G);

GAP output A stabiliser chain, and the product of the sizes of the orbits. Query output The proof that the stabiliser chain is correct is given in

Section 7.

References

[1] Chapter 8: Working with finite groups of ”Some tapas of computer algebra” by Cuypers, Soicher, and Sterk. Springer, 1999.

[2] Caprotti & Oostdijk: Pocklington.