Posts

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:

astrallexicon

the embers of a falling star