algorithm - 算法。添加两个n位二进制数。这个问题的循环不变性是什么？

Question

我正在解决CLRS“算法简介”中的练习2.1-4。

问题描述为:

考虑将两个n位二进制整数存储在两个n元素数组A和B中的问题。两个整数之和应以二进制形式存储在元素数组C中。

这个问题的循环不变性是什么？
我对此问题有一些想法，并在解决该问题的过程中将其写为注释(用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
    }
}

编辑1:我扩展了原来的问题。因此，数组A和B现在可以具有任意长度，分别为m和n。例子A = [1,0,1]，B = [1,0](m = 3，n = 2)

Answer 1

考虑将两个n位二进制整数存储在两个n元素数组A和B中的问题。两个整数之和应以二进制形式存储在元素数组C中。

这个问题可以保证A和B是n元素数组，我认为这是可以减少代码工作的重要条件。

What is a loop invariant?
简而言之，循环不变式是某个谓词(条件)，对于循环的每次迭代都适用。

在此问题中，如果假设len = len(C)，在i中迭代[0, len)，则循环不变式是r[len-1-i:len]始终是a[len-2-i:len-1]较低位的b[len-2-i:len-1]和i + 1的总和。因为在每个循环之后，您将使一位正确，所以可以证明算法是正确的。