| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Analysis of List Update Algorithms
| Title: | Analysis of List Update Algorithms |
| Authors: | Maximilian P.L. Haslbeck and Tobias Nipkow |
| Submission date: | 2016-02-17 |
| 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. |
| 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.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | List-Index, Regular-Sets |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |