Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows

Lukas Heimes, Dmitriy Traytel 🌐 and Joshua Schneider

April 10, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Basin et al.'s sliding window algorithm (SWA) is an algorithm for combining the elements of subsequences of a sequence with an associative operator. It is greedy and minimizes the number of operator applications. We formalize the algorithm and verify its functional correctness. We extend the algorithm with additional operations and provide an alternative interface to the slide operation that does not require the entire input sequence.


BSD License


Session Sliding_Window_Algorithm