From: Tobias Nipkow <nipkow@in.tum.de>
Formalization of an Algorithm for Greedily Computing Associative Aggregations on
Sliding Windows
Lukas Heimes, Dmitriy Traytel and Joshua Schneider
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.
https://www.isa-afp.org/entries/Sliding_Window_Algorithm.html
Enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC