Priority Search Trees

Title:	Priority Search Trees
Authors:	Peter Lammich and Tobias Nipkow
Submission date:	2019-06-25
Abstract:	We present a new, purely functional, simple and efficient data structure combining a search tree and a priority queue, which we call a priority search tree. The salient feature of priority search trees is that they offer a decrease-key operation, something that is missing from other simple, purely functional priority queue implementations. Priority search trees can be implemented on top of any search tree. This entry does the implementation for red-black trees. This entry formalizes the first part of our ITP-2019 proof pearl Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra.
BibTeX:	@article{Priority_Search_Trees-AFP, author = {Peter Lammich and Tobias Nipkow}, title = {Priority Search Trees}, journal = {Archive of Formal Proofs}, month = jun, year = 2019, note = {\url{http://isa-afp.org/entries/Priority_Search_Trees.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Used by:	Prim_Dijkstra_Simple
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.