Abstract: |
Skip lists are sorted linked lists enhanced with shortcuts
and are an alternative to binary search trees. A skip lists consists
of multiple levels of sorted linked lists where a list on level n is a
subsequence of the list on level n − 1. In the ideal case, elements
are skipped in such a way that a lookup in a skip lists takes O(log n)
time. In a randomised skip list the skipped elements are choosen
randomly. This entry contains formalized proofs
of the textbook results about the expected height and the expected
length of a search path in a randomised skip list. |
BibTeX: |
@article{Skip_Lists-AFP,
author = {Max W. Haslbeck and Manuel Eberl},
title = {Skip Lists},
journal = {Archive of Formal Proofs},
month = jan,
year = 2020,
note = {\url{https://isa-afp.org/entries/Skip_Lists.html},
Formal proof development},
ISSN = {2150-914x},
}
|