extract large church numbers from abstract algorithm

extract_church_numbers.md

This allows you to extract large church numbers from abstract's algorithm. It is just a very efficient implementation of natToBinary : Nat -> Bits.

  U= x.(x x)

  8= s.z.(s (s (s (s (s (s (s (s z))))))))

  19= s.z.(s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))))))))

  succ=
    (U r.x.a.b.(x b x.(a (r r x))))

  zero=
    (U r.a.b.(a (r r)))

  peek= n.x.(n
    t.(t x.(x
      x.r.t.(t x a.b.c.(r a b (a c)))
      x.r.t.(t x a.b.c.(r a b (b c)))))
    t.(t x a.b.c.c)
    x.r.r)

  extract= bitCount. nat. (peek bitCount (nat succ zero))

  (extract 8 (19 19))

Here, (extract bitCount nat) gets the bitCount first bits of nat, which can be a large number. On this example I extracted the first 8 bits of 19^19 (which is about 2^24, so obviously way too large). This costs about 1m rewrites.

It works:

$ echo 'obase=2; 1000000000' | bc
111011100110101100101000000000
$ lambda -p '
Succ = Y (self, x, a, b: x b (y: a (self y)));
Zero = Y (self, a, b: a self);
Magic = p, x, r, t: t x (a, b, c: r a b (p a b c));
Extract = b, n: b (t: t (Cons (Magic T) (Magic F)))
        (Cons (n Succ Zero) (K F)) F;
Extract 32 1g
'
1352881(154042), 7113 ms
v1, v2, v3: v1 (v1 (v1 (v1 (v1 (v1 (v1 (v1 (v1 (v2 (v1 (v2 (v1 (v1 (v2 (v2 (v1 (v2 (v1 (v2 (v2 (v1 (v1 (v2 (v2 (v2 (v1 (v2 (v2 (v2 (v1 (v1 v3)))))))))))))))))))))))))))))))
$ 

Thanks!