This post is about gray codes a.k.a. gray encoding of binary numbers. We will also cover some interesting properties, ideas and symmetries behind this encoding.
The Gray encoding is a special binary encoding for numbers, which is especially efficient for counting, because the hamming distance between any 2 successive values differ in exactly 1 bit (i.e. have Hamming distance 1). For this reason, counters in low power embedded environments are often implemented with this encoding. For example, for numbers from to the corresponding gray codes are:
The idea behind the increment operation is the following:
- Go through the bits of the previous gray code one-by-one starting from the rightmost bit.
- If flipping the current bit leads to a new code word, flip it and return the code word.
- Otherwise, proceed with the next bit.
The gray code of a binary number is (right hand sides in these equations mean bit sequences), where:
For example, for , the gray code would be :
This encoding can be easily implemented, for example in Python:
def gray_encode(x: int) -> int: return x ^ (x >> 1)
We can calculate the bits of by knowing the gray code as follows:
Continuing the example above, we can decode and get the initial codeword by calculating the prefix sums of in this notation:
Proof of correctness: We can prove that the formula above for decoding gray codes is correct by induction on the length of the codeword:
Induction base: :
Induction step: :
The implementation of the decoding algorithm is also not hard:
def gray_decode(g: int) -> int: b = 0 while g != 0: b ^= g g >>= 1 return b
Recursive definition for gray codes
We can formalize the intuition behind the increment operation above by an alternative, recursive definition for gray codes:
Let for be a mapping that maps numbers from to to the corresponding gray code as a bit string.
The first 2 gray codes are and , so we define:
For , define recursively:
The idea behind this definition is that we “flip” the mapping and prepend 1 to all of the gray codes in in reverse order (because of the “flip”). This is how we obtain the second half of the mapping. Because of the reverse order, the hamming distance between 2 successive values is always 1. We can visualize this idea of the recursive mapping for the first gray codes:
So, the key patterns that we see in the gray code table are the following:
- The second half of any is the first part of in reverse order with a leading 1-bit.
- In order to reverse the first part of , it is sufficient to just flip the first bit of every gray code.
We can formalize the second very important fact with the following theorem:
For all and in the second half of , it holds that:
In other words, it means that is equal to with the first bit of flipped.
Proof: by induction on :
Induction base: ():
Induction step: ():
- When defining , we prepended bit 1 to every code in the second half (). Because of that, it is correct to flip the first bit of .
- We now argue why it is correct to just leave other bits as-is. Consider all the bits at an arbitrary, but fixed position in the gray codes generated by . Formally, let where and .
- By definition of , the second part of is the reversed first half of , or, formally, .
- By induction hypothesis, we know that .
- By combining the last 2 observations, it follows that both and are palindromes.
- is a concatenation of 2 equal palindromes and is therefore also a palindrome.
This completes the proof. We can also illustrate, for example, the induction step:
Here, is illustrated for .
Equivalence of definitions
Of course, we need to prove that both definitions (recursive and non-recursive) are equivalent. Formally, we will prove the equivalence of definitions of all gray codes by induction for all :
Induction base: () Both definitions are equivalent for the first 4 gray codes.
Induction step: ():
- is part of , so we only need to prove that the definitions for gray codes for from the second part of are equivalent.
- Let . As defines first gray codes, it follows that (this fact is clearly seen on the illustrations above — the leading ones are marked with orange).
- By the symmetry theorem, we know that the gray code of is equal to the gray code of with the first bit flipped and 1 prepended. On the other hand, by the first definition of gray codes and because of defining gray codes, the gray code for is also equal to the gray code of with the first bit flipped because and 1 prepended (see above). By induction hypothesis, both definitions for were equivalent, so the definitions are equivalent for .