| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Optimal Binary Search Trees
| Title: | Optimal Binary Search Trees |
| Authors: | Tobias Nipkow and Dániel Somogyi |
| Submission date: | 2018-05-27 |
| 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. |
| BibTeX: |
@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{http://isa-afp.org/entries/Optimal_BST.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Monad_Memo_DP |
| 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. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |