Skip to content

Instantly share code, notes, and snippets.

@VictorTaelin

VictorTaelin/binary_addition.md

Last active November 30, 2017 13:22
Download ZIP

Revisions

  1. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -60,4 +60,4 @@ It performs the same computation, but on arbitrary bit-strings instead of mod-32

    *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, which is doing amazing progress :)
    Gist per request of Anton Salikhmetov, who is doing amazing progress :)
  2. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -60,4 +60,4 @@ It performs the same computation, but on arbitrary bit-strings instead of mod-32

    *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.*

    cc Anton Salikhmetov :)
    Gist per request of Anton Salikhmetov, which is doing amazing progress :)
  3. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -21,7 +21,7 @@ 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

    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 simpler solutions. By understanding how to make those terms lightweight, you could write this:
    Of course, there are faster solutions. By understanding how to make those terms lightweight, you could write this:

    ```
    binAdd= x.y.
  4. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -21,7 +21,7 @@ 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

    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 better ways to do it. By understanding how to make those terms lightweight, you could, for example, write this:
    Of course, there are simpler solutions. By understanding how to make those terms lightweight, you could write this:

    ```
    binAdd= x.y.
  5. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -24,7 +24,7 @@ This works by converting both bitstrings to unary (i.e., Nat), and then applying
    Of course, there are better ways to do it. By understanding how to make those terms lightweight, you could, for example, write this:

    ```
    add= x.y.
    binAdd= x.y.
    (x.(x x)
    r.x.y.k.(x
    xs.(y
    @@ -53,7 +53,7 @@ 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 (add X Y))
    (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.
  6. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 6 additions and 6 deletions.
    12 changes: 6 additions & 6 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -27,14 +27,14 @@ Of course, there are better ways to do it. By understanding how to make those te
    add= 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.(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.(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
  7. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -56,7 +56,7 @@ 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
    (binFold (add 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 curry-passing recursive addition, though, so no sharing wizardry.
    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.*

  8. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -25,7 +25,7 @@ Of course, there are better ways to do it. By understanding how to make those te

    ```
    add= x.y.
    (x. (x x)
    (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))
  9. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 3 deletions.
    4 changes: 1 addition & 3 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -24,10 +24,8 @@ This works by converting both bitstrings to unary (i.e., Nat), and then applying
    Of course, there are better ways to do it. By understanding how to make those terms lightweight, you could, for example, write this:

    ```
    U= x. (x x)
    add= x.y.
    (U
    (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))
  10. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -27,8 +27,8 @@ Of course, there are better ways to do it. By understanding how to make those te
    U= x. (x x)
    add= x.y.
    (U r.x.y.k.
    (x
    (U
    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))
  11. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 3 additions and 3 deletions.
    6 changes: 3 additions & 3 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -42,9 +42,9 @@ add= x.y.
    k.f.a.b.c.c
    k
    (r r))
    x
    y
    a.b.b)
    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)
  12. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 40 additions and 40 deletions.
    80 changes: 40 additions & 40 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -3,59 +3,59 @@ This is a term that performs modulo 32 addition on two 32-bit binary numbers eff
    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))
    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))))))))))))))))))))))))))))))))
    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))
    (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 better ways to do it. By understanding how to make those terms lightweight, you could, for example, write this:

    ```
    U= x. (x x)
    U= x. (x x)
    add= x.y.
    (U 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)
    add= x.y.
    (U 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)
    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))))))))))))))))))))))))))))))))
    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 (add X Y))
    (binFold (add 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 curry-passing recursive addition, though, so no sharing wizardry.
  13. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 20 additions and 14 deletions.
    34 changes: 20 additions & 14 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -26,19 +26,25 @@ Of course, there are better ways to do it. By understanding how to make those te
    ```
    U= x. (x x)
    adder= (U r.x.y.k.
    (x
    xs. (y
    ys. f.a.b.c.(k b a (f xs ys a.b.b))
    ys. f.a.b.c.(k a b (f xs ys k))
    f.a.b.c.c)
    xs. (y
    ys. f.a.b.c.(k a b (f xs ys k))
    ys. f.a.b.c.(k b a (f xs ys a.b.a))
    f.a.b.c.c)
    f.a.b.c.c
    (r r)))
    add= x.y.(adder x y a.b.b)
    add= x.y.
    (U 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)
    @@ -52,7 +58,7 @@ Of course, there are better ways to do it. By understanding how to make those te
    (binFold (add X Y))
    ```

    It performs the same computation, but on arbitrary bit-strings instead of mod-32, and takes only `10501` total rewrites. It is just the equivalent of an usual Haskellish curry-passing recursive addition, though, so no sharing wizardry.
    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 curry-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.*

  14. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -54,6 +54,6 @@ Of course, there are better ways to do it. By understanding how to make those te

    It performs the same computation, but on arbitrary bit-strings instead of mod-32, and takes only `10501` total rewrites. It is just the equivalent of an usual Haskellish curry-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, though. As expected, it turned out to be amazingly simple.*
    *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.*

    cc Anton Salikhmetov :)
  15. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -19,7 +19,7 @@ On this example, I compute `279739872 + 496122620 = 775862492`.
    (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 with that shouldn't 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.
    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 better ways to do it. By understanding how to make those terms lightweight, you could, for example, write this:

  16. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -19,7 +19,7 @@ On this example, I compute `279739872 + 496122620 = 775862492`.
    (binFold (binAdd X Y))
    ```

    This works by converting both bitstrings to unary (i.e., Nat), and then applying `succ` `279739872 + 496122620` times to the bitstring `zero`. So, yes, it applies a linear-time function millions of times to a term with that shouldn't 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.
    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 with that shouldn't 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 better ways to do it. By understanding how to make those terms lightweight, you could, for example, write this:

  17. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -19,7 +19,7 @@ On this example, I compute `279739872 + 496122620 = 775862492`.
    (binFold (binAdd X Y))
    ```

    This works by converting both bitstrings to unary (i.e., Nat), and then applying successor 279739872 + 496122620 times to the bitstring zero. So, yes, it applies a linear-time function millions of times to a term with that shouldn't 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.
    This works by converting both bitstrings to unary (i.e., Nat), and then applying `succ` `279739872 + 496122620` times to the bitstring `zero`. So, yes, it applies a linear-time function millions of times to a term with that shouldn't 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 better ways to do it. By understanding how to make those terms lightweight, you could, for example, write this:

    @@ -52,7 +52,7 @@ Of course, there are better ways to do it. By understanding how to make those te
    (binFold (add X Y))
    ```

    It performs the same computation, but on arbitrary bit-strings instead of mod-32, and takes only 10501 total rewrites. It is just the equivalent of an usual Haskellish curry-passing recursive addition, though, so no sharing wizardry.
    It performs the same computation, but on arbitrary bit-strings instead of mod-32, and takes only `10501` total rewrites. It is just the equivalent of an usual Haskellish curry-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, though. As expected, it turned out to be amazingly simple.*

  18. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 4 additions and 2 deletions.
    6 changes: 4 additions & 2 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -19,10 +19,11 @@ On this example, I compute `279739872 + 496122620 = 775862492`.
    (binFold (binAdd X Y))
    ```

    This works by converting both bitstrings to unary (i.e., Nat), and then applying successor 279739872 + 496122620 times to the bitstring zero. So, yeas, it applies a linear-complexity function 279739872 + 496122620 times, to a term with a size that couldn't fit in your memory, yet it reaches normal form in merely 152715 rewrites! That's amazing, isn't it? This example is great, because showcases well the power of optimal sharing.
    This works by converting both bitstrings to unary (i.e., Nat), and then applying successor 279739872 + 496122620 times to the bitstring zero. So, yes, it applies a linear-time function millions of times to a term with that shouldn't 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 better ways to do it. By understanding how to make those terms lightweight, you could, for example, write this:

    ```
    U= x. (x x)
    adder= (U r.x.y.k.
    @@ -49,7 +50,8 @@ Of course, there are better ways to do it. By understanding how to make those te
    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 (add X Y))

    ```

    It performs the same computation, but on arbitrary bit-strings instead of mod-32, and takes only 10501 total rewrites. It is just the equivalent of an usual Haskellish curry-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, though. As expected, it turned out to be amazingly simple.*
  19. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 35 additions and 2 deletions.
    37 changes: 35 additions & 2 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -1,6 +1,6 @@
    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.
    On this example, I compute `279739872 + 496122620 = 775862492`.

    ```
    binSize= 32
    @@ -19,6 +19,39 @@ On this example, I compute `279739872 + 496122620 = 775862492`. This takes only
    (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; and, trust me, I tried A LOT of things. All my previous attempts had exponential complexity, though. As expected, it turned out to be amazingly simple.*
    This works by converting both bitstrings to unary (i.e., Nat), and then applying successor 279739872 + 496122620 times to the bitstring zero. So, yeas, it applies a linear-complexity function 279739872 + 496122620 times, to a term with a size that couldn't fit in your memory, yet it reaches normal form in merely 152715 rewrites! That's amazing, isn't it? This example is great, because showcases well the power of optimal sharing.

    Of course, there are better ways to do it. By understanding how to make those terms lightweight, you could, for example, write this:

    U= x. (x x)

    adder= (U r.x.y.k.
    (x
    xs. (y
    ys. f.a.b.c.(k b a (f xs ys a.b.b))
    ys. f.a.b.c.(k a b (f xs ys k))
    f.a.b.c.c)
    xs. (y
    ys. f.a.b.c.(k a b (f xs ys k))
    ys. f.a.b.c.(k b a (f xs ys a.b.a))
    f.a.b.c.c)
    f.a.b.c.c
    (r r)))
    add= x.y.(adder 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 (add X Y))

    It performs the same computation, but on arbitrary bit-strings instead of mod-32, and takes only 10501 total rewrites. It is just the equivalent of an usual Haskellish curry-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, though. As expected, it turned out to be amazingly simple.*

    cc Anton Salikhmetov :)
  20. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -19,6 +19,6 @@ On this example, I compute `279739872 + 496122620 = 775862492`. This takes only
    (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.*
    *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; and, trust me, I tried A LOT of things. All my previous attempts had exponential complexity, though. As expected, it turned out to be amazingly simple.*

    cc Anton Salikhmetov :)
  21. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -2,8 +2,6 @@ This is a term that performs modulo 32 addition on two 32-bit binary numbers eff

    On this example, I compute `279739872 + 496122620 = 775862492`. This takes only 152715 total rewrites.

    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.

    ```
    binSize= 32
    binZero= (binSize r.a.b.c.(a r) a.b.c.c)
    @@ -21,4 +19,6 @@ Not so fun fact: it took me years to develop the right techniques and intuition
    (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 :)
  22. VictorTaelin revised this gist Nov 23, 2017. 1 changed file with 2 additions and 3 deletions.
    5 changes: 2 additions & 3 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -8,10 +8,9 @@ Not so fun fact: it took me years to develop the right techniques and intuition
    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)
    binNot= (binSize r.x.a.b.c.(x x.f.(b (f x)) x.f.(a (f x)) f.c r) 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)
    toNat= (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. (toNat a binSucc (toNat b binSucc binZero))
    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)
  23. VictorTaelin created this gist Nov 23, 2017.
    25 changes: 25 additions & 0 deletions binary_addition.md
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,25 @@
    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.

    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.

    ```
    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)
    binNot= (binSize r.x.a.b.c.(x x.f.(b (f x)) x.f.(a (f x)) f.c r) 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)
    toNat= (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. (toNat a binSucc (toNat 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))
    ```

    cc Anton Salikhmetov :)