0

I'm solving the exercise 2.1-4 from CLRS "introduction to algorithms".

The problem is described as:

Consider the problem of adding two n-bit binary integers, stored in two n-element arrays A and B. The sum of the two integers should be stored in binary form in element array C.

What is the loop invariant of this problem? I have some thoughts about this question, and wrote them as comments in my solution to this problem, written in golang.

package additoin_binary

/*
Loop invariant:
At the start of each iteration of the loop digits in the subarray r[len(r) - 1 - i:] are
a[len(a) - 1 - i:] + b[len(b) - 1 - i:] + carry | provided that (len(a) - 1 - i) and (len(b) - 1 - i) are positive
a[len(a) - 1 - i:] + carry                      | provided that (len(a) - 1 - i) is positive and (len(b) - 1 - i) is negative
carry                                           | provided that (len(a) - 1 - i) and (len(b) - 1 - i) are negative
*** carry for i = a[(len(a) - 1) - i - 1] + b[(len(b) - 1) - i - 1] == 2 ? 1 : 0
*/

func BinaryAddition(a, b []int) []int {
    // a and b can have arbitrary number of digits.
    // We should control a length of the second term. It should be less or equal to a length of first term.w
    // Other vise we swap them
    if len(b) > len(a) {
        b, a = a, b
    }
    // loop invariant initialization:
    // before first loop iteration (i=0) index b_i is out of the array range (b[-1]),  so we don't have second term and sum = a
    // another way of thinking about it is we don't get b as argument and then sum = a, too
    if len(b) == 0 {
        return a
    }
    // result array to store sum
    r := make([]int, len(a)+1)
    // overflow of summing two bits (1 + 1)
    carry := 0
    // loop invariant maintenance:
    // we have right digits (after addition) in r for indexes r[len(r) - 1 - i:]
    for i := 0; i < len(r); i++ {
        a_i := len(a) - 1 - i // index for getting a last digit of a
        b_i := len(b) - 1 - i // index for getting a last digit of b
        r_i := len(r) - 1 - i // index for getting a last digit of r

        var s int
        if b_i >= 0 && a_i >= 0 {
            s = a[a_i] + b[b_i] + carry
        } else if a_i >= 0 {
            s = a[a_i] + carry
        } else { // all indexes run out of the game (a < 0, b < 0)
            s = carry
        }

        if s > 1 {
            r[r_i] = 0
            carry = 1
        } else {
            r[r_i] = s
            carry = 0
        }
    }
    // loop invariant termination:
    // i goes from 0 to len(r) - 1, r[len(r) - 1 - ([len(r) - 1):] => r[:]
    // This means, that for every index in r we have a right sum
    //*At i=0, r[i] a sum can be equal to 0, so we explicitly check that before return r
    if r[0] == 0 {
        return r[1:]
    } else {
        return r
    }
}

Edit 1: I extended the original problem. So now arrays A and B can have arbitrary lengths, respectively m and n. Example A = [1,0,1], B = [1,0] (m=3, n=2)

maxim-glyzin
  • 1
  • 3
  • The algorithm is not correct, so answering the question concerning the loop invariant is not very practical. – trincot May 12 '20 at 09:30
  • @trincot Can you provide an input to prove incorrectness of implementation? – maxim-glyzin May 12 '20 at 09:32
  • `{1}` and `{1, 1}` (in that order) gives `{0}`. Because you should determine the length of `r` *after* the swap of `a` and `b`. But I see you just corrected it. – trincot May 12 '20 at 09:44
  • @trincot you are right, thanks. I've corrected that. But do you have ideas about a loop invariant? – maxim-glyzin May 12 '20 at 10:19
  • Given that this is a positional notation and that the sum of two n-bit numbers could be an n+1-bit number (and that you've extended the problem to handle A=length m, B=length n) you'll need to decide which bit is the most-significant bit. It looks like you've chosen the first bit (A[0], B[0], r[0]) to be the MSBit, i.e., you've chosen to treat the numbers as big-endian. That's fine, but consider maybe using little-endian to simplify the algorithm. – torek May 12 '20 at 21:02
  • (None of the above is any kind of answer to anything you asked, it's just a note/comment.) – torek May 12 '20 at 21:02

2 Answers2

0

Consider the problem of adding two n-bit binary integers, stored in two n-element arrays A and B. The sum of the two integers should be stored in binary form in element array C.

The problem has a guarantee that A and B are n-element arrays, I think it's an important condition which could reduce code work.

What is a loop invariant?

In simple words, a loop invariant is some predicate (condition) that holds for every iteration of the loop.

In this problem, if assume len = len(C), iterate i in [0, len), the loop invariant is that r[len-1-i:len] is always the sum of a[len-2-i:len-1] and b[len-2-i:len-1] in lower i + 1 bit. Because after each loop, you will make one bit correct, it could prove that algorithm is correct.

Community
  • 1
  • 1
hyz
  • 472
  • 3
  • 10
  • Thanks for the answer. If I understand the last part of your answer right, it's not correct. Counter example: let's say we have a = [1,0] and b = [1]. Then follow your logic let's look what's going on when i = 0 (first iteration). We have `r[len-1-i:len]=r[3-1-0:3]=r[2:3]`, `a[len-2-i:len-1]=a[3-2-0:3-1]=a[1:2]` and `b[3-2-0:2]=b[1:2]`. So `a[1,2]` is the correct range to get a last digit of `a`, but `b[1,2]` is out of range, because `b` has only one element. So the only one range `b` can hold is `b[0,1]`. – maxim-glyzin May 12 '20 at 15:17
  • Maybe here "a[len-2-i:len-1] and b[len-2-i:len-1]" you mean the lengths of arrays itself? `len_a = len(a) = 2 and len_b = len(b) = 1` – maxim-glyzin May 12 '20 at 15:20
  • "Consider the problem of adding two n-bit binary integers, stored in two n-element arrays A and B." I think what it means is `len(A) == len(B) == n`. If `len(A)` is not equal to `len(B)`, that may need a more complicated way to represent a meaningful loop invariant. – hyz May 13 '20 at 03:53
  • yes, this was my mistake. I updated the question, but have you ideas about new problem with arbitrary lengths? – maxim-glyzin May 13 '20 at 05:52
0

The loop invariant condition can be taken as the number of bits yet to be added n - p (assuming you start by adding the lsb bits first from right to left), where p I have taken as the current bit significant position and n the size of the Augend and Addend bit-sequences.

chrispin2510
  • 1
  • 1
  • 2