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 competitive- ness of deterministic list update algorithms and 1.6-competitiveness of the randomized COMB algorithm, the best randomized list update algorithm known to date.
An informal description is found in an accompanying
report.
The material is based on the first two chapters of Online Computation
and Competitive Analysis by Borodin and El-Yaniv.
|
BibTeX: |
@article{List_Update-AFP,
author = {Maximilian P.L. Haslbeck and Tobias Nipkow},
title = {Analysis of List Update Algorithms},
journal = {Archive of Formal Proofs},
month = feb,
year = 2016,
note = {\url{http://isa-afp.org/entries/List_Update.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|