Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.segment-tree

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

AHoF Segment Tree: answer range-aggregate queries (sum / min / max) AND point updates on an array, both in O(log n), by a balanced binary tree over array segments in which every internal node stores the aggregate of its two children. For a range-SUM tree the node combine is addition: combine left-child right-child = left-child + right-child, and a range query merges the O(log n) canonical segments that cover the query range with the same combine. Unlike a static prefix-sum array it supports updates (re-combining along one root path). Proved native and axiom-free: the node combine as nnrat/add; a worked node value; and the identity that combining with the additive identity (empty segment = 0) leaves a segment's aggregate unchanged. The tree layout and the recursive query/update are executable; what is proved is the aggregate-combine at each node. 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.segment-tree` prints this classification.

segment-tree/combine :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

segment-tree/combine-example :
  → astar/f-value 3 4 = 7

segment-tree/empty-segment-identity :
  → astar/f-value 0 5 = 5