Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.fenwick-tree

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/fenwick_tree.clj1 definitions, 2 theorems

AHoF Fenwick Tree (Binary Indexed Tree): maintain prefix sums of an array under point updates, both in O(log n), using a clever low-bit indexing where each index is responsible for a range of size equal to its lowest set bit. A prefix query ACCUMULATES the responsible node values while stripping the low bit off the index; an update adds a delta while adding the low bit. Both walk O(log n) nodes and combine additively: accumulate partial node-value = partial + node-value. Unlike a plain prefix-sum array (fast query, O(n) update) it supports fast updates, and unlike a segment tree it uses half the memory and simpler code. Proved native and axiom-free: the accumulation as nnrat/add; a worked prefix accumulation; and that accumulating the additive identity (an out-of-range node contributing 0) leaves the running sum unchanged. The low-bit index walks for query and update are executable; what is proved is the additive node combine. Requires nnrat/add (in the D63 checkpoint). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.fenwick-tree` prints this classification.

fenwick-tree/accumulate :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

fenwick-tree/accumulate-example :
  → astar/f-value 3 4 = 7

fenwick-tree/identity-node-unchanged :
  → astar/f-value 5 0 = 5