Tuply singleton v2

In my previous post I showed how we can encode a pair into a single number.

I found out that encoding is wrong for some numbers. For example, consider the pairs $\{ (0.4, 3), (2.8, 2) \}$ . If you encode either of those using the formula we derived, you will get the same answer: 137.2.

In this post, we will change our strategy and slightly adjust our formula.

Here is the Haskell code I used to determine whether a formula is valid or not:

generateGroupsForFormula
  :: (Double -> Integer -> Double) -> [[(Double, Integer, Double)]]
generateGroupsForFormula = filterIt . groupIt . sortIt . genList'
    where
    genList x1s x2s f = [(x1, x2, s) | x1 <- x1s, x2 <- x2s, let s = f x1 x2]
    genList'          = genList [0,0.01..5] [0..100]
    sortIt            = sortBy (\(_,_,x) (_,_,y) -> if (x - y) < 0.0001 then LT else GT)
    groupIt           = groupBy (\(_,_,x) (_,_,y) -> abs (x - y) < 0.0001)
    filterIt          = filter (\x -> length x > 1)

isFormulaValid :: (Double -> Integer -> Double) -> Bool
isFormulaValid f = null (generateGroupsForFormula f)

As we saw the pairs $\{ (0.4, 3), (2.8, 2) \}$ do not really encode to two different numbers. To see that we can invoke these functions as follows:

> isFormulaValid (\x1 x2 -> x1 * (3 ** fromIntegral x2))
False
> generateGroupsForFormula (\x1 x2 -> x1 * (7 ** fromIntegral x2)) !! 100
[(0.4,3,137.20000000000002),(2.8,2,137.2)]

So it fails the very definition of a pair: $(a, b) = (u, v) \iff a = u \land b = v$ .

We will try to use a different approach. Consider we have these base numbers $b_1, b_2 \in \mathbb{N}$ together with some numbers $x_1 \in \mathbb{R}, x_2 \in \mathbb{N}$ . We are looking at ${b_1}^{x_1} \cdot {b_2}^{x_2}$ . This makes a single number in the same way it did in the previous post.

To extract numbers, we just have to use division. But how do we know what to divide, and until when? First, it is important to know the bounds of $x_1$ . For example, if $b_1 = 2$ and $0 \leq x_1 \leq 5$ then $2^5 = 32$ is the maximum bound of the first element. This information is useful as we now know that the second element must be larger than the maximum bound – this will tell us when to stop dividing. In general, we’re looking for a number larger than ${b_1}^{x_1}$ .

Back to our example, we already used $b_1 = 2$ . 33 is the first natural number larger than 32.

mkPair :: Double -> Integer -> Double
mkPair a b = if a > 5 || a < 0 then error "Out of bounds" else (2 ** a) * (33 ** fromIntegral b)

To extract $x_1$ out of $2^{x_1} \cdot 33^{x_2}$ we have to keep dividing our number by 33 until it is less than or equal to 32, (to get to just $2^{x_1}$ ) and finally take the log2 of that. For example if we had $2^3 \cdot 33^3$ , we divide that number by 33 just 3 times and then we reach $\leq 32$ , since $0 \leq 2^{x_1} = 2^3 = 8 \leq 32$ , and then take the log2 of $2^3$ which is 3. This gives our first element.

fst' :: Double -> Double
fst' x = if x > 32 then fst' (x / 33) else logBase 2 x

Now that we have the first element, the second element will be easy. To extract $x_2$ out of $2^{x_1} \cdot 33^{x_2}$ , we divide the number by $2^{x_1}$ (remember we already know how to get the first element $x_1$ ), and then take log33 to get the $x_2$ out of $33^{x_2}$ .

snd' :: Double -> Integer
snd' x = round $ logBase 33 (x / (2 ** fst' x))

Running it:

> isFormulaValid (\x1 x2 -> (2 ** x1) * (33 ** fromIntegral x2))
True
> let p = mkPair 5.0 1 in printf "Pair: %f, First: %f, Second: %d\n" p (fst' p) (snd' p)
Pair: 1056.0, First: 5.0, Second: 1
> let p = mkPair 3.9 17 in printf "Pair: %f, First: %f, Second: %d\n" p (fst' p) (snd' p)
Pair: 974437437460685000000000000.0, First: 3.9, Second: 17
> let p = mkPair 4.9 10 in printf "Pair: %f, First: %f, Second: %d\n" p (fst' p) (snd' p)
Pair: 45728439116678304.0, First: 4.9, Second: 10

It would be good to write a mathematical proof that this encoding doesn’t break, but I’ll try to do that in a future post. 🙂