Multidimensional Binary Search Trees

Martin Rau

May 30, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This entry provides a formalization of multidimensional binary trees, also known as k-d trees. It includes a balanced build algorithm as well as the nearest neighbor algorithm and the range search algorithm. It is based on the papers Multidimensional binary search trees used for associative searching and An Algorithm for Finding Best Matches in Logarithmic Expected Time.

License

BSD License

History

April 15, 2020
Change representation of k-dimensional points from 'list' to HOL-Analysis.Finite_Cartesian_Product 'vec'. Update proofs to incorporate HOL-Analysis 'dist' and 'cbox' primitives.

Topics

Session KD_Tree

Depends on

Cite

× 
@article{KD_Tree-AFP,
  author  = {Martin Rau},
  title   = {Multidimensional Binary Search Trees},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2019},
  note    = {\url{https://isa-afp.org/entries/KD_Tree.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: