### Abstract

These theories formalize the quantitative analysis of a number of classical algorithms for the list update problem: 2-competitiveness of move-to-front, the lower bound of 2 for the competitiveness of deterministic list update algorithms and 1.6-competitiveness of the randomized COMB algorithm, the best randomized list update algorithm known to date. The material is based on the first two chapters of Online Computation and Competitive Analysis by Borodin and El-Yaniv.

For an informal description see the FSTTCS 2016 publication Verified Analysis of List Update Algorithms by Haslbeck and Nipkow.

### License

BSD License

### Topics

- Computer science/Algorithms/Online
- Computer science/Algorithms/Randomized

### Related publications

- Haslbeck, M. P. L., & Nipkow, T. (2016). Verified Analysis of List Update Algorithms. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.FSTTCS.2016.49

### Session List_Update

- Inversion
- Swaps
- On_Off
- Prob_Theory
- Competitive_Analysis
- Move_to_Front
- Bit_Strings
- MTF2_Effects
- BIT
- Partial_Cost_Model
- RExp_Var
- OPT2
- Phase_Partitioning
- List_Factoring
- TS
- BIT_pairwise
- BIT_2comp_on2
- Comb

### Depends on

- List Index
- Regular Sets and Expressions

## Cite

×

List_Update-AFP

    @article{List_Update-AFP,
      author  = {Maximilian P. L. Haslbeck and Tobias Nipkow},
      title   = {Analysis of List Update Algorithms},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/List_Update.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
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Oct 15, 2016 : Isabelle2016
- Feb 23, 2016 : Isabelle2016
- Feb 22, 2016 : Isabelle2016