### 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.

### License

BSD License

### Topics

- Computer science/Data structures

### Related publications

- Eberl, M., Haslbeck, M. W., & Nipkow, T. (2020). Verified Analysis of Random Binary Tree Structures. Journal of Automated Reasoning, 64(5), 879–910. https://doi.org/10.1007/s10817-020-09545-0
- Wikipedia

### Session Treaps

- Probability_Misc
- Treap
- Random_List_Permutation
- Treap_Sort_and_BSTs
- Random_Treap

### Depends on

- Lower bound on comparison-based sorting algorithms
- Expected Shape of Random Binary Search Trees

### Auto-related entries

- Prime Number Theorem with Remainder Term
- Skip Lists
- Verifying Imperative Programs using Auto2
- Pell’s Equation
- Descartes' Rule of Signs

## Cite

×

Treaps-AFP

    @article{Treaps-AFP,
      author  = {Max W. Haslbeck and Manuel Eberl and Tobias Nipkow},
      title   = {Treaps},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Treaps.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
- Feb 7, 2018 : Isabelle2017
- Feb 6, 2018 : Isabelle2017