Efficient, easy, and formally verified segment trees
I’ve been spending the past month or so formalizing a folklore optimized implementation of
segment trees, a workhorse data structure in competitive programming.
Compared to the implementation I learned when I was starting out (similar to the one in Implementation), this has the advantage
of only needing to store 2 * n elements, compared to 4 * n, and being conceptually much simpler than the ‘Memory efficient implementation’
linked above.
Implementation
The common implementation that explicitly allocates a node (whether on the heap, or within an struct-of-arrays data structure) can be modeled as follows: