### Abstract

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.

### License

BSD License

### Topics

- Computer science/Algorithms

### Session Sliding_Window_Algorithm

- SWA

## Cite

×

Sliding_Window_Algorithm-AFP

    @article{Sliding_Window_Algorithm-AFP,
      author  = {Lukas Heimes and Dmitriy Traytel and Joshua Schneider},
      title   = {Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Sliding_Window_Algorithm.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Apr 12, 2020 : Isabelle2019