Email Gateway (Aug 23 2022 at 08:53): Email Gateway (Aug 23 2022 at 08:53):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: Apr 24 2024 at 20:16 UTC