2
$\begingroup$

Unfortunately (like many other authors) Fenwick does a very bad job of explaining his work (the Binary Indexed Tree) in the original text. The paper lacks a proper formal proof of why this structure should work and only provides examples. This seems to be a very widespread issue regarding this topic and no tutorial or blog post out there seems to prove the correctness of this beast.

Just to be clear, I'm not looking for intuition or an explanation of how this data structure works, I already know that, what I am asking for is a formal proof that says a tree built this way will do what it is supposed to do correctly.

There is already another question here, with a very detailed and well-written answer that still doesn't provide a proof (though the question didn't really ask for proof either) and also seems to rely on a logic much different from what is presented in the original paper so please do not mark this as a duplicate.

$\endgroup$
2
  • $\begingroup$ Since a Fenwick tree for $n$-bit integers is very nearly two Fenwick trees for $(n-1)$-bit integers plus a new root node, I think you could get a pretty straightforward proof of correctness using induction on the number of bits. $\endgroup$ Jan 16, 2018 at 9:10
  • 1
    $\begingroup$ @j_random_hacker well this is not at all obvious and needs a proof itself! $\endgroup$
    – Paghillect
    Jan 17, 2018 at 7:17

1 Answer 1

1
$\begingroup$

Both my formatting and proving techniques are a bit rusty. Please let me know if any of the following proof is done dirty.

In Fenwick's paper, which will be called paper for short in the rest of the proof, at least half of it is revolved around partial sums under logarithmic time. I think it is a good application but when it comes to wrapping your head around the intuition and nuance, there are still work to do.

The key idea of the paper, imo, is outlined in this statement in P.2

The basic idea is that, just as an integer is the sum of appropriate powers of two, so can a cumulative frequency be represented as the appropriate sum of sets of cumulative 'subfrequencies'.

Suppose there are 2 mappings per each positive integer. First one being the indexed item

$item(n)$

and second one being the partial sum starting from some weird indexed item to this indexed item. The only known fact is that the difference between them is $LSB - 1$

$weird(n) = \sum_{i=n - LSB + 1}^{n}item(i)$

if the positive integer is 1 LSB away from being all 0's, then

$weird(n) = \sum_{i1}^{n}item(i)$

With this weird mapping, $\sum_{i=1}^{11}item(i)$ can be written in this way instead,

$weird(1000_2)+weird(1010_2)+weird(1011_2)$

Since this is almost everything of the paper, I will write in full detail of the indexes represented by each term. For $1011_2$, there are at least 2 LSB away from all 0's, so

$weird(1011_2) = \sum_{i=11 - 1 + 1}^{11}item(i) = item(11)$

For $1010_2$, again, at least 2 LSB away from all 0's so,

$weird(1010_2) = \sum_{i=10 - 2 + 1}^{10}item(i) = item(9) + item(10)$

For $1000_2$, since it is 1 LSB away from all 0's so,

$weird(1000_2) = \sum_{i=1}^{8}item(i)$

Together, you can see why the sum of the 3 terms are correct. That's the end of the foreplay and it will be full throttle from here on. I argue that the following algorithm will visit each term from 1 to that positive integer one time only, no more, no less and it applies to each positive integer.

n = positive integer
cumulation = 0

while n > 0
  cumulation += weird(n)
  strip LSB from n

return cumulation

Note that each positive integer can be written in binary form with at least one 1's in it. So there must exist a sequence wherein each preceding term is the successive term stripping of its LSB. This is just a convoluted way of saying

$11_{10}: 0000_2, 1000_2, 1010_2, 1011_2$.

This sequence, if viewed as half-interval, will cover the entire range from 1 to that positive integer. Again, one convoluted way of saying

$(0000_2,1000_2]\cup(1000_2,1010_2]\cup(1010_2,1011_2]=(0000_2,1011_2]$

Each half-interval is covered entirely by a weird function indexed at the end of that interval. Again, one convoluted way of saying

$weird(1000_2)$ covers all indexes from $(0000_2, 1000_2]$

Each term from 1 to n will be reached at least once. Suppose there exist a positive index which its mapped item is not reached. It must exist in $(0, n]$ and it must fall into one of the half-intervals from the said sequence, which is covered by all weird functions. This contradicts that it is not reached. Hence, each term from 1 to that positive integer must be reached at least once.

By construction, each half-interval from the said sequence will be visited once only in each loop of the algorithm. By construction, weird function will only include all its member in the half-interval once only. Therefore, each item will be reached at most once.

Since each item is reached at most and at least once, I conclude each item is reached once only in this algorithm.

What follows will be the proof of the construction algorithm of weird function. For a while it has been taken for granted. No longer will it be the case. I argue the following algorithm makes weird function at each index cover whatever in their half-interval once only. Again and again, one convoluted of saying the following is indeed true in the construct of the coming algorithm.

$weird(1010_2) = \sum_{i=1001_2}^{1010_2}item(i)$

The algorithm is

n = positive integer
for each index from 1 to n
  while index <= n
    weird[index] += item[index]
    add LSB to index

For each index, there exists a half-interval which the weird function should hit. Again and again, one convoluted of saying the following is indeed true in the construct of the coming algorithm.

$weird(1010_2) = \sum_{i=1001_2}^{1010_2}item(i)$

For each index, if every member in its half interval hits weird[index] once only, then the proposition is correct.

Suppose, by contradiction, there exists an index such that there exists a member in its half interval which doesn't hit weird[that index]. I argue that this member must have at least 1 LSB as well as the fact that adding LSB will eventually equate the member to the index. Hence, the member will hit that index, contradicting it doesn't that index. By proof of contradiction, for each index, each member that should hit weird[index] will hit at least once.

Why is there at least 1 LSB?

Each index is at least 1. The least value after stripping of LSB is 0. Since 1 is added, the value is at least 1, which translates to have at least 1 LSB.

Why adding LSB will eventually hit the index?

In base case where there is no 0 bit on or after the LSB of the index, this is trivially true. For example,

index = $1_2$, half interval = (0, $1_2$]

Suppose, inductively, any members with less than or equal to k zero bits on or after the LSB will hit the index. Bits, if any, after the rightmost 0 bit must be 1. Regardless, adding 1 will turn the 0 bit to 1, which left a sum of k zero bits. By induction, it is correct.

I also argue that for each index, each member will not hit the index more than once because according to the algorithm, each value won't hit another index more than once. Addition does wonders.

The proposition is correct.

Fenwick, Peter M. "A new data structure for cumulative frequency tables." Software: Practice and experience 24.3 (1994): 327-336.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.