Treaps

 

Title: Treaps
Authors: Maximilian Haslbeck, Manuel Eberl and Tobias Nipkow
Submission date: 2018-02-06
Abstract:

A Treap is a binary tree whose nodes contain pairs consisting of some payload and an associated priority. It must have the search-tree property w.r.t. the payloads and the heap property w.r.t. the priorities. Treaps are an interesting data structure that is related to binary search trees (BSTs) in the following way: if one forgets all the priorities of a treap, the resulting BST is exactly the same as if one had inserted the elements into an empty BST in order of ascending priority. This means that a treap behaves like a BST where we can pretend the elements were inserted in a different order from the one in which they were actually inserted.

In particular, by choosing these priorities at random upon insertion of an element, we can pretend that we inserted the elements in random order, so that the shape of the resulting tree is that of a random BST no matter in what order we insert the elements. This is the main result of this formalisation.

BibTeX:
@article{Treaps-AFP,
  author  = {Maximilian Haslbeck and Manuel Eberl and Tobias Nipkow},
  title   = {Treaps},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2018,
  note    = {\url{http://isa-afp.org/entries/Treaps.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Comparison_Sort_Lower_Bound, Random_BSTs
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.