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. This takes only 152715 total rewrites.

  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))

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

cc Anton Salikhmetov :)

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.