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

- Computer science/Algorithms
- Computer science/Data structures

### Related publications

- Wikipedia

### Session Optimal_BST

- Weighted_Path_Length
- Optimal_BST
- Quadrilateral_Inequality
- Optimal_BST2
- Optimal_BST_Examples
- Optimal_BST_Code
- Optimal_BST_Memo

### Depends on

- Monadification, Memoization and Dynamic Programming

## Cite

×

Optimal_BST-AFP

    @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:

- 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
- May 29, 2018 : Isabelle2017