Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Optimal Binary Search Trees

view this post on Zulip Email Gateway (Aug 22 2022 at 17:12):

From: Gerwin.Klein@data61.csiro.au
Optimal Binary Search Trees
by Tobias Nipkow and Dániel Somogyi

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.

https://www.isa-afp.org/entries/Optimal_BST.html

Enjoy!
Gerwin

Last updated: Apr 17 2024 at 20:15 UTC