Wednesday, November 1, 2017

How to Become an Astronaut

On Tim Peake's selection exam to become an astronaut, the group of rotations of a cube, solving the question the long way, using Knuth Bendix Completion.
(updated on 15-06-2020)

Introduction


Recently, Tim Peake tweeted a Friday Night Brain Teaser about a question he was asked when taking the selection examination for admission to the astronaut program. The question was about the capacity for one to imagine 3D manipulations of a cube.

In this post, we will use the results of a previous post on Knuth Bendix Completion to find an answer to the question. No doubt this is not the shortest solution, but it surely is an interesting one.

The Question


Imagine a cube in front of you. The cube can be rolled left and right, and backward and forward. The bottom of the cube is marked with a black dot.


Imagine rolling the cube forward, left, left, forward, right, backward, right. Where is the black dot now ?

The Solution


Although the solution is quite obvious for those of us with good spatial sense, it is interesting to approach the problem from an algebraic view.

In a previous post, we talked about Knuth-Bendix Completion on Non-Abelian Group Theory. As the set of transformations of a cube with composition as an operation is a non-Abelian group, we will unleash the Knuth-Bendix Completion procedure on this group.

If the procedure terminates, we will have a decidable rewrite system that implements this group. We will then apply this rewrite system to find the normal form of the sequence of rotations specified in the question and see what comes out.

Transformations of a Cube


The number of positions, including orientation, of a cube is easy to determine. There are six sides to a cube, and for each side there are four possible orientations. This brings the total number of positions to 24 (6x4).

Imagine a given starting position for a cube. Each of the 24 positions corresponds to a transformation of the cube from the starting position to that position. This gives a collection of 24 transformations that, with composition as an operator, forms a non-Abelian group. This group is referred to as the transformation group of a cube.

Permutations of Four


The Internet is full of sources stating that the group of transformations of a cube is isomorphic to the group of permutations of four elements, referred to as S4. An isomorphism is a one-to-one relationship between the elements of two groups groups that preserves the group operation. We will come back to this property lateron.

Consider an ordered collection of 4 objects, say 1234. Then consider all the possible ways in which these 4 elements can be ordered, called permutations of these 4 objects.

To create such a configuration of 4, we have 4 possiblities for the first position, 3 for the second position (as one object is already used), 2 for the third position and then only one object is left for the fourth position. This gives a total of 24 (4x3x2x1 or 4!) permutations.

Some sources are providing a proof of the isomorphism. We will take a more visual approach.

The Cayley Graph


A Cayley graph visualizes the structure of a group based on a limited number of elements, called generators. The idea is that any element of the group, without exception, can be written as a composition of generators. For the permutation group of four, this gives an interesting diagram:


In the bottom left corner is our starting configuration 1234. A red arrow, representing the rotation to the right, brings us to 4123. A blue arrow, representing the rotation to the left of the 3 leftmost objects while keeping the righmost object in place, brings us to 2314. We will refer to the transformation represented by the red arrow as C, and the transformation represented by the blue arrow as S.

As you can see in the diagram, compositions of only these two generating elements of the group can be used to construct any of the 24 permutations, in various ways. Moreover, C is cyclic after four compositions, resulting in a number of red squares, while S is cyclic after three compositions, resulting in a number of blue triangles. Although the squares are not connected and the triangles are not connected, together, they create a fully connected graph.

Note that the collection of generators is not unique, in the sense that different collections of elements of the group may be used as generators. What's special about this collection is that it results in a nice graphical representation without crossing arrows, which is certainly not always the case.

You will find the Cayley graph and a lot more visuals on the wikiversity page on the Symmetric Group S4.

The Isomorphism


Coming back to the group of transformations of a cube, we could try to find a collection of generators and construct a Cayley diagram. However, as the two groups are isomorphic, with the right representation of the positions of a cube and the right choice of generators, we should get the same Cayley diagram.

First, let's look at the representation of the position of a cube. We will use a dice for this purpose, to easily distinguish between different positions. We will label the corners of the dice with labels 1, 2, 3 and 4, in such a way that each side has four different labels. It turns out that, after choosing the labels for one side, only one possibility is left to complete the labeling for the whole dice:


For the top side of the dice, we choose the labels to start with 1 for the corner closest to us, and continue clockwise while counting to 4, as illustrated by the blue labels. The labels of the corners of the bottom side can then only be chosen equal to the diagonally opposite corner, as illustrated by the red labels (where label 1 is at the back and not shown). The position of the dice when labeling is important, but arbitrary.

We will then represent the position of a cube by enumerating the labels of the corners of the top side, starting with the corner closest to us, and continuing clockwise. This results in the following observations:
  • The representations of all possible positions of a cube correspond exactly with the permutations of four.
  • The transformation represented by C is clockwise rotation around the vertical axis.
  • The transformation represented by S is anti-clockwise rotation around the horizontal axis (front left to back right), followed by clockwise rotation around the vertical axis.

With this representation, the Cayley graph for both groups is identical. Grab a dice and try it out ! And since any element of each group can be written as the same composition of generators, the relation preserves the group operation.

Knuth-Bendix Completion


We are now ready to start solving the question. We will start with the axioms of non-Abelian groups, define constants for the generators and add some axioms related to the generators. Then, Knuth-Bendix Completion will solve the question for us.

The Alphabet


An intuitive alphabet to represent the set of rotations on a cube, besides the identity, consists of a 90° rotation around each axis in 3D-space:
  • R - Right: Rolling the cube around the Y-axis, to the right.
  • C - Clockwise: Rolling the cube around the Z-axis, clockwise.
  • B - Backward: Rolling the cube around the X-axis, towards yourself.

Yes, we added an extra degree of freedom here, to prepare for interplanetary travel, say.

For readability, and because they are used in the question, we will add the inverse operations to the alphabet as well:
  • L - Left: Rolling the cube around the Y-axis, to the left.
  • A - Anti-Clockwise: Rolling the cube around the Z-axis, anti-clockwise.
  • F - Forward: Rolling the cube around the X-axis, away from yourself.

However, we will construct our theory using only the two generators introduced before, defined as:
  • C - Clockwise rotation around the vertical axis (hey, what a coincidence).
  • S - Rotate anti-clockwise around the horizontal axis, followed by rotate clockwise around the vertical axis.

One can easily express the transformations used in the question in function of these generators as follows:
  • R = S*S*C*S
  • L = C*S*S
  • B = S*S*C
  • F = C*C*C*S

Remember, the composition operator reverses the order of operation: C*S reads as "C after S".

The Theory


We will start off with the three axioms of non-Abelian group theory. Closure is implicit.

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

Then, we will add a minimum set of axioms defining the interaction of the transformations C and S.
[4] i(C) = C*C*C
[5] i(S) = S*S

Here we express the cyclic character of these transformations, as stated before: C is cyclic after four compositions and S is cyclic after three compositions. Note that these axioms correspond to loops in the Cayley diagram.

Observing the diagram somewhat closer, we notice one other type of loop, involving a combination of red and blue arrows. We add this relationship as an axiom too.
[6] i(C) = S*C*S

This completes our theory. Note that we did not orient the axioms lexicographically, from "complex" to "simple", as mentioned in the post on the Knuth-Bendix Completion procedure. This is not necessary, as the procedure does the orientation by itself.

The Rewrite System


As explained in our previous post on Knuth-Bendix Completion, we will try generating a decidable rewrite system out of this theory. And indeed, after the ninth iteration, a rewrite system is produced consisting of 39 rewrite rules.
[1]  a*1 -> a
[2]  a*i(a) -> 1
[3]  a*b*c -> a*(b*c)
[4]  S*(C*S) -> i(C)
[5]  i(S) -> S*S
[6]  C*(C*C) -> i(C)
[7]  a*(i(a)*b) -> b
[8]  S*(S*S) -> 1
[9]  1*a -> a
[10] S*(C*(S*a)) -> i(C)*a
[11] C*(C*(C*a)) -> i(C)*a
[12] S*(S*(S*a)) -> a
[13] i(C)*i(C) -> C*C
[14] S*(S*i(C)) -> C*S
[15] i(C)*(i(C)*a) -> C*(C*a)
[16] i(C)*(S*S) -> S*C
[17] S*(S*(i(C)*a)) -> C*(S*a)
[18] i(C)*(S*(S*a)) -> S*(C*a)
[19] i(1) -> 1
[20] S*(S*(C*C)) -> C*(S*i(C))
[21] S*(C*(C*S)) -> i(C)*(S*i(C))
[22] S*(S*(C*(C*a))) -> C*(S*(i(C)*a))
[23] C*(S*C) -> S*S
[24] C*(C*(S*S)) -> i(C)*(S*C)
[25] i(b)*(b*a) -> a
[26] i(i(a)) -> a
[27] S*(C*(C*(S*a))) -> i(C)*(S*(i(C)*a))
[28] C*(S*(C*a)) -> S*(S*a)
[29] C*(C*(S*(S*a))) -> i(C)*(S*(C*a))
[30] S*(i(C)*(S*i(C))) -> C*(S*(i(C)*S))
[31] i(C)*(S*(i(C)*S)) -> S*(i(C)*(S*C))
[32] C*(S*(i(C)*(S*C))) -> S*(i(C)*S)
[33] i(a)*a -> 1
[34] S*(i(C)*(S*(i(C)*a))) -> C*(S*(i(C)*(S*a)))
[35] i(C)*(S*(i(C)*(S*a))) -> S*(i(C)*(S*(C*a)))
[36] C*(S*(i(C)*(S*(C*a)))) -> S*(i(C)*(S*a))
[37] i(b*a) -> i(a)*i(b)
[38] S*(i(C)*(S*(C*(C*a)))) -> C*(C*(S*(i(C)*(S*a))))
[39] C*(C*(S*(i(C)*S))) -> S*(i(C)*(S*(C*C)))

The rewrite system has the same expressive power as the theory it originates from, but it has the advantage of decidability: semantic equality of terms can be verified using syntactic equality of normal forms, which are unique and guaranteed to exist.

Rewriting


Comes the time to take the sequence of rotations mentioned in the question and try rewriting it. Taking into account that our composition operator reverses the order of operation, the sequence forward, left, left, forward, right, backward, right should be represented as R*B*R*F*L*L*F. We then substitute the tranformations in this expression by their representation in terms of generators, and rewrite this term:
S*S*C*S*(S*S*C)*(S*S*C*S)*(C*C*C*S)*(C*S*S)*(C*S*S)*(C*C*C*S)
  [3]  -> S*S*C*S*(S*S*C)*(S*S*C*S)*(C*C*C*S)*(C*S*S)*(C*S*S*(C*C*C*S))
  [3]  -> S*S*C*S*(S*S*C)*(S*S*C*S)*(C*C*C*S)*(C*S*S*(C*S*S*(C*C*C*S)))
  [3]  -> S*S*C*S*(S*S*C)*(S*S*C*S)*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S))))
  [3]  -> S*S*C*S*(S*S*C)*(S*S*C*S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S)))))
  [3]  -> S*S*C*S*(S*S*C*(S*S*C*S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S))))))
  [3]  -> S*S*C*(S*(S*S*C*(S*S*C*S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S)))))))
  [3]  -> S*S*(C*(S*(S*S*C*(S*S*C*S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S))))))))
  [3]  -> S*(S*(C*(S*(S*S*C*(S*S*C*S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S)))))))))
  [10] -> S*(i(C)*(S*S*C*(S*S*C*S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S)))))))
  [3]  -> S*(i(C)*(S*S*(C*(S*S*C*S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S))))))))
  [3]  -> S*(i(C)*(S*(S*(C*(S*S*C*S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S)))))))))
  [18] -> S*(S*(C*(C*(S*S*C*S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S))))))))
  [23] -> C*(S*(i(C)*(S*S*C*S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S)))))))
  [3]  -> C*(S*(i(C)*(S*S*C*(S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S))))))))
  [3]  -> C*(S*(i(C)*(S*S*(C*(S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S)))))))))
  [3]  -> C*(S*(i(C)*(S*(S*(C*(S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S))))))))))
  [18] -> C*(S*(S*(C*(C*(S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S)))))))))
  [22] -> C*(C*(S*(i(C)*(S*(C*C*C*S*(C*S*S*(C*S*S*(C*C*C*S))))))))
  [3]  -> C*(C*(S*(i(C)*(S*(C*C*C*(S*(C*S*S*(C*S*S*(C*C*C*S)))))))))
  [3]  -> C*(C*(S*(i(C)*(S*(C*C*(C*(S*(C*S*S*(C*S*S*(C*C*C*S))))))))))
  [3]  -> C*(C*(S*(i(C)*(S*(C*(C*(C*(S*(C*S*S*(C*S*S*(C*C*C*S)))))))))))
  [36] -> C*(S*(i(C)*(S*(C*(C*(S*(C*S*S*(C*S*S*(C*C*C*S)))))))))
  [36] -> S*(i(C)*(S*(C*(S*(C*S*S*(C*S*S*(C*C*C*S)))))))
  [10] -> S*(i(C)*(i(C)*(C*S*S*(C*S*S*(C*C*C*S)))))
  [15] -> S*(C*(C*(C*S*S*(C*S*S*(C*C*C*S)))))
  [3]  -> S*(C*(C*(C*S*(S*(C*S*S*(C*C*C*S))))))
  [3]  -> S*(C*(C*(C*(S*(S*(C*S*S*(C*C*C*S)))))))
  [11] -> S*(i(C)*(S*(S*(C*S*S*(C*C*C*S)))))
  [18] -> S*(S*(C*(C*S*S*(C*C*C*S))))
  [3]  -> S*(S*(C*(C*S*(S*(C*C*C*S)))))
  [3]  -> S*(S*(C*(C*(S*(S*(C*C*C*S))))))
  [22] -> C*(S*(i(C)*(S*(S*(C*C*C*S)))))
  [18] -> C*(S*(S*(C*(C*C*C*S))))
  [3]  -> C*(S*(S*(C*(C*C*(C*S)))))
  [3]  -> C*(S*(S*(C*(C*(C*(C*S))))))
  [22] -> C*(C*(S*(i(C)*(C*(C*S)))))
  [25] -> C*(C*(S*(C*S)))
  [28] -> C*(S*(S*S))
  [8]  -> C*1
  [1]  -> C

So, the transformation mentioned in the question is equal to a single rotation around the Z-axis, clockwise. Consequently, the cube will still be positioned on the side with the black dot, albeit rotated by 90°, which is irrelevant for answering the question.

A Note on Expressivity


Admitted, the reduction is quite verbose. This is obviously caused by the fact that we limit our alphabet to the two generators only. A similar exercise where all the 90° rotations and their inverse are added to the alphabet, and the theory is extended with the axioms reflecting their relationships, works equally well, with the desired brevity. However, the rewrite system generated by the Knuth-Bendix completion procedure consists of 92 rewrite rules, as there are a lot more relationships to capture.

We will not present the completed rewrite system over the extended alphabet here, but we do provide the reduction of the term using this extended alphabet:
R*B*R*F*L*L*F
  [3]  -> R*B*R*F*L*(L*F)
  [3]  -> R*B*R*F*(L*(L*F))
  [3]  -> R*B*R*(F*(L*(L*F)))
  [3]  -> R*B*(R*(F*(L*(L*F))))
  [3]  -> R*(B*(R*(F*(L*(L*F)))))
  [33] -> B*(C*(R*(F*(L*(L*F)))))
  [32] -> B*(B*(C*(F*(L*(L*F)))))
  [58] -> A*(B*(B*(F*(L*(L*F)))))
  [55] -> A*(B*(L*(L*F)))
  [49] -> B*(L*F)
  [21] -> B*(C*L)
  [56] -> C

Conclusion


We are going to Mars !

The group of rotations of a cube nicely passes Knuth-Bendix Completion and the resulting rewrite system solves the Friday night brain teaser, mechanically, deterministically, in the blink of an eye.

We cannot be sure of our theory to be true, but it is correct, and, more importantly, it solves the issue.

No comments:

Post a Comment