deriving]

我们现在终于可以推导出在芬威克数组索引上移动所需的运算了，方法是从二叉索引树上的操作开始，并通过与芬威克索引的转换进行变换。首先，为了融合掉由此产生的转换，我们需要几个引理。

Theorem 1. shr-inc-dec [blog/fenwick/thm/thm3]

对于所有为奇数（即以 I 结尾）的 $bs : \text{Bits}$，

$\text{shr}(\text{dec}(bs)) = \text{shr}(bs)$
$\text{shr}(\text{inc}(bs)) = \text{inc}(\text{shr}(bs))$

证明两者均由定义直接可得。

Theorem 2. while-inc-dec [blog/fenwick/thm/thm4]

以下两条定理对所有 Bits 值均成立：

$\text{inc}(\text{while}(\text{odd}, \text{shr}, \cdot)) = \text{while}(\text{even}, \text{shr}, \text{inc}(\cdot))$
$\text{dec}(\text{while}(\text{even}, \text{shr}, \cdot)) = \text{while}(\text{odd}, \text{shr}, \text{dec}(\cdot))$

证明简单的 Bits 归纳证明。例如，对于 inc 的情况，两侧的函数都会丢弃连续的 1 位，然后将第一个 0 位翻转为 1。

最后，我们需要一个关于将零位移入和移出值右侧的引理。

Theorem 3. shl-shr [blog/fenwick/thm/thm5]

对于所有 $0 \lt x \lt 2^{n+2}$，

$$ \text{while}(\text{not}(\text{test}(\cdot, n + 1)), \text{shl}, \text{while}(\text{even}, \text{shr}, x)) = \text{while}(\text{not}(\text{test}(\cdot, n + 1)), \text{shl}, x) $$

（注：$\text{test}$ 在代码中是 test_helper，$\cdot$ 在此处是匿名函数简写： fn { x => not(test_helper(x, n + 1)) }）

证明直观上，这表明如果我们先移出所有零位，然后左移直到第 $n+1$ 位被设置，这可以通过完全忘记右移来获得相同的结果；移出零位然后再将它们移回来应该是恒等操作。

形式上，证明通过对 $x$ 进行归纳。如果 $x = xs : \text{I}$ 为奇数，等式立即成立，因为 $\text{while}(\text{even}, \text{shr}, x) = x$。否则，如果 $x = xs : \text{O}$，在左侧，O 会被 $\text{shr}$ 立即丢弃，而在右侧，$xs : \text{O} = \text{shl}(xs)$，并且由于 $xs \lt 2^{n+1}$，额外的 $\text{shl}$ 可以被吸收到 $\text{while}$ 循环中。剩下的就是归纳假设。

有了这些引理在手，让我们看看如何在芬威克数组中移动以实现 update 和 query；我们先从 update 开始。在实现 update 操作时，我们需要从一个叶节点开始，沿着路径向上到达根节点，更新沿途所有活跃的节点。实际上，对于任何给定的叶节点，其最近的活跃父节点恰好是存储在过去对应于该叶节点的槽中的节点（参见图 13）。因此，要更新索引 $i$，我们只需从芬威克数组中的索引 $i$ 开始，然后重复找到最近的活跃父节点，边走边更新。回想一下，用于 update 的命令式代码就是这样做的，通过在每一步加上当前索引的 LSB 来找到最近的活跃父节点：

pub fn update(self : FenwickTree, i : Int, delta : Int) -> Unit {
  let mut i = i
  while i < self._.length() {
    self._[i] += delta
    i += FenwickTree::lsb(i)
  }
}

让我们看看如何推导出这种行为。要在二叉索引方案下找到一个节点的最近活跃父节点，我们首先向上移动到直接父节点（通过将索引除以二，即执行一次右位移）；然后只要当前节点是右子节点（即索引为奇数），就继续向上移动到下一个直接父节点。这产生了如下定义：

pub fn active_parent_binary(self : Bits) -> Bits {
  while_(odd, shr, self.shr())
}

这就是为什么我们使用了根节点索引为 2 的略显奇怪的索引方案——否则这个定义对于任何活跃父节点是根节点的节点都不起作用！

现在，要推导出芬威克索引上的相应操作，我们通过与芬威克索引的转换进行共轭，计算如下。为了使计算更易读，每一步中被重写的部分都用下划线标出。

$$ \begin{align*} & \underline{\text{b2f}(n, \text{activeParentBinary}(\text{f2b}(n, \cdot)))} \\ & \{ \text{展开定义} \} \\ = & \text{unshift}(n + 1, \underline{\text{inc}(\text{while}(\text{odd}, \text{shr}}, \text{shr}(\text{dec}(\text{shift}(n + 1, \cdot)))))) \\ & \{ \text{引理 (while-inc-dec)} \} \\ = & \text{unshift}(n + 1, \text{while}(\text{even}, \text{shr}, \text{inc}(\underline{\text{shr}(\text{dec}}(\text{shift}(n + 1, \cdot)))))) \\ & \{ \text{引理 (shr-inc-dec); shift(n+1, x) 总是奇数} \} \\ = & \text{unshift}(n + 1, \text{while}(\text{even}, \text{shr}, \underline{\text{inc}(\text{shr}}(\text{shift}(n + 1, \text{dec}(\cdot)))))) \\ & \{ \text{引理 (shr-inc-dec)} \} \\ = & \text{unshift}(n + 1, \underline{\text{while}(\text{even}, \text{shr}, \text{shr}}(\text{inc}(\text{shift}(n + 1, \cdot))))) \\ & \{ \text{while(even, shr, shr(x)) = while(even, shr, x) 在偶数输入上} \} \\ = & \underline{\text{unshift}(n + 1}, \text{while}(\text{even}, \text{shr}, \text{inc}(\text{shift}(n + 1, \cdot)))) \\ & \{ \text{unshift} \} \\ = & \text{clear}(n + 1, \underline{\text{while}(\text{not}(\text{test}(n + 1, \cdot)), \text{shl}, \text{while}(\text{even}, \text{shr}}, \text{inc}(\underline{\text{shift}(n + 1, \cdot)})))) \\ & \{ \text{引理 (shl-shr); shift} \} \\ = & \text{clear}(n + 1, \text{while}(\text{not}(\text{test}(n + 1, \cdot)), \text{shl}, \text{inc}(\text{while}(\text{even}, \text{shr}, \text{set}(n + 1, \cdot))))) \\ \end{align*} $$

在最后一步中，由于输入 $x$ 满足 $x \le 2^n$，我们有 $\text{inc}(\text{shift}(n + 1, x)) \lt 2^{n+2}$，因此引理 shl-shr 适用。

从右到左阅读，我们刚刚计算出的流水线执行以下步骤：

设置位 $n+1$
移出连续的零，直到找到最低有效位的 1
加 1
将零移回，使最高有效位回到位置 $n+1$，然后清除它。

直观地说，这看起来很像加上 LSB！一般来说，要找到 LSB，必须移过连续的 0 位，直到找到第一个 1；问题是如何跟踪移过了多少个 0 位。lsb 函数本身通过递归栈来跟踪；找到第一个 1 位后，递归栈展开并将所有递归经过的 0 位重新追加回去。上述流水线代表了一种替代方法：将位 $n+1$ 设置为“哨兵”来跟踪我们移动了多少；右移直到第一个 1 确实在个位上，此时我们加 1；然后通过左移将所有 0 位移回，直到哨兵位回到 $n+1$ 的位置。这个过程的一个例子如图 19 所示。当然，这只适用于值足够小，以至于哨兵位在整个操作过程中不会受到干扰的情况。

为了使这一点更形式化，我们首先定义一个辅助函数 at_lsb，它执行一个“在 LSB 处”的操作，即它移出 0 位直到找到一个 1，应用给定的函数，然后恢复 0 位。

fn at_lsb(self : Bits, f : (Bits) -> Bits) -> Bits {
  match self {
    Rep(O) => Rep(O)
    s =>
      match s.pat_match() {
        (bs, O) => bs.at_lsb(f) |> Bits::make(O)
        (bs, I) => Bits::make(bs, I) |> f
      }
  }
}

Theorem 4. add-lsb [blog/fenwick/thm/thm6]

对于所有 $x : \text{Bits}$， $\text{add}(x, \text{lsb}(x)) = \text{atLSB}(\text{inc}, x)$ 且 $\text{subtract}(x, \text{lsb}(x)) = \text{atLSB}(\text{dec}, x)$。

（注：代码中 $\text{atLSB}$ 的定义为 at_lsb）

证明对 $x$ 进行简单的归纳即可。

我们可以将“带哨兵的移位”方案与 atLSB 形式化地关联起来，通过以下（相当复杂的）引理：

Theorem 5. sentinel [blog/fenwick/thm/thm7]

令 $n \ge 1$ 且令 $f : \text{Bits} \to \text{Bits}$ 是一个函数，使得

$f(\text{set}(n + 1, x)) = \text{set}(n + 1, f(x))$ 对于任何 $0 \lt x \lt 2^n$ 成立，且

$f(x) \lt 2^{n+1}$ 对于任何 $0 \lt x \lt 2^n + 2^{n-1}$ 成立。

那么对于所有 $0 \lt x \lt 2^n$， $$ \text{unshift}(n + 1, f(\text{shift}(n + 1, x))) = \text{atLSB}(f, x). $$

证明相当繁琐但并非特别具有启发性，因此我们省略它（一个包含完整证明的扩展版本可以在作者的网站上找到）。然而，我们确实注意到 inc 和 dec 都符合 $f$ 的标准：只要 $n \ge 1$，对某个 $0 \lt x \lt 2^n$ 进行递增或递减不会影响第 $(n+1)$ 位，并且对一个小于 $2^n + 2^{n-1}$ 的数进行递增或递减的结果将是一个小于 $2^{n+1}$ 的数。我们现在可以将所有部分组合起来，证明在每一步加上 LSB 是实现 update 的正确方法。

Theorem 6. [blog/fenwick/thm/thm8]

加上 LSB 是沿芬威克索引树向上移动到最近活跃父节点的正确方法，即 $$\begin{align*} & \text{activeParentFenwick}(x) \\ &= \text{b2f}(n, \text{activeParentBinary}(\text{f2b}(n, x))) \\ &= \text{add}(x, \text{lsb}(x)) \end{align*} $$ 在范围 $[1, 2^n)$ 上处处成立。（我们排除了 $2^n$，因为它对应于芬威克索引方案下的树根。）

证明

$$ \begin{aligned} & \text{b2f}(n, \text{activeParentBinary}(\text{f2b}'(n, x))) \\ = & \text{unshift}(n + 1, \text{inc}(\text{shift}(n + 1, x))) & \{ \text{先前的计算} \} \\ = & \text{atLSB}(\text{dec}, x) & \{ \text{引理 (sentinel)} \} \\ = & \text{add}(x, \text{lsb}(x)) & \{ \text{引理 (add-lsb)} \} \end{aligned} $$

我们可以进行类似的过程来推导前缀查询的实现（据称它涉及减去 LSB）。同样，如果我们想计算 $[1, j]$ 的和，我们可以从芬威克数组中的索引 $j$ 开始，它存储了结束于 $j$ 的唯一段的和。如果索引 $j$ 处的节点存储了段 $[i, j]$，我们接下来需要找到存储结束于 $i-1$ 的段的唯一节点。我们可以重复这样做，一路累加段的和。

从图 20 中寻找灵感，我们可以看到我们想要做的是找到我们最近的非活跃父节点的左兄弟，也就是说，我们向上走直到找到第一个作为右子节点的祖先，然后移动到它的左兄弟。在二叉索引方案下，这可以简单地实现为：

fn prev_segment_binary(self : Bits) -> Bits {
  while_(even, shr, self).dec()
}

Theorem 7. [blog/fenwick/thm/thm9]

减去 LSB 是将芬威克树向上移动到覆盖当前段的之前段的活动节点的正确方法、 $$\begin{align*} & \text{prevSegmentFenwick}(x) \\ &= \text{b2f}(n, \text{prevSegmentBinary}(\text{f2b}(n, x))) \\ &= \text{subtract}(x, \text{lsb}(x)) \end{align*} $$ 在范围 $[1, 2^n)$ 上处处成立。

证明

$$ \begin{aligned} & \text{b2f}(n, \text{prevSegmentBinary}(\text{f2b}(n, x))) \\ & \{ \text{展开定义} \} \\ = & \text{unshift}(n + 1, \underline{\text{inc}(\text{dec}}(\text{while}(\text{even}, \text{shr}, \text{dec}(\text{shift}(n + 1, x)))))) \\ & \{ \text{引理 (while-inc-dec)} \} \\ = & \underline{\text{unshift}(n + 1}, \text{while}(\text{even}, \text{shr}, \text{dec}(\text{shift}(n + 1, x)))) \\ & \{ \text{unshift} \} \\ = & \text{clear}(n + 1, \underline{\text{while}(\text{not}(\text{test}(n + 1, \cdot)), \text{shl} , \text{while}(\text{even}, \text{shr}}, \text{dec}(\text{shift}(n + 1, x)))))) \\ & \{ \text{引理 (shl-shr)} \} \\ = & \underline{\text{clear}(n + 1, \text{while}(\text{not}(\text{test}(n + 1, \cdot)), \text{shl}}, \text{dec}(\text{shift}(n + 1, x)))) \\ & \{ \text{unshift} \} \\ = & \text{unshift}(n + 1, \text{dec}(\text{shift}(n + 1, x))) \\ & \{ \text{引理 (sentinel)} \} \\ = & \text{atLSB}(\text{dec}, x) \\ & \{ \text{引理 (add-lsb)} \} \\ = & \text{subtract}(x, \text{lsb}(x)) \\ \end{aligned} $$