一句话:用等式推理从段树导出 Fenwick 树,并用 Haskell EDSL 揭示其位运算原理。
Fenwick 树(二叉索引树)能在亚线性时间内支持序列更新和区间查询,实现简洁高效,但基于索引的非显然位运算,难以理解。本文从更直接、易验证的纯函数式段树出发,通过等式推理解释如何将段树优化为 Fenwick 树,从而“发明”其实现。作者借助 Haskell 嵌入式 DSL 对无限二进制补码数进行运算,将索引位操作置于严格语义下逐步推导。结果不是实验性能评估,而是一种构造性解释,使 Fenwick 树的魔幻位运算变得可理解、可验证,并展示函数式等式推理在数据结构教学与设计中的价值。
Abstract Fenwick trees , also known as binary indexed trees are a clever solution to the problem of maintaining a sequence of values while allowing both updates and range queries in sublinear time. Their implementation is concise and efficient—but also somewhat baffling, consisting largely of nonobvious bitwise operations on indices. We begin with segment trees , a much more straightforward, easy-to-verify, purely functional solution to the problem, and use equational reasoning to explain the implementation of Fenwick trees as an optimized variant, making use of a Haskell EDSL for operations on infinite two’s complement binary numbers.