Priority Search Trees (Q7361385)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Priority_Search_Trees
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Priority Search Trees |
AFP entry Priority_Search_Trees |
Statements
25 June 2019
0 references
Peter Lammich
0 references
Tobias Nipkow
0 references
Priority Search Trees (English)
0 references
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 .
0 references
0 references
