Binary addition on the abstract algorithm!

binary_addition.md

This is a term that performs modulo 32 addition on two 32-bit binary numbers efficiently on the abstract algorithm.

On this example, I compute 279739872 + 496122620 = 775862492.

binSize= 32
binZero= (binSize r.a.b.c.(a r) a.b.c.c)
binSucc= (binSize r.x.a.b.c.(x b x.(a (r x)) c) a.a)
binFold= x.a.b.c.(binSize r.x.(x x.f.(a (f x)) x.f.(b (f x)) f.c r) a.c x)
binToNat= (binSize r.n.x.(x x.f.(f x) x.f.(add n (f x)) f.0 (r (mul 2 n))) n.x.0 1)
binAdd= a. b. (binToNat a binSucc (binToNat b binSucc binZero))

A= x.a.b.c.(a x)
B= x.a.b.c.(b x)
C= a.b.c.c
X= (A (A (A (A (A (B (B (B (B (A (B (B (B (B (B (A (A (A (B (B (A (B (A (B (A (A (A (A (B (A (A (A C))))))))))))))))))))))))))))))))
Y= (A (A (B (B (B (B (B (B (A (B (A (B (B (B (A (A (A (B (A (A (B (A (A (B (B (A (B (B (B (A (A (A C))))))))))))))))))))))))))))))))

(binFold (binAdd X Y))

This works by converting both bitstrings to unary (i.e., Nat), and then applying the binary succ function 279739872 + 496122620 times to the bitstring zero. So, yes, it applies a linear-time function millions of times to a term that shouldn't even fit in your computer's memory, yet it reaches normal form in merely 152715 rewrites! That's amazing, isn't it? This example shows well the power of optimal sharing.

Of course, there are faster solutions. By understanding how to make those terms lightweight, you could write this:

binAdd= x.y.
  (x.(x x)
    r.x.y.k.(x
      xs.(y
        ys.xs.k.f.a.b.c.(k b a (f xs ys a.b.b))
        ys.xs.k.f.a.b.c.(k a b (f xs ys k))
        xs.k.f.a.b.c.c
        xs)
      xs.(y
        ys.xs.k.f.a.b.c.(k a b (f xs ys k))
        ys.xs.k.f.a.b.c.(k b a (f xs ys a.b.a))
        xs.k.f.a.b.c.c
        xs)
      k.f.a.b.c.c
      k
      (r r))
    x
    y
    a.b.b)

binSize= 32
binFold= x.a.b.c.(binSize r.x.(x x.f.(a (f x)) x.f.(b (f x)) f.c r) a.c x)

A= x.a.b.c.(a x)
B= x.a.b.c.(b x)
C= a.b.c.c
X= (A (A (A (A (A (B (B (B (B (A (B (B (B (B (B (A (A (A (B (B (A (B (A (B (A (A (A (A (B (A (A (A C))))))))))))))))))))))))))))))))
Y= (A (A (B (B (B (B (B (B (A (B (A (B (B (B (A (A (A (B (A (A (B (A (A (B (B (A (B (B (B (A (A (A C))))))))))))))))))))))))))))))))

(binFold (binAdd X Y))

It performs the same computation, but on arbitrary bit-strings instead of mod-32, and takes only 7817 total rewrites. It is just the equivalent of an usual Haskellish carry-passing recursive addition, though, so no sharing wizardry.

Not so fun fact: it took me years to develop the right techniques and intuition to be able to write those. Yes, for all that time I wasn't able to code a fast binary addition term; and, trust me, I tried A LOT of things. All my previous attempts had exponential complexity. As expected, it turned out to be amazingly simple.

Gist per request of Anton Salikhmetov, who is doing amazing progress :)

For 32-bit arithmetic, boolean 32-tuples perform better:

$ bc
obase = 16
279739872
10AC7DE0
496122620
1D923AFC
obase = 2
775862492
101110001111101011100011011100
$ lambda -pem lib.mlc 'Pri32 (Add32 hex(10ac7de0) hex(1d923afc))'
4900(1092), 96 ms
_0 _0 _1 _0 _1 _1 _1 _0 _0 _0 _1 _1 _1 _1 _1 _0 _1 _0 _1 _1 _1 _0 _0 _0 _1 _1 _0 _1 _1 _1 _0 _0
$ 

Bitwise operations are also clearly more efficient on boolean 32-tuples.