Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New entry:


view this post on Zulip 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: Nov 21 2024 at 12:39 UTC