Optimal Binary Search Trees

Tobias Nipkow 🌐 and Dániel Somogyi

May 27, 2018

Abstract

This article formalizes recursive algorithms for the construction of optimal binary search trees given fixed access frequencies. We follow Knuth (1971), Yao (1980) and Mehlhorn (1984). The algorithms are memoized with the help of the AFP article Monadification, Memoization and Dynamic Programming, thus yielding dynamic programming algorithms.

License

BSD License

Topics

Related publications

Session Optimal_BST

Depends on

Cite

× 
@article{Optimal_BST-AFP,
  author  = {Tobias Nipkow and Dániel Somogyi},
  title   = {Optimal Binary Search Trees},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2018},
  note    = {\url{https://isa-afp.org/entries/Optimal_BST.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: