The Collatz map is defined as:
c(x) = if even(x) then x/2 else 3x + 1
then the Collatz problem is answering the question: do all positive numbers x, iterated by the Collatz
function c, eventually reach the trivial cycle c(1) = 4, c(4) = 2, c(2) = 1.
Today, we're going to consider the problem in a different lens. Instead of defining the Collatz map in
terms of c(x) we're going to define
d(x) = if even(x) then x/2^v2(x) else (3x + 1)/2
v2(x) is defined as the highest exponent i such that 2^i divides x.
Interestingly, there is a productive way to see d as a function on binary
strings. To see this, lets consider the case where x is even: x/v2(x)
essentially strips the leading zeros from the binary representation of x.
This is straightforward, as the string of leading zeros is v2(x) long, and
dividing by 2^v2(x) will remove this string. To consider the case where
x is odd, we'll have to unpack the binary addition algorithm.
When represented in binary, the addition algorithm proceeds something like this, representing numbers as a list of their bits starting from the least significant:
add :: [Bool] -> [Bool] -> [Bool]
add xs ys = adder xs ys False
adder (x : xs) (y : ys) c = x xor y xor c : adder xs ys (maj x y c)
adder [] ys c = adder [False | _ <- ys] ys c
adder xs [] c = adder [False | _ <- xs] xs c
adder [] [] True = [True]
adder [] [] False = []
maj x y z = ind x + ind y + ind z >= 2
ind b = if b then 1 else 0
We can rewrite 3x + 1 as (2x + 1) + x, then we realize that 2x + 1 in
binary is simply the binary form of x with a 1 appended as the least
significant digit. Thus, we can see that (3x + 1)/2 = tail (add x (True : x)). We
also know that the first bit of x is True, because x
is odd.
add xs0 (True : xs0) = adder xs0 (True : xs0) False
let True : xs1 = xs0
adder (True : xs1) (True : True : xs1) False = False : adder xs1 (True : xs1) True
let x1 : xs2 = xs1
adder (x1 : xs2) (True : x1 : xs2) True = x1 : adder xs2 (x1 : xs2) True
let x2 : xs3 = xs2
adder (x2 : xs3) (x1 : x2 : xs3) True = not (x2 xor x1) : adder xs3 (x2 : xs3) (maj x2 x1 x0)
NB: x0 is True, but we don't simplify maj for clarity.
let x3 : xs4 = xs3
adder (x3 : xs4) (x2 : x3 : xs4) (maj x2 x1 x0) = x3 xor x2 xor (maj x2 x1 x0) : adder xs4 (x3 : xs4) (maj x3 x2 (maj x2 x1 x0))
let x4 : xs5 = xs4
adder (x4 : xs5) (x3 : x4 : xs5) (maj x3 x2 (x2 || x1))
= x4 xor x3 xor (maj x3 x2 (x2 || x1)) : adder xs5 (x4 : xs5) (maj x4 x3 (maj x3 x2 (x2 || x1)))
...
Overall, we can see a pattern: (3x + 1) / 2 has bits:
x1
not (x2 xor x1)
x3 xor x2 xor (maj x2 x1 x0)
...
xN xor xN-1 xor (maj xN-1 xN-2 (... (maj x2 x1 x0) ...))
XN xor (maj XN xN-2 (maj xN-1 xN-2 (... (maj x2 x1 x0) ...)))