paperbot · PL 论文追踪

全部论文 待读 收藏

P2 You could have invented Fenwick trees

你可以发明 Fenwick 树
JFP vol.352025匹配度 1/10 · 该论文属于函数式编程、算法推导与领域特定语言方向,核心是 Fenwick 树的等式推导和 Haskell EDSL 实现,与用户关注的静态分析、LLM/Agent 程序分析、浮点程序分析及贝叶斯程序分析均无直接关系。引用 2 inbox
BRENT YORGEY
crossref: 2026-09-10

AI 速览

一句话:用等式推理从段树导出 Fenwick 树,并用 Haskell EDSL 揭示其位运算原理。

Fenwick 树(二叉索引树)能在亚线性时间内支持序列更新和区间查询,实现简洁高效,但基于索引的非显然位运算,难以理解。本文从更直接、易验证的纯函数式段树出发,通过等式推理解释如何将段树优化为 Fenwick 树,从而“发明”其实现。作者借助 Haskell 嵌入式 DSL 对无限二进制补码数进行运算,将索引位操作置于严格语义下逐步推导。结果不是实验性能评估,而是一种构造性解释,使 Fenwick 树的魔幻位运算变得可理解、可验证,并展示函数式等式推理在数据结构教学与设计中的价值。

问题
Fenwick 树实现高效但索引位运算晦涩,缺乏直观、可验证的推导。
方法
从纯函数式段树出发,用等式推理和 Haskell EDSL 对无限二进制补码数建模,导出 Fenwick 树优化实现。
评估
通过构造性推导和 EDSL 示例说明位运算语义,而非性能基准测试。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@article{Yorgey25,
  title = {You could have invented Fenwick trees},
  author = {BRENT YORGEY},
  journal = {Journal of Functional Programming},
  volume = {35},
  year = {2025},
  doi = {10.1017/s0956796824000169}
}